Plain MIT licence; publish binaries as releases - #1
Closed
TrevorHansen wants to merge 3 commits into
Closed
Conversation
STP's benchmark pages live in the manual, in stp/stp. The measurements behind them do not belong there: a full campaign is tens of megabytes of results, a 24 MB binary and a corpus index, several times a year, and none of it is source. Keeping it here means the source repo's history stays about the solver, and a new campaign reaches the website without a commit to STP. Both are project sites under stp.github.io, so the pages fetch this data same-origin. What is published beyond the JSON the site already read: the full per-run archive (every column the working store holds), the corpus index those runs are keyed to, each run's retained stdout, and the statically linked binary that produced the campaign, with its provenance. Together those make a campaign checkable rather than only viewable -- the SQLite working store stays local, because rewriting 90 MB of binary per campaign would bloat this history to no purpose when the same content exports as append-only text. Two rules bound what publishes. A campaign over an ad-hoc file list is an experiment rather than a result about STP, so only the standing tiers publish. A campaign whose binary was not archived cannot be re-run by anyone, so it does not publish either -- which excludes fast-001, the dynamically linked validation baseline. Fixes two faults in the harness that the reboot during full-001 exposed: - The output log is appended to as a gzip stream, one member per process, so a process killed mid-member left an unterminated stream with the resumed run's records after it. Every standard tool then stops at the seam: zcat reads 61,511 of full-001's 160,610 records, where walking the members recovers 154,519. Logs are now repaired before anything appends to them, and flushed on the same boundary as the database commit. - output_offset, which joins a run to its saved output, was a per-process counter that restarted at zero on resume. full-001 therefore has two records numbered 0..93007, and reclassify -- which builds a dict on that key -- would have paired runs with other runs' output. It now continues from the database, and the published log is keyed by benchmark path instead. Manifests become corpus-relative so the frozen fast tier can be published and still name the same benchmarks on another machine.
The initial commit copied STP's LICENSE verbatim, which brought with it the per-author copyright list and the inventory of components vendored into STP's source. Neither describes this repository: it holds measurements, a compiled binary and a harness, not STP's source, and the people listed did not write what is here.
A plain MIT file covers what is written here, but each published binary is a statically linked STP and carries the licences of everything STP is built from. Say so, and point at the list rather than copying it, so it cannot drift from the one in the source repository. Also corrects the publishing recipe, which still said to commit a campaign straight to master.
TrevorHansen
changed the title
TrevorHansen
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Three things, all consequences of the initial commit having been landed without review.
1. The licence. The initial commit copied STP's
LICENSEverbatim, which brought across the per-author copyright list and the inventory of third-party code vendored into STP's source. Neither describes this repository: it holds measurements, a harness and a compiled binary, not STP's source, and the people named did not write what is here. It is now a plain MIT withThe STP Projectas the holder.2. What that inventory was doing. Dropping it leaves something real unsaid, so the README says it instead: each published binary is a statically linked STP and embeds the code STP is built from, so redistributing it carries those licences whatever this repo's file says. The README points at
LICENSE_COMPONENTSrather than copying the list, so the two cannot drift. It also notes that the SAT backend is linked at build time and therefore is not in that list — which one a binary carries is in itsbinaries/<sha256>.json.3. Binaries move to releases. A binary is 24 MB and does not delta against the previous one, so one per campaign grows every clone without bound for a file most readers never fetch. They are now releases, one per distinct binary, tagged
binary-<first 12 of sha256>so two campaigns sharing a binary do not upload it twice. Release assets count against neither the repository size nor the site's 1 GB budget.What stays committed is the 2 KB of provenance saying which binary a campaign ran and where to fetch it.
check-published.pyverifies that provenance — file present,download_urlset, hash agreeing with the campaign — instead of the presence of a file, since a campaign naming a binary nobody can locate is not reproducible.The already-committed binary was removed from the history in the same change, while the repository is new enough that a rewrite costs nothing: master was force-pushed and the clone drops from 36 MB to 12 MB.
Also: the exports are deterministic now. gzip stamps the current time into every header, so re-exporting unchanged data rewrote several megabytes and a no-op publish looked like new results. Verified byte-identical across runs.
Checked
check-published.pypasses; the release asset downloads and hashes tob5198265…; publishing twice in a row produces an empty diff.