diff --git a/.gitignore b/.gitignore index 0426c0c..b4a4e36 100644 --- a/.gitignore +++ b/.gitignore @@ -80,3 +80,6 @@ CoqMakefile.conf *.pem *.key .venv/ + +# Claude Code session worktrees (untracked second checkouts of this repo) +.claude/worktrees/ diff --git a/.machine_readable/6a2/ECOSYSTEM.a2ml b/.machine_readable/6a2/ECOSYSTEM.a2ml index 02d3157..10bedd0 100644 --- a/.machine_readable/6a2/ECOSYSTEM.a2ml +++ b/.machine_readable/6a2/ECOSYSTEM.a2ml @@ -4,15 +4,17 @@ # ECOSYSTEM.a2ml — My Lang ecosystem position [metadata] version = "1.1" -last-updated = "2026-06-02" +last-updated = "2026-08-07" [project] name = "My Lang" purpose = """ Multi-dialect programming language with Quantitative Type Theory (QTT) semantic core. Combines affine/linear type discipline, echo-type loss modelling, formal -mechanised proofs, and AI-adjacent effect tracking. Four dialects: solo, duet, -ensemble, me. +mechanised proofs, and AI-adjacent effect tracking. Dialects are NESTED +conservative extensions — solo ⊂ duet ⊂ ensemble — plus `me`, an agent-generated +PROJECTION over that hierarchy rather than a fourth dialect. Only solo is +authoritative in f0. """ role = "flagship-language-experiment" licence = "MPL-2.0" @@ -72,11 +74,11 @@ projects = [ reference = "proofs/ALIGNMENT-PLAN.md" gaps-closed = [ "G1-partial: mechanised QTT solo-core scaffold on dual Coq + Idris2 tracks (F1.0 done)", + "G1-remainder: F1.1 small-step semantics, F1.3 progress, F1.4 preservation + ht_subst + affine_pres — all machine-checked and axiom-free on the Coq track (closed 2026-06-14)", + "G2: mechanised operational semantics constructors present on both tracks (F1.1)", + "G3: proof CI leg live — .github/workflows/proofs.yml with per-rung Print-Assumptions gates (F5, closed 2026-06-14)", + "G5: coqc + idris2 --build both run in CI (same workflow)", ] gaps-open = [ - "G1-remainder: F1.1–F1.4 (small-step semantics, progress/preservation proofs)", - "G2: no mechanised operational semantics constructors yet", - "G3: proof CI leg absent (Phase F5)", "G4: paper-proof topic parity (quantitative-types doc, row-polymorphism, Hoare semantics, categorical semantics, complexity analysis)", - "G5: no coqc/idris2 CI leg", ] diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 4584e35..a23bdb5 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -5,7 +5,7 @@ [metadata] project = "my-lang" version = "0.2.0" # matches Cargo.toml [workspace.package] -last-updated = "2026-07-27" +last-updated = "2026-08-07" status = "active" session = "CI/CD + supply-chain close-out (PRs #143/#146/#147): codeql-action repointed off a NONEXISTENT SHA; all 15 Hypatia findings triaged (8 fixed at source incl. a self-referential critical, 7 baselined to 2026-10-27 under issue #145); unsafe_block ruled unsatisfiable and scoped-exempted; GitHub Pages un-stuck (workflow was disabled_manually) and LIVE; ARCHITECTURE.md + Justfile de-boilerplated. main FULLY GREEN — 2026-07-27" prior-session = "Coq solo-core: R2–R5b (SEMIRING functor / affine_pres / Tropical / usage-walk checker / aff_type_dec) + M1 me→solo elaboration + structure climb S1.0–S3c.3-msg (session-π: subject reduction, fidelity, progress, duet-by-projection, n-party projection totality, static n-party config, label-union merge, union-projection, n-ary located operational semantics, head-coupled message subject reduction = first earned n-party safety half) + E4 residue-measure SEAM (Coq mirror) — all axiom-free, CI-gated — 2026-06-14" @@ -44,7 +44,7 @@ qtt-semiring-idris2 = "locally-checked" solo-syntax-contexts-typing = "machine-checked" operational-semantics = "machine-checked" # F1.1 — CBV step/Step committed both tracks progress = "machine-checked" # F1.3 — Coq Qed (axiom-free), CI Print Assumptions closed; Idris total/hole-free -preservation = "machine-checked" # F1.4 — Coq Qed (axiom-free, ht_subst), CI-gated; Idris ?todo_preservation deliberately open (D1 option A) +preservation = "machine-checked" # F1.4 — Coq Qed (axiom-free, ht_subst), CI-gated. CORRECTION 2026-08-07: the Idris ?todo_preservation hole was DISCHARGED 2026-06-21 (#108) — zero ?todo holes remain in proofs/verification/idris/. proofs/STATUS.md still grades the Idris track locally-checked (its CI job runs idris2 --build with NO hole assertion — DEBT.md P-2). resource-algebra-functor = "machine-checked" # R2 — SoloCoreF over Module Type SEMIRING; Include Linear3 = R0 axiom-free affine-pres = "machine-checked" # R3 — distinct affine budget-preservation over ORDERED_SEMIRING qle tropical-instance = "machine-checked" # R4 — SoloCoreF Tropical, infinite min-plus carrier, axiom-free @@ -89,7 +89,8 @@ milestones = [ { id = "S3c.1", description = "Union-projection proj_u/projectable_u_wf + keystone existence theorem projection_total_u + one-directional monotonicity bridge projectable_wf_implies_u (on keystone merge_forces_eq: plain merge is the identity-meet); SEPARATE proj_u added ALONGSIDE proj (canonical proj byte-identical, NOT re-pointed); projection-EXISTENCE only, non-vacuity g_union3 in union-projectable minus plain-projectable; axiom-free", status = "done", date = "2026-06-14" }, { id = "S3c.2", description = "n-ary LOCATED operational semantics: nstep (located mirror of fused cstep; one comm ra_set-updates exactly the two roles) + ra_set + global gstep + nstar/gstar closures + functional wf_assignment_f (wf_assignment_to_f keeps S3b green); 3-party ring run 0->1->2->0 witnessed both sides (ring_runs_to_end, g_ring_gsteps); ADEQUACY-only, nstep_breaks_wf_at_fixed_G PROVES no fixed-G subject reduction; axiom-free", status = "done", date = "2026-06-14" }, { id = "S3c.3-msg", description = "Head-coupled message subject reduction nstep_sr_msg_head (the FIRST EARNED n-party safety half): the head communication sanctioned by GMsg p q t G' carries wf_assignment_f from G to its continuation G' (3-way located role split; same v:t sender ships = receiver substitutes via pty_subst0); coupled corollary nstep_gstep_sr_msg_head; earned-safety headline sr_earns_safety_across_step (same ra_ring1 S3c.2 refuted at fixed g is wf at stepped g); run-ahead fence SELF-WITNESSED (runahead_breaks_head_coupling). Design-panel-validated + independently adversary-verified (sound-and-honest). HEAD message fragment, preservation only; axiom-free", status = "done", date = "2026-06-14" }, - { id = "S3c.3-choice/perm + S3c.4", description = "remaining n-party safety: select/branch SR (S3c.3-choice, couple NStep_Sel with a choice-gstep), run-ahead/permutation SR (S3c.3-perm, needs gstep-with-swap relation), n-party progress (S3c.4 = coherence ⇒ safety, research-hard — fence; wf_assignment ra -> deadlock-free is FALSE)", status = "pending", note = "S3c.0/.1/.2/.3-msg landed; the message-HEAD safety half is earned; choice/permutation/progress remain, solo" }, + { id = "S3c.3-choice", description = "head-coupled select/branch subject reduction — the CHOICE analogue of nstep_sr_choice_head; couples NStep_Sel with a choice-gstep to the selected continuation Gl = gbget l bs", status = "done", date = "2026-08-07", note = "CORRECTION 2026-08-07: recorded as pending here while .github/workflows/proofs.yml:319-343 already gates nstep_sr_choice_head / nstep_gstep_sr_choice_head / proj_br_selected / proj_uninv_selected / wf_ra_choice3 / choice3_head_fires_end_to_end as axiom-free. The CI was ahead of this file; re-verify the landing date against git history." }, + { id = "S3c.3-perm + S3c.4", description = "remaining n-party safety: run-ahead/permutation SR (S3c.3-perm, needs gstep-with-swap relation), n-party progress (S3c.4 = coherence ⇒ safety, research-hard — fence; wf_assignment ra -> deadlock-free is FALSE)", status = "pending", note = "S3c.0/.1/.2/.3-msg/.3-choice landed; permutation SR and n-party progress remain, solo" }, { id = "E4", description = "Echo residue-measure SEAM (Coq mirror): RESIDUE_MEASURE + EchoTraceTropical + echo_measure_not_injective; full measure-independence upstream-cited", status = "done", date = "2026-06-14" }, { id = "F2", description = "Effects metatheory mechanised", status = "pending" }, { id = "F3", description = "Memory model mechanised", status = "pending" }, @@ -148,10 +149,10 @@ idris2 = "built from source in CI — see proofs.yml" task-runner = "just (Justfile); parse-verified 2026-07-27" [maintenance-status] -last-run-utc = "2026-07-27T18:15:00Z" -last-result = "pass" -main-commit = "8636e15" -main-board = "FULLY GREEN — every workflow on main succeeds or is deliberately skipped" +last-run-utc = "2026-08-07T07:56:37Z" +last-result = "mixed — see main-board" +main-commit = "e68bb3d" +main-board = "MIXED — the six standards-reusable wrappers parse again after the lockfile work (#152/#153), but dependabot bumps #155/#157 restaked 7 of 15 workflows: CodeQL + OSSF Scorecard startup_failure, Governance red on its own actions-lock --verify-local step. Repaired in PR #158. Lockfile regeneration is a RECURRING obligation on every action bump — see DEBT.md I-1." ci-governance = "pass" # incl. Validate Hypatia Baseline, green for the first time since >=2026-07-22 ci-security-scan = "pass" # Hypatia Security Scan + Secret Scanner + CodeQL + Scorecard ci-rust-tests = "pass" # Coverage (llvm-cov, floor 40%) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 4a48565..3bff8b9 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,122 +1,179 @@ - + - -# Clone the repository + +# Contributing to my-lang + +Thanks for your interest. my-lang is an early-alpha research language: an +affine / Quantitative-Type-Theory core whose metatheory is mechanised in Coq +and Idris2, with a Rust compiler that is being brought into correspondence +with those proofs. + +That last part shapes everything below. **Changes to typing rules are proof +obligations, not just code changes.** See [Proof-affecting changes](#proof-affecting-changes). + +## Getting set up + +```sh +# Clone git clone https://github.com/hyperpolymath/my-lang.git cd my-lang -# Using Nix (recommended for reproducibility) -nix develop +# Initialise submodules (proof tracks and vendored specs) +just init -# Or using toolbox/distrobox -toolbox create my-lang-dev -toolbox enter my-lang-dev -# Install dependencies manually - -# Verify setup -just check # or: cargo check / mix compile / etc. -just test # Run test suite +# Verify the toolchain works +just check # fmt-check + lint + test +just test # unit + conformance tests (excludes my-llvm) ``` -### Repository Structure -``` -my-lang/ -├── src/ # Source code (Perimeter 1-2) -├── lib/ # Library code (Perimeter 1-2) -├── extensions/ # Extensions (Perimeter 2) -├── plugins/ # Plugins (Perimeter 2) -├── tools/ # Tooling (Perimeter 2) -├── docs/ # Documentation (Perimeter 3) -│ ├── architecture/ # ADRs, specs (Perimeter 2) -│ └── proposals/ # RFCs (Perimeter 3) -├── examples/ # Examples (Perimeter 3) -├── spec/ # Spec tests (Perimeter 3) -├── tests/ # Test suite (Perimeter 2-3) -├── .well-known/ # Protocol files (Perimeter 1-3) -├── .github/ # GitHub config (Perimeter 1) -│ ├── ISSUE_TEMPLATE/ -│ └── workflows/ -├── CHANGELOG.md -├── CODE_OF_CONDUCT.md -├── CONTRIBUTING.md # This file -├── GOVERNANCE.md -├── LICENSE -├── MAINTAINERS.md -├── README.adoc -├── SECURITY.md -├── flake.nix # Nix flake (Perimeter 1) -└── Justfile # Task runner (Perimeter 1) -``` +You need a stable Rust toolchain. The LLVM back end (`my-llvm`) additionally +needs **system LLVM 21**, which is why the default `build`/`test` recipes +exclude it — use `just build-all` / `just test-all` when you have it. ---- +Proof work additionally needs **Coq/Rocq** and/or **Idris2**: -## How to Contribute +```sh +just proofs # both tracks +just proofs-coq # the authoritative track +just proofs-idris # the Idris2 twin +``` -### Reporting Bugs +Run `just --list` for the full recipe set. -**Before reporting**: -1. Search existing issues -2. Check if it's already fixed in `main` -3. Determine which perimeter the bug affects +## Repository structure -**When reporting**: +``` +my-lang/ +├── crates/ # the Cargo workspace — all live compiler code +│ ├── my-lang/ # core: lexer, parser, checker, interpreter, stdlib +│ ├── my-parser/ # standalone parser +│ ├── my-qtt/ # QTT kernel — the port of the verified Coq checker +│ ├── my-hir/ my-mir/ my-llvm/ # lowering pipeline → native +│ ├── my-cli/ # the `my` binary +│ ├── my-fmt/ my-lint/ my-lsp/ my-dap/ my-debug/ my-pkg/ my-test/ +│ └── my-ai/ # AI-assist surface (mock operations — see DEBT.md) +├── proofs/ # mechanised metatheory (Coq + Idris2) + STATUS.md +├── dialects/ # dialect definitions (solo, duet) +├── docs/ # design notes, ADRs, and the in-tree wiki +├── spec/ conformance/ tests/ fuzz/ # specification and test surfaces +├── examples/ # sample programs +├── .machine_readable/ # machine-facing state, contractiles, service metadata +└── Justfile # task runner — the golden path +``` -Use the [bug report template](.github/ISSUE_TEMPLATE/bug_report.md) and include: +Note: the root `src/`, `lib/` and `tests/` trees are **orphaned** — not +referenced by any crate. They are tracked as debt in [`DEBT.md`](DEBT.md); +do not add to them. -- Clear, descriptive title -- Environment details (OS, versions, toolchain) -- Steps to reproduce -- Expected vs actual behaviour -- Logs, screenshots, or minimal reproduction +## How to contribute -### Suggesting Features +### Reporting bugs -**Before suggesting**: -1. Check the [roadmap](ROADMAP.md) if available -2. Search existing issues and discussions -3. Consider which perimeter the feature belongs to +Search existing issues first, then use the +[bug report template](.github/ISSUE_TEMPLATE/bug_report.md). Include the +environment, steps to reproduce, expected vs actual behaviour, and a minimal +reproduction where possible. -**When suggesting**: +For a miscompilation or a type-checker soundness bug, say so explicitly — those +are triaged ahead of everything else, and may indicate a divergence between the +implementation and the mechanised specification. -Use the [feature request template](.github/ISSUE_TEMPLATE/feature_request.md) and include: +### Suggesting features -- Problem statement (what pain point does this solve?) -- Proposed solution -- Alternatives considered -- Which perimeter this affects +Check [`ROADMAP.adoc`](ROADMAP.adoc) and +[`proofs/STATUS.md`](proofs/STATUS.md) first — a surprising amount of "missing" +functionality is deliberately fenced pending a proof. Then use the +[feature request template](.github/ISSUE_TEMPLATE/feature_request.md). -### Your First Contribution +### Good first contributions -Look for issues labelled: +- [`good first issue`](https://github.com/hyperpolymath/my-lang/labels/good%20first%20issue) +- [`help wanted`](https://github.com/hyperpolymath/my-lang/labels/help%20wanted) +- [`documentation`](https://github.com/hyperpolymath/my-lang/labels/documentation) -- [`good first issue`](https://github.com/hyperpolymath/my-lang/labels/good%20first%20issue) — Simple Perimeter 3 tasks -- [`help wanted`](https://github.com/hyperpolymath/my-lang/labels/help%20wanted) — Community help needed -- [`documentation`](https://github.com/hyperpolymath/my-lang/labels/documentation) — Docs improvements -- [`perimeter-3`](https://github.com/hyperpolymath/my-lang/labels/perimeter-3) — Community sandbox scope +Documentation accuracy fixes are especially welcome — see [`DEBT.md`](DEBT.md) +for a catalogue of known-stale pages. ---- +## Development workflow -## Development Workflow +### Branches -### Branch Naming ``` -docs/short-description # Documentation (P3) -test/what-added # Test additions (P3) -feat/short-description # New features (P2) -fix/issue-number-description # Bug fixes (P2) -refactor/what-changed # Code improvements (P2) -security/what-fixed # Security fixes (P1-2) +docs/short-description # documentation +test/what-added # test additions +feat/short-description # new features +fix/issue-number-description # bug fixes +refactor/what-changed # internal improvements +security/what-fixed # security fixes +proof/what-proved # mechanised proof work ``` -### Commit Messages +### Commits We follow [Conventional Commits](https://www.conventionalcommits.org/): + ``` (): [optional body] [optional footer] +``` + +**Commits must be cryptographically signed.** The `main` branch ruleset +enforces `required_signatures`, so unsigned commits are rejected at push time: + +```sh +git config --global commit.gpgsign true +git config --global user.signingkey +``` + +SSH signing works too (`gpg.format = ssh`). A linear history is also enforced — +rebase rather than merge. + +### Pull requests + +1. Branch from `main`. +2. Keep the change focused; unrelated cleanups belong in their own PR. +3. Run `just check` before pushing. +4. Update `CHANGELOG.md` under `[Unreleased]`. +5. If you touched documentation claims, make sure they are still true — this + repository has an explicit honesty discipline (below). + +CI gates include governance/licence checks, the Hypatia neurosymbolic scanner, +secret scanning, CodeQL, and both proof tracks. A red proof gate blocks merge. + +## Proof-affecting changes + +If your change touches the typing rules, usage/quantity discipline, the QTT +kernel (`crates/my-qtt/`), or anything in `proofs/`: + +- [`proofs/STATUS.md`](proofs/STATUS.md) is **the single authoritative record** + of what is proved. If your change makes it inaccurate, update it in the same + PR. +- Use its status vocabulary precisely: *machine-checked*, *locally-checked*, + *conformance-checked*, *proved-on-paper*, *statement-only*, + *definitions-only*, *absent*. +- **No proof hole is ever described as proved.** A `statement-only` theorem is + an obligation, not a result. +- The Coq trusted base carries no `Admitted`/`Axiom`; soundness results are + asserted axiom-free via `Print Assumptions` in CI. Keep it that way. + +## Documentation standards + +- Prose is `CC-BY-SA-4.0`; code is `MPL-2.0`. Every file carries **exactly + one** `SPDX-License-Identifier` on its first line. +- Don't document unimplemented behaviour as if it ships. If you must describe + intended design, mark it explicitly as planned and record it in + [`DEBT.md`](DEBT.md). +- Prefer fixing a stale claim to adding a new page. + +## Code of conduct + +Participation is governed by [`CODE_OF_CONDUCT.md`](CODE_OF_CONDUCT.md). + +## Licence + +By contributing you agree that your contributions are licensed under +**MPL-2.0** (code) or **CC-BY-SA-4.0** (documentation), matching the file you +are editing. See [`LICENSE`](LICENSE). diff --git a/DEBT.md b/DEBT.md new file mode 100644 index 0000000..3894a71 --- /dev/null +++ b/DEBT.md @@ -0,0 +1,390 @@ + + + +# my-lang — Debt Register + +**Measured 2026-08-07** against commit `e68bb3d`. One index of known debt across +seven domains. Every item records the command that produced its evidence, so it +can be re-measured rather than re-argued. + +This register **links to** the existing specialised registers rather than +duplicating them: + +- [`proofs/STATUS.md`](proofs/STATUS.md) — authoritative proof-status registry +- [`PROOF-NEEDS.md`](PROOF-NEEDS.md) — proof-side cleanup notes +- [`TESTING.md`](TESTING.md) — per-crate coverage measurements +- [`.machine_readable/6a2/STATE.a2ml`](.machine_readable/6a2/STATE.a2ml) — authoritative machine state + +Severity: **HIGH** = correctness, licensing or security exposure · +**MEDIUM** = misleads users or blocks work · **LOW** = tidiness. + +Items marked **DIAGNOSIS (unconfirmed)** are hypotheses, not established facts. + +--- + +## Summary + +| Domain | Items | High | Medium | Low | +|---|---|---|---|---| +| Licence | 6 | 3 | 2 | 1 | +| Documentation | 8 | 2 | 5 | 1 | +| Code | 6 | 1 | 4 | 1 | +| Proof | 3 | 1 | 2 | 0 | +| Test | 3 | 0 | 2 | 1 | +| CI/CD | 3 | 1 | 2 | 0 | +| Metadata | 5 | 0 | 4 | 1 | +| **Total** | **34** | **8** | **21** | **5** | + +--- + +## Licence (L) + +### L-1 — Undefined SPDX identifier `Palimpsest-0.8` · HIGH +`dialects/solo/compiler/Cargo.toml:6` declares `license = "MIT OR Palimpsest-0.8"`. +`Palimpsest-0.8` is **not a registered SPDX identifier** and there is no +`LICENSES/Palimpsest-0.8.txt`. Any REUSE/SPDX validator rejects this, and the +expression is legally ambiguous. + +```sh +grep -rn '^license' --include=Cargo.toml . | grep -v 'workspace = true' +``` +**Next:** decide the licence for this crate and use a valid expression +(`MPL-2.0` to match the workspace, most likely). + +### L-2 — MIT declared with no MIT licence text · HIGH +`my-ssg/Cargo.toml:6` and `playground/hives/me/Cargo.toml:7` declare +`license = "MIT"`, but `LICENSES/` contains only `AGPL-3.0-or-later.txt`, +`CC-BY-SA-4.0.txt` and `MPL-2.0.txt`. README and the workspace both state +MPL-2.0. +**Next:** either relicense these to MPL-2.0 or add `LICENSES/MIT.txt` and record +the exception deliberately. + +### L-3 — SPDX tag contradicts licence body · HIGH +`frontier-practices/LICENSE` and `playground/LICENSE` both open with +`SPDX-License-Identifier: MPL-2.0`, but their body is the **Palimpsest-MPL +Licence 1.0** text, copyright *"Palimpsest Stewardship Council"* — not the repo +author. A machine reads MPL-2.0; a human reads modified terms. + +```sh +head -3 frontier-practices/LICENSE playground/LICENSE +``` +**Next:** this repo migrated off PMPL on 2026-05-26 (standards#196) — these are +leftovers. Replace with the MPL-2.0 text or delete the subtree licences. + +### L-4 — AGPL text committed while policy bans AGPL · MEDIUM +`LICENSES/AGPL-3.0-or-later.txt` (34 KB) is present; nothing in the tree declares +AGPL, and `.machine_readable/6a2/AGENTIC.a2ml` states *"Never use AGPL licence"*. +Licence scanners will report AGPL for this repository. +**Next:** delete unless a dependency genuinely requires the text. + +### L-5 — 24 manifests carry no `license` key · MEDIUM +Includes `fuzz/Cargo.toml`, `dialects/duet/compiler/Cargo.toml`, and all +`_exploratory/me-scaffolding` + `playground/hives/me` sub-crates. +**Next:** add `license.workspace = true`. + +### L-6 — SPDX header gaps · LOW +`.rs`, `.idr` and `.adoc` are **100% covered**. Missing: **31 of 48 `.toml`** +(including the root `Cargo.toml`), 7 `.yml`, 2 `.v` +(`proofs/verification/coq/{Syntax,Typing}.v`), 1 `.md` (`GOVERNANCE.md`). +**Next:** sweep. Note the estate trap — the header must be **line 1**; a header +on line 3 reads as missing to `head -1` linters. + +--- + +## Documentation (D) + +### D-1 — Wiki documents a toolchain that does not exist · HIGH +`docs/wiki/guides/installation.md` (432 lines) and `getting-started.md` document +`curl https://mylang.org/install.sh`, `brew install mylang`, `cargo install mylang`, +an `mlup` updater, apt/dnf repos at `packages.mylang.org`, and `ml --version`. + +None of it exists. The real binary is **`my`** (`crates/my-cli`), there is no +crates.io publication, and `mylang.org` is not this project's domain. A new user +following these pages cannot succeed. +**Next:** replace with the actual golden path (`git clone` → `just init` → +`just check`). Highest-value doc fix in the repo. + +### D-2 — Standard-library reference describes a retracted design · HIGH +`docs/wiki/reference/stdlib.md` (724 lines) documents a 17-module `std::` source +tree (`std::net`, `std::async`, `std::sync`…). `IMPLEMENTATION.md` explicitly +retracts exactly this: *"That was never built and was actively misleading."* The +real stdlib is ~60 flat Rust builtins in `crates/my-lang/src/stdlib.rs`. +**Next:** regenerate from the actual builtin list, or mark the page as a design +sketch. + +### D-3 — Concurrency and AI pages document unimplemented features · MEDIUM +`docs/wiki/language/concurrency.md` (611 lines) documents `async fn`/`.await`/ +channels; `ai-features.md` (527 lines) documents an `ai!` macro and live model +queries. Concurrency exists as *metatheory only*; the AI runtime performs **mock** +operations. `vscode-extension/README.md` separately calls my-lang "AI-native", +which `docs/wiki/README.md` contradicts. +**Next:** banner both as planned-not-implemented (started — see below), reconcile +the vscode blurb. + +### D-4 — Wiki understates proof status · MEDIUM +Three wiki pages say preservation is *"in progress"* / *"statement-only, gated on +the product-elimination decision"*. It is **machine-checked, axiom-free and +CI-gated** (F1.4, resolved 2026-06-14) per `proofs/STATUS.md`. +**Fixed in this pass** for `docs/wiki/README.md`, `language/dialects.md`, +`internals/formal-verification.md`. Recheck when rungs land. + +### D-5 — GitHub wiki was a 29-byte stub · MEDIUM +The published wiki contained one page (*"Welcome to the my-lang wiki!"*) while 26 +substantial pages sat unpublished in `docs/wiki/`. +**Addressed in this pass** — see [Wiki](#wiki-publication) below. + +### D-6 — Orphaned index and theory stubs point at a dead project · MEDIUM +`docs/MY-LANGUAGE-INDEX.md` is anchored to an *"October 26, 2025 master index +(My-Newsroom project summary)"*; every path in it is dead (`my-newsroom/`, +`docs/dialects/*.md`, `src/checker.rs`, `docs/NEWROOM-ROADMAP.md`). +`docs/theory/*` (5 files) are self-described pointer stubs referencing the same +dead tree. +**Next:** delete or rewrite. They are pure navigational traps. + +### D-7 — `docs/` is published by nothing · MEDIUM +`ARCHITECTURE.md` says `docs/` is *"published via Ddraig SSG"*, and README links +readers to GitHub Pages for documentation. But `pages.yml` builds from the +orphaned root `src/`, while `config.yaml` declares `input: site` — which holds a +single 12-line `index.md`. The 13,000-line `docs/wiki/` tree reaches no reader. +Three different domains are cited across docs (`mylang.org`, `my-lang.net`, +`hyperpolymath.github.io/my-lang`). +**Next:** point the SSG at `docs/`, or stop claiming `docs/` is published. +Publishing the wiki (D-5) mitigates but does not close this. + +### D-8 — `.adoc`/`.md` duplicate pairs · LOW +`README`, `CONTRIBUTING`, `GOVERNANCE`, `MAINTAINERS`, `FOUNDATIONS_BRIDGE` each +exist twice. The `.adoc` copies drifted badly; they cannot be deleted because +`.machine_readable/contractiles/{Mustfile,Trustfile}.a2ml` reference them. +**Partly addressed:** `README.adoc` and `PALIMPSEST.adoc` rewritten as short +accurate pointers rather than competing duplicates. +**Next:** update the contractiles to reference the `.md` files, then retire the +`.adoc` twins. Also: `MAINTAINERS` names *"Metadatastician / @metadatastician"*, +not the `hyperpolymath` identity used everywhere else. + +--- + +## Code (C) + +### C-1 — 7,317 LOC of orphaned duplicate source · HIGH +Root `src/` (8 files, 2,685 LOC) and root `lib/` (17 files, 4,632 LOC) are stale +divergent forks of `crates/my-lang/src/` and `crates/my-lang/lib/`. Neither is +referenced by any manifest, so neither compiles. Root `lib/` contains files that +exist nowhere else (`collections.rs`, `concurrency.rs`, `fs.rs`). + +```sh +find src lib -name '*.rs' | xargs wc -l | tail -1 # 7317 total +``` +This is actively dangerous: `docs/wiki/internals/architecture.md` documents these +orphans as the compiler, and `pages.yml` builds the site from `src/`. +**Next:** salvage the unique files, then delete both trees. `TESTING.md` already +flags them. + +### C-2 — `crates/my-parser` is a published-shape stub · MEDIUM +58 LOC total; `parse_program`/`parse_top_level`/`parse_fn_decl` all return +`Ok(())` unconditionally with `// TODO: Hook the Solo v1.0 grammar into this +method.` It is a full workspace member that parses nothing — the real parser is +`crates/my-lang/src/parser.rs` (100 KB). +**Next:** either wire it up or remove it from the workspace; a crate that always +succeeds is worse than an absent one. + +### C-3 — `dialects/solo/compiler` is all TODO and unbuilt · MEDIUM +`TODO(#parser)`, `TODO(#typeck)`, `TODO(#codegen)`, `TODO(#runtime)`. This is the +artefact the Coq `check_correct` spec exists *for* — README names it as the thing +that must meet the executable spec — yet it is outside the workspace, so nothing +builds or tests it. Corresponds to `STATE.a2ml`'s high-severity `#typeck`. +**Next:** the project's headline correctness goal. Track explicitly. + +### C-4 — Unimplemented handlers in shipped-looking crates · MEDIUM +22 TODOs in `crates/`: `my-lsp` 6 (completions, find-references, rename, +formatting, code actions, signature help), `my-pkg` 5 (registry query, tarball +extraction — i.e. it cannot resolve or install), `my-mir` 4 (closure conversion, +match decision trees), `my-hir` 3. +**Next:** these crates are presented as tooling in the docs; either scope them +down in prose or fill them in. + +### C-5 — Panic surface baselined, not fixed · MEDIUM +7 entries in `.hypatia-baseline.json`, **expiring 2026-10-27** (issue #145). The +gate re-reds at expiry. Counts have drifted from the recorded baseline (`my-fmt` +26→27). The `my-lang` `.expect(` bulk is the documented scanner false positive +(the parser's own `self.expect(TokenKind)` method), but `my-qtt` (12 unwrap + +5 expect) and `my-fmt` (27 unwrap) are not covered by that explanation. +**Next:** discharge before expiry. ~11 weeks. + +### C-6 — Untracked in-tree worktree · LOW +`.claude/worktrees/` is a full second checkout of the repo, **untracked and +absent from `.gitignore`** (`grep -c claude .gitignore` → 0). It doubles every +grep/scan result and inflates the tree. +**Next:** add `.claude/` to `.gitignore`. + +--- + +## Proof (P) + +### P-1 — Proof workflow does not run when the implementation changes · HIGH +`.github/workflows/proofs.yml` triggers only on `paths: proofs/verification/**`. +A change to the checker, the QTT bridge, or `Cargo.toml` never re-runs the proof +gate — precisely the changes most likely to break the correspondence between the +verified spec and the implementation. +**Next:** add `crates/my-qtt/**` and `crates/my-lang/src/{checker,qtt_bridge}.rs` +to the trigger paths. + +### P-2 — Idris track has no hole assertion · MEDIUM +The Coq job runs ~10 `Print Assumptions` gates asserting *"Closed under the +global context"* — a genuine axiom-freedom gate. The Idris job runs +`idris2 --build` only. **A typed hole type-checks**, so a reintroduced +`?todo_*` would pass. `proofs/STATUS.md` correctly grades the Idris results +`locally-checked` rather than `machine-checked`; the gate should match that +honesty. +**Next:** add an explicit hole grep to the Idris job. + +### P-3 — Proof registry is 8 weeks stale · MEDIUM +`proofs/STATUS.md` says *"Last verified: 2026-06-14"*, and it outranks every +other document by its own terms. Meanwhile `proofs.yml` already gates +S3c.3-choice, which `STATE.a2ml` still lists as `pending`. +**Next:** re-verify and re-date. The workflow is ahead of both registries. + +--- + +## Test (T) + +### T-1 — 34 property tests never run · MEDIUM +`tests/property_tests.rs` (23 KB, 34 `#[test]`/`proptest!` blocks) is not +referenced by any `[[test]]` target in any manifest, so it never compiles. Only +`tests/integration_test.rs` is wired (via `crates/my-lang/Cargo.toml:53-55`). +**Next:** wire it or delete it. Unrun tests read as coverage that does not exist. + +### T-2 — Coverage floor is 40% against a 46.7% baseline · MEDIUM +`.github/workflows/coverage.yml` sets `COVERAGE_FLOOR: "40"`, and `my-llvm` is +excluded from measurement entirely. The floor sits *below* the current baseline, +so coverage can regress ~7 points without the gate noticing. +**Next:** raise the floor to just under the measured baseline and ratchet. + +### T-3 — Test count claim reproduces · LOW *(verified, no action)* +Recorded here because it was checked rather than assumed. README's +**"221 tests pass, 0 failures"** reproduces exactly: + +```sh +cargo test --workspace --exclude my-llvm # passed=221 failed=0 ignored=0 +``` +Re-measured 2026-08-07. Contrast the estate pattern where published counts did +not reproduce. + +--- + +## CI/CD (I) + +### I-1 — Lockfile regeneration is a recurring manual step · HIGH +GitHub's Actions lockfile enforcement rejects any workflow whose `actions.lock` +is stale, with a 0-second `startup_failure` whose reason appears **only on the +run's HTML page**. Dependabot bumps action SHAs *without* regenerating the +lockfile, so every bump re-breaks the board — this happened on 2026-08-07 via +#155/#157 (7 of 15 workflows stale; CodeQL, Scorecard and Governance red). + +Additionally, `gh actions-lock` **omits reusable-workflow callers entirely**, so +the six standards wrappers need hand-authored entries plus a transitive `uses:` +sub-list every time. + +```sh +gh actions-lock --verify-local +``` +**Next:** automate. Either a dependabot post-update hook or a scheduled job +running the full recipe (regenerate → restore SHA pins → `relock-sha-keys.sh` → +restore caller entries). Fixed for now in PR #158. + +### I-2 — SPARK gate is advisory and has nothing to check · MEDIUM +`spark-theatre-gate.yml` calls an external reusable with +`enforce_zero_contract: false` — advisory only — and there is **no SPARK/Ada code +in the repository** for it to analyse. It reports green regardless. +**Next:** remove, or make it enforcing if Ada code arrives. + +### I-3 — Governance linter is a shared-fate dependency · MEDIUM +The governance job runs `gh actions-lock --verify-local` from the standards +reusable, so lockfile staleness surfaces as a *governance* failure rather than a +lockfile one — correct behaviour, but it means a standards-side linter change can +red this repo without any local change. Observed 2026-08-07. +**Next:** none required; documented so the failure mode is recognisable. + +--- + +## Metadata (M) + +### M-1 — `ECOSYSTEM.a2ml` is two months stale · MEDIUM +`last-updated = "2026-06-02"`. Lists gaps G1/G2/G3/G5 as open — **all closed** +per `STATE.a2ml`. Still describes *"Four dialects: solo, duet, ensemble, me"*, +which `STATE.a2ml` explicitly retracts (`dialect-model = "nested-subsets"`; `me` +is a projector). +**Next:** regenerate from `STATE.a2ml`. + +### M-2 — `STATE.a2ml` head-commit and proof claims drifted · MEDIUM +`main-commit = "8636e15"` — actual HEAD is `e68bb3d` (8 commits later). +The note *"Idris `?todo_preservation` deliberately open"* is contradicted by +`proofs/STATUS.md` (*discharged 2026-06-21, #108*) and by the tree — zero `?todo` +holes remain. `main-board = "FULLY GREEN"` was false on 2026-08-07. +**Next:** refresh; it is otherwise the best-maintained file in the repo. + +### M-3 — K9 self-validation contradicts the tree · MEDIUM +`.machine_readable/self-validating/my-lang-metadata.k9.ncl` declares +`required_dialects = ["me","solo","duet","ensemble"]` (me is not a dialect) and +`forbidden_patterns = ["unwrap()", "expect()", …]` — violated 85 + 183 times in +`crates/`. MSRV disagrees three ways: `msrv = "1.75"` vs `mise.toml` `1.97.0` vs +`.tool-versions` `stable`, and **no `rust-version` key exists in any +`Cargo.toml`**. +**Next:** a self-validation file that cannot pass is worse than none — reconcile +or scope the patterns to new code. + +### M-4 — Empty and contradictory manifests · MEDIUM +`PLAYBOOK.a2ml` has **zero uncommented keys**; `NEUROSYM.a2ml` is nearly all +commented placeholders; `AGENTIC.a2ml` (2026-04-11) is comment-only and states +*"Never place state files in repository root"* while four sit at root. +Two different `0-AI-MANIFEST.a2ml` files exist (root = S-expression, +`6a2/` = Markdown) with contradictory content. +`svc/README.adoc` documents a `k9/` directory that does not exist (the file lives +in `self-validating/`). +**Next:** fill or delete; deduplicate the manifest. + +### M-5 — Contractile drift · LOW +`contractiles/README.adoc` claims its `Justfile` is *"hardlinked from the repo +root"* — inodes differ (746328 vs 746300), and the copy still carries the +`@echo` stubs that `STATE.a2ml` records as resolved. `Intentfile.a2ml` and both +`bust/*.a2ml` mark already-resolved failure modes as `status: declared`. +**Next:** re-link or regenerate. + +--- + +## What this pass changed + +Fixed in the accompanying documentation PR: + +- **Licence ambiguity**: `PALIMPSEST.adoc` rewritten as a historical note — it + had asserted the repo was licensed PMPL-1.0, contradicting `LICENSE`. +- **`CONTRIBUTING.md`**: was structurally broken (rendered as an H1 mid-code-block, + ended unterminated, carried two conflicting SPDX ids). Rewritten with the real + repository layout, the real signing requirement (`required_signatures` is + enforced by the branch ruleset — not DCO), and a proof-obligations section. +- **`ROADMAP.adoc`**: was a mint-time placeholder (*"Initial development phase"*, + all boxes unchecked) contradicting a 0.2.0 tree with 221 passing tests. + Replaced with the real rung state and an explicit *Not planned* section. +- **`README.adoc`**: stale duplicate contradicting `README.md` on test count, + proof phase and dialect structure → short accurate pointer. +- **`EXPLAINME.adoc`**: corrected the false *"`.hypatia-baseline.json` is an + intentionally empty array"* claim (it has 7 expiring entries), the stale test + count, the four-co-equal-dialects framing, a dead `contractiles/` path, and the + ReScript→AffineScript survivals. +- **Wiki**: preservation status corrected on three pages; aspirational pages + bannered; the 26-page in-tree wiki published to the previously-stub GitHub wiki. +- **Repo metadata**: description and topics replaced (see below). + +## Wiki publication + +`docs/wiki/` is the source of truth; the GitHub wiki is generated from it. Do not +edit the GitHub wiki directly — edits there are overwritten. + +## Repository metadata + +Description and topics were rewritten on 2026-08-07. The previous topics +(`development`, `hyperpolymath`, `open-source`, `rust`, `software`, `tooling`) +duplicated what GitHub already derives from the language list, or named the +owner. The current nine are concept-level and chosen for discoverability: +`quantitative-type-theory`, `affine-types`, `linear-types`, +`mechanized-metatheory`, `session-types`, `verified-compiler`, +`programming-language-design`, `proof-engineering`, `type-systems`. diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index c0302ba..ed832ea 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -20,11 +20,13 @@ safety-critical and AI-adjacent applications. Its central concern is tracked at compile time using *Quantitative Type Theory* (QTT) — a semiring-based discipline that can express "this value is used exactly once (linear), at most once (affine), or arbitrarily (unrestricted)." -The `my-lang` umbrella covers four dialects (*solo*, *duet*, *ensemble*, -*me*) that share a QTT semantic core but differ in concurrency model and -surface syntax. Formal verification — paper proofs plus a mechanised -Coq + Idris2 solo-core — is a first-class deliverable, not an -afterthought. +The `my-lang` umbrella covers *nested* dialects — `solo ⊂ duet ⊂ +ensemble` — that share a QTT semantic core but differ in concurrency +model and surface syntax, plus *me*, an on-the-fly agent-generated +**projection** over that hierarchy rather than a fourth compiler. Only +**solo** is authoritative in `f0`. Formal verification — paper proofs +plus a mechanised Coq + Idris2 solo-core — is a first-class deliverable, +not an afterthought. == Why does this exist alongside `affinescript`? @@ -87,7 +89,8 @@ link:docs/design/echo-types-integration.md[docs/design/echo-types-integration.md | `crates/` | Rust compiler crates. `crates/my-lang/src/types.rs` is the type - checker; it includes `EchoMode`, `Ty::Echo`, and 137+ unit tests. + checker; it includes `EchoMode` and `Ty::Echo`. The workspace runs + **221 tests, 0 failures** (measured 2026-08-07, excluding `my-llvm`). | `dialects/` | Per-dialect surface syntax. `solo/` (affine, single-agent) is the @@ -119,7 +122,7 @@ link:docs/design/echo-types-integration.md[docs/design/echo-types-integration.md | Exploratory forward-looking research code (outside the Cargo workspace; not shipped). -| `contractiles/` +| `.machine_readable/contractiles/` | Mustfile / Dustfile invariant and recovery contracts for `my-lang`. | `.machine_readable/` @@ -167,10 +170,17 @@ Hypatia is the estate's neurosymbolic governance scanner * Trusted-base pollution (`Admitted`/`Axiom` in Coq files) * Licence consistency (SPDX headers on all files) -Exemptions live in link:.hypatia-ignore[`.hypatia-ignore`] with inline -rationale. The link:.hypatia-baseline.json[`.hypatia-baseline.json`] -file is an intentionally empty array (`[]`) — all scanner findings have -been resolved at source or exempted with documented rationale. +Two mechanisms, deliberately distinguished: + +* link:.hypatia-ignore[`.hypatia-ignore`] holds **permanent** scoped + exemptions with inline rationale — facts about rule imprecision, not + debt. +* link:.hypatia-baseline.json[`.hypatia-baseline.json`] holds + **expiring** acknowledged debt. It currently carries **7 entries, + expiring 2026-10-27**, tracked in + https://github.com/hyperpolymath/my-lang/issues/145[issue #145] — the + unwrap/expect panic surface. These are *baselined, not fixed*; the + gate re-reds at expiry. See `DEBT.md`. == Language policy summary @@ -178,9 +188,9 @@ The estate enforces strict language restrictions (see link:.claude/CLAUDE.md[`.claude/CLAUDE.md`]): * **Allowed**: Rust, Idris2, OCaml (AffineScript compiler), Coq, - Agda, ReScript, Deno, Gleam, Nickel, Guile Scheme, Julia, Ada. -* **Banned**: TypeScript (use ReScript), Node/npm/bun (use Deno), - Go (use Rust), Python (use Julia/Rust/ReScript), + Agda, AffineScript, Deno, Gleam, Nickel, Guile Scheme, Julia, Ada. +* **Banned**: TypeScript (use AffineScript), Node/npm/bun (use Deno), + Go (use Rust), Python (use Julia/Rust/AffineScript), Kotlin/Swift/Flutter (use Tauri 2.0+/Dioxus). All new source files require an SPDX licence header. diff --git a/PALIMPSEST.adoc b/PALIMPSEST.adoc index 04a4322..7f3637d 100644 --- a/PALIMPSEST.adoc +++ b/PALIMPSEST.adoc @@ -1,45 +1,50 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Owner: Jonathan D.A. Jewell // Copyright (c) Jonathan D.A. Jewell -= Palimpsest License += Palimpsest Licence — Historical Note (superseded) :toc: :toc-placement!: -image:https://img.shields.io/badge/License-MPL--2.0-blue.svg[License: PMPL-1.0,link="https://github.com/hyperpolymath/palimpsest-license"] -image:https://img.shields.io/badge/Philosophy-Palimpsest-indigo.svg[Palimpsest,link="https://github.com/hyperpolymath/palimpsest-license"] +image:https://img.shields.io/badge/License-MPL--2.0-blue.svg[License: MPL-2.0,link="https://www.mozilla.org/en-US/MPL/2.0/"] toc::[] -== Legal Status +[IMPORTANT] +==== +**This document is historical. my-lang is licensed under MPL-2.0.** -This project is licensed under the **Palimpsest-MPL License 1.0 (PMPL-1.0)**. -For SPDX and tooling, use **MPL-2.0**. +The authoritative licence is the `LICENSE` file at the repository root +(Mozilla Public License 2.0, `SPDX-License-Identifier: MPL-2.0`). This +file is retained only to record the migration; it does **not** state the +current licensing terms. +==== -PMPL-1.0 incorporates the Mozilla Public License 2.0 by reference and adds -ethical-use, provenance, and lineage requirements. +== Current legal status -== What PMPL Adds +my-lang is licensed under the **Mozilla Public License 2.0 (MPL-2.0)**. -* **Emotional Lineage** - preserve narrative intent and cultural context -* **Provenance Integrity** - retain attribution and lineage metadata -* **Ethical Use Constraints** - explicit consent for non-interpretive AI training -* **Quantum-Safe Provenance (optional)** - post-quantum signature support +* Licence text: `LICENSE` (repository root) +* SPDX identifier for all code: `MPL-2.0` +* SPDX identifier for prose/documentation: `CC-BY-SA-4.0` -== How to Adopt +Third-party licence texts kept for REUSE compliance live in `LICENSES/`. -1. Include the PMPL-1.0 license text in `LICENSE`. -2. Add SPDX headers to source files: - `SPDX-License-Identifier: CC-BY-SA-4.0` -// Owner: Jonathan D.A. Jewell -3. Add a Palimpsest badge to your README (see `assets/badges/` and `embed/license-blocks/`). +== Migration record + +my-lang previously carried the **Palimpsest-MPL Licence 1.0 +(PMPL-1.0-or-later)**, an MPL-2.0 superset adding ethical-use, provenance +and lineage requirements. -== Versioning +It was **migrated to plain MPL-2.0 on 2026-05-26** as part of the estate +licence-debt audit (`hyperpolymath/standards#196`). The reasons recorded +at the time were SPDX/tooling interoperability and removing ambiguity +about which terms actually bind a downstream consumer. -See `VERSIONING.adoc` for the release process and the "-or-later" model. -The current legal text is PMPL-1.0. +Nothing in this repository is offered under PMPL-1.0. -== References +== Where PMPL lives now -* `legal/README.adoc` -* `assets/badges/README.md` -* `embed/license-blocks/README.md` +The Palimpsest licence remains an active estate project in its own right — +see https://github.com/hyperpolymath/palimpsest-license[hyperpolymath/palimpsest-license]. +Repositories that *do* use it say so in their own `LICENSE` file. my-lang +does not. diff --git a/README.adoc b/README.adoc index 160ed85..db61472 100644 --- a/README.adoc +++ b/README.adoc @@ -1,176 +1,76 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Owner: Jonathan D.A. Jewell -// Copyright (c) 2026 Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> - -= my-lang (AsciiDoc edition) -:author: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> -:revdate: 2026-06-02 -:toc: left -:toclevels: 2 - -`my-lang` is the *next-generation language* working project — a -multi-dialect surface for the hyperpolymath language stack. It is one -of two flagship language experiments in the estate (the other being -link:https://github.com/hyperpolymath/affinescript[`affinescript`]). -The two projects are *siblings*, not a fork — they share design -principles but diverge in dialect scope and proof strategy. - -For a gentler entry point see link:EXPLAINME.adoc[EXPLAINME.adoc]. - -== What's in here - -`crates/`:: -Rust crates implementing the compiler / interpreter layers. The core -type checker lives in `crates/my-lang/src/types.rs` and includes -`EchoMode`, `Ty::Echo`, and full affine-weakening semantics. - -`dialects/`:: -Per-dialect surface-syntax definitions. The `my-lang` umbrella admits -multiple surface dialects sharing a common semantic core: *solo* -(affine, single-agent), *duet* (session-typed, two-party), *ensemble* -(multi-agent), and *me* (block/visual/pedagogic). - -`proofs/`:: -Formal verification assets — paper proofs, mechanised Coq + Idris2 -solo-core, and the alignment roadmap toward AffineScript parity. -See link:proofs/STATUS.md[`proofs/STATUS.md`] for the authoritative -proof-status registry and link:proofs/ALIGNMENT-PLAN.md[`proofs/ALIGNMENT-PLAN.md`] -for the phased roadmap. - -`conformance/`:: -Conformance tests — programs that any compliant `my-lang` implementation -must accept (or reject) identically. - -`examples/`:: -Worked examples covering each dialect, suitable as a learning -reference and CI smoke-test. - -`docs/`:: -Design notes, language-reference drafts, and ADRs (Architecture Decision -Records). Includes link:docs/design/echo-types-integration.md[the echo-types -integration design note]. - -`frontier-practices/`:: -Forward-looking experiments — things that may become part of the -language but are not yet stable. - -`contractiles/`:: -Project-level Mustfile / Dustfile contracts: invariant checks and -recovery semantics for `my-lang` tooling. - -== Quickstart - -[source,bash] ----- -git clone git@github.com:hyperpolymath/my-lang.git -cd my-lang +// Copyright (c) Jonathan D.A. Jewell += my-lang +:revdate: 2026-08-07 -just build # builds the workspace (Rust) -just test # runs unit + conformance tests ----- +[IMPORTANT] +==== +**`README.md` is the canonical README for this repository.** -To check a single Coq proof file: +This AsciiDoc file is retained because estate tooling references it. It is a +short summary only — for the full picture (proof-status table, repository map, +golden path, security posture) read +https://github.com/hyperpolymath/my-lang/blob/main/README.md[`README.md`]. -[source,bash] ----- -cd proofs/verification/coq/solo-core -coq_makefile -f _CoqProject -o CoqMakefile && make -f CoqMakefile ----- +An earlier, much longer version of this file drifted badly out of date and +contradicted `README.md` on test counts, proof phase, dialect structure and +directory layout. It was replaced on 2026-08-07 rather than left to mislead. +==== -To check the Idris2 solo-core: +== What this is -[source,bash] ----- -cd proofs/verification/idris/solo-core -idris2 --check solo-core.ipkg ----- +my-lang is a research programming language with a *mechanised metatheory*: an +affine / Quantitative-Type-Theory (QTT `{0, 1, ω}`) core whose soundness is +proved on two independent tracks — Coq/Rocq (authoritative) and Idris2 (twin) — +with the verified usage-checker ported into the Rust compiler. -== Proof and verification status +It is a *sibling* of https://github.com/hyperpolymath/affinescript[AffineScript], +not a fork. -`my-lang` follows a *statements-first, machine-checked later* proof -methodology (mirroring `affinescript`'s solo-core approach). The -link:proofs/STATUS.md[Proof Status Registry] is the single -authoritative source — no proof is described as "proved" there until -a proof assistant accepts it. +== Dialects -Current state (2026-06-02): +The dialects are *nested conservative extensions*, not four peers: -* **QTT semiring + laws** — *locally-checked* on both Coq and Idris2 - tracks. All semiring and ordering laws proved by exhaustive case - analysis (`Qed` / `Refl`). -* **Solo-core syntax, contexts, typing** — *definitions-only* on - both tracks. -* **Progress / Preservation** — *statement-only* obligations; - proofs are Phase F1.3 / F1.4 deliverables. -* **Echo type former** — *locally-checked* in Rust (5 Agda-mirroring - unit tests covering `EchoMode` ordering and affine-weakening - semantics). Mechanised residue layer in Coq/Idris is Phase F1 work. -* **Paper proofs** — ~6.3 k lines across `proofs/shared/` and - per-dialect subdirectories (solo/duet/ensemble/me): type-system - soundness, effect soundness, memory model, operational and - denotational semantics, AI semantics. +.... +Solo ⊂ Duet ⊂ Ensemble (+ me, a projection — not a fourth compiler) +.... -Proof CI (running `coqc`/`idris2 --check` in CI) is Phase F5. +Only **Solo** is authoritative in `f0`, per the scope-arrest anchor +(`ANCHOR.scope-arrest.2026-01-01.Jewell.scm`). Duet and Ensemble exist as proof +developments and scaffolding; `me` is an on-the-fly, agent-generated projection +over the hierarchy with a machine-checked `me → solo` elaboration-correctness +theorem. -== Echo type integration - -`my-lang` integrates the link:https://github.com/hyperpolymath/echo-types[`echo-types`] -Agda library — a formal account of *loss that is not total erasure*. +== Status -[source] +* **Version**: 0.2.0 — early alpha, experimental. No tagged release. +* **Licence**: MPL-2.0 (code), CC-BY-SA-4.0 (documentation). Migrated from + PMPL-1.0-or-later on 2026-05-26; see `PALIMPSEST.adoc`. +* **Tests**: 221 pass, 0 failures (`just test`, excludes `my-llvm`). +* **Proofs**: `proofs/STATUS.md` is the single authoritative registry. + Progress, preservation and `affine_pres` are machine-checked and axiom-free + on the Coq track, CI-gated per rung. + +== Key documents + +[cols="1,3",options="header"] +|=== +| File | Purpose +| `README.md` | Canonical README +| `EXPLAINME.adoc` | Gentle conceptual orientation +| `ARCHITECTURE.md` | Structure and dialect containment +| `ROADMAP.adoc` | What is done, next, and explicitly not planned +| `DEBT.md` | Known licence / docs / code / proof / CI debt +| `proofs/STATUS.md` | Authoritative proof-status registry +| `.machine_readable/6a2/STATE.a2ml` | Authoritative machine-readable state +|=== + +== Golden path + +[source,sh] ---- -Echo B> // "a proof-relevant residue of a lossy collapse from A to B" +just init # submodules +just check # fmt-check + lint + test +just proofs # both proof tracks ---- - -`EchoMode { Linear, Affine }` mirrors the `EchoLinear.agda` two-point -poset `linear ⊑ affine`. A `Linear` echo may be weakened to `Affine` -(one-way, no section). Domain and codomain are invariant under subtyping. - -Claim boundary (retraction R-2026-05-18): -____ -Echo models irreversible weakening as a one-way, proof-relevant residue -transformation. It is a *loss-graded reindexing modality over a thin -poset*, not a graded comonad or free construction. -____ - -For full design rationale see link:docs/design/echo-types-integration.md[docs/design/echo-types-integration.md]. - -== Architectural authority - -* link:ANCHOR.scope-arrest.2026-01-01.Jewell.scm[`ANCHOR.scope-arrest.*`] - — the scope-arrest anchor file enumerating what `my-lang` will and - will not be. -* link:AUTHORITY_STACK.mustfile-nickel.scm[`AUTHORITY_STACK.mustfile-nickel.scm`] - — the cross-cutting authority stack for the design. - -These two files are the source-of-truth for "is `X` in scope for -`my-lang`?" — consult them before opening a feature request. - -== Status - -* **Licence**: MPL-2.0. (Migrated from PMPL-1.0-or-later 2026-05-26 per - the estate licence-debt audit, hyperpolymath/standards#196.) -* **Maturity**: design-iteration / early alpha. Working Rust compiler - core exists (137 passing tests); surface syntax and semantics still - settling. -* **Proof phase**: F1.0 complete — QTT semiring proved, soundness - statements committed on dual Coq + Idris2 tracks. -* **Governance**: CI green on all shipped checks; proof CI (F5) pending. - -== Contributing - -See link:CONTRIBUTING.adoc[CONTRIBUTING.adoc] (or -link:CONTRIBUTING.md[CONTRIBUTING.md]). GPG-signed commits required. - -Language policy, package management, and security requirements are -enforced by the estate governance workflow -(`hyperpolymath/standards`). New contributors should read -link:EXPLAINME.adoc[EXPLAINME.adoc] first. - -== Companion repositories - -* link:https://github.com/hyperpolymath/standards[`hyperpolymath/standards`] — canonical estate-wide standards and governance. -* link:https://github.com/hyperpolymath/affinescript[`hyperpolymath/affinescript`] — sibling language project; the target AffineScript parity state is defined in link:proofs/ALIGNMENT-PLAN.md[`proofs/ALIGNMENT-PLAN.md`]. -* link:https://github.com/hyperpolymath/echo-types[`hyperpolymath/echo-types`] — upstream Agda echo-types library integrated into the `my-lang` type checker. -* link:https://github.com/hyperpolymath/EchoTypes.jl[`hyperpolymath/EchoTypes.jl`] — Julia executable companion to `echo-types`; planned differential oracle for Phase 2 echo-type testing. -* link:https://github.com/hyperpolymath/typed-wasm[`hyperpolymath/typed-wasm`] — the typed-wasm backend `my-lang` shares with `affinescript`. diff --git a/ROADMAP.adoc b/ROADMAP.adoc index 3f8a61b..1324d52 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -1,24 +1,129 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Owner: Jonathan D.A. Jewell // Copyright (c) Jonathan D.A. Jewell -= My Lang Roadmap += my-lang Roadmap +:toc: +:toc-placement!: +:revdate: 2026-08-07 -== Current Status +toc::[] -Initial development phase. +[NOTE] +==== +This roadmap is *derived*, not authoritative. The machine-readable source of +truth is `.machine_readable/6a2/STATE.a2ml`; for proofs specifically it is +`proofs/STATUS.md`. Where they disagree with this file, they win. +==== -== Milestones +== Current status -=== v0.1.0 - Foundation -* [ ] Core functionality -* [ ] Basic documentation -* [ ] CI/CD pipeline +*Version 0.2.0 — early alpha, experimental.* No tagged release yet. -=== v1.0.0 - Stable Release -* [ ] Full feature set -* [ ] Comprehensive tests -* [ ] Production ready +What actually works today: -== Future Directions +* 15-crate Cargo workspace; **221 tests pass, 0 failures** (`just test`, + excluding `my-llvm`), ~46.7% line-coverage baseline. +* Working compiler pipeline: parse → HIR → MIR → LLVM → native, on x86_64 + and aarch64. +* **Solo** is the only live dialect. Duet and Ensemble exist as proof + developments plus scaffolding, not as usable compilers. +* Mechanised metatheory on two tracks (Coq/Rocq authoritative, Idris2 twin), + gated in CI by `proofs.yml` with per-rung `Print Assumptions` checks. -_To be determined based on community feedback._ +Scope is deliberately arrested at Solo for `f0` — see +`ANCHOR.scope-arrest.2026-01-01.Jewell.scm`. + +== Done + +=== Foundations (F) + +[cols="1,4",options="header"] +|=== +| Rung | Result +| F1.0 | Dual-track QTT solo-core scaffold; semiring laws proved +| F1.1 | Small-step CBV operational semantics, both tracks +| F1.3 | *Progress* proved on both tracks +| F1.4 | *Preservation* + QTT substitution lemma (`ht_subst`) + `affine_pres`; product/elimination resolved (additive `&` and multiplicative `⊗` both coherent) +| F5 | Proof CI live (`coqc` + `idris2 --build`, Print-Assumptions gated per rung) +|=== + +=== Resource-algebra parametricity (R) + +[cols="1,4",options="header"] +|=== +| Rung | Result +| R2 | Solo core functorised over `Module Type SEMIRING`; `Include Linear3` recovers progress/preservation/`affine_pres` *axiom-free* +| R3 | `ORDERED_SEMIRING` + subusage; `affine_pres` becomes a genuinely distinct theorem +| R4 | Tropical (min-plus, *infinite* carrier) instance — soundness survives with no new proof +| R5 | Executable usage-walk checker `check` + `check_correct` (sound **and** complete); `aff_type_dec` +|=== + +=== Elaboration and structure (M, S) + +* *M1* — `me → solo` elaboration with `me_wt_sound` over the whole `me_tm`, axiom-free. +* *S1–S2* — session-π subject reduction, session fidelity, progress/deadlock-freedom; duet-by-projection (S2.0–S2.2) with `projection_duality`. +* *S3a/S3b* — n-party projection totality; static n-party configuration. +* *S3c.0/.1/.2* — full label-union merge; union-projection; n-ary located operational semantics. +* *S3c.3-msg* — head-coupled message subject reduction: the **first earned n-party safety half**. + +== Next + +Ordered as recorded in `STATE.a2ml [critical-next-actions]`: + +. **S3c completion** — remaining n-party safety: select/branch subject + reduction (S3c.3-choice), run-ahead/permutation SR (S3c.3-perm), then + n-party progress (S3c.4). _Large._ S3c.4 is research-hard and explicitly + fenced: `wf_assignment ra → deadlock-free` is **false**, so progress needs a + coherence⇒safety argument, not an extension of the current lemmas. +. **S1.3b-meta** — μ typing and subject reduction up-to-unfolding + (`PT_Unfold` + soundness + up-to-unfolding inversions). _Large._ +. **F1.2** — extend to the four-point affine semiring (`0 ⊏ ? ⊏ 1 ⊏ ω`), + adding the *at-most-once* quantity. _6–8 hours._ +. **Echo stage 2** — `Echo B>` surface syntax in the Solo parser + (`echo-2`). _4–6 hours._ The type former and its proof layer (`echo-1`, + `echo-3`) already landed. + +== Open gaps + +[cols="1,3,1",options="header"] +|=== +| Id | Gap | Severity + +| `#typeck` +| The Solo affine type-checker is still a **hand-written Rust checker tested + against** the mechanised `check` (R5) — *not proved equal to it*. The + verified core leads the implementation and is its specification; closing + this is the project's headline correctness goal. +| high + +| `panic-surface` +| Hypatia unwrap/expect debt **baselined, not fixed** — 7 entries expiring + *2026-10-27* (issue #145). Must be revisited before expiry or the gate + re-reds. +| medium + +| F3 | Memory model not mechanised. | pending +| F4 | Paper-proof topic parity with AffineScript. | pending +|=== + +Documentation, licence, CI and code debt is catalogued separately in +`DEBT.md`. + +== Not planned + +To set expectations, these appear in older drafts and are **not** committed +work: + +* A published package registry, installer script, or Homebrew/apt/dnf + distribution. The binary is `my`; it is not published to crates.io. +* `async`/`await`, futures, or a channel runtime in the surface language. + Concurrency currently exists as *metatheory*, not as an implemented feature. +* A shipped `std::` source-module tree. The standard library is a flat set of + Rust builtins. +* Real AI model integration. The AI surface performs **mock** operations. + +== Release criteria + +There is no `1.0`. The next meaningful milestone is a tagged **0.3.0**, which +requires at minimum: `#typeck` closed or honestly re-scoped, the `#145` +baseline discharged, and the documentation debt in `DEBT.md` cleared. diff --git a/docs/wiki/README.md b/docs/wiki/README.md index 5e110b1..b4f69fb 100644 --- a/docs/wiki/README.md +++ b/docs/wiki/README.md @@ -38,7 +38,7 @@ integration is one capability among many — not the defining feature. | Aspect | Description | |--------|-------------| | **Affine / QTT core** | Every binder carries a quantity `0` (erased), `1` (linear), or `ω` (unrestricted) | -| **Formally verified** | Solo-core mechanised in **Coq + Idris2**; *progress* proved, *preservation* in progress | +| **Formally verified** | Solo-core mechanised in **Coq + Idris2**. On the Coq track *progress*, *preservation* and `affine_pres` are machine-checked, **axiom-free** and CI-gated per rung | | **Echo types** | `echo-types` integrated into the type system — *loss that is not total erasure* (a loss-graded reindexing modality) | | **Progressive disclosure** | `Solo ⊂ Duet ⊂ Ensemble`; only Solo is authoritative in `f0` | | **Rust implementation** | The compiler/interpreter is implemented in Rust | @@ -105,7 +105,7 @@ integration is one capability among many — not the defining feature. ## Project status -- **Version:** `0.1.0` (early-alpha) — see +- **Version:** `0.2.0` (early-alpha, experimental; no tagged release) — see [`.machine_readable/6a2/STATE.a2ml`](../../.machine_readable/6a2/STATE.a2ml) for the authoritative state, and [`proofs/STATUS.md`](../../proofs/STATUS.md) for the proof-status registry. @@ -120,5 +120,8 @@ See [`CONTRIBUTING.md`](../../CONTRIBUTING.md) and ## License My Language is open source under the **Mozilla Public License 2.0 (MPL-2.0)** — -see [`LICENSE`](../../LICENSE). Every source file carries an -`SPDX-License-Identifier: CC-BY-SA-4.0` header. +see [`LICENSE`](../../LICENSE). + +Code files carry `SPDX-License-Identifier: MPL-2.0`; prose and documentation +carry `CC-BY-SA-4.0`. Known licensing inconsistencies are tracked as **L-1** +through **L-6** in [`DEBT.md`](../../DEBT.md). diff --git a/docs/wiki/guides/getting-started.md b/docs/wiki/guides/getting-started.md index 4f586fb..edc2528 100644 --- a/docs/wiki/guides/getting-started.md +++ b/docs/wiki/guides/getting-started.md @@ -4,6 +4,12 @@ Copyright (c) Jonathan D.A. Jewell --> # Getting Started +> [!WARNING] +> **Parts of this page assume an installed toolchain that does not exist yet.** +> +> Ignore any `ml` command or package-manager install step — the binary is **`my`** and the only supported path is a source build (`just init && just check`). Tracked as debt **D-1** in [`DEBT.md`](https://github.com/hyperpolymath/my-lang/blob/main/DEBT.md). + + Welcome to My Language! This guide will help you install the toolchain and write your first program. ## Installation diff --git a/docs/wiki/guides/installation.md b/docs/wiki/guides/installation.md index 3e446aa..64d5cd1 100644 --- a/docs/wiki/guides/installation.md +++ b/docs/wiki/guides/installation.md @@ -4,6 +4,23 @@ Copyright (c) Jonathan D.A. Jewell --> # Installation Guide +> [!WARNING] +> **Most of this page describes an installation surface that does not exist.** +> +> There is no `mylang.org` installer, no Homebrew/apt/dnf package, no `mlup`, and no crates.io publication. The binary is **`my`**, not `ml`. +> +> The only supported install today is from source: +> +> ```sh +> git clone https://github.com/hyperpolymath/my-lang.git +> cd my-lang +> just init +> just check +> ``` +> +> Tracked as debt **D-1** in [`DEBT.md`](https://github.com/hyperpolymath/my-lang/blob/main/DEBT.md). + + Detailed instructions for installing My Language on various platforms. ## System Requirements diff --git a/docs/wiki/internals/formal-verification.md b/docs/wiki/internals/formal-verification.md index e50d389..3846e21 100644 --- a/docs/wiki/internals/formal-verification.md +++ b/docs/wiki/internals/formal-verification.md @@ -44,7 +44,7 @@ resource may go unused. | F1.0 | QTT semiring + laws (both tracks) | ✅ **proved** (exhaustive case analysis) | | F1.1 | CBV small-step operational semantics (`Step`/`step`) | ✅ **committed** (both tracks) | | F1.3 | **Progress** | ✅ **proved** — Coq `Theorem … Qed.` (axiom-free); Idris total, hole-free | -| F1.4 | **Preservation** + QTT substitution lemma | ⏳ statement-only — **gated** on the product/elimination decision ([#93](https://github.com/hyperpolymath/my-lang/issues/93)) | +| F1.4 | **Preservation** + QTT substitution lemma (`ht_subst`) + `affine_pres` | ✅ **proved** (2026-06-14) — Coq `Qed.`, **axiom-free**, CI-gated. The product/elimination question ([#93](https://github.com/hyperpolymath/my-lang/issues/93)) is **resolved**: additive `&` and multiplicative `⊗` are both coherent | | F1.2 | Four-point affine semiring (`0 ⊏ ? ⊏ 1 ⊏ ω`) | ⏳ planned | | F5 | **Proof CI** | ✅ **live** — `.github/workflows/proofs.yml` | diff --git a/docs/wiki/language/ai-features.md b/docs/wiki/language/ai-features.md index 16dac98..4eaf7bb 100644 --- a/docs/wiki/language/ai-features.md +++ b/docs/wiki/language/ai-features.md @@ -4,6 +4,14 @@ Copyright (c) Jonathan D.A. Jewell --> # AI Features +> [!WARNING] +> **The AI runtime performs mock operations.** +> +> The `ai!` macro and model queries described here are not wired to any real provider. AI integration is *one capability among many*, not the defining feature of the language. +> +> Tracked as debt **D-3** in [`DEBT.md`](https://github.com/hyperpolymath/my-lang/blob/main/DEBT.md). + + My Language provides first-class AI integration, making AI operations as natural as any other language feature. ## Overview diff --git a/docs/wiki/language/concurrency.md b/docs/wiki/language/concurrency.md index ab58687..df6c89f 100644 --- a/docs/wiki/language/concurrency.md +++ b/docs/wiki/language/concurrency.md @@ -4,6 +4,14 @@ Copyright (c) Jonathan D.A. Jewell --> # Concurrency +> [!WARNING] +> **None of the concurrency described here is implemented.** +> +> There is no `async`/`await`, no futures runtime and no channel implementation in the surface language. Concurrency currently exists as **metatheory** — a mechanised session-typed π-calculus in `proofs/` (subject reduction, session fidelity, deadlock-freedom) — not as a language feature. +> +> Tracked as debt **D-3** in [`DEBT.md`](https://github.com/hyperpolymath/my-lang/blob/main/DEBT.md). + + My Language provides modern concurrency primitives for safe, efficient parallel and asynchronous programming. ## Async/Await diff --git a/docs/wiki/language/dialects.md b/docs/wiki/language/dialects.md index 4cec45f..f92a1f8 100644 --- a/docs/wiki/language/dialects.md +++ b/docs/wiki/language/dialects.md @@ -31,7 +31,8 @@ not ship partial semantics** — their design lives in paper proofs not in shipping code. This containment is deliberate: make one dialect real and correct before widening. -The Solo kernel's metatheory (progress proved; preservation in progress) is +The Solo kernel's metatheory (progress, preservation and `affine_pres` all +machine-checked and axiom-free on the Coq track) is documented under [Formal Verification](../internals/formal-verification.md). ## Me is *not* a fourth dialect diff --git a/docs/wiki/reference/stdlib.md b/docs/wiki/reference/stdlib.md index 84fddf8..17c2b1c 100644 --- a/docs/wiki/reference/stdlib.md +++ b/docs/wiki/reference/stdlib.md @@ -4,6 +4,14 @@ Copyright (c) Jonathan D.A. Jewell --> # Standard Library Reference +> [!WARNING] +> **This page documents a `std::` module tree that was never built.** +> +> `IMPLEMENTATION.md` explicitly retracts this design: *"That was never built and was actively misleading."* The real standard library is a flat set of ~60 Rust builtins in `crates/my-lang/src/stdlib.rs` (`fs_read_file`, `map_new`, `json_parse`, …). +> +> Read this as a **design sketch**, not a reference. Tracked as debt **D-2** in [`DEBT.md`](https://github.com/hyperpolymath/my-lang/blob/main/DEBT.md). + + Complete reference for the My Language standard library. ## Overview diff --git a/docs/wiki/roadmap/compiler.md b/docs/wiki/roadmap/compiler.md index 8aace32..115ea82 100644 --- a/docs/wiki/roadmap/compiler.md +++ b/docs/wiki/roadmap/compiler.md @@ -4,6 +4,10 @@ Copyright (c) Jonathan D.A. Jewell --> # Compiler Roadmap +> [!WARNING] +> **Status markers on this page are stale** (last updated 2025-12-17). Several items marked *Planned* have shipped (LLVM backend, formatter, linter, LSP), and the Type Checker marked *Complete* is in fact the open `#typeck` obligation. [`ROADMAP.adoc`](https://github.com/hyperpolymath/my-lang/blob/main/ROADMAP.adoc) and `.machine_readable/6a2/STATE.a2ml` are authoritative. + + This document outlines the development plan for the My Language compiler infrastructure. ## Architecture Overview diff --git a/docs/wiki/roadmap/ecosystem.md b/docs/wiki/roadmap/ecosystem.md index 8068a38..fb29f35 100644 --- a/docs/wiki/roadmap/ecosystem.md +++ b/docs/wiki/roadmap/ecosystem.md @@ -4,6 +4,12 @@ Copyright (c) Jonathan D.A. Jewell --> # Ecosystem Roadmap +> [!WARNING] +> **This page describes an ecosystem that does not exist.** +> +> No package registry, forum, or playground is deployed, and the package counts quoted are illustrative. See [`ROADMAP.adoc`](https://github.com/hyperpolymath/my-lang/blob/main/ROADMAP.adoc) for what is actually planned, including an explicit *Not planned* section. + + This document outlines the development plan for the My Language ecosystem: frameworks, libraries, and community resources. ## Ecosystem Vision diff --git a/docs/wiki/roadmap/language.md b/docs/wiki/roadmap/language.md index e8359d1..2dbf0ab 100644 --- a/docs/wiki/roadmap/language.md +++ b/docs/wiki/roadmap/language.md @@ -4,6 +4,10 @@ Copyright (c) Jonathan D.A. Jewell --> # Language Roadmap +> [!WARNING] +> **Status markers on this page are stale** (last updated 2025-12-17). Several items marked *Planned* have shipped (LLVM backend, formatter, linter, LSP), and the Type Checker marked *Complete* is in fact the open `#typeck` obligation. [`ROADMAP.adoc`](https://github.com/hyperpolymath/my-lang/blob/main/ROADMAP.adoc) and `.machine_readable/6a2/STATE.a2ml` are authoritative. + + This document details the evolution of My Language's core features and syntax. ## Current State (v0.1.0) diff --git a/docs/wiki/roadmap/overview.md b/docs/wiki/roadmap/overview.md index c2ba0a0..5831ecd 100644 --- a/docs/wiki/roadmap/overview.md +++ b/docs/wiki/roadmap/overview.md @@ -4,6 +4,10 @@ Copyright (c) Jonathan D.A. Jewell --> # My Language Roadmap Overview +> [!WARNING] +> **Status markers on this page are stale** (last updated 2025-12-17). Several items marked *Planned* have shipped (LLVM backend, formatter, linter, LSP), and the Type Checker marked *Complete* is in fact the open `#typeck` obligation. [`ROADMAP.adoc`](https://github.com/hyperpolymath/my-lang/blob/main/ROADMAP.adoc) and `.machine_readable/6a2/STATE.a2ml` are authoritative. + + *Last Updated: 2025-12-17* This document outlines the complete development roadmap for My Language, covering the language itself, compiler infrastructure, tooling, and ecosystem. diff --git a/docs/wiki/roadmap/tooling.md b/docs/wiki/roadmap/tooling.md index 00698f4..035dec5 100644 --- a/docs/wiki/roadmap/tooling.md +++ b/docs/wiki/roadmap/tooling.md @@ -4,6 +4,10 @@ Copyright (c) Jonathan D.A. Jewell --> # Tooling Roadmap +> [!WARNING] +> **Status markers on this page are stale** (last updated 2025-12-17). Several items marked *Planned* have shipped (LLVM backend, formatter, linter, LSP), and the Type Checker marked *Complete* is in fact the open `#typeck` obligation. [`ROADMAP.adoc`](https://github.com/hyperpolymath/my-lang/blob/main/ROADMAP.adoc) and `.machine_readable/6a2/STATE.a2ml` are authoritative. + + This document outlines the development plan for My Language development tools. ## Overview diff --git a/docs/wiki/tooling/overview.md b/docs/wiki/tooling/overview.md index 823275f..d5c8178 100644 --- a/docs/wiki/tooling/overview.md +++ b/docs/wiki/tooling/overview.md @@ -4,6 +4,12 @@ Copyright (c) Jonathan D.A. Jewell --> # Tooling Overview +> [!WARNING] +> **Tool names and registry URLs on this page are aspirational.** +> +> The real crates are `my-fmt`, `my-lint`, `my-pkg`, `my-lsp` (not `mlfmt`/`mllint`/`mlpkg`), and several have unimplemented handlers. There is no package registry at `packages.mylang.org`. See debt **C-4** and **D-3** in [`DEBT.md`](https://github.com/hyperpolymath/my-lang/blob/main/DEBT.md). + + Development tools for My Language. ## Core Tools