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
    • Complete support for type parameters + families Implement type indexing and adapt spec #72 (1, rossberg, 4w)
    • Add support for numerics (3, ?, ?)
    • Add support for sets (3, rossberg, 1d)
  • Latex backend
    • Add support for macro hints (2, rossberg, 1w)
    • Handle cross-references (2, rossberg, 2w)
  • Prose backend
    • Proper error messages [backend-prose/interpreter] Error messages from backends #73 (2, kang, 1w)
    • Fully roundtrip atoms [backend-prose] Roundtrip atoms #74 (3, ?, ?)
    • (Support Latex generation) (4, ?, ?)
    • Polishing (2-4, ?, ?)
  • Interpreter backend
    • Adapt to Implement type indexing and adapt spec #72 (1, ryu&lee, 1w)
    • Proper error messages [backend-prose/interpreter] Error messages from backends #73 (2, kang, 1w)
    • Change level of abstraction for external logic (3, ryu&lee, 3d)
  • Documentation
    • Overview (rossberg)
    • Language (rossberg)
    • Usage (rossberg)
    • Splicing (rossberg)
    • Latex backend (rossberg)
    • Prose backend (?)
    • Interpreter backend (?)

• Complete spectec specs

  • Use type families to fix main TODOs Implement type indexing and adapt spec #72 (1, rossberg, 1w)
  • Missing vector instructions [spec-2.0/3.0] Add missing SIMD instructions #70 (1, _, _)
  • Binary format for vector instructions [spec-2.0/3.0] Add binary format for SIMD instructions #71 (1, ryu&lee, 1d)
  • Complete syntax hints (2, rossberg, 1w)
  • Text format (3, rossberg, 1w)
  • Numerics (3, ?, 2w)
  • Other TODOs (2-3)

• Infrastructure for using spectec in document build

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

• Porting spec by incrementally replacing content with spectec anchors

  • Math in Syntax chapter (1, rossberg, 2w)
    • Conventions
    • Types
    • Values
    • Instructions
    • Modules
  • Math in Validation chapter (1-2, rossberg, 5d)
    • Conventions
    • Types
    • Matching
    • Instructions
    • Modules
  • Math in Execution chapter (1-2, rossberg, 5d)
    • Conventions
    • Runtime
    • Types
    • Numerics (*)
    • Instructions
    • Modules
  • Math in Binary Format chapter (3, rossberg, 5d)
    • Conventions
    • Types
    • Values
    • Instructions
    • 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
    • Conventions (2, rossberg, 1h)
    • Types (***) (2, ?, ?)
    • Instructions (2, ?, ?)
    • Modules (***) (2, ?, ?)
  • Prose in Execution chapter
    • 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