search

digama0 / lean-sys

Rust bindings for the Lean 4 proof assistant
Apache License 2.0
17 stars 5 forks source link

Version bump #10

Closed imbrem closed 1 year ago

imbrem commented 1 year ago

If everything looks good can publish this version to crates.io!

digama0 commented 1 year ago

@SchrodingerZhu any comments? LGTM

SchrodingerZhu commented 1 year ago

lgtm.

imbrem commented 1 year ago

Well this is embarrassing...

image

Any idea how to solve? The file seems to be there...

~/Projects/lean-sys % ls /home/tekne/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/lib/lean
Init        Init.olean  Lake.ilean  Lean        Lean.olean  libLean.a     libleanrt.a       libStd.a  Std.ilean
Init.ilean  Lake        Lake.olean  Lean.ilean  libInit.a   libleancpp.a  libleanshared.so  Std       Std.olean
digama0 commented 1 year ago

You are using an old version of lean, note the lack of libLake.a. More recent versions of the lean toolchain ship with libLake so that you can statically compile programs depending on lake, which is what lean-sys is supporting.

imbrem commented 1 year ago

Ah, I didn't even read the version number; I just updated to 4.0.0 and got confused, not realizing for some reason I had a lean-toolchain file in the parent folder... this is what I get for trying to get stuff done at 2 AM. OK, fixed!