fix: update to latest version of lean, and fix the lakefile.lean

leanprover / LeanInk

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.

Apache License 2.0

60 stars 16 forks source link

fix: update to latest version of lean, and fix the lakefile.lean #26

Closed lovettchris closed 2 years ago

lovettchris commented 2 years ago

This makes it easier to build the lean reference manual.

Description

leanink needs to be built with the latest lean in order to work in alectryon.

Notable Changes

Additional Notes

tydeu commented 2 years ago

Another update for the lakefile.lean would be to use supportInterpreter := trur (on the exe) instead of the manual moreLinkArgs (on the package).

lovettchris commented 2 years ago

Thanks: https://github.com/leanprover/LeanInk/pull/28