Version 1.0.1

Update for leanprover/lean4:nightly-2022-03-21

Version 1.0.0

This is the first formal release of LeanInk.
Please take a look at the README.md to learn more about usage and all features supported by LeanInk.

The official version of Alectryon does not yet support LeanInk, until the first of two pull requests is merged. Until then please use our Alectryon Fork to test LeanInk.

Improvements since last release

• Greatly reduce complexity of Alectryon output algorithm
• Add tailPos property to Compound
• Filter empty output fragments in Alectryon output
• Output .leanInk as compressed JSON instead of prettified JSON (use --verbose to output a prettified version)
• Greatly improve performance of compound generation (matchTokens)
• Traverse each InfoTree in seperate and concurrent task
• Fallback to standard library if provided lakefile does not exist
• Fix incorrect termination guard in InfoTree traversal
• Activate additional metadata export for test case outputs
• Catch pretty printing errors (thanks @Kha)
• Improve the output format of messages

Version 1.0.0-beta2

Improvements since last release

• support of nested tactics
• say hello to the octopus
• important fix to compound generation
• improvements to semantic syntax highlighting

Version 1.0.0-beta1

This is the first beta of LeanInk.
It now includes all features that we anticipated for the first release and for our thesis.

New Features since 1.0.0-pre.3

• Implement Output structure to use custom Output type instead of default Alectryon type. The interface is not ideal right now and will probably undergo some changes in the near future.
• --x-enable-semantic-token experimental feature that extracts the SemanticToken types for each token. This is used to implement semantic syntax highlighting in our fork of Alectryon.,

Version 1.0.0-pre.3

• Major restructure and rewrite of Analysis code. This is to improve the cleanliness of the code and improve extensibility for custom output types.
• Support list of input files for sequential analysis

Experimental Features:

• Split --experimental-type-tokens flag into --x-enable-type-info and --x-enable-docStrings flags
• Major fixes to tokenization of info tree nodes.

Version 1.0.0-pre.2

This is the second official pre-release of LeanInk.
For more information on LeanInk, specifically how to install it, take a look at the readme.

Supported Lean 4 version:
leanprover/lean4:nightly-2022-01-07

Bug fixes:

• Fixes an issue that cause clipping of text at the end of the source file output

Experimental Features:

• Use the --experimental-type-tokens flag to activate the new features supported by the typeid branch of the Alectryon fork. This is still WIP atm.

Version 1.0.0-pre.1

This is the first official pre-release of LeanInk.
For more information on LeanInk, specifically how to install it, take a look at the readme.

Supported Lean 4 version:
leanprover/lean4:nightly-2021-12-15