Leni Aniva
|
c0090dec97
|
fix: Quote string literal in sexp
|
2024-12-15 12:40:47 -08:00 |
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 |