chore: Version 0.3 #136

1. Rename {Commands, Protocol}, and {Symbols, Symbol}
2. Store the root mvarId in the proof state along with goal indices
3. Add diagnostics function which prints out the state
4. Bump version to 0.2.6 (breaking change)

Documentations pending

3d7d5d6b4d feat: Add nix flake

a9294e0338 Add documentation about flake

d991533170 feat: Add proof continue and root extraction

8029298db7 feat: Display user name in Goal structure

1. Modify `serialize_expression_ast` so its no longer a monad
2. Test existence of root expression

c852db2f46 test: m-coupled goals

269e5c707c refactor: Separate goal printing and processing

Added a test for delta proof variables

f064bb21a4 feat: Assigning a goal with an expression

3b1746490d feat: Add REPL command for assigning an expression

41e1f64d44 Merge branch 'dev' into goal/dependency

045181356c feat: Add REPL function for root expression

4ce932eb3b Merge pull request 'Enable handling of m-Coupled goals' (#20 ) from goal/dependency into dev

Reviewed-on: #20

c0dfa04b18 feat: Simplify name printing

de250eafd0 feat: Print names in one segment separated with .

e523e8bcc6 chore: Version bump (breaking change)

60854525b9 feat: Simplify printing of function applications

1a99a2e7b2 fix: Sanitize name in universe levels

6cf328a84f Merge pull request 'feat: Simplify printing of names and expressions' (#25 ) from io/serial into dev

Reviewed-on: #25

d1c0dc376f feat: Print metavariable name in goal

59ac83f0b7 bug: Fix quote escape problem

1638c308a9 Merge pull request 'feat: Minor updates to serialization' (#26 ) from io/serial into dev

Reviewed-on: #26

4a4a33cea7 test: Separate mvar coupling tests

333355a85d feat: Partial state continuation

97d658cfc5 feat: Add goal.continue command

4be9dbc84a feat: Goal continuation fails if target has goals

a5b5e01858 chore: Version bump to 0.2.8

ce1cb13e54 fix: Use Lean's built in name parser

The `str_to_name` parser cannot handle numerical names and escapes.

c6bb4be597 chore: Update documentation

8182da436d chore: Remove unnecessary unsafe's

32fedede6a Merge branch 'dev' into goal/continuation

ce585f7288 feat: Print the root mvar name

4396da3e65 chore: Code formatting

53b63bf46c fix: Remove the error prone SemihashMap

d9745094fa fix: Remove the error prone SemihashMap

d35803791e Merge branch 'dev' into goal/continuation

e654613182 fix: New goal state not inserted correctly

a491316541 fix: Do not show parent state in continue

cc9e659c06 Merge pull request 'feat: Allow selective continuation of goals' (#27 ) from goal/continuation into dev

Reviewed-on: #27

a1d991f5db fix: Rectify error format

aaebb6b121 feat: Read dependencies of library symbols

fe850ded98 feat: Shorter symbol category

e0cfdfaf16 chore: Version bump to 0.2.9

860d2e239a feat: Remove | in symbol output

35f411041e feat: Remove printing projections

f72a82a4c9 feat: Remove stem deduce

Some private subproofs are not shown in the catalog and this breaks
dependencies

c80d7567b6 feat: Expose _private names

cdb1e8576f feat: Display whether a symbol is private

dbfee00420 feat!: Display public name only if name is private

d846210b9e Merge pull request 'feat: Print structural projection as application' (#35 ) from io/serial into dev

Reviewed-on: #35

079f12d6d3 chore: Version bump

3c2d93259f Merge branch 'dev' into library/catalog

f2b54ec018 Merge pull request 'feat: Handling of private names' (#36 ) from library/catalog into dev

Reviewed-on: #36

8a8db545a5 fix: Printing projection leads to crash

924a67f46d doc: getUsedConstants bug about projections

94c4b2cfe3 Merge pull request 'fix: Printing projection leads to crash' (#37 ) from io/sexp into dev

Reviewed-on: #37

d7fcc502f9 chore: Version downgrade to 0.2.10-alpha

There is a currently known bug

2fe4fa9bc4 fix: Change the main interaction monad to MetaM

bd0c66facc fix: Consolidate TermElabM blocks

ac9f6f810c doc: TermElabM metavariable generation

085b12c255 feat: Use CoreM as the main interaction monad

ff4671cdd0 chore: Rename lib. commands to env.

This is done to improve clarity and align with Lean's terminology

3c96a7c0ea feat: env_add command

83ff58dffc Merge pull request 'feat: Change the main interaction monad' (#40 ) from core/loop into dev

Reviewed-on: #40

69be7c3920 Merge branch 'dev' into env/add-decl

85eb42207c fix: env_add monads

a540dd4540 test: env.add

aef93cf506 fix: Force instantiate all mvars in env.add

da194a1165 refactor: env. operations into its own file

dc90b6b73e chore: Move environment functions to its own file

Symbol.lean is now subsumed

1c370ef2ae refactor: Rename Test/{Catalog,Environment}

a8bfa56587 Merge pull request 'feat: Add definitions and theorems to the environment' (#41 ) from env/add-decl into dev

Reviewed-on: #41

6692303da6 test: Simplify monad execution

6fb1b2e787 feat: Print inductives in env.inspect

50ac2fea4b feat: Print constructor and recursor info

6a81d83c1f test: Option controlled mvar instantiation

30eda7ef8c Merge pull request 'feat: Print inductives, constructors, and recursors in env.inspect' (#43 ) from env/inspect into dev

Reviewed-on: #43

34d9b02797 Merge branch 'dev' into goal/diag

d5ef05a7b0 Merge pull request 'test: Option controlled mvar instantiation' (#44 ) from goal/diag into dev

Reviewed-on: #44

25f3a2f19d feat: Print parent expression assignment

40d61fecc5 doc: Correct comment about parent filling expr

fe5c1eda7d feat: Prevent crash during rootExpr call

4acd367ca7 chore: Version bump to 0.2.12-alpha

5f5d06f1d8 feat: Add lake and lean to the package output

df4e044e5f chore: Expose `leanPkgs` in flake

0254759581 Merge pull request 'feat: Add leanpkgs to the flake output' (#46 ) from nix/toolchain into dev

Reviewed-on: #46

18c318cb73 Merge branch 'dev' into goal/relation

111781816f test: Delayed metavariable assignment

cb0712ccf6 Merge pull request 'feat: Print parent expression assignment' (#45 ) from goal/relation into dev

Reviewed-on: #45

7e28ded23f test: More diagnostics for tests

93b7d8b67d feat: Output shared library in flake

267d635c05 feat(build): Add shared facet for lean_lib

7bc0f82654 feat: Add exported version function

2ad7ad8778 feat(lib): Catalog command FFI

eeb149a32c feat(lib): Search path function

f18a9dd1d5 refactor: Move some functions to `Library.lean`

996f16bbb8 feat(lib): CoreM execution function

a5b0721482 feat(lib): Expose goal state interface

0b91c41ad2 fix: Execute expr parsing within goal.start

ef864ea16d feat(lib): Option creation function

4eec930dd4 fix: Pass options by reference

3debcc021a feat(lib): Export goal.print function

e6dbf88ce2 fix: Use Arrays only in the ABI

81aabc52ea chore: Lean version bump to 4.7.0-rc2

Multithreading in ABI was not stabilized in 4.1.0

aae19ec942 chore: Version bump to 4.8.0 prerelease

f016d60d07 chore: Version bump to 0.2.13

516ab15961 feat: Bump toolchain version

62d20be841 build: Nix build targets and checks

47fabf333b doc: Update README.md

a698a4250f feat: Unfold aux lemmas when printing root expr

9e68a9cae4 test: Elimination of aux lemmas

8fa1a7d383 feat: Stop cataloging internal/detail dependencies

e79e386b39 test: Catalog has no numeric symbols

46faa5c089 chore: Version bump

4a89aaf70e doc: Main README.md

4a1114ab00 build: Ignore test files when building target

cfd74aba91 build: Dev shell

431e81ca2f Merge pull request 'feat: Remove display of implementation details' (#50 ) from io/serial into dev

Reviewed-on: #50

2ea8b1c73c Merge branch 'dev' into misc/toolchain

14011945a0 Merge pull request 'chore: Version bump and toolchain cleanup' (#51 ) from misc/toolchain into dev

Reviewed-on: #51

252f85e66c feat: Instantiation tests

Note that delay assigned metavariables are not instantiated.

10e6877f0e Merge branch 'dev' into goal/relation

e09a6c7c9d Merge pull request 'feat: Query arbitrary assignment in goal' (#47 ) from goal/relation into dev

Reviewed-on: #47

1bea2ca4e1 fix: Lean build failure on macOS

140055b16b fix: Update flake so lean builds on Darwin

7f6b57bc08 Merge branch 'dev' into misc/toolchain

73e4c1d81c doc: Reason why not to follow nixpkgs

621b10c354 Merge pull request 'fix: Build failure on macOS due to LLVM version' (#53 ) from misc/toolchain into dev

Reviewed-on: #53

2c48ff9e42 Merge branch 'dev' into io/serial

f939388dbf Merge pull request 'feat: Instantiation tests' (#52 ) from io/serial into dev

Reviewed-on: #52

2b71203c1e fix: Instantiation causes infinite loop

e9c9548f17 fix: unfoldAuxLemma should be coreM

2802cc204f feat: Specify type in echo

7988a25ce8 refactor: Use library goalStartExpr function

a1ed8f4b3d refactor: Use library functions when possible

f462843218 docs: Update README.md

216bb9e920 test: Library test

9c8cc33e07 Merge pull request 'fix: Instantiation causes infinite loop' (#54 ) from output/expr into dev

Reviewed-on: #54

744c9ee286 Merge pull request 'feat: Specify type in echo' (#55 ) from expr/echo into dev

Reviewed-on: #55

8b43dc0f25 feat: Instantiate mvars during echo

ed196494c1 Merge pull request 'feat: Instantiate mvars during echo' (#56 ) from expr/echo into dev

Reviewed-on: #56

8a447e67cd test: Parallel testing infrastructure

92351c9a3d test: Move parallelism to Test/Main.lean

042dc8f530 doc: Documentation for `nix flake check`

1b7b6a644b feat: `GoalState.tryHave` tactic (tests failing)

058f5a98b2 feat: Bindings for the `have` tactic

41cb3f68cd test: Tests for conv and calc

5a60ca74d5 fix: Auto bound implicit in elab

7fe73551c3 feat: The `have` tactic

013cb8bb57 Merge pull request 'fix: Auto bound implicit in elab' (#60 ) from elab/level into dev

Reviewed-on: #60

38cb91652f Merge branch 'dev' into goal/have-conv-calc

d9ed051b4d feat: Partial implementation of `conv`

d50720f622 refactor: Metavariable set diff function

19d2f5ff3f feat: Conv tactic mode

09189ce600 perf: Lazy run print monads

7af24a4f0a Merge branch 'dev' into goal/have-conv-calc

63e64a1e9f feat: Conv tactic functions

22bb818a1c refactor: Use the `tactic interface for `conv

2f48cfbc19 doc: Remove outdated comments

d4e49310f0 feat: FFI interface to conv functions

0e63583a1d refactor: Monads in library

f02f9592d7 feat: Focus command

30c1fd894f fix: Coupling from unrelated goals

55b44c3fa1 fix: Serialization of .proj

823c9635c7 fix: Leading element in .proj sexp

535770bbd7 feat: Calc tactic

6b44d9ef14 fix: Remove `calcPrevRhs?` in non-calc tactics

6d85c19589 feat: Add library bindings for calc

7eb5419f36 feat: REPL interface for `calc`

ed220bc7fb doc: New tactics in README.md

a11df9f2e9 feat: Print recursor rules

a41b95e540 Merge branch 'dev' into goal/have-conv-calc

f20ee8dc87 Merge pull request 'feat: Add support for the `have`, `conv`, and `calc` tactics' (#59 ) from goal/have-conv-calc into dev

Reviewed-on: #59

036fab0ad6

fix: Prevent incorrect inheritance of calc rhs

dc6e79def7

doc: Update error message in interaction

e834765896

refactor: Code simplification

a864c4d3ff

refactor: Code simplification

4d4f660f3f

chore: Update version

7a4d462a87

Merge branch 'dev' into goal/calc

991ee5ad94

refactor: Rename functions to camel case

8e377c2092

refactor: CamelCase rename

e5d55e31ff

feat: Print expression dependent mvars

00a3613036 Merge pull request 'fix: Prevent incorrect inheritance of calc rhs' (#66 ) from goal/calc into dev

Reviewed-on: #66

4b01af7cef

Merge branch 'dev' into serial/goal

4ee955c21f

test: Tests the `let` tactic

77907fd060

feat: `goalLet` function

07094730b7 Merge pull request 'feat: Option to collect dependent metavariables' (#69 ) from serial/goal into dev

Reviewed-on: #69

b45b90b810

test: Metavariable name matches in let

614b9aa4ae

Merge branch 'dev' into goal/let

72dd20ea87 Merge pull request 'feat: Let tactic' (#70 ) from goal/let into dev

Reviewed-on: #70

adbb07af2d

fix: Option setting in REPL

b954f12526

refactor: Move all tactic operations to the bottom

75b4648ba9

feat: mapply stub

dbd54f7679

feat: Implement the mapply tactic

7aa7e6d7e9

feat: Library interface for mapply

52e5b5df50

doc: README.md fix

7531ad628c

doc: Documentation about conditional arguments

fec13ddb51

chore: Code cleanup

398b1c39ed

refactor: Common tactic execute function

4a92e655f6

test: Tactic test stub

3812aa56ec

feat: Phantom var in mapply

feff62a3c5

fix: Remove determination of major

6ffb227cd6

feat: Conduit modus ponens

4cff6677d2

chore: Lean version bump to 4.8.0-rc1

63417ef179

fix: Motive extra arguments not instiantiated

1e1995255a

test: mapply captures dependent types

cf1289f159

feat: NoConfuse tactic

2937675044

feat: Library interface for calling no_confuse

679871cbc6

fix: NoConfuse arg name

aa106f7591

feat: Do not filter mvars from mapply

69ec70ffbe

feat: Do not explicitly show delay assigned mvar

66a5dfcf3c

feat: Diagnostics command for FFI users

e58dbc66a9

fix: Consistent naming in library functions

0b88f6708e

test: Delayed mvar assignment for mapply

03ecb6cf19

feat: Partial instantiate metavariables

c04b363de7

feat: Handle delay assigned mvars

f813d4a8dd

refactor: Delayed mvar instantiation function

bc09f4a29d

refactor: Expr related functions to Expr.lean

5c7bb288b2

feat: Display full free variable list in subst

cf17428001

fix: Panic in partial instantiation

6ad24b72d4

fix: Nested delayed assignment instantiation

e165e41efa

chore: Version bump to v4.8.0-rc1

e05c01109c

Merge branch 'dev' into doc/readme

0aec757601 Merge pull request 'doc: README.md fix' (#73 ) from doc/readme into dev

Reviewed-on: #73

2f951c8fef

fix: Decoupling of mvars during instantiation

cc74d41b15

feat: Congruence tactics

cf1c884c8c

Merge branch 'dev' into goal/mapply

92acf7782c

test: CongruenceArg tactic

75df7268c5

test: Simplify testing structure for tactics

bbc00cbbb8

feat: Congruence tactic FFI interface and tests

bd42c396d7

chore: Code cleanup

09628309a9

feat: Basic tactic extraction (before/after/tactic)

b9b16ba0e9

refactor: Code cleanup

855e771609

feat: Add compilation unit boundary command

a2c5c7448c

chore: Code simplification, version bump

67e7f22b0a Merge pull request 'feat: Extraction of tactics from compiler' (#76 ) from compile/tactic into dev

Reviewed-on: #76

3c90c94645

fix: Execute instantiateAll in goal state diag

6dcff8b151

fix: Print diag in mvar context

3a53493089

feat: Show delayed assignment in goal diag

773a0afbd8

feat: Handling of universe level names in elab

c0e6e3ec39

Merge branch 'parse/level' into goal/mapply

2d2cf75183

Merge branch 'dev' into goal/mapply

bd20bf76da Merge pull request 'feat: Elementarized tactics with motives, congruence, and absurdity' (#72 ) from goal/mapply into dev

Reviewed-on: #72

b3a60fcea8

refactor: Rename TacticExecute to SyntheticTactic

f80d90ce87

fix: Goal diag missing newline character

8707dbc9bb

fix: aux lemmas in env inspect

aceee85b05

Merge branch 'env/inspect' into tactic/congruence

361e2e8926 Merge pull request 'fix: aux lemmas in env inspect' (#82 ) from env/inspect into dev

Reviewed-on: #82

fbe6e8fcb3

Merge branch 'dev' into tactic/congruence

472cd54868 Merge pull request 'refactor: Cleanup the congruence tactics' (#81 ) from tactic/congruence into dev

Reviewed-on: #81

25a7025c25

feat: Evaluation tactic

e282d9f781

test: Evaluation tactic

ffbea41f62

feat: Condensed interface

8e78718447

feat: Extract MetaM context and state from goal

c0124b347f

Merge branch 'serial/expr' into tactic/eval

58f9d72288

test: Evaluate tactic context

7acf1ffdf1

refactor: Move `have` to prograde tactic

2d2ff24017

feat: FFI interface for `evaluate` tactic

fc0d872343

refactor: Simplify proof test infrastructure

6ddde2963d

test: Eval instantiate

c404564a2b

chore: Bump Lean version to 4.10.0-rc1

4549ae1f65

Merge branch 'misc/version' into tactic/eval

9b1dd0ffda

chore: Update flake

df8b6602ee

Merge branch 'misc/version' into tactic/eval

a7fe7cbd7c

Merge branch 'misc/version' into serial/expr

193d94e798

feat: Expression creation and pretty printing

94c7b021f7

fix: Signature of ppExpr

eb5ee8c57c

feat: Expose TermElab context and state

431ca4e481

fix: Move elab context to condensed

3b415e8dc1

chore: Rename exports

2682ce5b7b

refactor: Move condensed functions to condensed

bf941cd686

feat: Expose parent and root expr functions

9db5463499

feat: Export `GoalState.resume`

4c81f226d1

feat: Expose environment functions

29f437f859

feat: Export GoalState.create

7b5567d784

fix: Name internal order

1c9a411d4d

feat: Export constant info type/value

3ca52517ab

feat: Refactor out projToApp

caa463f410

feat: Export GoalState.goalsArray

abef7a6f0d

feat: Export fvar names function

651afa75f4

feat: Filter in `visibleFVarsOfMVar`

2c08ef1e23

refactor: Remove old `visibleFVars` interface

c0e2a592ea

feat: Expose `mkAppM'`

394fb73137

feat: Add direct expression to string

c9ee31bbfd

feat: Export `mkFun`

64269868d5

feat: Expose project and leanPkgs in flake

caac70f0cf

feat: Move non package outputs to dependencies

0bc7bc5856

refactor: Remove export of Lean functions

If the user wishes to use Lean functions, they should add the bindings manually.

e943a4b065

refactor: Assign into its own tactic

56100a30af Merge pull request 'feat: Condensed interface' (#85 ) from serial/expr into dev

Reviewed-on: #85

e07f9d9b3f

Merge branch 'dev' into tactic/eval

7968072097

refactor: Remove the newMVarSet mechanism

This field has ambiguous purpose and does not account for different
types of mvars

9b0456a5e0

refactor: MetaM form of have and let

1e7a186bb1

refactor: MetaM form of define (evaluate)

5b4f8a37eb

refactor: All Tactic/ tactics into MetaM form

d17b21e282

fix: Use `getMVarsNoDelayed`

e1b7eaab12

fix: Let tactic not bringing binder into scope

0c469027c6

fix: Refactor mvar collection in assign tactic

43e11f1ba3

refactor: Always display isInaccessible

f87eed817f

build: Move non-package output to legacyPackages

5d43068ec3

fix: Flake check failure

3733c10a4e

refactor: Unify call convention

Induction like tactics should return `Array InductionSubgoal`. Branching
tactics should return their branch first.

76765c913c

test: Use `lake test`. Retired `Makefile`

0c529c5cd9

Merge branch 'misc/test-driver' into tactic/eval

edec0f5733

feat: Use CoreM for diag monad

948b535b5d Merge pull request 'feat: Prograde tactics' (#83 ) from tactic/eval into dev

Reviewed-on: #83

8d2cd6dfc7

fix: Bindings in prograde tactics

f8df2599f9

fix: Use `replaceMainGoal` instead of `setGoals`

9c40a83956

fix: Instantiate type when detecting `eq`

02556f3c79

feat: Expose `GoalState` functions

82d99ccf9b

refactor: Use `MVarId` across the board

37473b3efb

feat: Automatic mode (auto resume)

e2ad6ce6b3

doc: Documentation for automatic mode

a7b30af36b

refactor: Refactor REPL out of main library

fix: Calc previous rhs not found bug

9b3eef35ec

fix: Forgot to include the current goals in resume

8394e1b468

feat: Expose `conv` and `calc` tactics

4042ec707e

refactor: Use `Meta.mapMetaM`

68dac4c951

chore: Version bump to 0.2.18

e4d53733d0

feat: Simplify repl

f11c5ebaa3

doc: Add GPL License

7c49fcff27

refactor: Un-export two field accessor functions

User should use `lean_ctor_get`

25bb964604

test: Automatic mode testing

refactor: Simplified integration test structure

414f1c70fd

Merge branch 'dev' into lib/export

e36954a589 Merge pull request 'feat: Expose `GoalState` functions' (#94 ) from lib/export into dev

Reviewed-on: #94

b645d79fda

Merge branch 'dev' into goal/automatic

27e4e45418 Merge pull request 'feat: Automatic Mode' (#92 ) from goal/automatic into dev

Reviewed-on: #92

860344f9c5

refactor: Factor out `FrontendM` driver

5e99237e09

fix: Tactics should produce `.syntheticOpaque` goals

8e3241c02a

refactor: Move all frontend functions to `Frontend`

08fb53c020

test: Frontend process testing

4f5950ed78

feat: Convert holes to goals

762a139e78

feat: Export frontend functions

9f0de0957e

doc: Update documentation for frontend command

9075ded885

feat: Set `automaticMode` to true by default

f729a357b9

Merge branch 'dev' into frontend/collect-holes

fe8b259e4f

feat: Set root when there's just one mvar

bec84f857b

fix: repl build failure

18cd1d0388

fix: Extracting sorrys from sketches

143cd289bb

fix: Extraction of sorry's from nested tactics

ed1f96d7f7

Merge branch 'dev' into goal/tactic

b174b4ea79 Merge pull request 'fix: Tactics should produce `.syntheticOpaque` goals' (#100 ) from goal/tactic into dev

Reviewed-on: #100

530a1a1a97

fix: Extracting `sorry`s from coupled goals

a03eeddc9b

fix: Variable duplication in nested translation

10cb32e03f

Merge branch 'dev' into frontend/collect-holes

452c390711 Merge pull request 'feat: Collect holes in Lean file and put them into a `GoalState`' (#99 ) from frontend/collect-holes into dev

Reviewed-on: #99

d0321e72dd

feat: Add message diagnostics to frontend.process

22ddfaaf21 Merge pull request 'feat: Error reporting in frontend' (#107 ) from frontend/error into dev

Reviewed-on: #107

c3076cbb7d

chore: Update Lean to v4.12.0

8d774d3281 feat: Remove most filters on catalog

9119f47a8f chore: Remove more thin wrappers

25dd1a32ba

Merge branch 'dev' into misc/version

c3494edc75

fix: Flake build

2e1276c21c

chore: Update LSpec dependency

5e776a1b49

feat: Catch and print IO errors

05d0b7739a

feat: Catch IO errors in json format

1f4f2d7d6d Merge pull request 'chore: Update Lean to v4.12.0' (#108 ) from misc/version into dev

Reviewed-on: #108

420e863756

fix: Delayed mvars in MetaTranslate

0e8c9f890b

fix: Translate fvars in pending context

f03c47207b

Merge branch 'dev' into repl/io-exception

1cd41b4993 Merge pull request 'feat: Catch and print IO errors in REPL' (#109 ) from repl/io-exception into dev

Reviewed-on: #109

0bac4fdecd

Merge branch 'dev' into bug/frontend-translate-delayed-mvar

641f8c3883

fix: Translate level mvars

e0ba65a7cd Merge pull request 'fix: Delayed MVars in MetaTranslate' (#110 ) from bug/frontend-translate-delayed-mvar into dev

Reviewed-on: #110

645d9c9250

feat: Let tactic in REPL

5a2ae880f4

feat: Capture environment in drafting

946e688dec

test(frontend): Environment capture

5b278d68d4 Merge pull request 'feat: Let tactic in REPL' (#111 ) from repl/tactic-let into dev

Reviewed-on: #111

72e41e1e1e

Merge branch 'dev' into frontend/environment

a11127a64e Merge pull request 'feat: Capture environment in drafting' (#113 ) from frontend/environment into dev

Reviewed-on: #113

d23f99fd44

feat: Update Lean4 upstream to unofficial flake

8fe4c78c2a

doc: Change license to Apache2

23efed960b

chore: Update `lean4-nix`

b99fecdb50

chore: Update `lean4-nix`

d7c9590780

feat: Extract used constants from invocation

1c4f38e5eb

refactor: Rename {Serial,Delate}.lean

0d57027681

refactor: Merge Condensed into Delate

70f86f6e93

doc: Update delation documentation

ee8063e1f5

refactor: Merge all Delation functions

495ea1ac14

feat: Environment pickling

77b577d0e3

Merge branch 'dev' into frontend/data

4f6ccd3e82 Merge pull request 'feat: Extract used constants from invocation' (#119 ) from frontend/data into dev

Reviewed-on: #119

2790553180

feat: Environment save/load commands

e5d0459956

fix: Flake Build failure on x86_64-darwin

600c27a616

Merge branch 'dev' into misc/build

0ee7d57570

feat: Expose iTree for LSP Configuration

6a7ff46fb0 Merge pull request 'chore: Update Lean4 upstream to unofficial flake' (#115 ) from misc/build into dev

Reviewed-on: #115

f9d31597ec

chore: Update lean4-nix

4bfd606e2a

Merge branch 'dev' into serial/pickle

1da9180473 Merge pull request 'feat: State and environment pickling' (#120 ) from serial/pickle into dev

Reviewed-on: #120

af256123f3

doc: Update icon

ce3af887be

doc: Rationale document

5d676154f1

doc: Fix documentation link

a51bf6f807

Merge branch 'dev' into doc/rationale

a8e7a1a726

feat: Erase macro scopes in sexp

44aef76a10

refactor: Remove sanitization for mvarId/fvarId

7c9b092200

test: Dual monad testing stub

0f946880ae

test: Environment pickling

49b0101862 Merge pull request 'feat: Erase macro scopes in sexp' (#130 ) from delate/sexp into dev

Reviewed-on: #130

105fb7af4b

feat: Goal state pickling

c54ce93ef5

feat: Goal State IO in REPL

3da85b7f04

doc: Documentation for save/load

bfdc7dd39e

doc: Fix code environment

ebf9ab24f7 Merge pull request 'feat: Pickling goal states' (#129 ) from serial/pickle into dev

Reviewed-on: #129

d00e376943

doc: Remove outdated documentation

95408d1d52

doc: Unify types

f59df97c84 Merge pull request 'doc: Documentation cleanup and update' (#133 ) from chore/cleanup into dev

Reviewed-on: #133

4bd50c17ac

Merge branch 'dev' into doc/rationale

adb44c4fdb Merge pull request 'doc: Design Rationale Document' (#123 ) from doc/rationale into dev

Reviewed-on: #123

2e2658bde7

test: Add test case for composite tactic

7aafd6956f

fix: Capture composite tactic failure

a62ac51c37

chore: Remove all redundant filenames

34a4bf5b73

feat: Export GoalState.tryTactic

0415baaaff

chore: Cleanup old `TestM`

929311a042

fix: Only signal failure when there is error

d7457cd386 Merge pull request 'fix: Capture nested tactic failure' (#135 ) from bug/nested-tactic-failure into dev

Reviewed-on: #135

aniva added 1 commit 2024-12-09 21:43:05 -08:00

e9cbc6eab3

chore: Update version

aniva added 1 commit 2024-12-11 00:30:21 -08:00

c96df2ed1c

chore: Add `aarch64` build targets to flake

aniva added 4 commits 2024-12-11 09:09:35 -08:00

f2f71a6028

fix: Reset core message log

ab77418e24

fix: Drop previous message lists

396a787771

feat: Reset message log in MainM

f14a37897b Merge pull request 'fix: Reset core message log' (#144 ) from bug/core-state-error-linger into dev

Reviewed-on: #144

aniva added 1 commit 2024-12-11 16:47:56 -08:00

bb445f4d73

chore: Update version

aniva added 3 commits 2024-12-11 16:51:26 -08:00

fecab387dc

merge: branch 'dev' into doc/rationale

f111da7de7

doc: Add limitations

b9c114fe21 Merge pull request 'doc: Add limitations' (#145 ) from doc/rationale into dev

Reviewed-on: #145

aniva added 5 commits 2024-12-11 16:52:22 -08:00

0725d865de

feat: Print value of arbitrary mvar in goal state

eeb336c944

Merge branch 'dev' into goal/print

2f732a7f20

feat: Print goals in `goal.print`

0fa57a5a15

Merge branch 'dev' into goal/print

3744cfaa96 Merge pull request 'feat: Print value of arbitrary mvar and goals in goal state' (#141 ) from goal/print into dev

Reviewed-on: #141

aniva added 4 commits 2025-01-07 17:31:31 -08:00

c0090dec97

fix: Quote string literal in sexp

7a3b89cc0e

feat: Simplify sexp binder

53bad1c4c9

refactor: Remove obsolete sanitize option

07e737eb81 Merge pull request 'feat: Simplify sexp printing' (#149 ) from delate/sexp into dev

Reviewed-on: #149

aniva added 3 commits 2025-01-10 12:47:38 -08:00

97eaadc93c

feat: Add source location extraction

4a4b02d7b0

test: Source location extraction

814f36eb63 Merge pull request 'feat: Add source location extraction' (#154 ) from env/inspect into dev

Reviewed-on: #154

aniva added 5 commits 2025-01-10 12:49:17 -08:00

48b924fae2

fix(frontend): Incorrect capture of binder term

5a05e9e8d4

test: Add binder capturing test

524314721b

feat: Gate type error collection behind flag

9eec14503a

Merge branch 'dev' into bug/incorrect-binder-capture

a374af3a5f Merge pull request 'fix: Incorrect binder capture' (#152 ) from bug/incorrect-binder-capture into dev

Reviewed-on: #152

aniva added 7 commits 2025-01-13 10:22:38 -08:00

5ce6123de7

feat: Draft tactic

cb46b47a60

test: Draft tactic test

072d351f04

fix: Delete extraneous test

aa066b8634

fix: Add test

ebde7c9eed

feat: Prohibit coupling in drafting

6a9ba4bb15

Merge branch 'dev' into goal/tactic-draft

db24650aec Merge pull request 'feat: Draft tactic' (#153 ) from goal/tactic-draft into dev

Reviewed-on: #153

aniva added 10 commits 2025-01-13 12:28:52 -08:00

13dd11e995

chore: Update Lean to v4.14

fb3d36584f

chore: Add formatter, update lean4-nix

13e01b9e62

Merge branch 'dev' into misc/version

6302b747b8

feat: Improve error message clarity

f891960362

fix: Volatile test

9d2a999a4f

merge: branch 'dev' into misc/version

5e61282660

test: Source location extraction

06fdf7e678

chore: Update Lean to v4.15.0

60e78b322e

fix: Test failures

b8b46c4a9c Merge pull request 'chore: Update Lean to v4.15.0' (#134 ) from misc/version into dev

Reviewed-on: #134

aniva added 3 commits 2025-01-16 10:32:50 -08:00

9d445783c2

feat: Draft tactic REPL interface

62363cb943

fix: Over-eager assertion of fvarId validity

59935e386b Merge pull request 'feat: Draft tactic REPL interface' (#158 ) from tactic/draft into dev

Reviewed-on: #158

aniva added 2 commits 2025-01-26 22:04:31 -08:00

003a63bd13

doc: Manual about `env.{describe,module_read}`

4d295bd9ff Merge pull request 'doc: Manual about `env.{describe,module_read}`' (#165 ) from env/module into dev

Reviewed-on: #165

aniva added 5 commits 2025-02-25 15:16:46 -08:00

31c76e0d00

chore: Version bump

aac39ca60c

fix: Some test errors

267290c8f7

fix: Draft tactic failure by new `sorry` semantics

ec3e1ff2c0

chore: Bump version to 0.3.0-rc.1

642bca42e9 Merge pull request 'chore: Version bump' (#168 ) from chore/version into dev

Reviewed-on: #168

aniva added 3 commits 2025-03-08 22:53:09 -08:00

5d0a7e8443

fix: Manifest key error

9e1ea54cbe

chore: Cleanup file filtering system

1dceb5428e Merge pull request 'fix: Manifest key error' (#172 ) from chore/build into dev

Reviewed-on: #172

aniva added 1 commit 2025-03-14 16:48:19 -07:00

896475848b

fix: Name generation not available due to context

aniva added 5 commits 2025-03-14 16:48:42 -07:00

0cfd73e44e

test(frontend): Add scope `open` test

8797bbe245

test(frontend): Fix the open test

79e4dc697e

feat(frontend): Add option to inherit environment

ef165b7045

fix(frontend): Test update

8063039f7e Merge pull request 'feat(frontend): Alternative methods of initializing environment' (#173 ) from frontend/env-init into dev

Reviewed-on: #173

aniva added 3 commits 2025-03-24 18:05:27 -07:00

d305918bb9

chore: Update Lean to v4.17.0

ebf514b92b

chore: Update nix flake

fb91b521fb Merge pull request 'chore: Update Lean to v4.17.0, version to v0.3' (#178 ) from chore/version into dev

Reviewed-on: #178

aniva added 6 commits 2025-03-28 18:56:24 -07:00

3e55b4b22f

feat(repl): Record last scope

0fea0b50c9

Merge branch 'dev' into frontend/env-init

c2b7501649

refactor: Remove `CoreM` from `MainM`

8adab24157

fix: Call sites in `Main.lean`

9980fd9c39

test(repl): Environment loading from header

48485a868b Merge pull request 'feat: Update `CoreM` options from parsed header' (#177 ) from frontend/env-init into dev

Reviewed-on: #177

aniva added 4 commits 2025-03-28 21:32:01 -07:00

be505b8050

feat: Run cancel token with timeout

4610348fed

feat: `CoreM` timeout

0528a1592e

fix: Print internal exceptions nicely

3c07188cdf Merge pull request 'feat: Tactic with timeout' (#179 ) from repl/timeout into dev

Reviewed-on: #179

aniva added 6 commits 2025-04-07 20:18:51 -07:00

cf4a5955e3

test: Non-matchers are not matchers

70152c7715

refactor: Optional levels

f42af9f6a8

fix: Level name capture

9216e4fa86

chore: Format code

5df3d2bee1

refactor: Remove `runTermElabM` from library

27a1f420ba Merge pull request 'fix: `variable` and `universe` commands in environment capture' (#183 ) from bug/variable-level-names-in-scope into dev

Reviewed-on: #183

aniva added 3 commits 2025-04-08 10:59:56 -07:00

b6c3f7d8fd

chore: Update Lean to v4.18.0

13b03b602b

chore: Update flake

c547d9c8dc Merge pull request 'chore: Update Lean to v4.18.0' (#185 ) from chore/version into dev

Reviewed-on: #185

aniva merged commit 4e44b147e0 into main

2025-04-09 00:23:19 -07:00

aniva referenced this issue from a commit

2025-04-09 00:23:22 -07:00

Merge pull request 'chore: Version 0.3' (#136) from dev into main

Sign in to join this conversation.

No reviewers

No Label

No Milestone

No project

No Assignees

1 Participants

Notifications

Due Date

The due date is invalid or out of range. Please use the format 'yyyy-mm-dd'.

No due date set.

Dependencies

No dependencies set.

Reference: aniva/Pantograph#136