Address opam archive review: rename, drop ocaml dep, fix maintainer

.github/workflows/package-robust-predicates.yml

@@ -1,7 +1,7 @@
-name: Package rocq-robust-predicates
+name: Package rocq-robust-geometric-predicates
 
-# Validate and publish the standalone `rocq-robust-predicates` opam package
-# (packaging/rocq-robust-predicates/), extracted from the corpus via its
+# Validate and publish the standalone `rocq-robust-geometric-predicates` opam package
+# (packaging/rocq-robust-geometric-predicates/), extracted from the corpus via its
 # MANIFEST + assemble.sh.
 #
 #   - validate: on PRs/pushes touching the package (and on demand) assemble
@@ -10,7 +10,7 @@ name: Package rocq-robust-predicates
 #     (build: [make]; install: [make install]).  This catches manifest drift
 #     (a renamed/removed source file makes assemble.sh fail), opam-file
 #     regressions, and build breakage.
-#   - publish: on a `rocq-robust-predicates-v*` release, build the self-contained
+#   - publish: on a `rocq-robust-geometric-predicates-v*` release, build the self-contained
 #     source tarball (`make package`), attach it to the release, and -- when
 #     an OPAM_PUBLISH_TOKEN secret is configured -- open the opam-repository
 #     PR via `opam publish`.  Without the secret it attaches the tarball and
@@ -25,13 +25,13 @@ on:
   pull_request:
     branches: [main]
     paths:
-      - 'packaging/rocq-robust-predicates/**'
+      - 'packaging/rocq-robust-geometric-predicates/**'
       - 'Dockerfile'
       - '.github/workflows/package-robust-predicates.yml'
   push:
     branches: [main]
     paths:
-      - 'packaging/rocq-robust-predicates/**'
+      - 'packaging/rocq-robust-geometric-predicates/**'
       - 'Dockerfile'
       - '.github/workflows/package-robust-predicates.yml'
   workflow_dispatch:
@@ -42,8 +42,8 @@ on:
 env:
   FORCE_JAVASCRIPT_ACTIONS_TO_NODE24: "true"
   TOOLCHAIN_IMAGE: ghcr.io/${{ github.repository_owner }}/nts-proofs-toolchain
-  PKG_DIR: packaging/rocq-robust-predicates
-  OPAM_FILE: rocq-robust-predicates.opam
+  PKG_DIR: packaging/rocq-robust-geometric-predicates
+  OPAM_FILE: rocq-robust-geometric-predicates.opam
 
 concurrency:
   group: package-robust-predicates-${{ github.ref }}
@@ -121,7 +121,7 @@ jobs:
   publish:
     name: Build tarball and publish on release
     # Only the package's own release tags; ignores corpus/oracle releases.
-    if: github.event_name == 'release' && startsWith(github.event.release.tag_name, 'rocq-robust-predicates-v')
+    if: github.event_name == 'release' && startsWith(github.event.release.tag_name, 'rocq-robust-geometric-predicates-v')
     needs: validate
     runs-on: ubuntu-latest
     permissions:
@@ -169,7 +169,7 @@ jobs:
 
       - name: Build self-contained source tarball
         # `make package` runs assemble.sh then archives the vendored tree to
-        # packaging/rocq-robust-predicates/dist/rocq-robust-predicates.tar.gz (builds with no corpus present).
+        # packaging/rocq-robust-geometric-predicates/dist/rocq-robust-geometric-predicates.tar.gz (builds with no corpus present).
         run: |
           chmod -R a+rwX .
           docker run --rm -v "$PWD:/workspace" -w /workspace \
@@ -181,22 +181,22 @@ jobs:
               make package
             '
           sudo chown -R "$(id -u):$(id -g)" .
-          ls -la packaging/rocq-robust-predicates/dist/rocq-robust-predicates.tar.gz
-          sha256sum packaging/rocq-robust-predicates/dist/rocq-robust-predicates.tar.gz | tee packaging/rocq-robust-predicates/dist/rocq-robust-predicates.tar.gz.sha256
+          ls -la packaging/rocq-robust-geometric-predicates/dist/rocq-robust-geometric-predicates.tar.gz
+          sha256sum packaging/rocq-robust-geometric-predicates/dist/rocq-robust-geometric-predicates.tar.gz | tee packaging/rocq-robust-geometric-predicates/dist/rocq-robust-geometric-predicates.tar.gz.sha256
 
       - name: Attach tarball to the release
         uses: softprops/action-gh-release@v2
         with:
           files: |
