Derivation trees - Githubissues

Building educational UI for constructing rule-based derivations and integrate it into Exercises mode in Hazel. 截屏2024-09-18 上午12 28 42

Try it here!

Bugs

[?] Fix Remolding issue
[x] Fix NumLit sort-inconsistency
[ ] Restrict var regex for each sort.
[x] Fix "re-enter" space remolding issue
[ ] Change d0 to d1
[ ] (Potential bugs) check all rules implemented yet.
- [x] All Rules except Bidirection
[x] Info Error if got comma prop not on Entail left
[x] Occasionally take on weird color.
[ ] Hole does not take on Info error.
[ ] (potenital) Should verification start from Concl or Prems or either.
[ ] Handle let pair bind to same var error
[ ] Handle plus concatenation for type.
[ ] Instructor mode not allowed to add abbr below

[x] Proposition derivation sementic
- [x] Port judgement type Judgement and component types Prop, Ctx to builtin functions
- [x] Introduce /\, \/, ==>, |- operator
[x] Refactor Derivation Exercise mode integration
- [x] Introduce Exercise mode choice: Programming & Proof
- [x] Separate model mapping and code manipulation.
[x] Sorts for ALFA (Judgement, Ctx, ALFAExpr, ALFATyp, ALFAPat, ALFATPat)
[ ] Undo: We only have this for each editor
[x] Enable PROP and EXP abbreviation in prelude & setup
- [ ] Use hazel Exp Sort required in curly braces.
- [ ] Rewrite remolding (A new sort exists in Drv Sort family)
[x] Make the editor truly requiring a JDMT sort
[ ] Make the terms and inner token not stick with each other
[x] Allow ninja-keys searching rule mistype?
[ ] Pop tree to abbr & push abbr back to tree
[ ] Derivation collapsing
[ ] Derivation automation
[ ] Exercise spec export & import
[ ] Write Sort info & sort term info for ExplainThis
[ ] Write DHDoc_common for Drv terms
[ ] LaTeX Export by translating plain code to latex comments act as specifiers.
[?] refactor all I have written (not really)
[?] refactor exercise mode

[x] Hover above rule label summon the choice panel
[x] Result of the current derivation: Pending, Error, Correct
[x] Click on the rules to switch
[x] Add/Del premises button
[x] Add/Del abbr button
[x] Derivation exercise scoring scheme
[x] Click on the button (between Derivation and Prelude) compose a derivation binding
[x] In choice panel we can choose either rules or derivation abbreviation (legal binding)
[x] Show error messages in the side bar
[x] Show rule definitions in sidebar
[ ] Make dots show only on hover using crazy CSS selector
[ ] Label dragging
[ ] Move popup menu to above and change the btn to summon Explainthis
[ ] Re-style Cells, many be each for a abbreviation, and show the whole result at the bottom of the cell
[ ] Re-style add abbreviation btn by tip words

*This is not an outline of my progress, but like a memo