2024-06-22T00:33:42Z - 2024-12-22T01:33:42Z
Overview
7 Releases published by 1 user
Published
v0.2.23
Published
v0.2.22
Published
v0.2.21
Published
v0.2.20
Published
v0.2.19
Published
v0.2.19-alpha
Published
v0.2.18
39 Pull requests merged by 1 user
Merged
#141 feat: Print value of arbitrary mvar and goals in goal state
Merged
#145 doc: Add limitations
Merged
#146 chore: Update version
Merged
#144 fix: Reset core message log
Merged
#128 feat: Extract type error and new constants
Merged
#139 fix: Tactic failure on synthesizing placeholder
Merged
#143 chore: Add aarch64 build targets to flake
Merged
#140 chore: Update version
Merged
#135 fix: Capture nested tactic failure
Merged
#123 doc: Design Rationale Document
Merged
#133 doc: Documentation cleanup and update
Merged
#129 feat: Pickling goal states
Merged
#130 feat: Erase macro scopes in sexp
Merged
#120 feat: State and environment pickling
Merged
#121 chore: Update lean4-nix to mainline
Merged
#115 chore: Update Lean4 upstream to unofficial flake
Merged
#119 feat: Extract used constants from invocation
Merged
#116 doc: Change license to Apache2
Merged
#113 feat: Capture environment in drafting
Merged
#111 feat: Let tactic in REPL
Merged
#110 fix: Delayed MVars in MetaTranslate
Merged
#109 feat: Catch and print IO errors in REPL
Merged
#108 chore: Update Lean to v4.12.0
Merged
#105 feat: Remove most filters on catalog
Merged
#107 feat: Error reporting in frontend
Merged
#99 feat: Collect holes in Lean file and put them into a GoalState
Merged
#100 fix: Tactics should produce .syntheticOpaque goals
Merged
#101 feat: Set automaticMode to true by default
Merged
#92 feat: Automatic Mode
Merged
#94 feat: Expose GoalState functions
Merged
#96 doc: Add GPL License
Merged
#91 fix: Instantiate type when detecting eq
Merged
#90 fix: Bindings in prograde tactics
Merged
#83 feat: Prograde tactics
Merged
#87 test: Use lake test. Retired Makefile
Merged
#85 feat: Condensed interface
Merged
#86 chore: Update Lean to v4.10.0-rc1
Merged
#81 refactor: Cleanup the congruence tactics
Merged
#82 fix: aux lemmas in env inspect
4 Pull requests proposed by 1 user
Proposed
#134 chore: Update Lean to v4.14.0
Proposed
#136 chore: Version 0.3
Proposed
#148 fix: Unnecessary instantiation call
Proposed
#149 feat: Simplify sexp printing
20 Issues closed from 1 user
Closed
#131 Add aarch64-{linux,darwin} targets in flake
Closed
#138 Articulation of Finished Proof
Closed
#126 Extraction of new symbols in each compilation unit
Closed
#125 Wrong code/Compilation Failure Extraction
Closed
#122 Mathlib4 Parsing Error
Closed
#114 Incremental and intercepted parsing of Lean code
Closed
#124 Erase macro scopes in sexp binders
Closed
#95 Pickling
Closed
#118 Used constant for tactic info extraction
Closed
#112 feat: Enable environment capture during frontend.process
Closed
#106 Report error when frontend parsing fails
Closed
#97 Parse and enter environment at arbitrary points of the input
Closed
#103 Metavariable not found bug with sorry collection
Closed
#93 Refactor out the Pantograph executable and lib into different targets
Closed
#88 Resumption not taking type unification into account
Closed
#74 Enable direct expression evaluation in context
Closed
#67 Extraction of atomization step
Closed
#80 Expose the String.toName interface
Closed
#84 Move towards Expr based interface
Closed
#77 Unclear error message
11 Issues created by 1 user
Opened
#98 Use MLList from Batteries
Opened
#102 Timeout for tactics
Opened
#104 goal.delete exceeds max recursion depth
Opened
#117 One stop env add
Opened
#127 Drafting tactic in goals
Opened
#132 Proof state merger
Opened
#137 Pickle environment extensions
Opened
#142 Pickle new constants generated in proof state
Opened
#147 Move Tactics to a Standalone Library
Opened
#150 Allow LSP-like behaviour of finding definition location via symbol
Opened
#151 Add unsafe detection in goal.print
2 Unresolved Conversations
Open
#78
Add option for Meta.ppGoal
Open
#23
Printing fine-grained delaboration structure