Proposal of LeanInk CLI

[insightmind]

Description

This issues shortly describes a proposal for the CLI of LeanInk.

Detailed behaviour

Following commands should be implementation:

Commands

Generate

leanInk generate <INPUT_FILES> This command generates the respective files for the input files. The user may supply a list of input files that can either be analyzed concurrently or sequentially. Concurrency is probably preferred here, although it's ok if the prototype only supports sequently analysis at first.

Analyze

leanInk analyze <LEAN_4_SNIPPET_FILES> similar to the generate command, this command allows the user to supply a list of input files. For each input file it will analyze the code and return the result of the analysis either using the json format of Alectryon or a proprietary solution.

Help

leanInk help and leanInk help <COMMAND> The help command displays helpful information for LeanInk in general or a specific command.

Licenses

leanInk licenses The licenses command displays LeanInks license as well as licenses by other tools used by LeanInk, prominently Alectryon.

---

Arguments

Debug

-d or --debug Every command should support the arguments for debug output of both LeanInk as well as Alectryon when summoned.

Version

-v or --version This command is already implemented in a basic manor. This argument may also support printing the explicit Lean4 version it supports. The last point is especially relevant because lean4 is still in active development.

Testscenarios

For testing the CLI of LeanInk we should probably provide short test scripts and evaluation files, with simple diffing between expected and actual output. We can then use this information for the CI/CD.

References

[insightmind]

Changes

• --version arg to version or v command. (--version is still allowed)
• -d and --debug renamed to -v and --verbose

Addition

• a command synonym for analyze
• h command synonym for h
• leanVersion (other options lV, --leanVersion) command provides only the supported lean version of LeanInk.

Removal

• generate command is not needed because we use Alectryon directly as our front-end
• licenses command is not necessary

[insightmind]

This is basically implemented as of now so I'll be closing this issue.