Skip to content

Releases: wcook04/plectis

v0.5.0

Choose a tag to compare

@wcook04 wcook04 released this 31 Jul 04:10
Immutable release. Only release title and notes can be modified.
9539695

Plectis 0.5.0 makes the public project substantially easier to inspect from a cold clone. It adds a compact coding-agent entry, a checked paper-corpus guide with source/PDF mirrors and hashes, and a public front-door contract; it also rewrites the README around the first runnable action and preserves claim ceilings across source, install, and standalone export.\n\nThe paired Lean companion is bound to public commit b028075c6fff596143db012d6f73912f2e30f731: 992 modules, 151,761 declarations, 149,812 theorem-like declarations, and 300 principal claim links.\n\nValidation: Python 3.11–3.13 CI, smoke/timing, CodeQL, local make ci (466 passed, 2 skipped), public-site parity, and exact live hashes for all 11 hosted papers.\n\nSee CHANGELOG.md for the full release notes.

v0.4.1

Choose a tag to compare

@wcook04 wcook04 released this 26 Jul 20:52
Immutable release. Only release title and notes can be modified.
afe3760

Patch release. v0.4.0 was cut one commit before the closeout audit stopped reporting an absent tool as a detected forgery, so the latest release shipped a behaviour main had already fixed.

Fixed

  • The closeout audit no longer reports an absent tool as a detected forgery. Its pytest lane shells out to pytest, which the advertised pip install . does not provide. On a plain install the lane found nothing to run and recorded the specimen as a planted-case detection. Absence and detection are now distinct outcomes, and the lane refuses rather than inventing a verdict.
  • The public site names the pip install .[test] precondition on the cold-rerun claim, so the advertised command's exit status matches what a reader following the page literally would see.

Verifying

The four-planted-case command needs the test extra:

pip install .[test]

A plain install leaves that lane nothing to run, and it will now say so instead of reporting a detection.

Full Changelog: v0.4.0...v0.4.1

v0.4.0

Choose a tag to compare

@wcook04 wcook04 released this 26 Jul 14:54
Immutable release. Only release title and notes can be modified.
1089de1

Plectis v0.4.0 makes a public open question inspectable before an expert answer is known.

  • plectis hypothesis-handoff validates and renders a source-linked declared gap, a tentative project prior, serious alternatives, outcome-to-hypothesis discriminators, and an exact expert request.
  • Every return names repository-relative landing targets and release checks; no expert answer changes claim status automatically.
  • The worked packet asks whether evaluator-selected cases would expose a different failure profile from the author-selected fixtures.
  • The public-system paper now explains why exposing a prior and update rule makes disagreement cheaper without turning that prior into evidence. Its searchable corpus and reader-facing 20-page PDF are refreshed.
  • The exact release commit passed 456 tests (2 skipped), source smoke, installed-package smoke, Python 3.11/3.12/3.13 CI, user smoke/timing, and CodeQL.

Full details are in CHANGELOG.md and HYPOTHESIS_HANDOFF.md.

v0.3.2

Choose a tag to compare

@wcook04 wcook04 released this 26 Jul 13:11
Immutable release. Only release title and notes can be modified.
45298a2

Plectis v0.3.2 restores the advertised command-line closeout-faithfulness audit.

  • The CLI now passes the semantic negative-case evaluator through to the audit kernel.
  • All four planted forgery cases are detected by name.
  • The dedicated regression suite is part of the normal public CI floor.
  • The clean release floor passes 433 tests (7 skipped), source smoke, package-install smoke, Python 3.11/3.12/3.13 CI, user smoke/timing, and CodeQL.

Full details are in CHANGELOG.md.

v0.3.1

Choose a tag to compare

@wcook04 wcook04 released this 20 Jul 17:55
Immutable release. Only release title and notes can be modified.
906544d

A patch release for two things a stranger would have hit.

A shallow clone stopped accusing the paper

