Milestones - Pantograph - git.leni.sh

1 Open 15 Closed

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.proj as 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 .syntheticOpaque goals
chore: Bump Lean version to v4.12.0
fix: Delayed MVar translation in MetaTranslate

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(frontend): Constants during tactic extraction
chore: Switch to lean4-nix

0.2.21

100%

feat(serial): Support environment pickling
feat(serial): Support goal state pickling
test(serial): Dual monad tests for pickling and IPC

0.2.22

100%

feat(frontend): Extract new symbols in each compilation unit
fix(frontend): Mathlib parsing error #122
fix(goal): Composite tactic failure capturing https://github.com/lenianiva/Pantograph/issues/1
chore: Add aarch64-{linux,darwin} build targets to flake

0.2.24

100%

feat(frontend): Extraction of symbol in source code position
fix(frontend): Divergence of behaviours between by sorry and sorry (can't triage)
fix(frontend): Remove type error extraction to tactic by default

0.2.25

100%

feat(goal): Draft tactic
fix(goal): Prohibit coupling in draft tactics and drafting
feat(serial): Pickle constants in goal state
feat(environment): Reading module and import data
chore: Update Lean to ~~v4.14.0~~ v4.15.0
fix(delate): Panic of projection normalization function

0.2.23

100%

feat(repl): Print goals in a goal state in goal.print
doc: Limitations section