docs: note lean_exe libstdc++ link failure on Linux (see #196)

[ide-developer]

Summary

Adds a Caveats entry documenting a real, reproducible link failure hit when a downstream project has a lean_exe target (not just a lean_lib) depending on Lean Copilot.

Context

Filed and fully root-caused in #196: a lean_lib target that imports Lean Copilot and calls suggest_tactics builds and runs correctly, but a lean_exe target in the same project fails to link with ~15 distinct undefined symbol errors for libstdc++ types (vtable for std::basic_ifstream, std::filesystem::path, etc.), all originating from ct2.cpp inside libleanffi.a.

Root cause (confirmed against Lean's own executable link command and clang's driver source): Lean's lean_exe link recipe statically links libc++/libc++abi and never links libstdc++ at all, while Lean Copilot's native code is built by system g++ against libstdc++. The library target works because its .so resolves libstdc++ transitively at runtime via libctranslate2.so.4; the executable's from-scratch link never gets that chance.

#196 also documents a working per-project moreLinkArgs workaround (including a subtlety where a literal -lstdc++ is silently rewritten by clang's driver and needs -Wl,-lstdc++ instead, plus a second, distinct glibc-version-mismatch issue this can expose once libstdc++ is actually linked).

This PR

This is a documentation-only change — a Caveats bullet pointing to #196, so anyone hitting this (likely as a confusing library-works-but-exe-fails discrepancy) can find the explanation and workaround quickly. I didn't attempt a lakefile.lean build-system change here, since:

• The workaround's exact -L path is distro-specific (found via gcc -print-file-name=libstdc++.so or equivalent), so baking it in generically needs more design thought than a doc fix.
• I don't have visibility into how a build-system-level fix would interact with the non-Linux build paths (macOS uses Accelerate instead of OpenBLAS/libstdc++ entirely) or with Lake's own link-arg propagation semantics across the CI matrix.

Happy to follow up with an actual lakefile.lean change (e.g. auto-detecting the GCC lib dir and applying -Wl,-lstdc++ + the glibc-compat stub automatically for Linux executable consumers) if a maintainer thinks that's the right direction — wanted to start with the lower-risk, purely-additive doc fix first.

Test plan

• Verified the underlying fix end-to-end on real hardware (Fedora 39, Lean 4.32.0-rc1, Lean Copilot v4.31.0) — a lean_exe target with the moreLinkArgs workaround from lean_exe link fails with undefined libstdc++ symbols from libleanffi.a (lean_lib works fine) #196 builds and the resulting binary runs successfully.
• This change itself is Markdown-only; no build/test impact.

[Peiyang-Song]

Thanks for the thorough root-cause writeup here and in #196. It made tracking this down much faster.

I've gone ahead and implemented a real fix rather than just documenting the workaround, in #195. I'm going to close this in favor of that.