Skip to content

Releases

shifted-docs: documentation release of 27 October 2026

shifted-docs: documentation release of 27 October 2026 Latest
Latest

Choose a tag to compare

View all tags
@mlelarge mlelarge released this 27 Oct 10:37
shifted-docs
efe7d9a

The documentation release of ellipsoid_fitting_rocq, of 27 October 2026.

  • Tag: shifted-docs
  • Commit: efe7d9a

The release

The Rocq sources of this release are those of the mathematical release
shifted, commit 305747a of 24 October 2026,
but for one header comment. No Rocq statement, definition or proof has changed
since shifted. The changes since then are of four kinds, and CHANGELOG.md
lists them.

  • Documentation: a short README.md and AGENTS.md, CHANGELOG.md,
    doc/README.md, the former README as doc/details.md, the agents' rules as
    doc/history/agent-rules.md, updates to doc/shifted-gaussian.tex,
    doc/formal_proof.tex, doc/paper_correspondence.md and the READMEs of
    library/, extension/ and applications/, and the deletion of .mcp.json.
  • License and citation metadata: LICENSE, NOTICE and CITATION.cff.
  • The metadata fields of rocq-ellipsoid-fitting.opam, whose depends and
    build fields do not change, and .gitignore.
  • One header comment, in extension/Shifted/SparseDimensions.v.

How it was checked

make check last passed on 25 October 2026, at 5893184 (run
d8bb8f380183817de780a550701eabc6), in the pinned Docker image
ellipsoid-rocq:2026-10-01, which is not public. The later commits change only
documentation and metadata, whose content the checker does not read. In a
clone with its full history, at the commit of this release,
python3 -I -B scripts/check_sources.py --before-build reports that the sources
follow the rules of scripts/check_sources.py, and
cffconvert --validate -i CITATION.cff passes.

What it adds for a reader

  • README.md: a short overview of the results, the statement files to trust,
    and how to build and check.
  • AGENTS.md: the guide for contributors and AI agents, which says how a
    change is checked.
  • CHANGELOG.md: the tagged versions, newest first.
  • doc/README.md: an index of doc/, with the terms used in the comments and
    records.
  • doc/details.md: the former long README, kept as a record.
  • doc/history/agent-rules.md: the rules given to the AI agents who worked on
    the repository.
  • LICENSE and NOTICE: the MIT license, for the code and the documents.
  • CITATION.cff: how to cite this repository.

The website, https://llm4rocq.github.io/ellipsoid-fitting-web/, has its own
repository, LLM4Rocq/ellipsoid-fitting-web. It presents the results, a guide
to the library GaussianAnalysis with a dated phase 12 browser, how the proofs
were made and PDFs of the notes. README.md links to it, and the field url
of CITATION.cff gives its address.

The PDF

shifted-gaussian-ellipsoid-fitting.pdf is the note Centered ellipsoid
fitting for non-centered Gaussian data, the informal proof of the seven
theorems on translated samples, S1 to S7. It is built from
doc/shifted-gaussian.tex, with doc/statements.bib, at commit
efe7d9a. Its title page gives 16 October
2026, the date of the commit that added the note. Its text includes the two
later changes of 25 October 2026, commits 0682ed2 and 15d9fb2, which
CHANGELOG.md describes.

  • SHA-256: 71e3f493718129e891263f1fd31930bf6e313a936bd274755f00292c3c37e258
  • Size: 435279 bytes
  • Pages: 20

It was built with TeX Live 2024 (pdfTeX 1.40.26, LaTeX2e 2023-11-01 patch
level 1, L3 programming layer 2024-02-20, hyperref 7.01h), with Latexmk 4.83
and BibTeX 0.99d. On that installation, these commands rebuild the same file,
as doc/shifted-gaussian.pdf:

git clone https://github.com/LLM4Rocq/ellipsoid_fitting_rocq.git
cd ellipsoid_fitting_rocq
git checkout --detach shifted-docs
cd doc
SOURCE_DATE_EPOCH=$(git log -1 --format=%ct) FORCE_SOURCE_DATE=1 latexmk -pdf -interaction=nonstopmode -halt-on-error shifted-gaussian.tex
shasum -a 256 shifted-gaussian.pdf

SOURCE_DATE_EPOCH is then the commit time of the release's commit,
1793082181 (2026-10-27 06:23:01 UTC). Another TeX installation, even of
TeX Live 2024, may give a PDF with other bytes.

How to cite

Cite the repository with CITATION.cff. To cite a formal result, give its
declaration, its file and the commit 305747a
of the tag shifted: for example, condition_kappa_theorem in
extension/ConditionKappaTheorem.v.

License

The code and the documents are under the MIT license, in LICENSE. NOTICE
gives the scope of the license, the inherited notice and a note on the OpenAI
math collection.

Assets 3
Loading