-            packaging/rocq-robust-predicates/dist/rocq-robust-predicates.tar.gz
-            packaging/rocq-robust-predicates/dist/rocq-robust-predicates.tar.gz.sha256
+            packaging/rocq-robust-geometric-predicates/dist/rocq-robust-geometric-predicates.tar.gz
+            packaging/rocq-robust-geometric-predicates/dist/rocq-robust-geometric-predicates.tar.gz.sha256
 
       - name: Submit to opam-repository (if OPAM_PUBLISH_TOKEN configured)
         env:
           OPAM_PUBLISH_TOKEN: ${{ secrets.OPAM_PUBLISH_TOKEN }}
           OPAM_TARGET_REPO: ${{ vars.OPAM_TARGET_REPO || 'coq/opam' }}
           TAG: ${{ github.event.release.tag_name }}
-          TARBALL_URL: ${{ github.server_url }}/${{ github.repository }}/releases/download/${{ github.event.release.tag_name }}/rocq-robust-predicates.tar.gz
+          TARBALL_URL: ${{ github.server_url }}/${{ github.repository }}/releases/download/${{ github.event.release.tag_name }}/rocq-robust-geometric-predicates.tar.gz
         run: |
           if [ -z "${OPAM_PUBLISH_TOKEN:-}" ]; then
             echo "::notice::OPAM_PUBLISH_TOKEN not set -- skipping automated opam-repository PR; tarball is attached to the release."
@@ -208,11 +208,11 @@ jobs:
             } >> "$GITHUB_STEP_SUMMARY"
             exit 0
           fi
-          # Clean semver from the tag (strip the "rocq-robust-predicates-v" prefix):
-          #   rocq-robust-predicates-v0.1.0 -> 0.1.0.  MUST be exported so `docker -e
+          # Clean semver from the tag (strip the "rocq-robust-geometric-predicates-v" prefix):
+          #   rocq-robust-geometric-predicates-v0.1.0 -> 0.1.0.  MUST be exported so `docker -e
           #   VERSION` passes it into the container (a bare assignment is not
           #   in the environment -> `set -u` would trip).
-          export VERSION="${TAG#rocq-robust-predicates-v}"
+          export VERSION="${TAG#rocq-robust-geometric-predicates-v}"
           # opam-publish reads its GitHub token from OPAM_PUBLISH_GH_TOKEN
           # (NOT GITHUB_TOKEN).  Best-effort: the tarball is already attached,
           # so if opam publish trips (auth/fork/etc.) we warn + print the
@@ -226,9 +226,9 @@ jobs:
               set -euxo pipefail
               opam install -y opam-publish
               # opam-publish takes the package NAME from the opam filename
-              # (rocq-robust-predicates) and the VERSION from the version: field;
+              # (rocq-robust-geometric-predicates) and the VERSION from the version: field;
               # set it from the tag so the submitted package is
-              # rocq-robust-predicates.$VERSION (not the raw tag).
+              # rocq-robust-geometric-predicates.$VERSION (not the raw tag).
               echo "version: \"$VERSION\"" >> "$PKG_DIR/$OPAM_FILE"
               # opam-publish reads its Continue/Submit confirmations from the
               # controlling TTY, not stdin, so in CI (no tty) it aborts with no

packaging/README.md

@@ -13,13 +13,13 @@ self-contained opam source tarball.
 
 | Package | Files | Deps | Axioms | What it is |
 |---|---|---|---|---|
-| [`rocq-robust-predicates`](./rocq-robust-predicates/) | 15 | Flocq | classical-reals only | Machine-checked robust binary64 geometric predicates (orientation, segment intersection, error-free expansions), sound vs. exact arithmetic. Fills a real ecosystem gap — no verified Rocq package for Shewchuk-style predicates existed before. |
+| [`rocq-robust-geometric-predicates`](./rocq-robust-geometric-predicates/) | 15 | Flocq | classical-reals only | Machine-checked robust binary64 geometric predicates (orientation, segment intersection, error-free expansions), sound vs. exact arithmetic. Fills a real ecosystem gap — no verified Rocq package for Shewchuk-style predicates existed before. |
 | [`rocq-spatial-algebra`](./rocq-spatial-algebra/) | 2 | Stdlib only | **none** (axiom-free) | DE-9IM intersection-matrix algebra + integer orientation-determinant overflow bounds. A tiny, dependency-free entry point for formal GIS / spatial-relation reasoning. |
 
 ## Releasing
 
 Each package publishes via its own GitHub Actions workflow
