search

digama0 / lean-sys

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

Linkage error on macos #5

Open SchrodingerZhu opened 1 year ago

SchrodingerZhu commented 1 year ago

I am still not able to run tests of this library on macos:

  1. the default c++ standard library on macos should be c++ instead of stdc++.
  2. the linker on macos does not understand --{start/end}-group.
  3. the linker on macos is not happy about the duplicate main symbol inside libLake.a.
digama0 commented 1 year ago

(3) sounds like a general issue with Lake that should be brought up upstream.