Switch to using Lean to run the tests (so it runs on Windows)

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

Switch to using Lean to run the tests (so it runs on Windows) #31

Closed lovettchris closed 2 years ago

lovettchris commented 2 years ago

Description

This uses the Lake "Script" feature to run the LeanInk tests.

Notable Changes

So make -C test run_tests becomes lake script run tests and make -C test capture becomes lake script run capture.

Also removed a problematic install.sh that was tinkering with the $HOME/.elan/bin folder. It is better for users to simply add the LeanInk/build/bin to their PATH environment when using alectryon.

Additional Notes

Fixes issue #21

Kha commented 2 years ago

Good work!