-(`.github/workflows/package-*.yml`): a release tagged `rocq-robust-predicates-v*`
+(`.github/workflows/package-*.yml`): a release tagged `rocq-robust-geometric-predicates-v*`
 or `rocq-spatial-algebra-v*` builds the source tarball, attaches it (+ sha256) to
 the release, and — when an `OPAM_PUBLISH_TOKEN` secret is configured — opens
 the opam-repository PR via `opam publish`.

packaging/rocq-robust-predicates/MANIFEST → packaging/rocq-robust-geometric-predicates/MANIFEST

@@ -1,4 +1,4 @@
-# MANIFEST for rocq-robust-predicates
+# MANIFEST for rocq-robust-geometric-predicates
 # ---------------------------------------------------------------------------
 # Source-of-record paths (relative to the NetTopologySuite.Proofs repo root)
 # for every .v file vendored into this standalone package.  `assemble.sh`

packaging/rocq-robust-predicates/Makefile → packaging/rocq-robust-geometric-predicates/Makefile

@@ -1,4 +1,4 @@
-# Makefile for rocq-robust-predicates.
+# Makefile for rocq-robust-geometric-predicates.
 #
 # Delegates to the Rocq-generated Makefile.coq.  Run ./assemble.sh first to
 # vendor the source .v files from the corpus (the opam source tarball produced
@@ -20,12 +20,12 @@ install: Makefile.coq
 package: clean
 	./assemble.sh
 	mkdir -p dist
-	tar czf dist/rocq-robust-predicates.tar.gz \
-	    --transform 's,^,rocq-robust-predicates/,' \
+	tar czf dist/rocq-robust-geometric-predicates.tar.gz \
+	    --transform 's,^,rocq-robust-geometric-predicates/,' \
 	    MANIFEST _CoqProject Makefile assemble.sh README.md LICENSE \
-	    rocq-robust-predicates.opam dune-project default.nix \
+	    rocq-robust-geometric-predicates.opam dune-project default.nix \
 	    theories theories-flocq
-	@echo "Wrote dist/rocq-robust-predicates.tar.gz"
+	@echo "Wrote dist/rocq-robust-geometric-predicates.tar.gz"
 
 clean:
 	@if [ -f Makefile.coq ]; then $(MAKE) -f Makefile.coq cleanall || true; fi

packaging/rocq-robust-predicates/README.md → packaging/rocq-robust-geometric-predicates/README.md

@@ -1,4 +1,4 @@
-# rocq-robust-predicates
+# rocq-robust-geometric-predicates
 
 Machine-checked **robust geometric predicates for binary64 (IEEE-754 double)
 coordinates**, with `Qed`-closed soundness against exact arithmetic — extracted
@@ -46,7 +46,7 @@ release tarball is already assembled, so this step is only for an in-repo
 build):
 
 ```sh
-cd packaging/rocq-robust-predicates
+cd packaging/rocq-robust-geometric-predicates
 ./assemble.sh            # copy the 21 source files from the corpus
 ```
 
@@ -76,7 +76,7 @@ To produce a standalone opam source tarball (self-contained, no corpus needed
 — bundles the opam, dune, and nix files):
 
 ```sh
-make package             # -> dist/rocq-robust-predicates.tar.gz
+make package             # -> dist/rocq-robust-geometric-predicates.tar.gz
 ```
 
 ## Namespace

packaging/rocq-robust-predicates/assemble.sh → packaging/rocq-robust-geometric-predicates/assemble.sh

@@ -12,7 +12,7 @@
 #   ./assemble.sh [CORPUS_ROOT]
 #
 # CORPUS_ROOT defaults to the repo root two levels up (this package lives at
-# <repo>/packaging/rocq-robust-predicates/).
+# <repo>/packaging/rocq-robust-geometric-predicates/).
 # ===========================================================================
 set -euo pipefail
 

packaging/rocq-robust-predicates/default.nix → packaging/rocq-robust-geometric-predicates/default.nix

