2023-12-03T17:19:06Z - 2024-12-03T17:19:06Z
Overview
10 Releases published by 1 user
Published
v0.2.20
Published
v0.2.19
Published
v0.2.19-alpha
Published
v0.2.18
Published
v0.2.14
Published
v0.2.13
Published
v0.2.12
Published
v0.2.11
Published
v0.2.10
Published
v0.2.10-alpha
62 Pull requests merged by 1 user
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
Merged
#72 feat: Elementarized tactics with motives, congruence, and absurdity
Merged
#76 feat: Extraction of tactics from compiler
Merged
#73 doc: README.md fix
Merged
#75 chore: Version bump to v4.8.0-rc1
Merged
#71 fix: Option setting in REPL
Merged
#70 feat: Let tactic
Merged
#69 feat: Option to collect dependent metavariables
Merged
#66 fix: Prevent incorrect inheritance of calc rhs
Merged
#68 chore: Update version to 0.2.15
Merged
#59 feat: Add support for the have, conv, and calc tactics
Merged
#65 feat: Print precursor rules in env/inspect
Merged
#64 fix: Serialization of projection operators
Merged
#63 perf: Lazy run print monads
Merged
#60 fix: Auto bound implicit in elab
Merged
#58 test: Parallel testing infrastructure
Merged
#56 feat: Instantiate mvars during echo
Merged
#55 feat: Specify type in echo
Merged
#54 fix: Instantiation causes infinite loop
Merged
#52 feat: Instantiation tests
Merged
#53 fix: Build failure on macOS due to LLVM version
Merged
#47 feat: Query arbitrary assignment in goal
Merged
#51 chore: Version bump and toolchain cleanup
Merged
#50 feat: Remove display of implementation details
Merged
#49 build: Toolchain bump and Nix flake fix
Merged
#48 feat: Output shared library in Nix flake
Merged
#45 feat: Print parent expression assignment
Merged
#46 feat: Add leanpkgs to the flake output
Merged
#44 test: Option controlled mvar instantiation
Merged
#43 feat: Print inductives, constructors, and recursors in env.inspect
Merged
#42 test: Deserialization
Merged
#41 feat: Add definitions and theorems to the environment
Merged
#40 feat: Change the main interaction monad
Merged
#38 chore: Version downgrade to 0.2.10-alpha
Merged
#37 fix: Printing projection leads to crash
Merged
#36 feat: Handling of private names
Merged
#35 feat: Print structural projection as application
4 Pull requests proposed by 1 user
Proposed
#123 doc: Design Rationale Document
Proposed
#128 feat: Extract type error and new constants
Proposed
#129 feat: Pickling goal states
Proposed
#130 feat: Erase macro scopes in sexp
20 Issues closed from 1 user
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
Closed
#9 Extraction of tactics from syntax tree
Closed
#62 Update README.md
Closed
#57 Add support for have, conv, calc, tactics.
Closed
#61 Could not reference local context variables
Closed
#24 The option on GoalTacticResult.goals? is redundant
Closed
#34 Print structures
Closed
#1 Allow adding definitions to environments
Closed
#39 The main interaction monad should be MetaM and not TermElabM
13 Issues created by 1 user
Opened
#78 Add option for Meta.ppGoal
Opened
#95 Pickling
Opened
#98 Use MLList from Batteries
Opened
#102 Timeout for tactics
Opened
#104 goal.delete exceeds max recursion depth
Opened
#114 Incremental and intercepted parsing of Lean code
Opened
#117 One stop env add
Opened
#122 Mathlib4 Parsing Error
Opened
#124 Erase macro scopes in sexp binders
Opened
#125 Wrong code/Compilation Failure Extraction
Opened
#126 Extraction of new symbols in each compilation unit
Opened
#127 Drafting tactic in goals
Opened
#131 Add aarch64-{linux,darwin} targets in flake
1 Unresolved Conversation
Open
#23
Printing fine-grained delaboration structure