git clone --depth 1 followed by make ci produced five failures naming worked-example, Lean-file-count and receipt-flow "drift". None of them mentioned the clone.

The public-system paper pins its evidence to a specific commit, and the checks read the repository as it stood there. A truncated clone does not contain that commit, so those comparisons ran against absent data — not against anything that had actually changed. The honest reading of the output was "the paper's numbers are wrong", which was false.

The history dependency is kept deliberately. The paper makes claims about a particular past commit; re-deriving them from a receipt that same commit produced would only check that file against itself. What changed is that absence is now reported as absence — the checker names the shallow clone and the fetch that resolves it, and the checks needing the pinned commit skip with that reason instead of failing as drift.

clone before after
--depth 1 5 failed 5 skipped, 0 failed
full passing unchanged, 0 skipped

One publication owner for the site

.github/workflows/pages.yml is deleted. GitHub Pages serves this site from the gh-pages branch builder; that workflow checked out the same branch and deployed the same tree again as an artifact to the same environment, so which one won depended on which ran last.

It had already taken the published site down once — an earlier version copied a hardcoded list of files, and all three papers plus .well-known/security.txt returned 404 until it was switched off. It was disabled rather than deleted, which left the second owner one toggle away. A test now asserts no workflow deploys Pages while the branch builder owns publication.

Verification

  • make ci green on a fresh full clone of main; CI green on Python 3.11 / 3.12 / 3.13, plus CodeQL and the smoke job
  • --depth 1 clone: 5 skips, 0 failures
  • live site checked after the change: /, /.well-known/security.txt and all three papers return 200, Pages still build_type: legacy from gh-pages

On v0.3.0

v0.3.0 is unchanged and stays exactly as published. Immutable releases were enabled on this repository after it was cut, and enabling them is not retroactive — the API still reports immutable: false for it. So an immutable release could only be a new one, and this is it. No previously published artifact was moved, rewritten, or deleted.

v0.3.0

Choose a tag to compare

@wcook04 wcook04 released this 20 Jul 02:54
69e1b5a

The declared version had been 0.2.0 since 11 July while main moved 105 commits past that tag, and the v0.2.0 tag was never given a release — so the newest release anyone could see was v0.1.0 from 25 June. This release makes the version name the tree again.

What is in it

Everything merged since v0.2.0 (2026-07-11). The bulk of it is the public-system paper, which went through its sixth, seventh, eighth and ninth passes: grounding borrowed claims in primary sources, stating the contribution as a claim–evidence–limit contract rather than a ladder, placing that contract beside assurance cases and CAE notation, and bounding what it says about correctness, authorship and record repair. Alongside that: the served page is called Plectis rather than the project's former name, the README opens on the one-system-two-demonstrations frame, and CI was repaired and made considerably faster.

The full list is in CHANGELOG.md.

Verification

make ci on a fresh unauthenticated clone of this tag: 426 passed, 2 skipped. The package smoke reports version: plectis 0.3.0 on both the served and packaged paths.

What this is not

A hosted product, and not the private system. Plectis is the runnable public slice — real components packaged so you can run them locally and check what each one claims. Authority ceilings are explicit and the gates fail closed.

Plectis v0.1.0

Choose a tag to compare

@wcook04 wcook04 released this 25 Jun 17:17

Plectis v0.1.0 binds the public clone/run path to CI-backed onboarding evidence.\n\nValidation:\n- CI run 28187654563 passed on Python 3.11, 3.12, and 3.13.\n- The user-smoke/timing job passed and uploaded the onboarding benchmark artifact.\n- Fresh public clone benchmark for b76fa19: clone 2.452s, bootstrap 0.878s, smoke 2.899s, install 14.815s, installed tour 1.257s, total 22.591s.\n\nSupported first-user path: Python 3.11+ with a POSIX shell, ./bootstrap.sh, then make smoke. Windows users should use WSL until native Windows CI exists.