Zulip Chat Archive

Stream: lean4

Topic: Gym


Patrick Massot (Aug 02 2022 at 10:20):

In https://github.com/dselsam/lean-gym/compare/master...PatrickMassot:lean-gym:master I tried to update @Daniel Selsam lean-gym experiment to current Lean 4 (including using lake). I managed to get the code to compile but running ./build/bin/lean-gym Nat.add_comm gives:

uncaught exception: could not find native implementation of external declaration 'UInt64.ofNatCore' (symbols 'l_UInt64_ofNatCore___boxed' or 'l_UInt64_ofNatCore')

This sounds above my pay grade so any help is welcome.

Sebastian Ullrich (Aug 02 2022 at 10:35):

You need supportInterpreter := true in your lean_exe. It corresponds to -rdynamic in the old Makefile.

Patrick Massot (Aug 02 2022 at 10:56):

Thanks!

Patrick Massot (Aug 02 2022 at 11:06):

I opened https://github.com/dselsam/lean-gym/pull/3. More importantly I can now study this code interactively without learning old Lean 4.


Last updated: Dec 20 2023 at 11:08 UTC