From 9d8b4431902d27127d1a8b26f3e3c6e5936c5fd2 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Dec 2025 14:14:15 +0000 Subject: [PATCH] Add executable milestones roadmap Define 16 milestones from foundation (complete) through 1.0 release, with specific verification commands for each task. Includes dependency graph and immediate next actions prioritized for unblocking progress. --- MILESTONES.md | 400 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 400 insertions(+) create mode 100644 MILESTONES.md diff --git a/MILESTONES.md b/MILESTONES.md new file mode 100644 index 00000000..f51d82ac --- /dev/null +++ b/MILESTONES.md @@ -0,0 +1,400 @@ + + + +# Ephapax Milestones + +Executable milestones for reaching production readiness. + +## Status Key + +- 🔲 Not started +- 🚧 In progress +- ✅ Complete + +--- + +## Milestone 0: Foundation (✅ Complete) + +**Goal**: Establish theoretical and architectural foundation. + +| Task | Status | Verification | +|------|--------|--------------| +| Define linear type system | ✅ | `spec/SPEC.md` exists | +| Mechanize semantics in Coq | ✅ | `coqc formal/*.v` succeeds | +| Prove Progress theorem | ✅ | `formal/Semantics.v` contains proof | +| Prove Preservation theorem | ✅ | `formal/Semantics.v` contains proof | +| Define AST crate | ✅ | `cargo build -p ephapax-syntax` | +| Set up CI pipeline | ✅ | `.github/workflows/ci.yml` exists | + +--- + +## Milestone 1: Lexer Complete (🚧 In Progress) + +**Goal**: Tokenize all Ephapax source constructs. + +| Task | Status | Verification | +|------|--------|--------------| +| Tokenize keywords | 🚧 | `cargo test -p ephapax-lexer -- keywords` | +| Tokenize operators | 🚧 | `cargo test -p ephapax-lexer -- operators` | +| Tokenize literals (int, float, string, bool) | 🚧 | `cargo test -p ephapax-lexer -- literals` | +| Tokenize identifiers | 🚧 | `cargo test -p ephapax-lexer -- identifiers` | +| Tokenize region annotations | 🚧 | `cargo test -p ephapax-lexer -- regions` | +| Span tracking for error reporting | 🚧 | `cargo test -p ephapax-lexer -- spans` | +| Lexer error recovery | 🔲 | `cargo test -p ephapax-lexer -- recovery` | + +**Exit Criteria**: +```bash +cargo test -p ephapax-lexer --all-features +# All tests pass, >90% token coverage +``` + +--- + +## Milestone 2: Parser Complete (🚧 In Progress) + +**Goal**: Parse all syntactic constructs into typed AST. + +| Task | Status | Verification | +|------|--------|--------------| +| Parse let bindings | 🚧 | `cargo test -p ephapax-parser -- let_binding` | +| Parse function definitions | 🚧 | `cargo test -p ephapax-parser -- functions` | +| Parse function application | 🚧 | `cargo test -p ephapax-parser -- application` | +| Parse product types (pairs) | 🚧 | `cargo test -p ephapax-parser -- products` | +| Parse sum types | 🚧 | `cargo test -p ephapax-parser -- sums` | +| Parse region expressions | 🚧 | `cargo test -p ephapax-parser -- regions` | +| Parse borrow expressions | 🚧 | `cargo test -p ephapax-parser -- borrows` | +| Parse conditionals | 🚧 | `cargo test -p ephapax-parser -- conditionals` | +| Error recovery with ariadne | 🔲 | Parse invalid input, emit ≥1 diagnostic | +| Operator precedence | 🔲 | `cargo test -p ephapax-parser -- precedence` | + +**Exit Criteria**: +```bash +cargo test -p ephapax-parser --all-features +# All tests pass +# Parse all examples in docs/wiki/language/ +``` + +--- + +## Milestone 3: Type Checker Hardened (🚧 In Progress) + +**Goal**: Full linear type checking with clear error messages. + +| Task | Status | Verification | +|------|--------|--------------| +| Check linearity (use exactly once) | 🚧 | `cargo test -p ephapax-typing -- linearity` | +| Check region scoping | 🚧 | `cargo test -p ephapax-typing -- region_scope` | +| Check borrow validity | 🚧 | `cargo test -p ephapax-typing -- borrows` | +| Infer function types | 🔲 | `cargo test -p ephapax-typing -- inference` | +| Reject use-after-move | 🔲 | `cargo test -p ephapax-typing -- use_after_move` | +| Reject region escape | 🔲 | `cargo test -p ephapax-typing -- region_escape` | +| Reject double-use | 🔲 | `cargo test -p ephapax-typing -- double_use` | +| Reject unused linear values | 🔲 | `cargo test -p ephapax-typing -- unused_linear` | +| Clear diagnostic messages | 🔲 | Manual review of error output | + +**Exit Criteria**: +```bash +cargo test -p ephapax-typing --all-features +# Reject all invalid programs in tests/reject/ +# Accept all valid programs in tests/accept/ +``` + +--- + +## Milestone 4: WASM Code Generation (🚧 In Progress) + +**Goal**: Compile type-checked programs to valid WebAssembly. + +| Task | Status | Verification | +|------|--------|--------------| +| Generate WASM for primitives | 🚧 | `wasm-validate output.wasm` | +| Generate WASM for functions | 🚧 | `wasmtime run output.wasm` | +| Generate WASM for products | 🔲 | Test pair creation/projection | +| Generate WASM for sums | 🔲 | Test inl/inr/case | +| Generate WASM for regions | 🔲 | Test region allocation | +| Linear memory management | 🔲 | No leaks in valgrind/wasm-tools | +| Region-based deallocation | 🔲 | Verify bulk free on region exit | +| WASM validation | 🔲 | All output passes `wasm-validate` | + +**Exit Criteria**: +```bash +# Compile and run hello world +cargo run -- compile examples/hello.eph -o hello.wasm +wasmtime run hello.wasm +# Output: "Hello, World!" +``` + +--- + +## Milestone 5: Test Suite (🔲 Not Started) + +**Goal**: Comprehensive automated testing. + +| Task | Status | Verification | +|------|--------|--------------| +| Unit tests for each crate | 🔲 | `cargo test --workspace` | +| Integration tests (end-to-end) | 🔲 | `cargo test --test integration` | +| Negative tests (reject invalid) | 🔲 | `tests/reject/` directory | +| Golden tests (expected output) | 🔲 | `tests/golden/` directory | +| Fuzzing harness | 🔲 | `cargo fuzz run lexer` | +| Property-based tests | 🔲 | `cargo test -- proptest` | +| Coq extraction tests | 🔲 | Compare extracted code to impl | + +**Exit Criteria**: +```bash +cargo test --workspace --all-features +# >80% code coverage (cargo tarpaulin) +# Zero panics under fuzzing (1M iterations) +``` + +--- + +## Milestone 6: Standard Library (🔲 Not Started) + +**Goal**: Provide essential safe primitives. + +| Task | Status | Verification | +|------|--------|--------------| +| Linear strings | 🔲 | `cargo test -p ephapax-stdlib -- strings` | +| Linear vectors | 🔲 | `cargo test -p ephapax-stdlib -- vectors` | +| Linear maps | 🔲 | `cargo test -p ephapax-stdlib -- maps` | +| I/O primitives | 🔲 | `cargo test -p ephapax-stdlib -- io` | +| Numeric operations | 🔲 | `cargo test -p ephapax-stdlib -- numeric` | +| Option/Result types | 🔲 | `cargo test -p ephapax-stdlib -- option_result` | +| Document all functions | 🔲 | `cargo doc -p ephapax-stdlib` | + +**Exit Criteria**: +```bash +cargo test -p ephapax-stdlib --all-features +cargo doc -p ephapax-stdlib --no-deps +# All public items documented +``` + +--- + +## Milestone 7: REPL Functional (🔲 Not Started) + +**Goal**: Interactive development environment. + +| Task | Status | Verification | +|------|--------|--------------| +| Evaluate expressions | 🔲 | Type `1 + 2`, get `3` | +| Multi-line input | 🔲 | `let f = \x -> \n x + 1` works | +| Type inspection (`:type`) | 🔲 | `:type \x -> x` shows type | +| History persistence | 🔲 | Arrow up recalls previous | +| Tab completion | 🔲 | `pri` → `print` | +| Error highlighting | 🔲 | Errors show source location | +| Load files (`:load`) | 🔲 | `:load example.eph` works | + +**Exit Criteria**: +```bash +cargo run -- repl +# Run tutorial examples interactively +# No crashes on malformed input +``` + +--- + +## Milestone 8: CLI Polish (🔲 Not Started) + +**Goal**: Production-quality command-line interface. + +| Task | Status | Verification | +|------|--------|--------------| +| `ephapax compile ` | 🔲 | Produces valid WASM | +| `ephapax run ` | 🔲 | Compiles and executes | +| `ephapax check ` | 🔲 | Type checks only | +| `ephapax fmt ` | 🔲 | Formats source code | +| `--emit=ast\|ir\|wasm` | 🔲 | Dump intermediate stages | +| `--verbose` / `--quiet` | 🔲 | Control output verbosity | +| Proper exit codes | 🔲 | 0=success, 1=error, 2=usage | +| Shell completions | 🔲 | `ephapax completions bash` | + +**Exit Criteria**: +```bash +ephapax --version # Shows version +ephapax --help # Shows help +ephapax compile examples/*.eph # All compile +``` + +--- + +## Milestone 9: Language Server (🔲 Not Started) + +**Goal**: IDE integration via LSP. + +| Task | Status | Verification | +|------|--------|--------------| +| Diagnostics (errors/warnings) | 🔲 | Red squiggles in editor | +| Go to definition | 🔲 | Ctrl+click navigates | +| Hover for type info | 🔲 | Hover shows type | +| Completion suggestions | 🔲 | Autocomplete works | +| Document symbols | 🔲 | Outline view works | +| Workspace symbols | 🔲 | Ctrl+T search works | +| Format on save | 🔲 | Auto-formats | +| Semantic highlighting | 🔲 | Linear vars highlighted | + +**Exit Criteria**: +```bash +# Install in VS Code/Helix/Neovim +# Open .eph file, verify features work +``` + +--- + +## Milestone 10: Documentation Complete (🔲 Not Started) + +**Goal**: Comprehensive user and developer documentation. + +| Task | Status | Verification | +|------|--------|--------------| +| Installation guide | 🔲 | Follow steps on fresh system | +| Language tutorial | 🔲 | Complete in <1 hour | +| API reference | 🔲 | `cargo doc --workspace` | +| Examples directory | 🔲 | 10+ working examples | +| Contributing guide | ✅ | `CONTRIBUTING.md` exists | +| Architecture docs | 🔲 | Explains compiler pipeline | +| Linearity explainer | 🔲 | Non-experts understand | + +**Exit Criteria**: +```bash +# New user can install, write, and run program +# Following only documentation +``` + +--- + +## Milestone 11: Performance Baseline (🔲 Not Started) + +**Goal**: Establish and track performance metrics. + +| Task | Status | Verification | +|------|--------|--------------| +| Compile-time benchmarks | 🔲 | `cargo bench --bench compile` | +| Runtime benchmarks | 🔲 | `cargo bench --bench runtime` | +| Memory usage benchmarks | 🔲 | Track peak memory | +| Binary size tracking | 🔲 | WASM output size | +| Comparison with peers | 🔲 | vs. Rust WASM, AssemblyScript | +| CI benchmark tracking | 🔲 | Detect regressions | + +**Exit Criteria**: +```bash +cargo bench +# Results stored in benches/results/ +# <5% regression on PR merge +``` + +--- + +## Milestone 12: Alpha Release (🔲 Not Started) + +**Goal**: First public release for early adopters. + +| Task | Status | Verification | +|------|--------|--------------| +| Version 0.1.0 | 🔲 | `Cargo.toml` version bump | +| Changelog | 🔲 | `CHANGELOG.md` exists | +| GitHub release | 🔲 | Release page with assets | +| Pre-built binaries | 🔲 | Linux, macOS, Windows | +| Announcement post | 🔲 | Blog/social media | +| Issue templates | 🔲 | `.github/ISSUE_TEMPLATE/` | + +**Exit Criteria**: +```bash +# User can download binary, run without cargo +# File issues using templates +``` + +--- + +## Milestone 13: Ecosystem Bootstrap (🔲 Not Started) + +**Goal**: Enable third-party development. + +| Task | Status | Verification | +|------|--------|--------------| +| Package format spec | 🔲 | Document in spec/ | +| Package registry design | 🔲 | RFC document | +| Build system integration | 🔲 | Works with Cargo/Deno | +| Tree-sitter grammar | 🔲 | Syntax highlighting | +| Example projects | 🔲 | 3+ real-world examples | + +**Exit Criteria**: +```bash +# Third party can create, share, install packages +``` + +--- + +## Milestone 14: Beta Release (🔲 Not Started) + +**Goal**: Feature-complete for general use. + +| Task | Status | Verification | +|------|--------|--------------| +| All major features stable | 🔲 | No breaking changes planned | +| Performance optimized | 🔲 | Benchmarks meet targets | +| Documentation complete | 🔲 | All features documented | +| Known bugs triaged | 🔲 | No critical issues open | +| Community feedback addressed | 🔲 | Top issues resolved | + +**Exit Criteria**: +```bash +# Used in 3+ non-trivial projects +# No P0 bugs for 30 days +``` + +--- + +## Milestone 15: 1.0 Release (🔲 Not Started) + +**Goal**: Production-ready stable release. + +| Task | Status | Verification | +|------|--------|--------------| +| Semantic versioning commitment | 🔲 | VERSIONING.md | +| Stability guarantees | 🔲 | Document in spec | +| Security audit | 🔲 | Third-party audit report | +| Long-term support policy | 🔲 | LTS.md document | +| Migration guide from beta | 🔲 | MIGRATING.md | + +**Exit Criteria**: +```bash +# Formal stability commitment +# No breaking changes without major version +``` + +--- + +## Quick Reference + +| Milestone | Target | Blocking | +|-----------|--------|----------| +| M0: Foundation | ✅ Done | - | +| M1: Lexer | M2, M7 | - | +| M2: Parser | M3 | M1 | +| M3: Type Checker | M4 | M2 | +| M4: WASM Codegen | M7, M8, M11 | M3 | +| M5: Test Suite | M12 | M4 | +| M6: Stdlib | M7, M12 | M4 | +| M7: REPL | M12 | M4, M6 | +| M8: CLI | M12 | M4 | +| M9: Language Server | M13 | M4 | +| M10: Docs | M12 | M4 | +| M11: Performance | M14 | M4 | +| M12: Alpha | M13 | M5-M8, M10 | +| M13: Ecosystem | M14 | M12 | +| M14: Beta | M15 | M11, M13 | +| M15: 1.0 | - | M14 | + +--- + +## Next Actions + +Priority tasks for immediate progress: + +1. **Complete lexer tests** - Unblock parser work +2. **Add parser tests** - Validate AST generation +3. **Create test fixtures** - `tests/accept/` and `tests/reject/` +4. **Implement hello world** - End-to-end compilation proof +5. **Set up benchmarks** - Establish baseline early