@@ -8,7 +8,7 @@
 , coqPackages ? pkgs.coqPackages
 }:
 coqPackages.mkCoqDerivation {
-  pname = "rocq-robust-predicates";
+  pname = "rocq-robust-geometric-predicates";
   owner = "grootstebozewolf";
   version = "0.1.0";
   src = ./.;

packaging/rocq-robust-predicates/rocq-robust-predicates.opam → packaging/rocq-robust-geometric-predicates/rocq-robust-geometric-predicates.opam

@@ -30,28 +30,19 @@ the package MANIFEST). Every theorem ends in `Qed`; the only axioms are the
 standard classical-reals + functional-extensionality used throughout the
 corpus (see `make`'s `Print Assumptions` output).
 """
-maintainer: "https://github.com/grootstebozewolf/NetTopologySuite.Proofs/issues"
+maintainer: "Jeroen Bloemscheer <jeroen.bloemscheer@merkator.com>"
 authors: ["NetTopologySuite.Proofs contributors"]
 license: "BSD-3-Clause"
 homepage: "https://github.com/grootstebozewolf/NetTopologySuite.Proofs"
 bug-reports: "https://github.com/grootstebozewolf/NetTopologySuite.Proofs/issues"
 dev-repo: "git+https://github.com/grootstebozewolf/NetTopologySuite.Proofs.git"
 
 depends: [
-  "ocaml"
   "rocq-core" {>= "9.2" & < "9.3~"}
   "rocq-stdlib"
-  # Flocq has no rocq-* release yet, so this package necessarily depends on a
-  # coq-* one.  The archive's ideal is that a rocq-* package depends only on
-  # rocq-* packages, so that CI can prove it builds without the compatibility
-  # binaries from coq-core; upstream guidance is that the rule is not
-  # universally followed, so the name follows the development.
-  #
-  # The >= 4.2.2 floor is not merely "the version we tested": 4.2.2 is the
-  # release that implements the Rocq standard library, so it is the first Flocq
-  # that is Rocq-native in substance despite carrying a coq-* name.  Anything
-  # older would pull the Coq compat layer back in and defeat the point of the
-  # rocq-* naming.
+  # Flocq has no rocq-* release yet. 4.2.2 is the first Flocq implementing
+  # the Rocq standard library, so the dependency is Rocq-native in substance
+  # even though its package name is still coq-*.
   "coq-flocq" {>= "4.2.2" & < "4.3~"}
 ]
 

packaging/rocq-robust-predicates/theories-flocq/dune → packaging/rocq-robust-geometric-predicates/theories-flocq/dune

@@ -1,4 +1,4 @@
 (coq.theory
  (name NTS.Proofs.Flocq)
- (package rocq-robust-predicates)
+ (package rocq-robust-geometric-predicates)
  (theories NTS.Proofs Flocq))

packaging/rocq-robust-geometric-predicates/theories/dune

@@ -0,0 +1,3 @@
+(coq.theory
+ (name NTS.Proofs)
+ (package rocq-robust-geometric-predicates))

packaging/rocq-spatial-algebra/assemble.sh

@@ -12,7 +12,7 @@
 #   ./assemble.sh [CORPUS_ROOT]
 #
 # CORPUS_ROOT defaults to the repo root two levels up (this package lives at
-# <repo>/packaging/rocq-robust-predicates/).
+# <repo>/packaging/rocq-robust-geometric-predicates/).
 # ===========================================================================
 set -euo pipefail
 

packaging/rocq-spatial-algebra/rocq-spatial-algebra.opam

@@ -24,15 +24,14 @@ formal GIS / spatial-relation reasoning or robust-predicate overflow analysis.
 Provenance: github.com/grootstebozewolf/NetTopologySuite.Proofs (assembled via
 the package MANIFEST).
 """
-maintainer: "https://github.com/grootstebozewolf/NetTopologySuite.Proofs/issues"
+maintainer: "Jeroen Bloemscheer <jeroen.bloemscheer@merkator.com>"
 authors: ["NetTopologySuite.Proofs contributors"]
 license: "BSD-3-Clause"
 homepage: "https://github.com/grootstebozewolf/NetTopologySuite.Proofs"
 bug-reports: "https://github.com/grootstebozewolf/NetTopologySuite.Proofs/issues"
 dev-repo: "git+https://github.com/grootstebozewolf/NetTopologySuite.Proofs.git"
 
 depends: [
-  "ocaml"
   "rocq-core" {>= "9.2" & < "9.3~"}
   "rocq-stdlib"
 ]

scripts/cut-releases.ps1

@@ -7,8 +7,7 @@ $ErrorActionPreference = 'Stop'
 $repo = 'grootstebozewolf/NetTopologySuite.Proofs'
 
 $releases = @(
-  @{ Tag='rocq-spatial-algebra-v0.1.0';   Title='rocq-spatial-algebra 0.1.0';   Notes='Axiom-free DE-9IM algebra + integer determinant bounds.' }
-  @{ Tag='rocq-robust-predicates-v0.1.0'; Title='rocq-robust-predicates 0.1.0'; Notes='Robust binary64 geometric predicates, sound vs. exact arithmetic.' }
+  @{ Tag='rocq-robust-geometric-predicates-v0.1.0'; Title='rocq-robust-geometric-predicates 0.1.0'; Notes='Robust binary64 geometric predicates, sound vs. exact arithmetic.' }
 )
 
 if (-not (Get-Command gh -ErrorAction SilentlyContinue)) {