Gym

Stream: lean4

[Patrick Massot]

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]

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

[Patrick Massot]

Thanks!

[Patrick Massot]

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