Add rocq-spatial-algebra.0.1.0 and rocq-robust-predicates.0.1.0

[grootstebozewolf]

Two small, self-contained Rocq libraries extracted from the
NetTopologySuite.Proofs
corpus (BSD-3-Clause). First release of either package.

rocq-spatial-algebra.0.1.0

DE-9IM intersection-matrix algebra plus integer orientation-determinant bounds.
Two modules, Stdlib-only, no axioms — Print Assumptions reports Closed
under the global context for everything it exports.

rocq-robust-geometric-predicates.0.1.0

Machine-checked robust binary64 geometric predicates, proven sound against exact
arithmetic: exact orient2d sign via an error-free expansion, an adaptive
filter with expansion fallback, and integer-coordinate overflow bounds. Axiom
footprint is functional_extensionality_dep and Classical_Prop.classic, both
reported by Print Assumptions.

It depends on coq-flocq rather than a rocq--named Flocq because none exists
yet; 4.2.2 is the first Flocq implementing the Rocq standard library, so the
dependency is Rocq-native in substance even though the package name is not. A
short note to that effect is in the depends: block so it doesn't read as an
oversight.

Checks run before submitting

Both packages, from the released tarballs rather than a working tree:

• extract and make clean with no corpus present — self-contained
• opam lint → Passed
• Print Assumptions output matches the axiom claims above
• published sha256 assets re-verified against the tarballs; sha512 in the
  url blocks computed from the same files

Tested on Rocq 9.1.1 with Flocq 4.2.2. The declared floor is >= 9.2 because
that is what the project's CI builds — 9.1 demonstrably works, and if reach
matters I would rather earn it with a CI job and a +rocq9.1 version than widen
a bound I do not test. The upper bound is < 9.3~ since 9.3 is not yet
released.

Happy to adjust naming, bounds or metadata to house style — this is a first
submission and I would rather match your conventions than argue for mine.

[proux01]

A few comments but otherwise LGTM.

[proux01]

geometric seems like a very important keyword here, maybe it should appear somewhere in the name. I mean, robust-predicates seems a bit overly generic.

[proux01]

Should this say anything about JTS? (I'm not sure how important the link is)

[proux01]

Does this really need ocaml? I don't see any ml code in the tarball.

[proux01]

The maintainer OPAM field is the maintainer of the package (so yourself as the one opening this PR I guess).

[grootstebozewolf]

Thanks for the review — all four are useful. Status:

ocaml dependency — dropped, you're right. I checked: zero .ml/.mli/.mll/.mly in either tarball, and the Makefile's only ocaml/dune mentions are a tar file list and a comment. The build is pure rocq makefile. I'd copied this from rocq-bignums, which genuinely ships OCaml — mine doesn't, so it was an unearned dependency. Fixed for both packages.

maintainer — fixed. Now a person rather than the issue-tracker URL; bug-reports already carries the tracker.

Both of the above are pushed for rocq-spatial-algebra already.

Name — agreed, renaming to rocq-robust-geometric-predicates. "Overly generic" is fair, and geometric was only in the synopsis where it can't help anyone searching. Since the published tarball ships an internal opam file under the old name, I'd rather cut a correctly-named release than point a renamed entry at a mismatched tarball — so this lands as a second push shortly, replacing the rocq-robust-predicates.0.1.0 directory with rocq-robust-geometric-predicates.0.1.0 and a fresh URL + checksum. Flagging it now so the rename isn't a surprise.

JTS — I'd rather leave it out, if you're happy with that. The package is standalone Rocq with no JTS dependency, and someone installing it needs nothing about the Java libraries; homepage leads anyone curious to the corpus, where the connection is the whole point. Happy to add a provenance clause if you think it aids discoverability.

[grootstebozewolf]

Pushed — all three actionable comments are addressed, and the branch now holds exactly two files.

Renamed to rocq-robust-geometric-predicates. Rather than repoint the entry at the old tarball, I cut a fresh release so the artifact matches the package name: the tarball now ships rocq-robust-geometric-predicates.opam internally, not a stale one under the previous name. New URL and sha512 in the entry; the old rocq-robust-predicates.0.1.0 path is deleted, so no empty directory is left behind.

ocaml dropped from both packages, and maintainer is a person in both.

Re-verified against the new tarball, not a working tree: extracts and makes clean with no corpus present, opam lint Passed, and the published sha256 re-checked against the bytes the sha512 was computed from.

On JTS — I've left it out. Thinking it through, the link is provenance for the corpus rather than a fact about either package: neither ships JTS code nor depends on it, and someone installing a Rocq library shouldn't need to care which Java ecosystem prompted the proofs. homepage covers anyone curious. Happy to reconsider if you'd still prefer a line.

Thanks for the review — the ocaml catch in particular was a real unearned dependency I'd copied from a neighbouring package.