|
| 1 | +# Map — An MMF release bar for the opam packages |
| 2 | + |
| 3 | +Charted 2026-08-24 · Tickets: [`docs/scout/tickets-opam-mmf/`](tickets-opam-mmf/README.md) |
| 4 | + |
| 5 | +## Destination |
| 6 | + |
| 7 | +A **locked release bar** — a named checklist plus the gate evidence it cites, on a |
| 8 | +pinned corpus commit — which, when met, makes **`rocq-spatial-algebra 0.1.0`** |
| 9 | +and **`rocq-robust-predicates 0.1.0`** *installable from the Rocq opam |
| 10 | +archive*. The map is done |
| 11 | +when nothing remains to decide before someone can write that bar and clear it. |
| 12 | + |
| 13 | +This map does **not** cut the releases. Plan, don't mint. |
| 14 | + |
| 15 | +## Notes |
| 16 | + |
| 17 | +- **Domain:** [`CONTEXT.md`](../../CONTEXT.md). Consult it before naming anything; |
| 18 | + add terms there as they settle. |
| 19 | +- **These are Rocq libraries, not OCaml libraries.** Both packages ship `.v` |
| 20 | + files under the `NTS.Proofs` logpath and depend on `rocq-core` / `rocq-stdlib` |
| 21 | + / `coq-flocq`. Neither contains a line of OCaml. "The OCaml libraries" means |
| 22 | + "the things we distribute through opam" and is a phrase to retire. |
| 23 | +- **MMF is imported vocabulary.** The term appears nowhere in this repo; it comes |
| 24 | + from the `grootstebozewolf/jts` fork (`doc/MMF_OPTION_B.md`). We import its |
| 25 | + *shape* — a named checklist plus published gate evidence on a pinned mint — and |
| 26 | + define an **opam-specific** bar. The fork's own gates (TestBuilder queue, UX |
| 27 | + SIGN, laser ratchet) have no analogue here and are not inherited. |
| 28 | +- **Skills:** `/grilling` and `/domain-modeling` on decision tickets. Research |
| 29 | + tickets need a `/research` session. |
| 30 | +- **Standing preferences:** gates over prose — a claim that lives only in a |
| 31 | + comment has already failed once here. Optimise for maintainability → |
| 32 | + soundness → performance. Cite by name, never by line number. |
| 33 | +- **Tracker:** this map and its tickets are tracked markdown under `docs/scout/`, |
| 34 | + matching [the epic-block map](map-epic-block-64-69.md). One ticket per session; |
| 35 | + claim by adding `**Claimed:** <name>` under the title before doing any work. |
| 36 | + |
| 37 | +### Settled while charting (do not re-litigate) |
| 38 | + |
| 39 | +- **The bar requires opam-installable.** A GitHub release with an attached |
| 40 | + tarball is not a mint. An MMF nobody can `opam install` has no "M". |
| 41 | +- **Both packages are `rocq-*` and restart at 0.1.0.** Settled by ticket 01 — |
| 42 | + no objection upstream, nothing was ever released to the archive, so there is |
| 43 | + no lineage to continue. Supersedes the original 0.1.4 / 0.1.3 targets. |
| 44 | +- **The manifest stays pinned.** Same module set, updated content — that is what |
| 45 | + a `0.1.x` patch means here. Growing the packages is a separate effort. |
| 46 | +- **Manifest closure is part of the bar, and gated.** Not a nice-to-have. |
| 47 | +- **Mint before the module split.** A split renames files and changes package |
| 48 | + contents materially; ship the current known-good set first. |
| 49 | + |
| 50 | +### Findings that seeded this map (verified 2026-08-24) |
| 51 | + |
| 52 | +- **No prior release ever landed upstream.** `released/packages/` in |
| 53 | + `rocq-prover/opam` (which `coq/opam` redirects to) has no entry for either |
| 54 | + package, and an archive-wide code search for all four name spellings returns |
| 55 | + zero hits. `coq-flocq` is present at four versions, so the path convention is |
| 56 | + confirmed. All six published releases are GitHub tarballs only. |
| 57 | +- **`assemble.sh` never verifies manifest closure.** The claim lives only in a |
| 58 | + MANIFEST header comment, and that comment is already wrong: it describes a |
| 59 | + "15-file set" where the list holds 21 paths. |
| 60 | +- **`OPAM_PUBLISH_TOKEN` has been configured since 2026-06-24**, yet the |
| 61 | + workflow's silent-fallback branch is evidently the path every release took. |
| 62 | +- **The declared lower bound is untested:** both packages declare |
| 63 | + `rocq-core {>= "9.0"}`; CI builds only the pinned 9.2.0. |
| 64 | +- **`DE9IM.v` has changed since the last mint** (the `im_unsupported` sentinel), |
| 65 | + so `spatial-algebra` has real content to ship rather than a bare bump. |
| 66 | + |
| 67 | +## Decisions so far |
| 68 | + |
| 69 | +<!-- one line per closed ticket: enough to judge relevance, then open the ticket --> |
| 70 | + |
| 71 | +- [Collect the community verdict on the `rocq-*` rename](tickets-opam-mmf/closed/01-community-verdict-on-rocq-rename.md) |
| 72 | + — no objection; **both** packages become `rocq-*` and restart at **0.1.0**. The |
| 73 | + ideal "rocq-* depends only on rocq-*" rule initially suggested keeping |
| 74 | + `robust-predicates` as `coq-*` because of `coq-flocq`; dropped deliberately, |
| 75 | + since Flocq 4.2.2 already implements the Rocq standard library and only its |
| 76 | + upstream *name* is still `coq-*`. New tag prefix was forced: the old |
| 77 | + `*-v0.1.0` tags already exist. Old releases kept as history. |
| 78 | + |
| 79 | +- [Decide the Rocq version constraint](tickets-opam-mmf/closed/03-rocq-version-constraint.md) |
| 80 | + — match `rocq-bignums`, not `coq-fourcolor`: `rocq-core {>= "9.2" & < "9.4~"}` |
| 81 | + with `rocq-stdlib` unconstrained, `coq-flocq {>= "4.2.2" & < "4.3~"}`, and a |
| 82 | + published tested-on date. A wider Rocq range is served by publishing |
| 83 | + `+rocqX.Y` versions, never by widening a bound. Carries rename evidence to |
| 84 | + ticket 01 (archive is 1111 `rocq-*` to 5302 mostly-legacy `coq-*`) and three |
| 85 | + bar lines to ticket 06. **Amended same day:** the upper bound was wrong — |
| 86 | + Rocq 9.3 is not released (stable tops out at 9.2.0), so `< "9.4~"` permitted |
| 87 | + two nonexistent versions; corrected to `< "9.3~"`. Both packages verified to |
| 88 | + build and lint locally in the same pass. |
| 89 | + |
| 90 | +## Not yet specified |
| 91 | + |
| 92 | +- **What verifies "installable".** A consumer smoke test — fresh switch, |
| 93 | + `opam install`, `Require Import NTS.Proofs.DE9IM` — is the obvious shape, but |
| 94 | + it cannot be specified until ticket 04 establishes how publishing actually |
| 95 | + behaves here. |
| 96 | +- **Whether the bar requires a per-package CHANGELOG.** None exists anywhere |
| 97 | + today; six releases have shipped without one. |
| 98 | +- **The external-consumer doc surface**, particularly for |
| 99 | + `robust-predicates`, whose selling point includes machine-checked |
| 100 | + counterexamples to a textbook theorem. What a stranger needs in order to trust |
| 101 | + and use that is not yet a sharp question. |
| 102 | +- **Lockstep or independent release.** The two packages have always been tagged |
| 103 | + minutes apart, but nothing says they must move together — and their bars will |
| 104 | + differ on the axiom line. |
| 105 | +- **Whether the `NTS.Proofs` logpath is right for a distributed package.** Both |
| 106 | + packages install into the corpus's own namespace; whether that is |
| 107 | + neighbourly in a shared opam namespace is unexamined. |
| 108 | + |
| 109 | +## Out of scope |
| 110 | + |
| 111 | +- **Packaging the `oracle/` OCaml as an opam library.** Real OCaml exists |
| 112 | + (`driver.ml`, `extracted.ml`, `nts_ffi.ml`, `relate_matrix.ml`) and is |
| 113 | + entirely unpackaged, but this map is about the two existing Rocq packages. A |
| 114 | + separate effort if it is ever wanted. |
| 115 | +- **The module split of `Orient_b64_exact.v`** and the release it will drive. |
| 116 | + Sequenced explicitly after this mint. |
| 117 | +- **Growing either package's module set.** Follows from the pinned-manifest |
| 118 | + decision. |
| 119 | +- **The jts fork's MMF gates.** Named here only to record that they are |
| 120 | + deliberately not inherited. |
0 commit comments