Skip to content

dev/releases: Document automatic mirroring of releases - #6476

Merged
fingolfin merged 1 commit into
masterfrom
mh/document-files-mirror
Aug 2, 2026
Merged

dev/releases: Document automatic mirroring of releases#6476
fingolfin merged 1 commit into
masterfrom
mh/document-files-mirror

Conversation

@fingolfin

Copy link
Copy Markdown
Member

The last two manual steps of a release — copying the archives to
https://files.gap-system.org and building the manuals for
https://docs.gap-system.org — were done over SSH and were easy to forget. Both
hosts now poll GitHub hourly and pick up any release they do not have yet, so
neither needs a step in this guide any more.

This drops those steps from both the quick and the detailed guide, and instead
documents how to check on the two jobs, how to trigger them early, and the fact
that both deliberately ignore pre-releases: nothing appears until the release has
been switched from "pre-release" to "latest release". The scripts that used to do
this by hand, download_release.sh and download_manuals.sh, remain on the
respective hosts as a fallback and are mentioned as such.

The automation lives in:

Important

Please do not merge this before gap-system/GapWWW#416 is merged and its
timer has been enabled on the docs host. The files.gap-system.org half is
already live, but until then this would describe manual building as automatic.

AI disclosure: prepared with Claude Code, which drafted this change and this
description; reviewed by the pull request author.

Copying the release archives to files.gap-system.org and building
the manuals for docs.gap-system.org used to be the last two manual
steps of a release, done over SSH and easy to forget. Both hosts now
poll GitHub hourly and pick up any release they do not yet have, so
neither needs a step in this guide any more.

Describe how to check on them and how to trigger them early, and
note that they deliberately ignore pre-releases, so nothing appears
until the release is marked as the latest one. The scripts that used
to do this by hand remain on the respective hosts as a fallback.

AI disclosure: prepared with Claude Code, which drafted this change
and its commit message; reviewed by the commit author.

Co-authored-by: Claude <noreply@anthropic.com>
@codecov

codecov Bot commented Jul 31, 2026

Copy link
Copy Markdown

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 79.04%. Comparing base (8215f5d) to head (62789df).

Additional details and impacted files
@@            Coverage Diff             @@
##           master    #6476      +/-   ##
==========================================
- Coverage   79.04%   79.04%   -0.01%     
==========================================
  Files         685      685              
  Lines      293710   293710              
  Branches     8664     8664              
==========================================
- Hits       232169   232167       -2     
- Misses      59740    59743       +3     
+ Partials     1801     1800       -1     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
  • 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

@fingolfin

Copy link
Copy Markdown
Member Author

The dependency is satisfied: gap-system/GapWWW#416 is merged, and the timer is now enabled and verified on the docs host — a run through systemd reports Result=success and correctly finds nothing to build, since all 10 installed releases are up to date. Both hosts are therefore live, so this is ready to merge.

@fingolfin fingolfin added topic: documentation Issues and PRs related to documentation release notes: not needed PRs introducing changes that are wholly irrelevant to the release notes topic: infrastructure labels Jul 31, 2026

@ruthhoffmann ruthhoffmann left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me! Glad to see that the last manual steps are now gone too.

Can’t spot any typos.

@ThomasBreuer ThomasBreuer left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good.

What I do not understand:
Where is a description which files are available at files.gap-system.org,
and who (except GAP.jl) knows about these files and uses them?
The download links on the GAP webpages point to github.com for GAP itself, and to the URLs listed in the PackageInfo.g files for individual packages.

@fingolfin

Copy link
Copy Markdown
Member Author

Looks good.

What I do not understand: Where is a description which files are available at files.gap-system.org, and who (except GAP.jl) knows about these files and uses them? The download links on the GAP webpages point to github.com for GAP itself, and to the URLs listed in the PackageInfo.g files for individual packages.

That's a very good question. It used to be that files.gap-system.org (or rather, its predecessor, which IIRC was a path under www.gap-system.org was browsable, so a user could go there and navigate around to find stuff. But we had to disable this, because site scrapers were generating many GB of traffic per day (and that was several years ago, before the AI bot scraper apocalypse). I don't think we can afford making it browsable again.

The existing structure was kinda "grandfathered in".

So, I think this is indeed something missing, and we should document this somewhere.

Note that from my POV, the main motivation to keep this around (at least initially) was to have a backup of everything: i.e. while it's good to have GitHub do the hosting for us (they use a CDN, meaning faster download speeds, and usually better reliability), if there is a catastrophic outage, we should not have all our eggs in one basket. But we initially deliberately stopped mirroring packages there when we rewrote the PackageDistro in 2022. That only came back later, and I must admit I forgot the details; perhaps it was indeed for GAP.jl? Regardless, thanks to AI, I decided it is easy enough to restore this service, so now I did.

@fingolfin

Copy link
Copy Markdown
Member Author

https://files.gap-system.org now shows some information about the mirroring. This file is also in the https://github.com/gap-system/gap-files repository

@fingolfin
fingolfin merged commit 69b8ef5 into master Aug 2, 2026
33 checks passed
@fingolfin
fingolfin deleted the mh/document-files-mirror branch August 2, 2026 14:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

release notes: not needed PRs introducing changes that are wholly irrelevant to the release notes topic: documentation Issues and PRs related to documentation topic: infrastructure

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants