search

ufmg-smite / lean-smt

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

Failure to run `lake build smt` #115

Closed zhuanhao-wu closed 1 week ago

zhuanhao-wu commented 2 weeks ago

Hi, I'm trying to use lean-smt in lean 4.8.0 and I included it in my lakefile as such:

require smt from git "https://github.com/ufmg-smite/lean-smt.git"@"main"

When I do lake build smt, the following error occurs:

✖ [9/2466] Building cvc5.Kind
trace: .> LEAN_PATH=././.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/ssreflect/.lake/build/lib:././.lake/packages/cvc5/.lake/build/lib:././.lake/packages/smt/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH=././.lake/packages/cvc5/.lake/build/lib:././.lake/packages/cvc5/.lake/build/lib /home/allen/.elan/toolchains/leanprover--lean4---v4.8.0/bin/lean --load-dynlib=libstdc++.so.6 ././.lake/packages/cvc5/././cvc5/Kind.lean -R ././.lake/packages/cvc5/./. -o ././.lake/packages/cvc5/.lake/build/lib/cvc5/Kind.olean -i ././.lake/packages/cvc5/.lake/build/lib/cvc5/Kind.ilean -c ././.lake/packages/cvc5/.lake/build/ir/cvc5/Kind.c --load-dynlib=././.lake/packages/cvc5/.lake/build/lib/libffi.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: __libc_single_threaded
error: Lean exited with code 134

I also have the following output from my system:

$ ldd --version
ldd (Ubuntu GLIBC 2.31-0ubuntu9.16) 2.31
Copyright (C) 2020 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
Written by Roland McGrath and Ulrich Drepper.
$ lsb_release -a
No LSB modules are available.
Distributor ID: Ubuntu
Description:    Ubuntu 20.04.6 LTS
Release:        20.04
Codename:       focal

This almost seems like some glibc version mismatch to me, but I'm not sure.

Do you have any suggestions on how I may fix this? Thanks

abdoo8080 commented 2 weeks ago

Hi @zhuanhao-wu! You’re absolutely right: it's a glibc mismatch. The issue stems from lean-cvc5, which is imported by lean-smt. Previously, I had to use a custom build of cvc5 on my Ubuntu 22.04 Linux machine because I relied on functionalities not available in the latest cvc5 releases. However, as of today, the newest cvc5 release includes all the features I need. Consequently, I've switched to that version, which is also built on the slightly older Ubuntu 20.04. This change should resolve the issue for you as well!

abdoo8080 commented 1 week ago

I think this issue is resolved. So, I am closing it. Feel Free to reopen it if you're still facing issues building the tactic.