aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 14 Pull Requests 2 Packages Projects Releases Wiki Activity
750 Commits 4 Branches 26 Tags 1.8 MiB
Commit Graph

750 Commits

Author SHA1 Message Date
Leni Aniva c1c7848bca
chore: Format code 2025-07-02 15:18:02 -07:00
Leni Aniva 48046b8b5a
fix(tomograph): Import search directory 2025-07-02 15:14:11 -07:00
Leni Aniva 80fb7f30c3
Merge branch 'dev' into frontend/tomogram 2025-07-02 15:03:24 -07:00
Leni Aniva 8ee1607b45 Merge pull request 'test(repl): MVar name mismatch fix' (#227) from chore/toolchain into dev 
Reviewed-on: #227
 2025-07-02 15:03:09 -07:00
Leni Aniva 726c2ed145
test(repl): MVar name mismatch fix 2025-07-02 15:02:35 -07:00
Leni Aniva e5a7b30f51
Merge branch 'dev' into frontend/tomogram 2025-07-02 14:59:39 -07:00
Leni Aniva d1998b129a Merge pull request 'chore: Update Lean to v4.21.0' (#223) from chore/toolchain into dev 
Reviewed-on: #223
 2025-07-02 14:59:29 -07:00
Leni Aniva 737fd607e8
refactor: Add heuristic case to `isAuxLemma` 2025-07-02 14:54:13 -07:00
Leni Aniva 1f35820e1d
test: Fix unit test failures 2025-07-02 14:40:47 -07:00
Leni Aniva ec78324f9f
feat(repl): Improve tomograph's info 2025-07-02 14:32:24 -07:00
Leni Aniva 2cec5bc881
Merge branch 'dev' into frontend/tomogram 2025-07-02 13:20:00 -07:00
Leni Aniva 7a18fb1f9c
chore: Update version to v0.3.4 2025-07-01 15:43:21 -07:00
Leni Aniva 4c7f77b7ca Merge pull request 'doc: Remove constraint on pick_goal' (#224) from doc/rationale into dev 
Reviewed-on: #224
 2025-07-01 15:41:55 -07:00
Leni Aniva 50bb48f2ed
doc: Remove constraint on pick_goal 2025-06-30 15:56:48 -07:00
Leni Aniva f26b7fc177 Merge pull request 'fix(goal): Unknown metavariable problem during fragment initialization' (#222) from bug/unknown-metavariable-fragment into dev 
Reviewed-on: #222
 2025-06-30 15:28:28 -07:00
Leni Aniva 16474b2ce8
test(repl): Add test for conv and calc 2025-06-30 15:27:51 -07:00
Leni Aniva 3fab7e7818
fix(repl): Allow .none in parentExpr 2025-06-30 15:08:46 -07:00
Leni Aniva 7b96652c87
chore: Update Lean to v4.21.0 2025-06-30 15:05:07 -07:00
Leni Aniva dd7c6c36c8
fix(goal): Allow parent expr to be fragments 2025-06-30 15:00:30 -07:00
Leni Aniva 8857b88d9a
fix(goal): Restore elaboration monad 2025-06-30 14:52:38 -07:00
Leni Aniva 2a87ed2e46 Merge pull request 'feat(serial): Pickle environment delta's' (#221) from serial/delta into dev 
Reviewed-on: #221
 2025-06-27 16:02:21 -07:00
Leni Aniva f4b6996f9e
test: Ignore branch unification test 
We'll handle this in Lean v4.21.0
 2025-06-27 16:01:13 -07:00
Leni Aniva 349cff6f05
test(goal): Collision of aux lemma names 2025-06-26 16:41:49 -07:00
Leni Aniva f914e161e8
fix(goal): Reset messages in replay 2025-06-26 16:23:10 -07:00
Leni Aniva 4df8fcda97
Merge branch 'dev' into serial/delta 2025-06-26 15:52:36 -07:00
Leni Aniva 7c300e081d Merge pull request 'feat(goal): Add unshielded tactic execution mode' (#219) from goal/automatic-mode into dev 
Reviewed-on: #219
 2025-06-26 15:52:16 -07:00
Leni Aniva 52f71f035e
feat(serial): Background environment in pickling 2025-06-26 15:51:42 -07:00
Leni Aniva 9a9659fdb2
feat(delate): Show fragments for each goal 2025-06-26 14:22:51 -07:00
Leni Aniva 1de8df73f8
refactor(goal): Delete unused functions 2025-06-26 14:08:22 -07:00
Leni Aniva 4d9e229707
refactor(repl): Tactic into goal section 2025-06-26 12:11:27 -07:00
Leni Aniva 7fba24d57a
fix(tactic): Filter out sibling fragments 2025-06-26 11:48:28 -07:00
Leni Aniva 425825bf20
test: Fragment cleanup 2025-06-26 11:45:15 -07:00
Leni Aniva 4b02d73374
fix: Tactic fragments inline with C/R paradigm 2025-06-26 11:37:14 -07:00
Leni Aniva ed5854841b
fix: Allow conv tactics to emit non-conv goals 2025-06-26 10:32:58 -07:00
Leni Aniva 25820aa188
test: Move fragment tests to their own file 2025-06-26 09:52:01 -07:00
Leni Aniva 86f2e64939
feat(repl): Use site to handle automatic mode 2025-06-25 16:27:04 -07:00
Leni Aniva 42bb20df4a
refactor(goal): Use site in goal state functions 2025-06-25 14:35:38 -07:00
Leni Aniva 0b731273b2
refactor(goal): A state can have multiple parents 2025-06-25 13:07:47 -07:00
Leni Aniva 53ea808c90
feat(frontend): Dissect syntax tree 2025-06-24 15:31:46 -07:00
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 8e35926b5c
feat(goal): Tactic action site 2025-06-24 15:05:24 -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