Leni Aniva
3744cfaa96
Merge pull request 'feat: Print value of arbitrary mvar and goals in goal state' ( #141 ) from goal/print into dev
...
Reviewed-on: #141
2024-12-11 16:52:19 -08:00
Leni Aniva
0fa57a5a15
Merge branch 'dev' into goal/print
2024-12-11 16:51:58 -08:00
Leni Aniva
b9c114fe21
Merge pull request 'doc: Add limitations' ( #145 ) from doc/rationale into dev
...
Reviewed-on: #145
2024-12-11 16:51:23 -08:00
Leni Aniva
2f732a7f20
feat: Print goals in `goal.print`
2024-12-11 16:49:52 -08:00
Leni Aniva
eeb336c944
Merge branch 'dev' into goal/print
2024-12-11 16:40:01 -08:00
Leni Aniva
bb445f4d73
chore: Update version
2024-12-11 16:38:59 -08:00
Leni Aniva
f111da7de7
doc: Add limitations
2024-12-11 15:09:14 -08:00
Leni Aniva
fecab387dc
merge: branch 'dev' into doc/rationale
2024-12-11 15:05:09 -08:00
Leni Aniva
f14a37897b
Merge pull request 'fix: Reset core message log' ( #144 ) from bug/core-state-error-linger into dev
...
Reviewed-on: #144
2024-12-11 09:09:33 -08:00
Leni Aniva
396a787771
feat: Reset message log in MainM
2024-12-11 09:06:42 -08:00
Leni Aniva
ab77418e24
fix: Drop previous message lists
2024-12-11 09:05:47 -08:00
Leni Aniva
f2f71a6028
fix: Reset core message log
2024-12-11 09:01:57 -08:00
Leni Aniva
5d76626912
Merge pull request 'feat: Extract type error and new constants' ( #128 ) from frontend/infotree into dev
...
Reviewed-on: #128
2024-12-11 01:25:35 -08:00
Leni Aniva
7cba8efd54
Merge branch 'dev' into frontend/infotree
2024-12-11 01:14:15 -08:00
Leni Aniva
e9fbce7b4d
Merge pull request 'fix: Tactic failure on synthesizing placeholder' ( #139 ) from bug/tactic-failure-placeholder into dev
...
Reviewed-on: #139
2024-12-11 01:13:14 -08:00
Leni Aniva
4217dbcf80
Merge branch 'dev' into bug/tactic-failure-placeholder
2024-12-11 01:08:44 -08:00
Leni Aniva
c96df2ed1c
chore: Add `aarch64` build targets to flake
2024-12-11 00:29:29 -08:00
Leni Aniva
aa122b2bb9
doc: Update rationale link
2024-12-11 00:24:56 -08:00
Leni Aniva
58956d33fe
doc: Update behaviour rationale
2024-12-11 00:21:26 -08:00
Leni Aniva
cb87fcd9dd
fix: Insert `mvarDeps`
2024-12-11 00:16:52 -08:00
Leni Aniva
e0e5c9ec68
chore: Code cleanup
2024-12-10 23:51:47 -08:00
Leni Aniva
755ba13c1b
fix: Set `synthesizeSyntheticMVarsNoPostponing`
2024-12-10 23:48:46 -08:00
Leni Aniva
1d10cd2b20
fix: Collect errored mvars by iterating errorInfo
2024-12-10 23:16:33 -08:00
Leni Aniva
95503c45e4
doc: frontend.process newConstants
2024-12-10 21:45:57 -08:00
Leni Aniva
0725d865de
feat: Print value of arbitrary mvar in goal state
2024-12-10 14:14:59 -08:00
Leni Aniva
681c3fb78d
fix: Disallow indeterminant type `sorry`
2024-12-10 12:21:56 -08:00
Leni Aniva
37a5884be4
fix: Use `ppSyntax` instead of `ppTactic`
2024-12-09 21:39:33 -08:00
Leni Aniva
1527743900
refactor: Optionalize CompilationUnit
2024-12-09 21:00:33 -08:00
Leni Aniva
eb0374dfb3
feat: Collect new constants in repl
2024-12-09 20:57:25 -08:00
Leni Aniva
9a69c48cb2
fix: Integration test failure
2024-12-09 20:42:05 -08:00
Leni Aniva
dd00d803d1
feat: Collect sorry/elab failure boundaries
2024-12-09 20:38:27 -08:00
Leni Aniva
e9cbc6eab3
chore: Update version
2024-12-09 20:17:55 -08:00
Leni Aniva
0b4ded1049
fix: Collect sorrys and type mismatches
2024-12-09 20:15:53 -08:00
Leni Aniva
5ef2b5c118
feat: Collect newly defined constants
2024-12-09 19:40:00 -08:00
Leni Aniva
d040d2006c
fix: Do not guard mvar errors in other tactics
2024-12-09 17:58:08 -08:00
Leni Aniva
47d26badc8
feat: Capture mvar errors
2024-12-09 17:30:33 -08:00
Leni Aniva
7fc2bd0d0f
test: Tactic failure on synthesizing placeholder
2024-12-09 08:15:01 -08:00
Leni Aniva
2d068ecd50
fix: Use guarded `isDefEq`
2024-12-09 00:06:20 -08:00
Leni Aniva
17ab2eafd8
fix: Halt on match guard
2024-12-09 00:03:53 -08:00
Leni Aniva
ea813e5bc5
feat: Monadic info collection
2024-12-08 23:21:36 -08:00
Leni Aniva
b950dc9b1a
fix: Verbose printing of infotree
2024-12-08 22:51:55 -08:00
Leni Aniva
9ede3cf717
feat: InfoTree printing
2024-12-08 15:38:03 -08:00
Leni Aniva
4de53e0547
Merge branch 'dev' into frontend/infotree
2024-12-08 12:54:19 -08:00
Leni Aniva
d7457cd386
Merge pull request 'fix: Capture nested tactic failure' ( #135 ) from bug/nested-tactic-failure into dev
...
Reviewed-on: #135
2024-12-07 18:51:25 -08:00
Leni Aniva
929311a042
fix: Only signal failure when there is error
2024-12-06 00:08:20 -08:00
Leni Aniva
0415baaaff
chore: Cleanup old `TestM`
2024-12-05 22:16:20 -08:00
Leni Aniva
34a4bf5b73
feat: Export GoalState.tryTactic
2024-12-05 22:12:04 -08:00
Leni Aniva
a62ac51c37
chore: Remove all redundant filenames
2024-12-05 22:11:37 -08:00
Leni Aniva
7aafd6956f
fix: Capture composite tactic failure
2024-12-05 22:07:21 -08:00
Leni Aniva
2e2658bde7
test: Add test case for composite tactic
2024-12-05 21:35:37 -08:00
Leni Aniva
adb44c4fdb
Merge pull request 'doc: Design Rationale Document' ( #123 ) from doc/rationale into dev
...
Reviewed-on: #123
2024-12-05 17:24:19 -08:00
Leni Aniva
4bd50c17ac
Merge branch 'dev' into doc/rationale
2024-12-05 17:23:32 -08:00
Leni Aniva
f59df97c84
Merge pull request 'doc: Documentation cleanup and update' ( #133 ) from chore/cleanup into dev
...
Reviewed-on: #133
2024-12-05 17:23:24 -08:00
Leni Aniva
95408d1d52
doc: Unify types
2024-12-05 17:21:06 -08:00
Leni Aniva
d00e376943
doc: Remove outdated documentation
2024-12-05 17:18:35 -08:00
Leni Aniva
ebf9ab24f7
Merge pull request 'feat: Pickling goal states' ( #129 ) from serial/pickle into dev
...
Reviewed-on: #129
2024-12-05 16:02:25 -08:00
Leni Aniva
bfdc7dd39e
doc: Fix code environment
2024-12-05 16:02:00 -08:00
Leni Aniva
3da85b7f04
doc: Documentation for save/load
2024-12-05 16:00:46 -08:00
Leni Aniva
c54ce93ef5
feat: Goal State IO in REPL
2024-12-05 14:31:43 -08:00
Leni Aniva
105fb7af4b
feat: Goal state pickling
2024-12-05 14:23:55 -08:00
Leni Aniva
49b0101862
Merge pull request 'feat: Erase macro scopes in sexp' ( #130 ) from delate/sexp into dev
...
Reviewed-on: #130
2024-12-04 11:24:15 -08:00
Leni Aniva
0f946880ae
test: Environment pickling
2024-12-04 10:44:33 -08:00
Leni Aniva
7c9b092200
test: Dual monad testing stub
2024-11-30 23:21:16 -08:00
Leni Aniva
44aef76a10
refactor: Remove sanitization for mvarId/fvarId
2024-11-26 12:57:19 -08:00
Leni Aniva
a8e7a1a726
feat: Erase macro scopes in sexp
2024-11-26 12:34:52 -08:00
Leni Aniva
9894ad7c7e
refactor: InfoTree functions
2024-11-26 12:16:14 -08:00
Leni Aniva
a51bf6f807
Merge branch 'dev' into doc/rationale
2024-11-17 17:38:27 -08:00
Leni Aniva
5d676154f1
doc: Fix documentation link
2024-11-16 21:27:40 -08:00
Leni Aniva
ce3af887be
doc: Rationale document
2024-11-15 23:36:28 -08:00
Leni Aniva
af256123f3
doc: Update icon
2024-11-15 23:29:37 -08:00
Leni Aniva
1da9180473
Merge pull request 'feat: State and environment pickling' ( #120 ) from serial/pickle into dev
...
Reviewed-on: #120
2024-11-15 23:10:33 -08:00
Leni Aniva
4bfd606e2a
Merge branch 'dev' into serial/pickle
2024-11-15 23:09:08 -08:00
Leni Aniva
f9d31597ec
chore: Update lean4-nix
2024-11-15 14:56:51 -08:00
Leni Aniva
6a7ff46fb0
Merge pull request 'chore: Update Lean4 upstream to unofficial flake' ( #115 ) from misc/build into dev
...
Reviewed-on: #115
2024-11-15 14:40:47 -08:00
Leni Aniva
0ee7d57570
feat: Expose iTree for LSP Configuration
2024-11-14 22:51:25 -08:00
Leni Aniva
600c27a616
Merge branch 'dev' into misc/build
2024-11-14 22:44:55 -08:00
Leni Aniva
e5d0459956
fix: Flake Build failure on x86_64-darwin
2024-11-14 22:20:06 -08:00
Leni Aniva
2790553180
feat: Environment save/load commands
2024-11-13 19:50:31 -08:00
Leni Aniva
4f6ccd3e82
Merge pull request 'feat: Extract used constants from invocation' ( #119 ) from frontend/data into dev
...
Reviewed-on: #119
2024-11-10 21:29:34 -08:00
Leni Aniva
77b577d0e3
Merge branch 'dev' into frontend/data
2024-11-08 14:52:03 -08:00
Leni Aniva
495ea1ac14
feat: Environment pickling
2024-11-08 14:49:49 -08:00
Leni Aniva
ee8063e1f5
refactor: Merge all Delation functions
2024-11-08 14:41:24 -08:00
Leni Aniva
70f86f6e93
doc: Update delation documentation
2024-11-08 14:34:15 -08:00
Leni Aniva
0d57027681
refactor: Merge Condensed into Delate
2024-11-08 13:05:48 -08:00
Leni Aniva
1c4f38e5eb
refactor: Rename {Serial,Delate}.lean
2024-11-08 13:04:00 -08:00
Leni Aniva
d7c9590780
feat: Extract used constants from invocation
2024-11-05 14:37:06 -08:00
Leni Aniva
b99fecdb50
chore: Update `lean4-nix`
2024-10-26 17:52:37 -07:00
Leni Aniva
23efed960b
chore: Update `lean4-nix`
2024-10-26 13:49:03 -07:00
Leni Aniva
8fe4c78c2a
doc: Change license to Apache2
2024-10-21 09:59:13 -07:00
Leni Aniva
d23f99fd44
feat: Update Lean4 upstream to unofficial flake
2024-10-14 21:16:41 -07:00
Leni Aniva
a11127a64e
Merge pull request 'feat: Capture environment in drafting' ( #113 ) from frontend/environment into dev
...
Reviewed-on: #113
2024-10-12 16:59:41 -07:00
Leni Aniva
72e41e1e1e
Merge branch 'dev' into frontend/environment
2024-10-12 16:57:55 -07:00
Leni Aniva
5b278d68d4
Merge pull request 'feat: Let tactic in REPL' ( #111 ) from repl/tactic-let into dev
...
Reviewed-on: #111
2024-10-12 16:54:12 -07:00
Leni Aniva
946e688dec
test(frontend): Environment capture
2024-10-12 16:52:36 -07:00
Leni Aniva
5a2ae880f4
feat: Capture environment in drafting
2024-10-12 16:46:44 -07:00
Leni Aniva
645d9c9250
feat: Let tactic in REPL
2024-10-12 16:17:21 -07:00
Leni Aniva
e0ba65a7cd
Merge pull request 'fix: Delayed MVars in MetaTranslate' ( #110 ) from bug/frontend-translate-delayed-mvar into dev
...
Reviewed-on: #110
2024-10-09 18:08:09 -07:00
Leni Aniva
641f8c3883
fix: Translate level mvars
2024-10-09 15:49:10 -07:00
Leni Aniva
0bac4fdecd
Merge branch 'dev' into bug/frontend-translate-delayed-mvar
2024-10-08 23:53:57 -07:00
Leni Aniva
1cd41b4993
Merge pull request 'feat: Catch and print IO errors in REPL' ( #109 ) from repl/io-exception into dev
...
Reviewed-on: #109
2024-10-08 23:50:36 -07:00
Leni Aniva
f03c47207b
Merge branch 'dev' into repl/io-exception
2024-10-08 23:49:51 -07:00
Leni Aniva
0e8c9f890b
fix: Translate fvars in pending context
2024-10-08 14:28:35 -07:00
Leni Aniva
420e863756
fix: Delayed mvars in MetaTranslate
2024-10-08 10:32:16 -07:00
Leni Aniva
1f4f2d7d6d
Merge pull request 'chore: Update Lean to v4.12.0' ( #108 ) from misc/version into dev
...
Reviewed-on: #108
2024-10-08 09:49:08 -07:00
Leni Aniva
05d0b7739a
feat: Catch IO errors in json format
2024-10-08 00:45:58 -07:00
Leni Aniva
5e776a1b49
feat: Catch and print IO errors
2024-10-08 00:17:31 -07:00
Leni Aniva
2e1276c21c
chore: Update LSpec dependency
2024-10-08 00:15:30 -07:00
Leni Aniva
c3494edc75
fix: Flake build
2024-10-06 16:46:39 -07:00
Leni Aniva
25dd1a32ba
Merge branch 'dev' into misc/version
2024-10-06 16:12:36 -07:00
Leni Aniva
9119f47a8f
chore: Remove more thin wrappers
2024-10-06 16:12:22 -07:00
Leni Aniva
8d774d3281
feat: Remove most filters on catalog
2024-10-06 16:12:22 -07:00
Leni Aniva
c3076cbb7d
chore: Update Lean to v4.12.0
2024-10-06 16:10:18 -07:00
Leni Aniva
22ddfaaf21
Merge pull request 'feat: Error reporting in frontend' ( #107 ) from frontend/error into dev
...
Reviewed-on: #107
2024-10-05 22:39:23 -07:00
Leni Aniva
d0321e72dd
feat: Add message diagnostics to frontend.process
2024-10-05 14:49:17 -07:00
Leni Aniva
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
2024-10-03 15:43:00 -07:00
Leni Aniva
10cb32e03f
Merge branch 'dev' into frontend/collect-holes
2024-10-03 11:47:38 -07:00
Leni Aniva
a03eeddc9b
fix: Variable duplication in nested translation
2024-10-03 11:46:09 -07:00
Leni Aniva
530a1a1a97
fix: Extracting `sorry`s from coupled goals
2024-10-03 11:35:54 -07:00
Leni Aniva
b174b4ea79
Merge pull request 'fix: Tactics should produce `.syntheticOpaque` goals' ( #100 ) from goal/tactic into dev
...
Reviewed-on: #100
2024-10-03 08:47:30 -07:00
Leni Aniva
ed1f96d7f7
Merge branch 'dev' into goal/tactic
2024-10-03 01:38:10 -07:00
Leni Aniva
143cd289bb
fix: Extraction of sorry's from nested tactics
2024-10-03 01:29:46 -07:00
Leni Aniva
18cd1d0388
fix: Extracting sorrys from sketches
2024-10-02 22:22:20 -07:00
Leni Aniva
bec84f857b
fix: repl build failure
2024-09-09 18:43:34 -07:00
Leni Aniva
fe8b259e4f
feat: Set root when there's just one mvar
2024-09-09 17:37:59 -07:00
Leni Aniva
f729a357b9
Merge branch 'dev' into frontend/collect-holes
2024-09-09 17:35:10 -07:00
Leni Aniva
9075ded885
feat: Set `automaticMode` to true by default
2024-09-09 17:29:43 -07:00
Leni Aniva
9f0de0957e
doc: Update documentation for frontend command
2024-09-09 12:39:32 -07:00
Leni Aniva
762a139e78
feat: Export frontend functions
2024-09-09 12:30:32 -07:00
Leni Aniva
4f5950ed78
feat: Convert holes to goals
2024-09-09 12:26:46 -07:00
Leni Aniva
08fb53c020
test: Frontend process testing
2024-09-09 10:18:20 -07:00
Leni Aniva
8e3241c02a
refactor: Move all frontend functions to `Frontend`
2024-09-08 15:02:43 -07:00
Leni Aniva
5e99237e09
fix: Tactics should produce `.syntheticOpaque` goals
2024-09-08 14:13:39 -07:00
Leni Aniva
860344f9c5
refactor: Factor out `FrontendM` driver
2024-09-08 13:44:46 -07:00
Leni Aniva
27e4e45418
Merge pull request 'feat: Automatic Mode' ( #92 ) from goal/automatic into dev
...
Reviewed-on: #92
2024-09-08 12:25:06 -07:00
Leni Aniva
b645d79fda
Merge branch 'dev' into goal/automatic
2024-09-08 12:13:42 -07:00
Leni Aniva
e36954a589
Merge pull request 'feat: Expose `GoalState` functions' ( #94 ) from lib/export into dev
...
Reviewed-on: #94
2024-09-08 12:10:46 -07:00
Leni Aniva
414f1c70fd
Merge branch 'dev' into lib/export
2024-09-08 12:01:02 -07:00
Leni Aniva
25bb964604
test: Automatic mode testing
...
refactor: Simplified integration test structure
2024-09-08 11:57:39 -07:00
Leni Aniva
7c49fcff27
refactor: Un-export two field accessor functions
...
User should use `lean_ctor_get`
2024-09-08 11:53:54 -07:00
Leni Aniva
f11c5ebaa3
doc: Add GPL License
2024-09-07 14:11:04 -07:00
Leni Aniva
e4d53733d0
feat: Simplify repl
2024-09-07 14:03:29 -07:00
Leni Aniva
68dac4c951
chore: Version bump to 0.2.18
2024-09-07 13:55:41 -07:00
Leni Aniva
4042ec707e
refactor: Use `Meta.mapMetaM`
2024-09-07 13:54:52 -07:00
Leni Aniva
8394e1b468
feat: Expose `conv` and `calc` tactics
2024-09-07 13:47:55 -07:00
Leni Aniva
9b3eef35ec
fix: Forgot to include the current goals in resume
2024-09-06 22:22:19 -07:00
Leni Aniva
a7b30af36b
refactor: Refactor REPL out of main library
...
fix: Calc previous rhs not found bug
2024-09-06 22:01:36 -07:00
Leni Aniva
e2ad6ce6b3
doc: Documentation for automatic mode
2024-09-06 21:32:02 -07:00
Leni Aniva
37473b3efb
feat: Automatic mode (auto resume)
2024-09-06 21:30:11 -07:00
Leni Aniva
82d99ccf9b
refactor: Use `MVarId` across the board
2024-09-06 21:07:12 -07:00
Leni Aniva
02556f3c79
feat: Expose `GoalState` functions
2024-09-05 11:56:06 -07:00
Leni Aniva
9c40a83956
fix: Instantiate type when detecting `eq`
2024-09-03 19:05:16 -07:00
Leni Aniva
f8df2599f9
fix: Use `replaceMainGoal` instead of `setGoals`
2024-09-03 14:18:47 -07:00
Leni Aniva
8d2cd6dfc7
fix: Bindings in prograde tactics
2024-09-03 14:15:52 -07:00
Leni Aniva
948b535b5d
Merge pull request 'feat: Prograde tactics' ( #83 ) from tactic/eval into dev
...
Reviewed-on: #83
2024-08-31 20:04:38 -07:00
Leni Aniva
edec0f5733
feat: Use CoreM for diag monad
2024-08-26 13:42:14 -04:00
Leni Aniva
0c529c5cd9
Merge branch 'misc/test-driver' into tactic/eval
2024-08-18 12:24:26 -07:00
Leni Aniva
76765c913c
test: Use `lake test`. Retired `Makefile`
2024-08-18 12:22:59 -07:00
Leni Aniva
3733c10a4e
refactor: Unify call convention
...
Induction like tactics should return `Array InductionSubgoal`. Branching
tactics should return their branch first.
2024-08-17 16:47:21 -07:00
Leni Aniva
5d43068ec3
fix: Flake check failure
2024-08-17 02:07:17 -07:00
Leni Aniva
f87eed817f
build: Move non-package output to legacyPackages
2024-08-17 01:59:48 -07:00
Leni Aniva
43e11f1ba3
refactor: Always display isInaccessible
2024-08-17 00:53:38 -07:00
Leni Aniva
0c469027c6
fix: Refactor mvar collection in assign tactic
2024-08-17 00:50:02 -07:00
Leni Aniva
e1b7eaab12
fix: Let tactic not bringing binder into scope
2024-08-17 00:47:12 -07:00
Leni Aniva
d17b21e282
fix: Use `getMVarsNoDelayed`
2024-08-16 00:32:34 -07:00
Leni Aniva
5b4f8a37eb
refactor: All Tactic/ tactics into MetaM form
2024-08-15 23:41:17 -07:00
Leni Aniva
1e7a186bb1
refactor: MetaM form of define (evaluate)
2024-08-15 23:23:17 -07:00
Leni Aniva
9b0456a5e0
refactor: MetaM form of have and let
2024-08-15 23:17:15 -07:00
Leni Aniva
7968072097
refactor: Remove the newMVarSet mechanism
...
This field has ambiguous purpose and does not account for different
types of mvars
2024-08-15 22:53:42 -07:00
Leni Aniva
e07f9d9b3f
Merge branch 'dev' into tactic/eval
2024-08-15 22:45:43 -07:00
Leni Aniva
56100a30af
Merge pull request 'feat: Condensed interface' ( #85 ) from serial/expr into dev
...
Reviewed-on: #85
2024-08-15 22:41:58 -07:00
Leni Aniva
e943a4b065
refactor: Assign into its own tactic
2024-08-15 22:39:40 -07:00
Leni Aniva
0bc7bc5856
refactor: Remove export of Lean functions
...
If the user wishes to use Lean functions, they should add the bindings manually.
2024-08-14 01:20:56 -07:00
Leni Aniva
caac70f0cf
feat: Move non package outputs to dependencies
2024-08-04 17:52:36 -07:00
Leni Aniva
64269868d5
feat: Expose project and leanPkgs in flake
2024-08-04 17:32:20 -07:00
Leni Aniva
c9ee31bbfd
feat: Export `mkFun`
2024-08-02 22:33:03 -07:00
Leni Aniva
394fb73137
feat: Add direct expression to string
2024-08-02 22:00:27 -07:00
Leni Aniva
c0e2a592ea
feat: Expose `mkAppM'`
2024-08-02 21:44:46 -07:00
Leni Aniva
2c08ef1e23
refactor: Remove old `visibleFVars` interface
2024-08-02 19:53:19 -07:00
Leni Aniva
651afa75f4
feat: Filter in `visibleFVarsOfMVar`
2024-08-02 19:49:11 -07:00
Leni Aniva
abef7a6f0d
feat: Export fvar names function
2024-07-31 00:00:33 -07:00
Leni Aniva
caa463f410
feat: Export GoalState.goalsArray
2024-07-30 17:02:41 -07:00
Leni Aniva
3ca52517ab
feat: Refactor out projToApp
2024-07-30 13:30:41 -07:00
Leni Aniva
1c9a411d4d
feat: Export constant info type/value
2024-07-29 18:39:22 -07:00
Leni Aniva
7b5567d784
fix: Name internal order
2024-07-28 14:19:47 -07:00
Leni Aniva
29f437f859
feat: Export GoalState.create
2024-07-28 13:58:20 -07:00
Leni Aniva
4c81f226d1
feat: Expose environment functions
2024-07-28 13:46:14 -07:00
Leni Aniva
9db5463499
feat: Export `GoalState.resume`
2024-07-27 18:20:34 -07:00
Leni Aniva
bf941cd686
feat: Expose parent and root expr functions
2024-07-27 17:39:51 -07:00
Leni Aniva
2682ce5b7b
refactor: Move condensed functions to condensed
2024-07-23 11:57:12 -07:00
Leni Aniva
3b415e8dc1
chore: Rename exports
2024-07-23 05:16:46 -07:00
Leni Aniva
431ca4e481
fix: Move elab context to condensed
2024-07-22 17:57:01 -07:00
Leni Aniva
eb5ee8c57c
feat: Expose TermElab context and state
2024-07-22 17:34:14 -07:00
Leni Aniva
94c7b021f7
fix: Signature of ppExpr
2024-07-15 12:22:47 -07:00
Leni Aniva
193d94e798
feat: Expression creation and pretty printing
2024-07-15 11:42:02 -07:00
Leni Aniva
a7fe7cbd7c
Merge branch 'misc/version' into serial/expr
2024-07-15 09:53:36 -07:00
Leni Aniva
df8b6602ee
Merge branch 'misc/version' into tactic/eval
2024-07-06 20:00:12 -07:00
Leni Aniva
9b1dd0ffda
chore: Update flake
2024-07-06 19:58:55 -07:00
Leni Aniva
4549ae1f65
Merge branch 'misc/version' into tactic/eval
2024-07-06 19:56:31 -07:00
Leni Aniva
c404564a2b
chore: Bump Lean version to 4.10.0-rc1
2024-07-06 19:53:50 -07:00
Leni Aniva
6ddde2963d
test: Eval instantiate
2024-06-27 14:51:16 -04:00
Leni Aniva
fc0d872343
refactor: Simplify proof test infrastructure
2024-06-27 14:34:21 -04:00
Leni Aniva
2d2ff24017
feat: FFI interface for `evaluate` tactic
2024-06-25 17:10:31 -04:00
Leni Aniva
7acf1ffdf1
refactor: Move `have` to prograde tactic
2024-06-25 16:58:35 -04:00
Leni Aniva
58f9d72288
test: Evaluate tactic context
2024-06-25 16:18:31 -04:00
Leni Aniva
c0124b347f
Merge branch 'serial/expr' into tactic/eval
2024-06-25 16:05:20 -04:00
Leni Aniva
8e78718447
feat: Extract MetaM context and state from goal
2024-06-25 15:54:55 -04:00
Leni Aniva
ffbea41f62
feat: Condensed interface
2024-06-25 15:13:58 -04:00
Leni Aniva
e282d9f781
test: Evaluation tactic
2024-06-25 11:03:08 -04:00
Leni Aniva
25a7025c25
feat: Evaluation tactic
2024-06-23 15:01:51 -07:00
Leni Aniva
472cd54868
Merge pull request 'refactor: Cleanup the congruence tactics' ( #81 ) from tactic/congruence into dev
...
Reviewed-on: #81
2024-06-23 13:35:36 -07:00
Leni Aniva
fbe6e8fcb3
Merge branch 'dev' into tactic/congruence
2024-06-23 13:35:07 -07:00
Leni Aniva
361e2e8926
Merge pull request 'fix: aux lemmas in env inspect' ( #82 ) from env/inspect into dev
...
Reviewed-on: #82
2024-06-23 13:33:35 -07:00
Leni Aniva
aceee85b05
Merge branch 'env/inspect' into tactic/congruence
2024-06-16 13:46:18 -07:00
Leni Aniva
8707dbc9bb
fix: aux lemmas in env inspect
2024-06-16 13:44:57 -07:00
Leni Aniva
f80d90ce87
fix: Goal diag missing newline character
2024-06-14 11:59:02 -07:00
Leni Aniva
b3a60fcea8
refactor: Rename TacticExecute to SyntheticTactic
2024-06-13 14:25:05 -07:00
Leni Aniva
bd20bf76da
Merge pull request 'feat: Elementarized tactics with motives, congruence, and absurdity' ( #72 ) from goal/mapply into dev
...
Reviewed-on: #72
2024-06-12 13:52:45 -07:00
Leni Aniva
2d2cf75183
Merge branch 'dev' into goal/mapply
2024-06-12 13:44:49 -07:00
Leni Aniva
c0e6e3ec39
Merge branch 'parse/level' into goal/mapply
2024-06-11 15:21:35 -07:00
Leni Aniva
773a0afbd8
feat: Handling of universe level names in elab
2024-06-11 12:44:42 -07:00
Leni Aniva
3a53493089
feat: Show delayed assignment in goal diag
2024-06-05 16:14:52 -07:00
Leni Aniva
6dcff8b151
fix: Print diag in mvar context
2024-06-05 15:56:20 -07:00
Leni Aniva
3c90c94645
fix: Execute instantiateAll in goal state diag
2024-06-05 13:45:13 -07:00
Leni Aniva
67e7f22b0a
Merge pull request 'feat: Extraction of tactics from compiler' ( #76 ) from compile/tactic into dev
...
Reviewed-on: #76
2024-05-31 20:23:50 -07:00
Leni Aniva
a2c5c7448c
chore: Code simplification, version bump
2024-05-31 20:23:10 -07:00
Leni Aniva
855e771609
feat: Add compilation unit boundary command
2024-05-31 16:35:46 -07:00
Leni Aniva
b9b16ba0e9
refactor: Code cleanup
2024-05-28 20:24:23 -07:00
Leni Aniva
09628309a9
feat: Basic tactic extraction (before/after/tactic)
2024-05-28 17:25:22 -07:00
Leni Aniva
bd42c396d7
chore: Code cleanup
2024-05-20 14:19:10 -07:00
Leni Aniva
bbc00cbbb8
feat: Congruence tactic FFI interface and tests
2024-05-20 14:00:04 -07:00
Leni Aniva
75df7268c5
test: Simplify testing structure for tactics
2024-05-20 11:55:38 -07:00
Leni Aniva
92acf7782c
test: CongruenceArg tactic
2024-05-20 11:51:35 -07:00
Leni Aniva
cf1c884c8c
Merge branch 'dev' into goal/mapply
2024-05-20 11:08:14 -07:00
Leni Aniva
cc74d41b15
feat: Congruence tactics
2024-05-20 10:55:52 -07:00
Leni Aniva
2f951c8fef
fix: Decoupling of mvars during instantiation
2024-05-19 15:43:10 -07:00
Leni Aniva
0aec757601
Merge pull request 'doc: README.md fix' ( #73 ) from doc/readme into dev
...
Reviewed-on: #73
2024-05-17 20:33:18 -07:00
Leni Aniva
e05c01109c
Merge branch 'dev' into doc/readme
2024-05-17 20:32:56 -07:00
Leni Aniva
e165e41efa
chore: Version bump to v4.8.0-rc1
2024-05-17 20:31:45 -07:00
Leni Aniva
6ad24b72d4
fix: Nested delayed assignment instantiation
2024-05-16 10:31:38 -07:00
Leni Aniva
cf17428001
fix: Panic in partial instantiation
2024-05-15 21:34:36 -07:00
Leni Aniva
5c7bb288b2
feat: Display full free variable list in subst
2024-05-14 19:09:04 -07:00
Leni Aniva
bc09f4a29d
refactor: Expr related functions to Expr.lean
2024-05-13 13:58:50 -07:00
Leni Aniva
f813d4a8dd
refactor: Delayed mvar instantiation function
2024-05-13 13:49:05 -07:00
Leni Aniva
c04b363de7
feat: Handle delay assigned mvars
2024-05-12 22:33:38 -07:00
Leni Aniva
03ecb6cf19
feat: Partial instantiate metavariables
2024-05-11 20:01:34 -07:00
Leni Aniva
0b88f6708e
test: Delayed mvar assignment for mapply
2024-05-09 14:02:43 -07:00
Leni Aniva
e58dbc66a9
fix: Consistent naming in library functions
2024-05-08 20:51:36 -07:00
Leni Aniva
66a5dfcf3c
feat: Diagnostics command for FFI users
2024-05-08 12:41:21 -07:00
Leni Aniva
69ec70ffbe
feat: Do not explicitly show delay assigned mvar
2024-05-06 22:39:17 -07:00
Leni Aniva
aa106f7591
feat: Do not filter mvars from mapply
2024-05-06 22:20:20 -07:00
Leni Aniva
679871cbc6
fix: NoConfuse arg name
2024-05-05 13:26:46 -07:00
Leni Aniva
2937675044
feat: Library interface for calling no_confuse
2024-05-05 13:25:48 -07:00
Leni Aniva
cf1289f159
feat: NoConfuse tactic
2024-05-05 13:24:29 -07:00
Leni Aniva
1e1995255a
test: mapply captures dependent types
2024-05-05 10:36:43 -07:00
Leni Aniva
63417ef179
fix: Motive extra arguments not instiantiated
2024-05-05 00:43:32 -07:00
Leni Aniva
4cff6677d2
chore: Lean version bump to 4.8.0-rc1
2024-05-04 23:36:42 -07:00
Leni Aniva
6ffb227cd6
feat: Conduit modus ponens
2024-04-22 10:02:09 -07:00
Leni Aniva
feff62a3c5
fix: Remove determination of major
2024-04-22 09:52:13 -07:00
Leni Aniva
3812aa56ec
feat: Phantom var in mapply
2024-04-22 00:11:41 -07:00
Leni Aniva
4a92e655f6
test: Tactic test stub
2024-04-20 13:09:41 -07:00
Leni Aniva
398b1c39ed
refactor: Common tactic execute function
2024-04-19 12:37:17 -07:00
Leni Aniva
fec13ddb51
chore: Code cleanup
2024-04-18 14:19:25 -07:00
Leni Aniva
7531ad628c
doc: Documentation about conditional arguments
2024-04-15 20:00:59 -07:00
Leni Aniva
52e5b5df50
doc: README.md fix
2024-04-15 19:57:05 -07:00
Leni Aniva
7aa7e6d7e9
feat: Library interface for mapply
2024-04-15 12:56:28 -07:00
Leni Aniva
dbd54f7679
feat: Implement the mapply tactic
2024-04-15 12:47:02 -07:00
Leni Aniva
75b4648ba9
feat: mapply stub
2024-04-14 15:40:57 -07:00
Leni Aniva
b954f12526
refactor: Move all tactic operations to the bottom
2024-04-13 19:41:49 -07:00
Leni Aniva
adbb07af2d
fix: Option setting in REPL
2024-04-12 22:39:47 -07:00
Leni Aniva
72dd20ea87
Merge pull request 'feat: Let tactic' ( #70 ) from goal/let into dev
...
Reviewed-on: #70
2024-04-12 21:42:32 -07:00
Leni Aniva
614b9aa4ae
Merge branch 'dev' into goal/let
2024-04-12 21:41:56 -07:00
Leni Aniva
b45b90b810
test: Metavariable name matches in let
2024-04-12 21:41:16 -07:00
Leni Aniva
07094730b7
Merge pull request 'feat: Option to collect dependent metavariables' ( #69 ) from serial/goal into dev
...
Reviewed-on: #69
2024-04-12 21:33:00 -07:00
Leni Aniva
77907fd060
feat: `goalLet` function
2024-04-12 21:30:56 -07:00
Leni Aniva
4ee955c21f
test: Tests the `let` tactic
2024-04-12 21:16:00 -07:00
Leni Aniva
4b01af7cef
Merge branch 'dev' into serial/goal
2024-04-12 20:52:38 -07:00
Leni Aniva
00a3613036
Merge pull request 'fix: Prevent incorrect inheritance of calc rhs' ( #66 ) from goal/calc into dev
...
Reviewed-on: #66
2024-04-12 20:52:17 -07:00
Leni Aniva
e5d55e31ff
feat: Print expression dependent mvars
2024-04-12 20:51:54 -07:00
Leni Aniva
8e377c2092
refactor: CamelCase rename
2024-04-12 16:34:21 -07:00
Leni Aniva
991ee5ad94
refactor: Rename functions to camel case
2024-04-12 12:37:37 -07:00
Leni Aniva
7a4d462a87
Merge branch 'dev' into goal/calc
2024-04-11 17:58:45 -07:00
Leni Aniva
4d4f660f3f
chore: Update version
2024-04-11 17:57:24 -07:00
Leni Aniva
a864c4d3ff
refactor: Code simplification
2024-04-11 16:29:47 -07:00
Leni Aniva
e834765896
refactor: Code simplification
2024-04-11 16:25:17 -07:00
Leni Aniva
dc6e79def7
doc: Update error message in interaction
2024-04-11 16:18:04 -07:00
Leni Aniva
036fab0ad6
fix: Prevent incorrect inheritance of calc rhs
2024-04-11 16:15:58 -07:00
Leni Aniva
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
2024-04-11 15:36:19 -07:00
Leni Aniva
a41b95e540
Merge branch 'dev' into goal/have-conv-calc
2024-04-11 15:35:30 -07:00
Leni Aniva
a11df9f2e9
feat: Print recursor rules
2024-04-11 15:35:14 -07:00
Leni Aniva
ed220bc7fb
doc: New tactics in README.md
2024-04-11 15:13:12 -07:00
Leni Aniva
7eb5419f36
feat: REPL interface for `calc`
2024-04-11 15:11:10 -07:00
Leni Aniva
6d85c19589
feat: Add library bindings for calc
2024-04-11 15:04:36 -07:00
Leni Aniva
6b44d9ef14
fix: Remove `calcPrevRhs?` in non-calc tactics
2024-04-11 15:03:14 -07:00
Leni Aniva
535770bbd7
feat: Calc tactic
2024-04-11 14:59:55 -07:00
Leni Aniva
823c9635c7
fix: Leading element in .proj sexp
2024-04-09 10:06:26 -07:00
Leni Aniva
55b44c3fa1
fix: Serialization of .proj
2024-04-09 10:03:36 -07:00
Leni Aniva
30c1fd894f
fix: Coupling from unrelated goals
2024-04-09 09:11:15 -07:00
Leni Aniva
f02f9592d7
feat: Focus command
2024-04-08 13:12:51 -07:00
Leni Aniva
0e63583a1d
refactor: Monads in library
2024-04-08 12:54:02 -07:00
Leni Aniva
d4e49310f0
feat: FFI interface to conv functions
2024-04-08 12:50:41 -07:00
Leni Aniva
2f48cfbc19
doc: Remove outdated comments
2024-04-08 12:45:03 -07:00
Leni Aniva
22bb818a1c
refactor: Use the `tactic interface for `conv
2024-04-08 12:32:27 -07:00
Leni Aniva
63e64a1e9f
feat: Conv tactic functions
2024-04-08 12:26:22 -07:00
Leni Aniva
7af24a4f0a
Merge branch 'dev' into goal/have-conv-calc
2024-04-08 10:38:18 -07:00
Leni Aniva
09189ce600
perf: Lazy run print monads
2024-04-08 10:32:13 -07:00
Leni Aniva
19d2f5ff3f
feat: Conv tactic mode
2024-04-07 17:03:49 -07:00
Leni Aniva
d50720f622
refactor: Metavariable set diff function
2024-04-07 14:32:25 -07:00
Leni Aniva
d9ed051b4d
feat: Partial implementation of `conv`
2024-04-07 14:22:20 -07:00
Leni Aniva
38cb91652f
Merge branch 'dev' into goal/have-conv-calc
2024-04-06 22:04:52 -07:00
Leni Aniva
013cb8bb57
Merge pull request 'fix: Auto bound implicit in elab' ( #60 ) from elab/level into dev
...
Reviewed-on: #60
2024-04-06 22:04:31 -07:00
Leni Aniva
7fe73551c3
feat: The `have` tactic
2024-04-06 21:52:25 -07:00
Leni Aniva
5a60ca74d5
fix: Auto bound implicit in elab
2024-04-06 17:45:36 -07:00
Leni Aniva
41cb3f68cd
test: Tests for conv and calc
2024-04-06 17:22:09 -07:00
Leni Aniva
058f5a98b2
feat: Bindings for the `have` tactic
2024-04-06 16:40:22 -07:00
Leni Aniva
1b7b6a644b
feat: `GoalState.tryHave` tactic (tests failing)
2024-04-06 16:33:20 -07:00
Leni Aniva
042dc8f530
doc: Documentation for `nix flake check`
2024-04-06 14:15:58 -07:00
Leni Aniva
92351c9a3d
test: Move parallelism to Test/Main.lean
2024-04-06 14:14:30 -07:00
Leni Aniva
8a447e67cd
test: Parallel testing infrastructure
2024-04-06 14:07:13 -07:00
Leni Aniva
ed196494c1
Merge pull request 'feat: Instantiate mvars during echo' ( #56 ) from expr/echo into dev
...
Reviewed-on: #56
2024-03-31 17:10:29 -07:00
Leni Aniva
8b43dc0f25
feat: Instantiate mvars during echo
2024-03-31 17:09:24 -07:00
Leni Aniva
744c9ee286
Merge pull request 'feat: Specify type in echo' ( #55 ) from expr/echo into dev
...
Reviewed-on: #55
2024-03-31 16:45:43 -07:00
Leni Aniva
9c8cc33e07
Merge pull request 'fix: Instantiation causes infinite loop' ( #54 ) from output/expr into dev
...
Reviewed-on: #54
2024-03-31 16:43:53 -07:00
Leni Aniva
216bb9e920
test: Library test
2024-03-31 16:43:30 -07:00
Leni Aniva
f462843218
docs: Update README.md
2024-03-31 16:12:23 -07:00
Leni Aniva
a1ed8f4b3d
refactor: Use library functions when possible
2024-03-31 16:11:41 -07:00
Leni Aniva
7988a25ce8
refactor: Use library goalStartExpr function
2024-03-31 16:06:30 -07:00
Leni Aniva
2802cc204f
feat: Specify type in echo
2024-03-31 15:55:08 -07:00
Leni Aniva
e9c9548f17
fix: unfoldAuxLemma should be coreM
2024-03-31 15:40:14 -07:00
Leni Aniva
2b71203c1e
fix: Instantiation causes infinite loop
2024-03-30 00:17:16 -07:00
Leni Aniva
f939388dbf
Merge pull request 'feat: Instantiation tests' ( #52 ) from io/serial into dev
...
Reviewed-on: #52
2024-03-30 00:08:32 -07:00
Leni Aniva
2c48ff9e42
Merge branch 'dev' into io/serial
2024-03-30 00:07:46 -07:00
Leni Aniva
621b10c354
Merge pull request 'fix: Build failure on macOS due to LLVM version' ( #53 ) from misc/toolchain into dev
...
Reviewed-on: #53
2024-03-30 00:07:26 -07:00
Leni Aniva
73e4c1d81c
doc: Reason why not to follow nixpkgs
2024-03-30 00:03:37 -07:00
Leni Aniva
7f6b57bc08
Merge branch 'dev' into misc/toolchain
2024-03-30 00:01:24 -07:00
Leni Aniva
140055b16b
fix: Update flake so lean builds on Darwin
2024-03-29 23:59:14 -07:00
Leni Aniva
1bea2ca4e1
fix: Lean build failure on macOS
2024-03-29 23:50:30 -07:00
Leni Aniva
e09a6c7c9d
Merge pull request 'feat: Query arbitrary assignment in goal' ( #47 ) from goal/relation into dev
...
Reviewed-on: #47
2024-03-29 23:48:20 -07:00
Leni Aniva
10e6877f0e
Merge branch 'dev' into goal/relation
2024-03-29 23:47:09 -07:00
Leni Aniva
252f85e66c
feat: Instantiation tests
...
Note that delay assigned metavariables are not instantiated.
2024-03-29 23:46:08 -07:00
Leni Aniva
14011945a0
Merge pull request 'chore: Version bump and toolchain cleanup' ( #51 ) from misc/toolchain into dev
...
Reviewed-on: #51
2024-03-28 22:36:25 -07:00
Leni Aniva
2ea8b1c73c
Merge branch 'dev' into misc/toolchain
2024-03-28 22:35:48 -07:00
Leni Aniva
431e81ca2f
Merge pull request 'feat: Remove display of implementation details' ( #50 ) from io/serial into dev
...
Reviewed-on: #50
2024-03-28 22:35:37 -07:00
Leni Aniva
cfd74aba91
build: Dev shell
2024-03-28 22:26:46 -07:00
Leni Aniva
4a1114ab00
build: Ignore test files when building target
2024-03-28 22:23:19 -07:00
Leni Aniva
4a89aaf70e
doc: Main README.md
2024-03-28 22:12:11 -07:00
Leni Aniva
46faa5c089
chore: Version bump
2024-03-28 22:08:22 -07:00
Leni Aniva
e79e386b39
test: Catalog has no numeric symbols
2024-03-28 20:44:09 -07:00
Leni Aniva
8fa1a7d383
feat: Stop cataloging internal/detail dependencies
2024-03-28 19:49:44 -07:00
Leni Aniva
9e68a9cae4
test: Elimination of aux lemmas
2024-03-28 19:27:45 -07:00
Leni Aniva
a698a4250f
feat: Unfold aux lemmas when printing root expr
2024-03-28 18:56:42 -07:00
Leni Aniva
47fabf333b
doc: Update README.md
2024-03-28 11:37:07 -07:00
Leni Aniva
62d20be841
build: Nix build targets and checks
2024-03-28 11:33:15 -07:00
Leni Aniva
516ab15961
feat: Bump toolchain version
2024-03-28 00:06:35 -07:00
Leni Aniva
f016d60d07
chore: Version bump to 0.2.13
2024-03-16 19:00:28 -07:00
Leni Aniva
aae19ec942
chore: Version bump to 4.8.0 prerelease
2024-03-15 18:44:28 -07:00
Leni Aniva
81aabc52ea
chore: Lean version bump to 4.7.0-rc2
...
Multithreading in ABI was not stabilized in 4.1.0
2024-03-15 06:01:25 -07:00
Leni Aniva
e6dbf88ce2
fix: Use Arrays only in the ABI
2024-03-14 22:40:14 -07:00
Leni Aniva
3debcc021a
feat(lib): Export goal.print function
2024-03-14 16:34:01 -07:00
Leni Aniva
4eec930dd4
fix: Pass options by reference
2024-03-11 21:31:59 -07:00
Leni Aniva
ef864ea16d
feat(lib): Option creation function
2024-03-10 15:33:32 -07:00
Leni Aniva
0b91c41ad2
fix: Execute expr parsing within goal.start
2024-03-10 15:09:38 -07:00
Leni Aniva
a5b0721482
feat(lib): Expose goal state interface
2024-03-10 08:13:10 -07:00
Leni Aniva
996f16bbb8
feat(lib): CoreM execution function
2024-03-10 06:41:35 -07:00
Leni Aniva
f18a9dd1d5
refactor: Move some functions to `Library.lean`
2024-03-09 20:37:48 -08:00
Leni Aniva
eeb149a32c
feat(lib): Search path function
2024-03-09 19:36:25 -08:00
Leni Aniva
2ad7ad8778
feat(lib): Catalog command FFI
2024-03-09 16:50:36 -08:00
Leni Aniva
7bc0f82654
feat: Add exported version function
2024-03-08 23:50:44 -08:00
Leni Aniva
267d635c05
feat(build): Add shared facet for lean_lib
2024-03-06 15:27:22 -08:00
Leni Aniva
93b7d8b67d
feat: Output shared library in flake
2024-03-06 15:26:35 -08:00
Leni Aniva
7e28ded23f
test: More diagnostics for tests
2024-03-06 15:14:08 -08:00
Leni Aniva
cb0712ccf6
Merge pull request 'feat: Print parent expression assignment' ( #45 ) from goal/relation into dev
...
Reviewed-on: #45
2024-02-15 14:55:02 -08:00
Leni Aniva
111781816f
test: Delayed metavariable assignment
2024-02-15 14:47:09 -08:00
Leni Aniva
18c318cb73
Merge branch 'dev' into goal/relation
2024-02-15 14:39:30 -08:00
Leni Aniva
0254759581
Merge pull request 'feat: Add leanpkgs to the flake output' ( #46 ) from nix/toolchain into dev
...
Reviewed-on: #46
2024-02-15 14:30:30 -08:00
Leni Aniva
df4e044e5f
chore: Expose `leanPkgs` in flake
2024-02-13 15:30:56 -05:00
Leni Aniva
5f5d06f1d8
feat: Add lake and lean to the package output
2024-02-05 11:50:22 -08:00
Leni Aniva
4acd367ca7
chore: Version bump to 0.2.12-alpha
2024-01-30 17:45:32 -08:00
Leni Aniva
fe5c1eda7d
feat: Prevent crash during rootExpr call
2024-01-30 17:22:20 -08:00
Leni Aniva
40d61fecc5
doc: Correct comment about parent filling expr
2024-01-30 16:37:35 -08:00
Leni Aniva
25f3a2f19d
feat: Print parent expression assignment
2024-01-24 18:19:04 -08:00
Leni Aniva
d5ef05a7b0
Merge pull request 'test: Option controlled mvar instantiation' ( #44 ) from goal/diag into dev
...
Reviewed-on: #44
2024-01-17 22:27:44 -08:00
Leni Aniva
34d9b02797
Merge branch 'dev' into goal/diag
2024-01-17 14:03:19 -08:00
Leni Aniva
30eda7ef8c
Merge pull request 'feat: Print inductives, constructors, and recursors in env.inspect' ( #43 ) from env/inspect into dev
...
Reviewed-on: #43
2024-01-17 14:02:55 -08:00
Leni Aniva
6a81d83c1f
test: Option controlled mvar instantiation
2024-01-16 16:44:54 -08:00
Leni Aniva
50ac2fea4b
feat: Print constructor and recursor info
2024-01-16 14:11:52 -08:00
Leni Aniva
6fb1b2e787
feat: Print inductives in env.inspect
2024-01-16 13:29:30 -08:00
Leni Aniva
6692303da6
test: Simplify monad execution
2024-01-07 14:14:20 -08:00
Leni Aniva
a8bfa56587
Merge pull request 'feat: Add definitions and theorems to the environment' ( #41 ) from env/add-decl into dev
...
Reviewed-on: #41
2023-12-26 12:41:01 -08:00
Leni Aniva
1c370ef2ae
refactor: Rename Test/{Catalog,Environment}
2023-12-26 12:22:57 -05:00
Leni Aniva
dc90b6b73e
chore: Move environment functions to its own file
...
Symbol.lean is now subsumed
2023-12-15 13:40:36 -05:00
Leni Aniva
da194a1165
refactor: env. operations into its own file
2023-12-15 13:37:55 -05:00
Leni Aniva
aef93cf506
fix: Force instantiate all mvars in env.add
2023-12-15 13:07:59 -05:00
Leni Aniva
a540dd4540
test: env.add
2023-12-14 11:11:24 -08:00
Leni Aniva
85eb42207c
fix: env_add monads
2023-12-14 05:52:12 -08:00
Leni Aniva
69be7c3920
Merge branch 'dev' into env/add-decl
2023-12-14 05:48:49 -08:00
Leni Aniva
83ff58dffc
Merge pull request 'feat: Change the main interaction monad' ( #40 ) from core/loop into dev
...
Reviewed-on: #40
2023-12-14 05:46:39 -08:00
Leni Aniva
3c96a7c0ea
feat: env_add command
2023-12-13 19:35:32 -08:00
Leni Aniva
ff4671cdd0
chore: Rename lib. commands to env.
...
This is done to improve clarity and align with Lean's terminology
2023-12-12 18:56:25 -08:00
Leni Aniva
085b12c255
feat: Use CoreM as the main interaction monad
2023-12-12 18:39:02 -08:00
Leni Aniva
ac9f6f810c
doc: TermElabM metavariable generation
2023-12-08 17:32:30 -08:00
Leni Aniva
bd0c66facc
fix: Consolidate TermElabM blocks
2023-12-08 17:31:25 -08:00
Leni Aniva
2fe4fa9bc4
fix: Change the main interaction monad to MetaM
2023-12-08 16:17:16 -08:00
Leni Aniva
d7fcc502f9
chore: Version downgrade to 0.2.10-alpha
...
There is a currently known bug
2023-12-07 12:38:02 -08:00
Leni Aniva
94c4b2cfe3
Merge pull request 'fix: Printing projection leads to crash' ( #37 ) from io/sexp into dev
...
Reviewed-on: #37
2023-12-07 12:33:01 -08:00
Leni Aniva
924a67f46d
doc: getUsedConstants bug about projections
2023-12-06 15:05:04 -08:00
Leni Aniva
8a8db545a5
fix: Printing projection leads to crash
2023-12-05 22:45:59 -08:00
Leni Aniva
f2b54ec018
Merge pull request 'feat: Handling of private names' ( #36 ) from library/catalog into dev
...
Reviewed-on: #36
2023-12-05 20:22:38 -08:00
Leni Aniva
3c2d93259f
Merge branch 'dev' into library/catalog
2023-12-05 20:21:22 -08:00
Leni Aniva
079f12d6d3
chore: Version bump
2023-12-05 20:21:07 -08:00
Leni Aniva
d846210b9e
Merge pull request 'feat: Print structural projection as application' ( #35 ) from io/serial into dev
...
Reviewed-on: #35
2023-12-05 20:20:51 -08:00
Leni Aniva
dbfee00420
feat!: Display public name only if name is private
2023-12-05 20:20:08 -08:00
Leni Aniva
cdb1e8576f
feat: Display whether a symbol is private
2023-12-05 19:07:00 -08:00
Leni Aniva
c80d7567b6
feat: Expose _private names
2023-12-04 23:36:09 -08:00
Leni Aniva
f72a82a4c9
feat: Remove stem deduce
...
Some private subproofs are not shown in the catalog and this breaks
dependencies
2023-12-04 16:40:15 -08:00
Leni Aniva
35f411041e
feat: Remove printing projections
2023-12-04 16:21:02 -08:00
Leni Aniva
860d2e239a
feat: Remove | in symbol output
2023-11-27 09:54:41 -08:00
Leni Aniva
e0cfdfaf16
chore: Version bump to 0.2.9
2023-11-26 23:48:47 -08:00
Leni Aniva
fe850ded98
feat: Shorter symbol category
2023-11-26 22:14:58 -08:00
Leni Aniva
aaebb6b121
feat: Read dependencies of library symbols
2023-11-25 15:07:56 -08:00
Leni Aniva
a1d991f5db
fix: Rectify error format
2023-11-09 22:24:17 -08:00
Leni Aniva
cc9e659c06
Merge pull request 'feat: Allow selective continuation of goals' ( #27 ) from goal/continuation into dev
...
Reviewed-on: #27
2023-11-07 16:49:55 -08:00
Leni Aniva
a491316541
fix: Do not show parent state in continue
2023-11-07 13:10:14 -08:00
Leni Aniva
e654613182
fix: New goal state not inserted correctly
2023-11-07 13:07:50 -08:00
Leni Aniva
d35803791e
Merge branch 'dev' into goal/continuation
2023-11-07 12:11:14 -08:00
Leni Aniva
d9745094fa
fix: Remove the error prone SemihashMap
2023-11-07 12:09:54 -08:00
Leni Aniva
53b63bf46c
fix: Remove the error prone SemihashMap
2023-11-07 12:04:17 -08:00
Leni Aniva
4396da3e65
chore: Code formatting
2023-11-06 12:20:08 -08:00
Leni Aniva
ce585f7288
feat: Print the root mvar name
2023-11-06 11:51:31 -08:00
Leni Aniva
32fedede6a
Merge branch 'dev' into goal/continuation
2023-11-06 11:45:24 -08:00
Leni Aniva
8182da436d
chore: Remove unnecessary unsafe's
2023-11-06 11:43:57 -08:00
Leni Aniva
c6bb4be597
chore: Update documentation
2023-11-06 11:04:28 -08:00
Leni Aniva
ce1cb13e54
fix: Use Lean's built in name parser
...
The `str_to_name` parser cannot handle numerical names and escapes.
2023-11-06 10:45:11 -08:00
Leni Aniva
a5b5e01858
chore: Version bump to 0.2.8
2023-11-04 15:54:28 -07:00
Leni Aniva
4be9dbc84a
feat: Goal continuation fails if target has goals
2023-11-04 15:53:57 -07:00
Leni Aniva
97d658cfc5
feat: Add goal.continue command
2023-11-04 15:51:09 -07:00
Leni Aniva
333355a85d
feat: Partial state continuation
2023-11-04 15:33:53 -07:00
Leni Aniva
4a4a33cea7
test: Separate mvar coupling tests
2023-11-04 15:01:41 -07:00
Leni Aniva
1638c308a9
Merge pull request 'feat: Minor updates to serialization' ( #26 ) from io/serial into dev
...
Reviewed-on: #26
2023-10-30 14:47:41 -07:00
Leni Aniva
59ac83f0b7
bug: Fix quote escape problem
2023-10-30 14:45:43 -07:00
Leni Aniva
d1c0dc376f
feat: Print metavariable name in goal
2023-10-30 14:44:06 -07:00
Leni Aniva
6cf328a84f
Merge pull request 'feat: Simplify printing of names and expressions' ( #25 ) from io/serial into dev
...
Reviewed-on: #25
2023-10-29 13:08:05 -07:00
Leni Aniva
1a99a2e7b2
fix: Sanitize name in universe levels
2023-10-29 13:03:48 -07:00
Leni Aniva
60854525b9
feat: Simplify printing of function applications
2023-10-29 12:50:36 -07:00
Leni Aniva
e523e8bcc6
chore: Version bump (breaking change)
2023-10-29 11:57:24 -07:00
Leni Aniva
de250eafd0
feat: Print names in one segment separated with .
2023-10-29 11:56:56 -07:00
Leni Aniva
c0dfa04b18
feat: Simplify name printing
2023-10-29 11:18:35 -07:00
Leni Aniva
4ce932eb3b
Merge pull request 'Enable handling of m-Coupled goals' ( #20 ) from goal/dependency into dev
...
Reviewed-on: #20
2023-10-27 19:30:20 -07:00
Leni Aniva
045181356c
feat: Add REPL function for root expression
2023-10-27 15:41:12 -07:00
Leni Aniva
41e1f64d44
Merge branch 'dev' into goal/dependency
2023-10-27 15:33:47 -07:00
Leni Aniva
3b1746490d
feat: Add REPL command for assigning an expression
2023-10-27 15:32:59 -07:00
Leni Aniva
f064bb21a4
feat: Assigning a goal with an expression
2023-10-27 15:15:22 -07:00
Leni Aniva
269e5c707c
refactor: Separate goal printing and processing
...
Added a test for delta proof variables
2023-10-26 22:47:42 -07:00
Leni Aniva
c852db2f46
test: m-coupled goals
2023-10-26 11:22:02 -07:00
Leni Aniva
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
2023-10-25 22:18:59 -07:00
Leni Aniva
d991533170
feat: Add proof continue and root extraction
2023-10-25 16:03:45 -07:00
Leni Aniva
a9294e0338
Add documentation about flake
2023-10-20 12:54:35 -07:00
Leni Aniva
3d7d5d6b4d
feat: Add nix flake
2023-10-20 12:41:56 -07:00
Leni Aniva
538ba6e7d7
Store states instead of goals
...
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
2023-10-15 17:15:23 -07:00
Leni Aniva
41db295ff5
Rename tactic to goal and restructure
2023-10-15 12:31:22 -07:00
Leni Aniva
7a5fe554ba
Add holes test stub
...
Move tests into their own namespaces
2023-10-06 17:31:36 -07:00
Leni Aniva
13f3460e9a
Fix test failures
2023-10-05 17:51:41 -07:00
Leni Aniva
a8cf94ccb1
Bump Lean version to 4.1.0
2023-10-05 17:49:43 -07:00
Leni Aniva
0948e71d60
Add dependency for lakefile and lean-toolchain
2023-10-02 10:30:58 -07:00
Leni Aniva
6d15d1e670
Use makefile instead of ad-hoc script
2023-10-02 10:26:19 -07:00
Leni Aniva
35b391881e
Add ready message to indicate the main loop is up
2023-10-02 10:14:03 -07:00
Leni Aniva
d7077ce854
Bump lean version to 4.0.0
2023-09-13 21:02:26 -07:00
Leni Aniva
75f43786fb
Merge pull request 'Simplify goal bookkeeping mechanism' ( #10 ) from tactic/book into dev
...
Reviewed-on: #10
2023-08-30 19:18:36 -07:00
Leni Aniva
f538f580bd
Merge branch 'dev' into tactic/book
2023-08-30 19:17:25 -07:00
Leni Aniva
f1f1c20ff9
Add SemihashMap interface, rename proof commands to goal commands, allow deletion
2023-08-30 19:16:33 -07:00
Leni Aniva
6b96f7893f
Separate max and imax in sort level
2023-08-27 22:50:18 -07:00
Leni Aniva
b98304f78a
Version bump to 0.2.4 due to breaking change
2023-08-27 19:59:31 -07:00
Leni Aniva
a6e337a89e
Rename proof commands to goal commands
2023-08-27 19:58:52 -07:00
Leni Aniva
a86af1bc57
Add SemihashMap structure for goal bookkeeping
2023-08-27 19:53:09 -07:00
Leni Aniva
b74119e378
Merge pull request 'Remove the obsolete name field from proof tree structure' ( #11 ) from misc/cleanup into dev
...
Reviewed-on: #11
2023-08-26 18:50:40 -07:00
Leni Aniva
9c4c43a9f1
Remove the obsolete name field from proof tree structure
2023-08-26 18:50:15 -07:00
Leni Aniva
bd4fbcc369
Add test cases for command error categories
2023-08-24 23:12:18 -07:00
Leni Aniva
ff8fed8741
Classify JSON error as command error
...
Also add documentation for this
2023-08-24 22:51:40 -07:00
Leni Aniva
98edaa3297
Merge pull request 'Add more serialisation options' ( #2 ) from io/serial into dev
...
Reviewed-on: #2
2023-08-23 13:29:00 -07:00
Leni Aniva
1f27532769
Merge branch 'dev' into io/serial
2023-08-23 13:25:08 -07:00
Leni Aniva
0c330c8778
Unify json and unknown error into command error
2023-08-23 13:00:11 -07:00
Leni Aniva
59c046efc6
Add proper printing of sorts
2023-08-23 12:51:06 -07:00
Leni Aniva
a8cbb3be4f
Move all json-string functions to Main.lean
2023-08-22 09:54:37 -07:00
Leni Aniva
96cbbf2551
Add compressed json print option; Rearrange commands into hierarchy
2023-08-16 19:25:32 -07:00
Leni Aniva
b2ba26528d
Add proof variable delta; Bump version to 0.2.1
2023-08-15 15:40:54 -07:00
Leni Aniva
7771408de1
Add expression sexp printing (2/2)
2023-08-14 21:43:40 -07:00
Leni Aniva
9eadd1d4d4
Add expression sexp printing (1/2, tests pending)
2023-08-14 17:07:53 -07:00
Leni Aniva
5cedb9d88c
version bump, restructure
2023-08-13 21:19:06 -07:00
Leni Aniva