[humuhumu33]

Part of #260; the first upload is the owner's. Builds on the offer on #34 (comment, item 3, crates.io): release.yml no longer fails after the tag is pushed because no lexlean crate exists, and the crate is proved before anyone uploads it.

Based on release/v0.4, the line #34 releases from and the target of the v0.4 milestone. Nothing is uploaded and no tag or release is created. lexlean is free on crates.io (checked 2026-10-23).

What changes

• crate.yml, called by release.yml on every run (a rehearsal included): packages lexlean twice to the same bytes, runs cargo publish --dry-run, checks the archive against what crates.io needs (description, license, repository, the readme it names, at most 10 MiB), runs cargo xtask release-artifacts, and requires the SHA-256 of the package to equal release/lexlean.crate and the line checksums.txt lists for it. All of crates/lexlean's metadata was already there; nothing in the manifests changed. The package is 5.0 MiB compressed.
• release.yml publish repeats the comparison against its own dry-run package, then decides how the upload is authorised: a CARGO_REGISTRY_TOKEN secret in the crates.io environment (the owner's first upload), trusted publishing once the repository variable CRATES_IO_TRUSTED_PUBLISHING is true, or neither. With neither it creates the GitHub release and says the crate was not uploaded.
• Pre-releases. Dispatching crate.yml on release/vX.Y packages X.Y.0-dev.N from a stamped throwaway copy, N being the commit's number of first-parent commits, and uploads it under the same authority. Proposal, not policy: it sorts below the release, is the same in every clone, and is pinned with =. Build metadata would not pin, because cargo ignores it when matching a requirement; the commit is in .cargo_vcs_info.json inside the crate.
• RP-18 (register 449): row, SPEC.md §31 and a §30.3 paragraph, scenario, and conformance_rp_18. The case reads both workflows and plants nine changes in release.yml and eight in crate.yml, and runs .github/crate-publication.sh against planted archives, checksums, refs and environments. RP-17 is [0.5.0] #113: release identity, §2.3 completion release 0.5.0 and §30 for languages 1.0-1.2 (RP-17, CL-18) #288 on release/v0.5, so this row takes RP-18 and the forward merge needs no renumbering; SPEC.md here is edited directly, and the forward merge will need the same paragraph and row in spec/src. The skeleton commit is first and fails (.github/workflows/crate.yml: No such file or directory).

The owner's part

Set the token for one run of one workflow (gh secret set CARGO_REGISTRY_TOKEN --env crates.io --repo UOR-Foundation/LexLean), then:

gh workflow run crate.yml --repo UOR-Foundation/LexLean --ref release/v0.4

That uploads 0.4.0-dev.N for the head of release/v0.4 after the checks above. A tag does the same for lexlean 0.4.0 once the version bump of #34 lands. After the first upload, configure trusted publishing for the crate, set CRATES_IO_TRUSTED_PUBLISHING, and delete the token.

Evidence

On this branch, WSL Ubuntu, Rust 1.97.1: conformance_rp_18, the bdd meta-gate, validate-model, validate-spec-links, check-test-inventory, cargo fmt --check and clippy -D warnings pass. The pre-release path was rehearsed on a throwaway worktree: 0.4.0-dev.243 packaged twice to identical bytes, cargo publish --dry-run ended with "aborting upload due to dry run", the metadata check passed, and .cargo_vcs_info.json named the commit. Planted defects and what each produced are in VERIFICATION.md.

Not done or not verified

The workflows have never run on GitHub, so crate.yml as a called workflow and the --allow-dirty pre-release packaging are read and rehearsed locally, not run as jobs; the first dispatch is the test. just vv was not run in full (the examples and Atlas legs need Lean and hours); the slices above are the ones this change can move. The version bump of #34 is not part of this PR.

🤖 Generated with Claude Code