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
|
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 |