From 24c8423876bede52c1c2407d43f615416975542d Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sat, 19 Sep 2026 09:26:29 +0000 Subject: [PATCH] refactor(root): relocate the contributing guide into .github/ The estate canonical location is .github/CONTRIBUTING.md, which GitHub auto-discovers; the root copy is removed and references are updated in the same change. * .github/CONTRIBUTING.md (new) * CONTRIBUTING.adoc (deleted) * README.adoc * frontier-practices/.gitlab-ci.yml * frontier-practices/README.adoc * spec/ARG-PROFILE.adoc --- .github/CONTRIBUTING.md | 189 ++++++++++++++++++++++++++++++ CONTRIBUTING.adoc | 187 ----------------------------- README.adoc | 2 +- frontier-practices/.gitlab-ci.yml | 2 +- frontier-practices/README.adoc | 2 +- spec/ARG-PROFILE.adoc | 2 +- 6 files changed, 193 insertions(+), 191 deletions(-) create mode 100644 .github/CONTRIBUTING.md delete mode 100644 CONTRIBUTING.adoc diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md new file mode 100644 index 0000000..cf09b24 --- /dev/null +++ b/.github/CONTRIBUTING.md @@ -0,0 +1,189 @@ +# 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 + +# Initialise submodules (proof tracks and vendored specs) +just init + +# Verify the toolchain works +just check # fmt-check + lint + test +just test # unit + conformance tests (excludes my-llvm) +``` + +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**: + +``` sh +just proofs # both tracks +just proofs-coq # the authoritative track +just proofs-idris # the Idris2 twin +``` + +Run `just` `--list` for the full recipe set. + +## Repository structure + + 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 + +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. + +## How to contribute + +### Reporting bugs + +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. + +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. + +### Suggesting features + +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). + +### Good first contributions + +- [`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) + +Documentation accuracy fixes are especially welcome — see +[`DEBT.md`](DEBT.md) for a catalogue of known-stale pages. + +## Development workflow + +### Branches + + 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 + +### 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/CONTRIBUTING.adoc b/CONTRIBUTING.adoc deleted file mode 100644 index 8afd528..0000000 --- a/CONTRIBUTING.adoc +++ /dev/null @@ -1,187 +0,0 @@ -== 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 -link:#proof-affecting-changes[Proof-affecting changes]. - -=== Getting set up - -[source,sh] ----- -# Clone -git clone https://github.com/hyperpolymath/my-lang.git -cd my-lang - -# Initialise submodules (proof tracks and vendored specs) -just init - -# Verify the toolchain works -just check # fmt-check + lint + test -just test # unit + conformance tests (excludes my-llvm) ----- - -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*: - -[source,sh] ----- -just proofs # both tracks -just proofs-coq # the authoritative track -just proofs-idris # the Idris2 twin ----- - -Run `+just --list+` for the full recipe set. - -=== Repository structure - -.... -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 -.... - -Note: the root `+src/+`, `+lib/+` and `+tests/+` trees are *orphaned* — -not referenced by any crate. They are tracked as debt in -link:DEBT.md[`+DEBT.md+`]; do not add to them. - -=== How to contribute - -==== Reporting bugs - -Search existing issues first, then use the -link:.github/ISSUE_TEMPLATE/bug_report.md[bug report template]. Include -the environment, steps to reproduce, expected vs actual behaviour, and a -minimal reproduction where possible. - -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. - -==== Suggesting features - -Check link:ROADMAP.adoc[`+ROADMAP.adoc+`] and -link:proofs/STATUS.md[`+proofs/STATUS.md+`] first — a surprising amount -of "`missing`" functionality is deliberately fenced pending a proof. -Then use the link:.github/ISSUE_TEMPLATE/feature_request.md[feature -request template]. - -==== Good first contributions - -* https://github.com/hyperpolymath/my-lang/labels/good%20first%20issue[`+good first issue+`] -* https://github.com/hyperpolymath/my-lang/labels/help%20wanted[`+help wanted+`] -* https://github.com/hyperpolymath/my-lang/labels/documentation[`+documentation+`] - -Documentation accuracy fixes are especially welcome — see -link:DEBT.md[`+DEBT.md+`] for a catalogue of known-stale pages. - -=== Development workflow - -==== Branches - -.... -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 -.... - -==== Commits - -We follow https://www.conventionalcommits.org/[Conventional Commits]: - -.... -(): - -[optional body] - -[optional footer] -.... - -*Commits must be cryptographically signed.* The `+main+` branch ruleset -enforces `+required_signatures+`, so unsigned commits are rejected at -push time: - -[source,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 - -[arabic] -. Branch from `+main+`. -. Keep the change focused; unrelated cleanups belong in their own PR. -. Run `+just check+` before pushing. -. Update `+CHANGELOG.md+` under `+[Unreleased]+`. -. 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/+`: - -* link: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 -link:DEBT.md[`+DEBT.md+`]. -* Prefer fixing a stale claim to adding a new page. - -=== Code of conduct - -Participation is governed by -link: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 link:LICENSE[`+LICENSE+`]. diff --git a/README.adoc b/README.adoc index dbb198d..f30044d 100644 --- a/README.adoc +++ b/README.adoc @@ -435,7 +435,7 @@ for the machine-readable version. === Contributing -See CONTRIBUTING.adoc. GPG-signed commits required. Language policy, +See .github/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 EXPLAINME.adoc first. diff --git a/frontier-practices/.gitlab-ci.yml b/frontier-practices/.gitlab-ci.yml index 9d214dd..4ee27d1 100644 --- a/frontier-practices/.gitlab-ci.yml +++ b/frontier-practices/.gitlab-ci.yml @@ -21,7 +21,7 @@ validate: - test -f LICENSE.txt - test -f SECURITY.md - test -f CODE_OF_CONDUCT.adoc - - test -f CONTRIBUTING.adoc + - test -f ../.github/CONTRIBUTING.md - test -f GOVERNANCE.adoc - test -d curriculum - test -d agents diff --git a/frontier-practices/README.adoc b/frontier-practices/README.adoc index e99b9a0..1897dad 100644 --- a/frontier-practices/README.adoc +++ b/frontier-practices/README.adoc @@ -157,7 +157,7 @@ seven-tentacles/ == Contributing -We welcome contributions! Please see our link:CONTRIBUTING.adoc[contribution guidelines]. +We welcome contributions! Please see our link:../.github/CONTRIBUTING.md[contribution guidelines]. === Priority Areas diff --git a/spec/ARG-PROFILE.adoc b/spec/ARG-PROFILE.adoc index cf4f257..f0444ab 100644 --- a/spec/ARG-PROFILE.adoc +++ b/spec/ARG-PROFILE.adoc @@ -63,7 +63,7 @@ Cross-axis rule: ARG ≤ TRG holds. | *D3 — Provenance* | YES -| MAINTAINERS.adoc + LICENSE + CITATION (via CONTRIBUTING.adoc) + +| MAINTAINERS.adoc + LICENSE + CITATION (via ../.github/CONTRIBUTING.md) + CODE_OF_CONDUCT | *TRG ≥ D estate-wide*