Sort
0.2.4
100%
- Allow deletion of individual proof states
- Most robust bookkeeping for proof states
- Allow monitoring of current resource usage so the client can know when bookkeeping becomes necessary (rather than waiting for the thing to crash and having to rebuild all proof states)
- Add pre-commit hooks to run the tests and check for white space usage
0.2.6
100%
- Allow hole filing ("Agda style") proof and expression generation
- Add more serialization options
- Allow for more robust bookkeeping
0.2.7
100%
Simplify expression serialization
0.2.8
100%
- Selectively continue goals
0.2.9
100%
- Fix error formatting
- Output dependency
0.2.10
100%
Minor serialization update:
- Print
Expr.projas function applications w.r.t. the projector of a structure - Print "private" symbols, which proofs somehow depend on, in the catalog. However unsafe and symbols in the
Lean.namespace should not be printed.
0.2.12
100%
- Print information about inducts, recursors, and constructors in
env.inspect.
0.2.19
100%
- feat: Add extraction of
sorrys from compilation steps - chore: Remove most catalog filters in
Environment.lean. A FFI user should implement these as they see fit. - fix: Tactics should produce
.syntheticOpaquegoals - chore: Bump Lean version to v4.12.0
- fix: Delayed
MVartranslation inMetaTranslate
TACAS '25
100%
Features that must be ready for TACAS '25
- feat: Automatic mode
- feat: Reading tactic steps from file
- feat: Collecting holes from file
- feat: REPL Tactics:
have,let,conv,calc
0.2.20
100%
Stabilize for artefact release
- doc: Use Apache 2 License
- feat: Constants during tactic extraction
- chore: Switch to lean4-nix