2024-12-13T00:31:11Z - 2025-06-12T23:31:11Z
Overview
4 Releases published by 1 user
Published
v0.3.1
Published
v0.3.0
Published
v0.2.25
Published
v0.2.24
37 Pull requests merged by 1 user
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
Merged
#181 fix: env.add Declarations with universe levels
Merged
#182 test: Update LSpec
Merged
#179 feat: Tactic with timeout
Merged
#177 feat: Update CoreM options from parsed header
Merged
#178 chore: Update Lean to v4.17.0, version to v0.3
Merged
#176 feat(delate): Unfold matchers
Merged
#173 feat(frontend): Alternative methods of initializing environment
Merged
#174 fix(goal): Name generation not available due to context
Merged
#172 fix: Manifest key error
Merged
#169 chore: Cleanup the library system
Merged
#168 chore: Version bump
Merged
#166 fix: Use in-context environment in sorry collection
Merged
#165 doc: Manual about env.{describe,module_read}
Merged
#164 chore: Code cleanup
Merged
#161 fix: Panic in exprProjToApp
Merged
#159 feat: Module reading functions
Merged
#157 feat: Pickle constants in goal state
Merged
#158 feat: Draft tactic REPL interface
Merged
#156 chore: Update version to 0.2.25
Merged
#134 chore: Update Lean to v4.15.0
Merged
#153 feat: Draft tactic
Merged
#155 chore: Update version
Merged
#152 fix: Incorrect binder capture
Merged
#154 feat: Add source location extraction
Merged
#149 feat: Simplify sexp printing
Merged
#148 fix: Unnecessary instantiation call
2 Pull requests proposed by 1 user
Proposed
#202 chore: Code cleanup
Proposed
#205 chore: Update Lean to v4.19.0
16 Issues closed from 1 user
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
Closed
#102 Timeout for tactics
Closed
#167 Allow alternative environment initiation
Closed
#175 Add tracing tags in delation
Closed
#147 Move Tactics to a Standalone Library
Closed
#171 GoalState.withContext should allow lifting
Closed
#162 Take generated constants into account
Closed
#163 Clean up code
Closed
#142 Pickle new constants generated in proof state
Closed
#160 Projection conversion function panics
Closed
#127 Drafting tactic in goals
Closed
#150 Allow LSP-like behaviour of finding definition location via symbol
10 Issues created by 1 user
Opened
#170 Recursive Functions and Termination Proofs
Opened
#180 Implement MonadBacktrack for MainM and backtrack goal states as well
Opened
#188 Unshielded Tactic
Opened
#190 Use non-computable section by default
Opened
#191 Code generation of recursors
Opened
#196 Documentation about safety
Opened
#197 Condition Unification
Opened
#203 Pickle proof object
Opened
#204 Pipe data extraction functions to file
Opened
#206 Execute tactic syntax
6 Unresolved Conversations
Open
#137
Pickle environment extensions
Open
#78
Add option for Meta.ppGoal
Open
#132
Branch unification
Open
#98
Use MLList from Batteries
Open
#104
goal.delete exceeds max recursion depth
Open
#117
One stop env.add