Commit Graph

710 Commits

Author SHA1 Message Date
Leni Aniva 1a9e450066
refactor: Rename `tomogram` to `tomograph` 2025-06-24 15:23:59 -07:00
Leni Aniva d7001c1b28
chore: Tomogram stub 2025-06-24 15:11:51 -07:00
Leni Aniva 3e266dc505 Merge pull request 'feat(goal): Branch unification' (#217) from goal/branch-unification into dev
Reviewed-on: #217
2025-06-24 13:56:14 -07:00
Leni Aniva 9eb5533166
Merge branch 'dev' into goal/branch-unification 2025-06-24 13:55:34 -07:00
Leni Aniva 7837ddff4f
feat(goal): Unify fragments in replay 2025-06-24 13:51:33 -07:00
Leni Aniva 8982cb13a9 Merge pull request 'feat(serial): Robust environment extension pickling' (#216) from serial/env-extensions into dev
Reviewed-on: #216
2025-06-24 13:41:05 -07:00
Leni Aniva 9b0d96f422
feat(goal): Trace messages for replay 2025-06-24 13:37:49 -07:00
Leni Aniva 9d4b1ae755
refactor(goal): Allow multiple fragments 2025-06-24 13:33:22 -07:00
Leni Aniva 58ae791da3
refactor: `conv` and `calc` into tactic fragments 2025-06-23 20:57:53 -07:00
Leni Aniva 05a8e3b13c
feat: Branch unification (modulo conv/calc) 2025-06-23 13:09:08 -07:00
Leni Aniva cb7c4d2723
chore: Add `_m` suffix to replay 2025-06-20 17:26:04 -07:00
Leni Aniva 343ecc2659
feat(goal): GoalState.replay stub 2025-06-20 17:25:23 -07:00
Leni Aniva cd8c08fe38 Merge pull request 'chore: Update Nix flake' (#214) from chore/toolchain into dev
Reviewed-on: #214
2025-06-20 14:03:06 -07:00
Leni Aniva 9304cf2368
chore: Update version to 0.3.3 2025-06-20 12:29:00 -07:00
Leni Aniva 6323c02f47
test: Fix pickle state name 2025-06-20 12:25:40 -07:00
Leni Aniva dfa491a5c2
test: Pickling of aux lemma 2025-06-20 12:10:31 -07:00
Leni Aniva 9d9f5dee88
test: Use synthetic tactic to generate aux lemmas 2025-06-20 12:00:25 -07:00
Leni Aniva b3f88f5d54
Merge branch 'dev' into serial/env-extensions 2025-06-20 10:50:29 -07:00
Leni Aniva 0db2451c8a Merge pull request 'fix: Use the correct unfold aux lemma' (#215) from bug/unfold-aux-lemma into dev
Reviewed-on: #215
2025-06-20 10:21:00 -07:00
Leni Aniva 771f8ad266
chore: Formatting 2025-06-20 10:20:33 -07:00
Leni Aniva 1b2a2d5c8d
test: Intentionally generate aux lemmas 2025-06-20 10:19:42 -07:00
Leni Aniva 7d9d3e4742
fix: Use the correct unfold aux lemma 2025-06-19 15:48:53 -07:00
Leni Aniva d1d6493d09
chore: Update Nix flake 2025-06-19 14:50:49 -07:00
Leni Aniva 9a8b5040f5 Merge pull request 'chore: Update Lean to v4.20.1' (#209) from chore/toolchain into dev
Reviewed-on: #209
2025-06-18 16:39:18 -07:00
Leni Aniva 66eb98397b
merge: branch 'dev' into chore/toolchain 2025-06-18 15:10:21 -07:00
Leni Aniva 9645f706d4
chore: Update lean4-nix 2025-06-18 14:38:56 -07:00
Leni Aniva b7f0ae435a
test: Use `withTempFile` to ensure graceful exit 2025-06-18 14:35:22 -07:00
Leni Aniva 8fd3649f32 Merge pull request 'chore: Update version to 0.3.2' (#212) from chore/version into dev
Reviewed-on: #212
2025-06-18 14:28:34 -07:00
Leni Aniva 04cbc55f3a
doc: Update invocations usage 2025-06-17 11:56:31 -07:00
Leni Aniva 292fb0be4b
chore: Update version to 0.3.2 2025-06-17 11:54:38 -07:00
Leni Aniva 86f69dd08c Merge pull request 'refactor: Use syntax tactic in unit test' (#207) from goal/tactic into dev
Reviewed-on: #207
2025-06-17 11:51:35 -07:00
Leni Aniva ba84456f89 Merge pull request 'feat: Output tactic invocation data to file' (#208) from frontend/tactic-invocation into dev
Reviewed-on: #208
2025-06-17 11:42:36 -07:00
Leni Aniva a8b7f69632
fix(env): Use documentUriFromModule 2025-06-17 11:10:52 -07:00
Leni Aniva b2b7cc388a
chore: Fix most test failures 2025-06-17 10:54:10 -07:00
Leni Aniva 3ce335ebfe
chore: Update Lean to v4.20.1 2025-06-17 08:38:03 -07:00
Leni Aniva 22716597d3
feat(frontend): Write invocation points to file 2025-06-16 18:10:11 -07:00
Leni Aniva 0bdb41635b
refactor: Use syntax tactic in unit test 2025-06-16 14:05:05 -07:00
Leni Aniva 3d65f6a69e Merge pull request 'chore: Code cleanup' (#202) from chore/cleanup into dev
Reviewed-on: #202
2025-06-16 13:57:26 -07:00
Leni Aniva b7c9867217
Merge branch 'dev' into chore/cleanup 2025-06-16 13:55:53 -07:00
Leni Aniva 975a6f525c Merge pull request 'chore: Update Lean to v4.19.0' (#205) from chore/toolchain into dev
Reviewed-on: #205
2025-06-16 13:54:08 -07:00
Leni Aniva 0fa5ac335e
fix: Load environment extensions 2025-06-16 13:45:57 -07:00
Leni Aniva d41ec67a63
chore: Update Lean to v4.19.0 2025-05-07 09:53:29 -04:00
Leni Aniva eb41c179d1
feat(repl): Conditional environment inheritance 2025-05-02 11:40:32 -04:00
Leni Aniva 4bb44dd56a
chore: Syntax cleanup in repl 2025-05-02 11:33:11 -04:00
Leni Aniva 3bb8e75787
chore: Code cleanup 2025-05-02 11:26:17 -04:00
Leni Aniva 120eb90291 Merge pull request 'chore: Update version' (#195) from chore/version into dev
Reviewed-on: #195
2025-05-01 10:41:47 -07:00
Leni Aniva 7578e9e180 Merge pull request 'doc: Add design limitations about memory' (#200) from doc/rationale into dev
Reviewed-on: #200
2025-05-01 10:40:52 -07:00
Leni Aniva df370b0bff
Merge branch 'dev' into chore/version 2025-05-01 13:39:28 -04:00
Leni Aniva 7b9361c72b Merge pull request 'feat(goal): Detect unsafe and sorry' (#201) from goal/detect-unsafe-sorry into dev
Reviewed-on: #201
2025-05-01 10:37:59 -07:00
Leni Aniva ad55ea1a27
feat(repl): Detection of sorrys 2025-05-01 13:37:35 -04:00