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 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 created branch doc in aniva/Pantograph 2023-08-24 22:52:19 -07:00
aniva pushed to doc at aniva/Pantograph 2023-08-24 22:52:19 -07:00
95d26a2f50 Classify JSON error as command error
aniva released "0.2.3: Full expression AST printing" at aniva/Pantograph 2023-08-24 15:14:59 -07:00
aniva pushed tag 0.2.3 to 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
aniva pushed to io/serial at aniva/Pantograph 2023-08-23 13:25:42 -07:00
7160f8aa61 Merge branch 'dev' into io/serial
85440e0278 Unify json and unknown error into command error
Compare 2 commits »
aniva closed issue aniva/Pantograph#4 2023-08-23 13:22:30 -07:00
Redundant error messages
aniva closed issue aniva/Pantograph#3 2023-08-23 13:22:25 -07:00
Dead code in proof tree
aniva pushed to dev at aniva/Pantograph 2023-08-23 13:22:19 -07:00
85440e0278 Unify json and unknown error into command error
aniva deleted branch misc/cleanup from aniva/Pantograph 2023-08-23 13:22:19 -07:00
aniva merged pull request aniva/Pantograph#5 2023-08-23 13:22:18 -07:00
Remove dead code and consolidate error types