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 |