Leni Aniva aniva
0 Followers · 1 Following
  • Stanford University Centaur Lab
  • https://leni.sh

  • Director of NorCal Hakkero Factory No. 1

  • Joined on 2023-08-21
Repositories
13
 Projects Packages Public Activity Starred Repositories
9
aniva commented on issue aniva/Pantograph#197 2025-06-26 13:51:19 -07:00
Goal dependency generation

This will require one tactic to act on two goals at the same time, which is doable, given #219.

aniva pushed to goal/automatic-mode at aniva/Pantograph 2025-06-26 12:11:54 -07:00
4d9e229707 refactor(repl): Tactic into goal section
aniva commented on issue aniva/Pantograph#132 2025-06-26 11:56:26 -07:00
Branch unification

Partially solved by #217 with more unit tests pending.

aniva created pull request aniva/Pantograph#221 2025-06-26 11:50:37 -07:00
feat: Pickle environment delta's
aniva pushed to serial/delta at aniva/Pantograph 2025-06-26 11:49:56 -07:00
aniva created branch serial/delta in aniva/Pantograph 2025-06-26 11:49:56 -07:00
aniva pushed to goal/automatic-mode at aniva/Pantograph 2025-06-26 11:48:43 -07:00
7fba24d57a fix(tactic): Filter out sibling fragments
aniva pushed to goal/automatic-mode at aniva/Pantograph 2025-06-26 11:45:21 -07:00
425825bf20 test: Fragment cleanup
aniva pushed to goal/automatic-mode at aniva/Pantograph 2025-06-26 11:37:44 -07:00
4b02d73374 fix: Tactic fragments inline with C/R paradigm
aniva pushed to goal/automatic-mode at aniva/Pantograph 2025-06-26 10:33:06 -07:00
ed5854841b fix: Allow conv tactics to emit non-conv goals
aniva pushed to goal/automatic-mode at aniva/Pantograph 2025-06-26 09:52:26 -07:00
25820aa188 test: Move fragment tests to their own file
aniva commented on issue aniva/Pantograph#213 2025-06-25 21:33:17 -07:00
🖇️ Articulation and Syntax Processing

I suspect articulation will have to work like Project No. 3 in Trillium, where we need to have a combination of syntax and expression based processing.

aniva pushed to goal/automatic-mode at aniva/Pantograph 2025-06-25 16:27:22 -07:00
86f2e64939 feat(repl): Use site to handle automatic mode
aniva pushed to goal/automatic-mode at aniva/Pantograph 2025-06-25 14:36:00 -07:00
42bb20df4a refactor(goal): Use site in goal state functions
aniva pushed to goal/automatic-mode at aniva/Pantograph 2025-06-25 13:08:11 -07:00
0b731273b2 refactor(goal): A state can have multiple parents
aniva pushed to frontend/tomogram at aniva/Pantograph 2025-06-24 15:31:54 -07:00
53ea808c90 feat(frontend): Dissect syntax tree
aniva pushed to frontend/tomogram at aniva/Pantograph 2025-06-24 15:24:19 -07:00
1a9e450066 refactor: Rename `tomogram` to `tomograph`
aniva commented on issue aniva/Pantograph#213 2025-06-24 15:17:48 -07:00
🖇️ Articulation and Syntax Processing

#220 gives a tool for analyzing the order of MetaM (and below) execution across a Lean file. It is still WIP.

aniva created pull request aniva/Pantograph#220 2025-06-24 15:12:39 -07:00
feat(frontend): Tomogram
aniva pushed to frontend/tomogram at aniva/Pantograph 2025-06-24 15:12:02 -07:00
d7001c1b28 chore: Tomogram stub