2025-04-04T00:02:39Z - 2025-07-04T00:02:39Z
Overview
4 Releases published by 1 user
Published
v0.3.3
Published
v0.3.2
Published
v0.3.1
Published
v0.3.0
29 Pull requests merged by 1 user
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
Merged
#195 chore: Update version
Merged
#200 doc: Add design limitations about memory
Merged
#201 feat(goal): Detect unsafe and sorry
Merged
#199 fix: Shield tactics from the environment generated by frontend.process
Merged
#187 fix(repl): Elaborate with errToSorry as false by default
Merged
#193 fix(goal): Prevent duplication in idempotent tactics
Merged
#194 feat(repl): Flush stdout
Merged
#189 doc: Update rationale
Merged
#136 chore: Version 0.3
Merged
#185 chore: Update Lean to v4.18.0
Merged
#183 fix: universe commands in environment capture
2 Pull requests proposed by 1 user
Proposed
#211 test(repl): Long-running tests of REPL
Proposed
#228 fix(tactic): Erase finished calc goal
11 Issues closed from 1 user
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
Closed
#151 Add unsafe detection in goal.print
Closed
#198 Add documentation about what we cannot implement
Closed
#192 Goal duplication
Closed
#184 Remove CoreM library functions
Closed
#186 Draft tactic hangs for some particular cases of have
7 Issues created by 1 user
Opened
#190 Use non-computable section by default
Opened
#191 Code generation of recursors
Opened
#196 Documentation about safety
Opened
#197 Goal dependency generation
Opened
#203 Pickle proof object
Opened
#210 Test long-running behaviour of the REPL executable
Opened
#213 🖇️ Articulation and Syntax Processing
6 Unresolved Conversations
Open
#137
🖇️ Environment Delta Pickling
Open
#170
🖇️ Recursive Functions and Termination Proofs
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
Open
#98
Use MLList from Batteries