Spec conversion burndown list

[rossberg]

Priorities:

• 0: Needs to be addressed ASAP
• 1: Needs to be done before CG presentation
• 2: Needs to be done before F2F
• 3: Needs to be done before fully replacing spec
• 4: Should be done eventually

Annotation: (priority, owner, estimated time)

• [ ] Complete spectec implementation

  • [ ] Language and frontend
  • [x] Complete support for type parameters + families #72 (1, rossberg, 4w)
  • [ ] Add support for numerics (3, ?, ?)
  • [x] Add support for sets (3, rossberg, 1d)
  • [x] Latex backend
  • [x] Add support for macro hints (2, rossberg, 1w)
  • [x] Handle cross-references (2, rossberg, 2w)
  • [ ] Prose backend
  • [ ] Proper error messages #73 (2, kang, 1w)
  • [x] Fully roundtrip atoms #74 (3, ?, ?)
  • [ ] (Support Latex generation) (4, ?, ?)
  • [ ] Polishing (2-4, ?, ?)
  • [ ] Interpreter backend
  • [x] Adapt to #72 (1, ryu&lee, 1w)
  • [ ] Proper error messages #73 (2, kang, 1w)
  • [x] Change level of abstraction for external logic (3, ryu&lee, 3d)
  • [ ] Documentation... (1-4, ?, ?)

• [ ] Complete spectec specs

  • [x] Use type families to fix main TODOs #72 (1, rossberg, 1w)
  • [x] Missing vector instructions #70 (1, , )
  • [x] Binary format for vector instructions #71 (1, ryu&lee, 1d)
  • [x] Complete syntax hints (2, rossberg, 1w)
  • [ ] Text format (3, rossberg, 1w)
  • [ ] Numerics (3, ?, 2w)
  • [ ] Other TODOs (2-3)

• [x] Infrastructure for using spectec in document build

  • [X] Merge spec/wasm3 branch into spectec (0, rossberg, 4h)
  • [X] Modify document/core Makefile to invoke spectec (0, rossberg, 1d)
  • [x] Merge gc repo into spec/wasm3 branch (1, rossberg, 1d)
  • [x] Replace git clone of gc interpreter with direct use of interpreter directory (2, rossberg, 2h)

• [ ] Porting spec by incrementally replacing content with spectec anchors

  • [x] Math in Syntax chapter (1, rossberg, 2w)
  • [x] Conventions
  • [x] Types
  • [x] Values
  • [x] Instructions
  • [x] Modules
  • [x] Math in Validation chapter (1-2, rossberg, 5d)
  • [x] Conventions
  • [x] Types
  • [x] Matching
  • [x] Instructions
  • [x] Modules
  • [ ] Math in Execution chapter (1-2, rossberg, 5d)
  • [x] Conventions
  • [x] Runtime
  • [x] Types
  • [ ] Numerics (*)
  • [x] Instructions
  • [x] Modules
  • [x] Math in Binary Format chapter (3, rossberg, 5d)
  • [x] Conventions
  • [x] Types
  • [x] Values
  • [x] Instructions
  • [x] Modules
  • [ ] Math in Text Format chapter (3, ?, 2w)
  • [ ] Conventions
  • [ ] Types (*)
  • [ ] Values (*)
  • [ ] Instructions (*)
  • [ ] Modules (*)
  • [ ] Math in Appendix
  • [ ] Embedding (3, rossberg, 2h)
  • [ ] Implementation (3, rossberg, 1h)
  • [ ] Algorithm (3, rossberg, 1h)
  • [ ] Custom Sections (3, rossberg, 1h)
  • [ ] Properties (3, rossberg, 5h)
  • [ ] Changes (3, rossberg, 3h)
  • [ ] Type Index (2, rossberg, 2h)
  • [ ] Instruction Index (2, ?, 4h)
  • [ ] Rules Index (2, rossberg, 3h)
  • [ ] Prose in Validation chapter
  • [x] Conventions (2, rossberg, 1h)
  • [ ] Types (***) (2, ?, ?)
  • [ ] Instructions (2, ?, ?)
  • [ ] Modules (***) (2, ?, ?)
  • [ ] Prose in Execution chapter
  • [x] Conventions (2, rossberg, 3h)
  • [ ] Types (2, ?, 3d)
  • [ ] Numerics (, , ) (3, ?, 3w)
  • [ ] Instructions (1, ?, 2w)
  • [ ] Modules (2, ?, 3w)
  • [ ] Cross-references in index ? (**, ***) (3, ?, ?)

( ) Requires extending watsup spec ( ) Requires extending spectec language ( ) Likely requires additions to spectec renderer