Concept of Editing and Restart a Proof Script
We need a concept/workflow for editing and restart of proof scripts.
- We record the set of goal nodes (and also key nodes) at the beginning of every statement.
- We can ignore all commands call until a certain position.
From this we can create an editing concept, answering following question:
- What is the user allowed to edit in debug mode?
- How can base upon the current interpreter state (pruning, call ignoring)?
To upload designs, you'll need to enable LFS and have admin enable hashed storage. More information