search

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

monadic commands #33

Closed lovettchris closed 1 year ago

lovettchris commented 2 years ago

Description

This is just code cleanup, giving the Command run methods a ReaderT AppContext so things like printVersion can be implemented in Command.run instead of in runCLI.

Notable Changes

This is dependent on PR https://github.com/leanprover/LeanInk/pull/31 so I could test it.

Additional Notes

This is not high priority -- it is mostly me learning the code base, and adding what I've recently learned about monads to see if that could clean things up a bit. It was an interesting test. I wanted to implement the helpCommand this way also, but ran into problems with polymorphism and casting. For example, helpCommand needs all the commands "List Command" which are not defined until inside runCLI, this would be ideal for monadic state, but Command.run can't depend on List Command, I could split this out into RunnableCommand, but I couldn't figure out how to then later cast a Command into a RunnableCommand...

Kha commented 2 years ago

Looks sensible to me. I'd probably hide the complex monad type behind a new abbreviation. You might also want to evaluate using https://github.com/mhuisi/lean4-cli instead.

lovettchris commented 2 years ago

Thanks for the review, I added the abbreviation. Switching to lean4-cli is a much bigger change, for later :-)