2025-06-14T21:37:26Z - 2025-07-14T21:37:26Z
Overview
3 Releases published by 1 user
Published
v0.3.4
Published
v0.3.3
Published
v0.3.2
29 Pull requests merged by 1 user
Merged
#244 test(frontend): Circular sorry
Merged
#242 fix(frontend): Capture local instances in MetaTranslate
Merged
#240 fix(serial): Erase closures in synthetic mvars
Merged
#237 chore: Update version to 0.3.5
Merged
#236 doc: Remove stale documentation
Merged
#235 fix(frontend): Tomograph compilation
Merged
#229 feat(frontend): Command-level frontend.process
Merged
#233 refactor: Use consistent error handling
Merged
#232 feat: Display Message metadata
Merged
#231 feat(repl): Replace StdIO when executing IO-based monads
Merged
#228 fix(tactic): Erase finished calc goal
Merged
#220 feat(frontend): Tomogram
Merged
#227 test(repl): MVar name mismatch fix
Merged
#223 chore: Update Lean to v4.21.0
Merged
#226 chore: Update version to v0.3.4
Merged
#224 doc: Remove constraint on pick_goal
Merged
#222 fix(goal): Unknown metavariable problem during fragment initialization
Merged
#221 feat(serial): Pickle environment delta's
Merged
#219 feat(goal): Add unshielded tactic execution mode
Merged
#217 feat(goal): Branch unification
Merged
#216 feat(serial): Robust environment extension pickling
Merged
#214 chore: Update Nix flake
Merged
#218 chore: Update version to 0.3.3
Merged
#215 fix: Use the correct unfold aux lemma
Merged
#209 chore: Update Lean to v4.20.1
Merged
#207 refactor: Use syntax tactic in unit test
Merged
#208 feat: Output tactic invocation data to file
Merged
#202 chore: Code cleanup
Merged
#205 chore: Update Lean to v4.19.0
2 Pull requests proposed by 1 user
Proposed
#211 test(repl): Long-running tests of REPL
Proposed
#234 feat(frontend): Refactor function
13 Issues closed from 1 user
Closed
#238 Test Lean-Repl bugs
Closed
#241 Sorry capture with instances doesn't work
Closed
#239 Pending mvars cause generation of closures
Closed
#98 Use MLList from Batteries
Closed
#23 Printing fine-grained delaboration structure
Closed
#196 Documentation about safety
Closed
#230 Isolate std I/O streams during tactic execution
Closed
#225 Could not load mathlib environment from saved file
Closed
#132 Branch unification
Closed
#188 Unshielded Tactic Execution
Closed
#104 goal.delete exceeds max recursion depth
Closed
#204 Pipe data extraction functions to file
Closed
#206 Execute tactic syntax
3 Issues created by 1 user
Opened
#210 Test long-running behaviour of the REPL executable
Opened
#213 🖇️ Articulation and Syntax Processing
Opened
#243 Potential memory leak in CompactedRegion
8 Unresolved Conversations
Open
#137
🖇️ Environment Delta Pickling
Open
#197
Goal dependency generation
Open
#191
Code generation of recursors
Open
#170
🖇️ Recursive Functions and Termination Proofs
Open
#203
Pickle proof object
Open
#117
One stop env.add
Open
#78
Add option for Meta.ppGoal
Open
#180
Implement MonadBacktrack for MainM and backtrack goal states as well