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 |