Milestones - Pantograph - git.leni.sh

2 Open 20 Closed

v0.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

v0.2.6

100%

Allow hole filing ("Agda style") proof and expression generation
Add more serialization options
More robust bookkeeping

v0.2.7

100%

Simplify expression serialization

v0.2.8

100%

Selectively continue goals

v0.2.9

100%

Fix error formatting
Output dependency

v0.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.

v0.2.12

100%

Print information about inducts, recursors, and constructors in env.inspect.

v0.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

v0.2.20

100%

Stabilize for artefact release

doc: Use Apache 2 License
feat(frontend): Constants during tactic extraction
chore: Switch to lean4-nix

v0.2.21

100%

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

v0.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

v0.2.23

100%

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

v0.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

v0.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

v0.3

100%

feat(env): Allow adding definitions/theorems to the environment
chore: Stabilize Lean to at least version 4.18.0
feat(goal): Add support for the have, conv, calc tactics
feat(frontend): Add proof scraping support
feat: Add ~~condensed~~ delated interface
feat(goal): Add automatic mode
feat(serial): Add environment/state pickling
doc: Add design rational documentation
feat(goal): Articulation of finished proof term (could be very ugly)
feat(goal): Tactic execution timeout

v0.3.1

100%

Accomodate adversarial inputs

feat(goal): Add unsafe and computability detection
doc: Update rationale about cooperative concurrency and cancellation
feat(repl): Flush stdout
fix(frontend): Prevent parsing of ambiguous statements

v0.3.2

100%

chore: Update Lean to at least ~~v4.19.0~~ 4.20.1
feat(frontend): Pipe data extraction output to file

v0.3.3

100%

feat(serial): Collect auxiliary lemmas in environments and goal states
feat(goal): Branch unification (beta)
feat(goal): Overhaul infrastructure for handling conv. Introduce the fragment-based system for handling partially-executed tactics.
refactor(goal): Allow a goal state to have multiple parent goals. Delete the GoalState.focus function since it does not fit into current paradigms.

Note: There has been many modifications to the API.

v0.3.4

100%

feat(frontend): Allow cancellation tokens in frontend.process.
feat(frontend): Tomograph, a tool for displaying the compilation structure of a Lean file.
feat(frontend): Compilation unit category information
refactor: Properly display Lean messages. Not as strings.
chore(toolchain): Update Lean to v4.21.0
fix(repl): Harden REPL against stray outputs in stdio