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
12
 Projects Packages Public Activity Starred Repositories
9
aniva created branch misc/cleanup in aniva/Pantograph 2023-08-26 18:49:34 -07:00
aniva pushed to misc/cleanup at aniva/Pantograph 2023-08-26 18:49:34 -07:00
84b2ae653e Remove the obsolete name field from proof tree structure
aniva created pull request aniva/Pantograph#10 2023-08-26 18:10:11 -07:00
WIP: Simplify goal bookkeeping mechanism
aniva pushed to tactic/book at aniva/Pantograph 2023-08-26 18:09:14 -07:00
aniva created branch tactic/book in aniva/Pantograph 2023-08-26 18:09:14 -07:00
aniva opened issue aniva/Pantograph#9 2023-08-24 23:20:14 -07:00
Allow the extraction of tactic based proof steps
aniva pushed to dev at aniva/Pantograph 2023-08-24 23:15:42 -07:00
51edc701fe Add test cases for command error categories
95d26a2f50 Classify JSON error as command error
Compare 2 commits »
aniva merged pull request aniva/Pantograph#7 2023-08-24 23:15:41 -07:00
Error category consolidation
aniva commented on issue aniva/Pantograph#8 2023-08-24 23:14:03 -07:00
Allow deletion of certain proof states and remove proof tree structure

Leaving this until Trillium backend can handle this bookkeeping.

aniva pushed to doc at aniva/Pantograph 2023-08-24 23:12:39 -07:00
51edc701fe Add test cases for command error categories
aniva commented on issue aniva/Pantograph#8 2023-08-24 23:04:52 -07:00
Allow deletion of certain proof states and remove proof tree structure

We can even directly save bare goals (actually just a mvarId with a saved state) since we do not store the tactic along with each ProofState:

structure Goal where
  mvar: MVarId
 …
aniva opened issue aniva/Pantograph#8 2023-08-24 22:58:30 -07:00
Allow deletion of certain proof states and remove proof tree structure
aniva created pull request aniva/Pantograph#7 2023-08-24 22:53:57 -07:00
Error category consolidation
aniva pushed to doc at aniva/Pantograph 2023-08-24 22:52:19 -07:00
95d26a2f50 Classify JSON error as command error
aniva created branch doc in aniva/Pantograph 2023-08-24 22:52:19 -07:00
aniva pushed tag 0.2.3 to aniva/Pantograph 2023-08-24 15:14:59 -07:00
aniva released "0.2.3: Full expression AST printing" at aniva/Pantograph 2023-08-24 15:14:59 -07:00
aniva pushed to dev at aniva/Pantograph 2023-08-23 13:29:02 -07:00
5978e5f4f3 Merge pull request 'Add more serialisation options' (#2) from io/serial into dev
7160f8aa61 Merge branch 'dev' into io/serial
e63f7c9afa Add proper printing of sorts
1d1fa60175 Move all json-string functions to Main.lean
Compare 4 commits »
aniva merged pull request aniva/Pantograph#2 2023-08-23 13:29:00 -07:00
Add more serialisation options
aniva opened issue aniva/Pantograph#6 2023-08-23 13:27:41 -07:00
The termination of Lean.Level serialization is not ensured