search

ufmg-smite / lean-smt

Tactics for discharging Lean goals into SMT solvers.
Apache License 2.0
79 stars 16 forks source link

Usage instructions in README give linking errors #118

Open dranov opened 2 days ago

dranov commented 2 days ago

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 2 days ago

See also: https://github.com/ufmg-smite/lean-smt/issues/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