Leni Aniva

aniva created branch frontend/tomogram in aniva/Pantograph

2025-06-24 15:12:02 -07:00

aniva created pull request aniva/Pantograph#219

2025-06-24 15:06:18 -07:00

feat(goal): Add unshielded tactic execution mode

aniva pushed to goal/automatic-mode at aniva/Pantograph

2025-06-24 15:05:42 -07:00

8e35926b5c feat(goal): Tactic action site

aniva created branch goal/automatic-mode in aniva/Pantograph

2025-06-24 15:05:42 -07:00

aniva deleted branch goal/branch-unification from aniva/Pantograph

2025-06-24 13:56:17 -07:00

aniva pushed to dev at aniva/Pantograph

2025-06-24 13:56:17 -07:00

3e266dc505 Merge pull request 'feat(goal): Branch unification' (#217) from goal/branch-unification into dev

9eb5533166 Merge branch 'dev' into goal/branch-unification

7837ddff4f feat(goal): Unify fragments in replay

9b0d96f422 feat(goal): Trace messages for replay

9d4b1ae755 refactor(goal): Allow multiple fragments

Compare 9 commits »

aniva merged pull request aniva/Pantograph#217

2025-06-24 13:56:15 -07:00

feat(goal): Branch unification

aniva pushed to goal/branch-unification at aniva/Pantograph

2025-06-24 13:55:56 -07:00

9eb5533166 Merge branch 'dev' into goal/branch-unification

8982cb13a9 Merge pull request 'feat(serial): Robust environment extension pickling' (#216) from serial/env-extensions into dev

cd8c08fe38 Merge pull request 'chore: Update Nix flake' (#214) from chore/toolchain into dev

9304cf2368 chore: Update version to 0.3.3

6323c02f47 test: Fix pickle state name

Compare 11 commits »

aniva pushed to goal/branch-unification at aniva/Pantograph

2025-06-24 13:51:56 -07:00

7837ddff4f feat(goal): Unify fragments in replay

aniva deleted branch serial/env-extensions from aniva/Pantograph

2025-06-24 13:41:08 -07:00

aniva pushed to dev at aniva/Pantograph

2025-06-24 13:41:07 -07:00

8982cb13a9 Merge pull request 'feat(serial): Robust environment extension pickling' (#216) from serial/env-extensions into dev

6323c02f47 test: Fix pickle state name

dfa491a5c2 test: Pickling of aux lemma

9d9f5dee88 test: Use synthetic tactic to generate aux lemmas

b3f88f5d54 Merge branch 'dev' into serial/env-extensions

Compare 7 commits »

aniva merged pull request aniva/Pantograph#216

2025-06-24 13:41:06 -07:00

feat(serial): Robust environment extension pickling

aniva pushed to goal/branch-unification at aniva/Pantograph

2025-06-24 13:38:09 -07:00

9b0d96f422 feat(goal): Trace messages for replay

aniva pushed to goal/branch-unification at aniva/Pantograph

2025-06-24 13:33:34 -07:00

9d4b1ae755 refactor(goal): Allow multiple fragments

aniva commented on pull request aniva/Pantograph#217

2025-06-24 11:16:13 -07:00

feat(goal): Branch unification

There is one more problem about conversion tactic mode. In such a mode, a goal state could have a mixture of conversion and non-conversion goals. When we decree an exit from conversion tactic…

aniva commented on pull request aniva/Pantograph#217

2025-06-24 10:02:35 -07:00

feat(goal): Branch unification

We need to think about the interaction between tactic fragments and resumption.

Examples

e.g. If there are states G = { ?0, ?1f } (where ?0f has a fragment) and G' = { ?2, ?3 }, it…

aniva pushed to goal/branch-unification at aniva/Pantograph

2025-06-23 20:58:11 -07:00

58ae791da3 refactor: `conv` and `calc` into tactic fragments

aniva pushed to goal/branch-unification at aniva/Pantograph

2025-06-23 13:09:26 -07:00

05a8e3b13c feat: Branch unification (modulo conv/calc)

aniva commented on issue aniva/Pantograph#188

2025-06-23 09:09:37 -07:00

Unshielded Tactic Execution

The goal for this is a rudimentary form of articulation. If the user executes a series of tactics at goal location 0, then they can string the tactics together to form a proof. It's not a perfect…

aniva pushed to home/cover at aniva/Chrysoblog

2025-06-23 08:58:13 -07:00

ed2f417999 fix: Graphics of the cover