Usage instructions in README give linking errors
Opened this issue · 3 comments
dranov commented
The README says:
To use lean-smt in your project, add the following line to your list of dependencies in lakefile.lean:
require smt from git "https://github.com/ufmg-smite/lean-smt.git"@"main"
but doing this in a fresh project (from lake new) leads to a linking error on lake build:
✖ [227/233] Building Smter.Basic
trace: .> LEAN_PATH=././.lake/packages/cvc5/.lake/build/lib:././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/packages/smt/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH=././.lake/packages/smt/.lake/build/lib:././.lake/packages/cvc5/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/build/lib:././.lake/packages/cvc5/.lake/build/lib /home/dranov/.elan/toolchains/leanprover--lean4---v4.8.0/bin/lean ././././Smter/Basic.lean -R ./././. -o ././.lake/build/lib/Smter/Basic.olean -i ././.lake/build/lib/Smter/Basic.ilean -c ././.lake/build/ir/Smter/Basic.c --load-dynlib=././.lake/packages/cvc5/.lake/build/lib/libffi.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-Prop-Core-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-Bool-Lemmas-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-Bool-Tactic-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-BitVec-Bitblast-1.so --load-dynlib=././.lake/packages/cvc5/.lake/build/lib/libcvc5-Kind-1.so --load-dynlib=././.lake/packages/cvc5/.lake/build/lib/libcvc5-ProofRule-1.so --load-dynlib=././.lake/packages/cvc5/.lake/build/lib/libcvc5-SkolemId-1.so --load-dynlib=././.lake/packages/cvc5/.lake/build/lib/libcvc5-Solver-1.so --load-dynlib=././.lake/packages/cvc5/.lake/build/lib/libcvc5-1.so --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-ForLean-ReduceEval-1.so --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-ForLean-ToExpr-1.so --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-Typ-1.so --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-Macro-1.so --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-Delab-1.so --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-MetaM-1.so --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-ForLean-Do-1.so --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-SortLocalDecls-1.so --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-Match-1.so --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-AssertInstancesCommute-1.so --load-dynlib=././.lake/packages/Qq/.lake/build/lib/libQq-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Attribute-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-BitVec-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Data-Sexp-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Dsl-Sexp-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Translate-Term-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Util-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Translate-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Translate-BitVec-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-BitVec-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Translate-Bool-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Bool-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-Builtin-AC-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-Util-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-Builtin-Lemmas-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-Builtin-Rewrites-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-Builtin-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Builtin-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-Int-Lemmas-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-Int-Polynorm-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-Int-Rewrites-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-Prop-Rewrites-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-Rewrite-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-Int-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Translate-Int-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Int-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Translate-Nat-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Nat-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Options-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-Prop-Lemmas-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-Prop-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Translate-Prop-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Prop-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-Quant-Lemmas-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-Quant-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Quant-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Translate-String-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-String-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Data-Graph-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Translate-Commands-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Tactic-WHNFConfigurableRef-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Tactic-WHNFConfigurable-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Tactic-WHNFSmt-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Tactic-EqnDef-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Translate-Query-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Tactic-Smt-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Tactic-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-UF-Congruence-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-UF-Rewrites-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Reconstruct-UF-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-UF-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-Translate-Solver-1.so --load-dynlib=././.lake/packages/smt/.lake/build/lib/libSmt-1.so --json
info: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, ././.lake/packages/cvc5/.lake/build/lib/libffi.so: undefined symbol: _ZNSt7__cxx1112basic_stringIcSt11char_traitsIcESaIcEED1Ev
What is the correct way to use lean-smt in a fresh Lean project? What should go in lakefile.lean?
dranov commented
See also: #115
$ ldd --version
ldd (Ubuntu GLIBC 2.38-1ubuntu6.3) 2.38
I can build a fresh clone of the lean-smt repo without issues, so I'm not sure exactly what's going on.
If I add the following to lakefile.lean:
def libcpp : String :=
if System.Platform.isWindows then "libstdc++-6.dll"
else if System.Platform.isOSX then "libc++.dylib"
else "libstdc++.so.6"
package «smter» where
precompileModules := true
moreLeanArgs := #[s!"--load-dynlib={libcpp}"]
moreGlobalServerArgs := #[s!"--load-dynlib={libcpp}"]I get linking issues that seem related to https://gcc.gnu.org/onlinedocs/libstdc++/manual/using_dual_abi.html, e.g.:
info: stderr:
ld.lld: error: undefined symbol: std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>::c_str() const
abdoo8080 commented
Hi @dranov! Thanks for opening this issue. You're right that the usage instructions in the README are insufficient for building and using lean-smt.
The complication arises because C++'s standard library isn't linked into cvc5's static libraries, and Lean doesn't assume much about C++. Your guess about needing to add moreLeanArgs := #[s!"--load-dynlib={libcpp}"] and moreGlobalServerArgs := #[s!"--load-dynlib={libcpp}"] is correct. The former tells Lean to load the standard library when compiling Lean code to C, and the latter does the same for the editor extension.
These two configurations are sufficient if you're using the smt tactic only for theorem proving. However, if you want to build an executable that imports Smt, you'll need one more configuration option to include the standard library in Lean's linker. Adding moreLinkArgs := #["-L/usr/lib/x86_64-linux-gnu", "/usr/lib/x86_64-linux-gnu/libstdc++.so.6"] worked for me. Could you try that?
Unfortunately, I don't have a more portable or platform-independent solution yet.
dranov commented
Thank you @abdoo8080! Yes, indeed that works for me. I guess this should be in the README.