Allow deletion of certain proof states and remove proof tree structure #8

New Issue

aniva · 2023-08-24T22:58:30-07:00

aniva commented

2023-08-24 22:58:30 -07:00

Since we are not going to do any book keeping about whether a proof tree is actually proven (in order to keep Pantograph's bookkeeping mechanism as light as possible), we should remove the ProofTree and directly store ProofStates in the State monad in the main loop. Then we should use some other data structure to save such ProofStates so the client can ask for the deletion of a proof state.

This would be a breaking change, so the version should be bumped to 0.2.4.

Since we are not going to do any book keeping about whether a proof tree is actually proven (in order to keep `Pantograph`'s bookkeeping mechanism as light as possible), we should remove the `ProofTree` and directly store `ProofState`s in the `State` monad in the main loop. Then we should use some other data structure to save such `ProofState`s so the client can ask for the deletion of a proof state. This would be a breaking change, so the version should be bumped to `0.2.4`.

aniva added this to the 0.2.6 milestone 2023-08-24 22:58:30 -07:00

aniva added the

category

optimization

part/Goal

labels 2023-08-24 22:58:30 -07:00

aniva self-assigned this 2023-08-24 22:58:30 -07:00

aniva commented

2023-08-24 23:04:52 -07:00

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
  savedState: Elab.Tactic.SavedState
  parent: Option Nat := None

instead of

structure ProofState where
  goals : List MVarId
  savedState : Elab.Tactic.SavedState
  parent : Option Nat := none
  parentGoalId : Nat  := 0

of course keeping track of a parent will require the index be unique, so this should be dropped as well.

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`: ```lean structure Goal where mvar: MVarId savedState: Elab.Tactic.SavedState parent: Option Nat := None ``` instead of ```lean structure ProofState where goals : List MVarId savedState : Elab.Tactic.SavedState parent : Option Nat := none parentGoalId : Nat := 0 ``` of course keeping track of a parent will require the index be unique, so this should be dropped as well.

aniva commented

2023-08-24 23:14:03 -07:00

Leaving this until Trillium backend can handle this bookkeeping.

aniva modified the milestone from 0.2.6 to 0.2.4

2023-08-24 23:18:20 -07:00

aniva referenced this issue

2023-08-26 18:10:10 -07:00

Simplify goal bookkeeping mechanism #10

aniva added reference tactic/book

2023-08-27 22:51:43 -07:00

aniva commented

2023-08-30 19:18:48 -07:00