Leni Aniva
|
1402a69eea
|
Merge pull request 'fix: `env.add` Declarations with universe levels' (#181) from bug/env-add-level into dev
Reviewed-on: #181
|
2025-03-29 15:48:12 -07:00 |
Leni Aniva
|
664516f148
|
Merge branch 'dev' into bug/env-add-level
|
2025-03-29 15:44:53 -07:00 |
Leni Aniva
|
18446f865e
|
Merge pull request 'test: Update LSpec' (#182) from test/build into dev
Reviewed-on: #182
|
2025-03-29 15:44:28 -07:00 |
Leni Aniva
|
91fbc4cdca
|
chore: Remove redundant code
|
2025-03-29 15:43:49 -07:00 |
Leni Aniva
|
2885671490
|
test: Update LSpec
|
2025-03-29 15:22:31 -07:00 |
Leni Aniva
|
b9ff9e8f13
|
feat(repl): Optional type argument in `env.add`
|
2025-03-29 14:51:35 -07:00 |
Leni Aniva
|
9ea099827f
|
fix(env): Adding declarations with universe levels
|
2025-03-29 14:39:42 -07:00 |
Leni Aniva
|
3c07188cdf
|
Merge pull request 'feat: Tactic with timeout' (#179) from repl/timeout into dev
Reviewed-on: #179
|
2025-03-28 21:31:58 -07:00 |
Leni Aniva
|
0528a1592e
|
fix: Print internal exceptions nicely
|
2025-03-28 21:31:30 -07:00 |
Leni Aniva
|
4610348fed
|
feat: `CoreM` timeout
|
2025-03-28 20:42:10 -07:00 |
Leni Aniva
|
be505b8050
|
feat: Run cancel token with timeout
|
2025-03-28 19:06:43 -07:00 |
Leni Aniva
|
48485a868b
|
Merge pull request 'feat: Update `CoreM` options from parsed header' (#177) from frontend/env-init into dev
Reviewed-on: #177
|
2025-03-28 18:56:21 -07:00 |
Leni Aniva
|
9980fd9c39
|
test(repl): Environment loading from header
|
2025-03-28 18:45:58 -07:00 |
Leni Aniva
|
8adab24157
|
fix: Call sites in `Main.lean`
|
2025-03-28 00:56:18 -07:00 |
Leni Aniva
|
c2b7501649
|
refactor: Remove `CoreM` from `MainM`
|
2025-03-28 00:50:39 -07:00 |
Leni Aniva
|
0fea0b50c9
|
Merge branch 'dev' into frontend/env-init
|
2025-03-25 12:27:32 -07:00 |
Leni Aniva
|
fb91b521fb
|
Merge pull request 'chore: Update Lean to v4.17.0, version to v0.3' (#178) from chore/version into dev
Reviewed-on: #178
|
2025-03-24 18:05:25 -07:00 |
Leni Aniva
|
ebf514b92b
|
chore: Update nix flake
|
2025-03-24 18:04:34 -07:00 |
Leni Aniva
|
d305918bb9
|
chore: Update Lean to v4.17.0
|
2025-03-24 17:57:34 -07:00 |
Leni Aniva
|
3e55b4b22f
|
feat(repl): Record last scope
|
2025-03-24 17:47:56 -07:00 |
Leni Aniva
|
bc37482212
|
Merge pull request 'feat(delate): Unfold matchers' (#176) from delate/instantiate into dev
Reviewed-on: #176
|
2025-03-17 18:37:55 -07:00 |
Leni Aniva
|
cb1082c7c7
|
chore: More code cleanup
|
2025-03-17 12:14:16 -07:00 |
Leni Aniva
|
678cc9b3c0
|
chore: Code cleanup
|
2025-03-17 11:30:24 -07:00 |
Leni Aniva
|
4643992c3b
|
refactor(delate): Unfold matchers into function
|
2025-03-17 11:26:13 -07:00 |
Leni Aniva
|
3b4b196a30
|
feat(delate): Add mdata annotation for matcher
|
2025-03-17 11:20:38 -07:00 |
Leni Aniva
|
a28ad9b239
|
feat(delate): Expand matcher applications
|
2025-03-17 10:47:11 -07:00 |
Leni Aniva
|
dc29d48b77
|
chore: Remove IO.println for trace
|
2025-03-17 09:31:39 -07:00 |
Leni Aniva
|
78485ae6e2
|
doc(frontend): Update documentation for `frontend.process`
|
2025-03-14 20:07:31 -07:00 |
Leni Aniva
|
98ad1ae283
|
feat(delate): Tracing tags
|
2025-03-14 16:54:34 -07:00 |
Leni Aniva
|
8063039f7e
|
Merge pull request 'feat(frontend): Alternative methods of initializing environment' (#173) from frontend/env-init into dev
Reviewed-on: #173
|
2025-03-14 16:48:40 -07:00 |
Leni Aniva
|
ef165b7045
|
fix(frontend): Test update
|
2025-03-14 16:47:46 -07:00 |
Leni Aniva
|
79e4dc697e
|
feat(frontend): Add option to inherit environment
|
2025-03-14 16:46:28 -07:00 |
Leni Aniva
|
8797bbe245
|
test(frontend): Fix the open test
|
2025-03-14 16:35:12 -07:00 |
Leni Aniva
|
896475848b
|
fix: Name generation not available due to context
|
2025-03-10 19:03:14 -07:00 |
Leni Aniva
|
0cfd73e44e
|
test(frontend): Add scope `open` test
|
2025-03-09 23:29:33 -07:00 |
Leni Aniva
|
1dceb5428e
|
Merge pull request 'fix: Manifest key error' (#172) from chore/build into dev
Reviewed-on: #172
|
2025-03-08 22:53:07 -08:00 |
Leni Aniva
|
9e1ea54cbe
|
chore: Cleanup file filtering system
|
2025-03-08 22:52:36 -08:00 |
Leni Aniva
|
5d0a7e8443
|
fix: Manifest key error
|
2025-03-08 22:50:04 -08:00 |
Leni Aniva
|
4f5dd97e55
|
Merge pull request 'chore: Cleanup the library system' (#169) from chore/cleanup into dev
Reviewed-on: #169
|
2025-03-08 21:19:00 -08:00 |
Leni Aniva
|
7ae50696ac
|
merge: branch 'dev' into chore/cleanup
|
2025-03-08 21:18:45 -08:00 |
Leni Aniva
|
9cf071eefe
|
chore: Read manifest for LSpec version
|
2025-03-08 21:16:47 -08:00 |
Leni Aniva
|
92515ea0f2
|
fix: Update flake lock
|
2025-03-08 21:11:59 -08:00 |
Leni Aniva
|
5a690c4421
|
chore: Use `fetchGit` for `LSpec` input
|
2025-03-08 21:11:34 -08:00 |
Leni Aniva
|
39ec79e6bb
|
feat: Monad lifting in `GoalState.withContext`
|
2025-03-08 21:07:15 -08:00 |
Leni Aniva
|
999bb146fa
|
chore: Remove all unused auxiliary tactics
|
2025-03-01 20:12:30 -08:00 |
Leni Aniva
|
642bca42e9
|
Merge pull request 'chore: Version bump' (#168) from chore/version into dev
Reviewed-on: #168
|
2025-02-25 15:16:43 -08:00 |
Leni Aniva
|
ec3e1ff2c0
|
chore: Bump version to 0.3.0-rc.1
|
2025-02-25 15:16:10 -08:00 |
Leni Aniva
|
76639d0266
|
fix: Panic edge case for module name
|
2025-02-24 15:45:31 -08:00 |
Leni Aniva
|
267290c8f7
|
fix: Draft tactic failure by new `sorry` semantics
|
2025-02-23 14:14:59 -08:00 |
Leni Aniva
|
aac39ca60c
|
fix: Some test errors
|
2025-02-23 14:13:44 -08:00 |