humuhumu33 · Oct 23, 2026 · Oct 23, 2026 · Oct 23, 2026 · Oct 23, 2026 · Oct 23, 2026
diff --git a/.github/crate-publication.sh b/.github/crate-publication.sh
@@ -0,0 +1,164 @@
+#!/usr/bin/env bash
+# The decisions of publishing the lexlean crate to crates.io (RP-18, #260), kept
+# in one script so that each can be run against planted inputs. release.yml
+# calls it; nothing here uploads, and nothing here reads or prints a token.
+#
+#   crate-publication.sh identity RELEASE_DIR PACKAGED
+#       PACKAGED, the crate `cargo publish` would upload, must have the SHA-256
+#       of RELEASE_DIR/lexlean.crate and the SHA-256 that RELEASE_DIR/checksums.txt
+#       lists for it. Prints the digest.
+#   crate-publication.sh metadata PACKAGED...
+#       What crates.io needs from an archive: description, license, repository,
+#       a readme the archive carries, and at most 10 MiB.
+#   crate-publication.sh mode
+#       How the upload is authorised, from HAS_CARGO_REGISTRY_TOKEN and
+#       TRUSTED_PUBLISHING (each `true` or anything else): token, trusted, or none.
+#   crate-publication.sh prerelease REF COUNT
+#       The version of a commit of a release line: `release/v0.4` and a count of
+#       first-parent commits give `0.4.0-dev.<count>`.
+#   crate-publication.sh stamp VERSION [ROOT]
+#       Rewrite the workspace version, and the version of the workspace's own
+#       crates, in ROOT/Cargo.toml (a throwaway checkout, never a commit).
+set -euo pipefail
+
+fail() {
+    printf '%s\n' "$1" >&2
+    exit 1
+}
+
+digest() {
+    sha256sum "$1" | cut -d' ' -f1
+}
+
+# The tag a pre-release names must be a SemVer pre-release of a release line.
+semver_prerelease='^[0-9]+\.[0-9]+\.[0-9]+-dev\.[0-9]+$'
+semver_release='^[0-9]+\.[0-9]+\.[0-9]+$'
+
+identity() {
+    release=$1 packaged=$2
+    [[ -f "$release/lexlean.crate" ]] || fail "identity: $release/lexlean.crate is missing"
+    [[ -f "$release/checksums.txt" ]] || fail "identity: $release/checksums.txt is missing"
+    [[ -f "$packaged" ]] || fail "identity: $packaged is missing"
+    actual=$(digest "$packaged")
+    staged=$(digest "$release/lexlean.crate")
+    [[ "$actual" == "$staged" ]] ||
+        fail "identity: cargo would upload $actual, and the release attaches lexlean.crate $staged"
+    listed=$(sed -n 's/^\([0-9a-f]\{64\}\)  lexlean\.crate$/\1/p' "$release/checksums.txt")
+    [[ -n "$listed" ]] || fail "identity: checksums.txt lists no lexlean.crate"
+    [[ "$(printf '%s\n' "$listed" | wc -l)" -eq 1 ]] || fail "identity: checksums.txt lists lexlean.crate twice"
+    [[ "$listed" == "$actual" ]] ||
+        fail "identity: cargo would upload $actual, and checksums.txt lists $listed for lexlean.crate"
+    printf '%s\n' "$actual"
+}
+
+metadata() {
+    limit=10485760
+    status=0
+    for archive in "$@"; do
+        if [[ ! -f "$archive" ]]; then
+            printf '%s: no such archive\n' "$archive" >&2
+            status=1
+            continue
+        fi
+        size=$(wc -c < "$archive" | tr -d ' ')
+        if ((size > limit)); then
+            printf '%s: %s bytes exceeds the crates.io limit of %s\n' "$archive" "$size" "$limit" >&2
+            status=1
+        fi
+        manifest=$(tar -xzOf "$archive" --wildcards '*/Cargo.toml' 2>/dev/null || true)
+        if [[ -z "$manifest" ]]; then
+            printf '%s: no Cargo.toml in the archive\n' "$archive" >&2
+            status=1
+            continue
+        fi
+        package=$(printf '%s\n' "$manifest" | sed -n '/^\[package\]/,/^\[/p')
+        field() {
+            printf '%s\n' "$package" | sed -n "s/^$1 = \"\\(.*\\)\"\$/\\1/p" | head -1
+        }
+        for required in description repository; do
+            if [[ -z "$(field "$required")" ]]; then
+                printf '%s: Cargo.toml has no `%s`\n' "$archive" "$required" >&2
+                status=1
+            fi
+        done
+        if [[ -z "$(field license)" && -z "$(field license-file)" ]]; then
+            printf '%s: Cargo.toml has neither `license` nor `license-file`\n' "$archive" >&2
+            status=1
+        fi
+        readme=$(field readme)
+        # The listing is read whole: `grep -q` leaves a pipe early, and pipefail
+        # would then call a present readme missing.
+        listing=$(tar -tzf "$archive")
+        if [[ -n "$readme" ]] && ! grep -q -- "/$readme\$" <<<"$listing"; then
+            printf '%s: `readme = "%s"` names a file the archive does not carry\n' "$archive" "$readme" >&2
+            status=1
+        fi
+    done
+    return "$status"
+}
+
+mode() {
+    if [[ "${HAS_CARGO_REGISTRY_TOKEN:-}" == true ]]; then
+        echo token
+    elif [[ "${TRUSTED_PUBLISHING:-}" == true ]]; then
+        echo trusted
+    else
+        echo none
+    fi
+}
+
+prerelease() {
+    ref=$1 count=$2
+    [[ "$ref" =~ ^release/v([0-9]+)\.([0-9]+)$ ]] ||
+        fail "prerelease: $ref is not a release line (release/vX.Y)"
+    major=${BASH_REMATCH[1]} minor=${BASH_REMATCH[2]}
+    [[ "$count" =~ ^[0-9]+$ ]] || fail "prerelease: the commit count $count is not a number"
+    printf '%s.%s.0-dev.%s\n' "$major" "$minor" "$count"
+}
+
+stamp() {
+    version=$1 root=${2:-.}
+    [[ "$version" =~ $semver_prerelease || "$version" =~ $semver_release ]] ||
+        fail "stamp: $version is not a SemVer version"
+    manifest=$root/Cargo.toml
+    current=$(sed -n '/^\[workspace\.package\]/,/^\[/s/^version = "\(.*\)"$/\1/p' "$manifest" | head -1)
+    [[ -n "$current" ]] || fail "stamp: $manifest has no workspace version"
+    escaped=${current//./\\.}
+    sed -i \
+        -e "/^\\[workspace\\.package\\]/,/^\\[/s/^version = \"$escaped\"\$/version = \"$version\"/" \
+        -e "s/^\\(repo-model\\|repo-conformance\\|lexlean\\) = { version = \"$escaped\", path/\\1 = { version = \"$version\", path/" \
+        "$manifest"
+    # The workspace version and its three crates, and nothing at the old version.
+    stamped=$(grep -c "version = \"$version\"" "$manifest" || true)
+    [[ "$stamped" -eq 4 ]] || fail "stamp: expected 4 versions at $version in $manifest, found $stamped"
+    printf '%s\n' "$current"
+}
+
+# The checkout the crate is packaged from. For a pre-release it is a throwaway
+# copy of a release line at one commit: the commit count and the line name give
+# the version, and the stamped manifest and lock are never committed.
+prepare() {
+    pre=$1
+    if [[ "$pre" == true ]]; then
+        [[ "$(git rev-parse --is-shallow-repository)" == false ]] ||
+            fail "prepare: the commit count needs the whole history (fetch-depth: 0)"
+        version=$(prerelease "${GITHUB_REF_NAME:?prepare: GITHUB_REF_NAME names the release line}" \
+            "$(git rev-list --first-parent --count HEAD)")
+        stamp "$version" . > /dev/null
+        cargo update --workspace --quiet
+        printf '%s\n' "$version"
+    else
+        sed -n '/^\[workspace\.package\]/,/^\[/s/^version = "\(.*\)"$/\1/p' Cargo.toml | head -1
+    fi
+}
+
+command=${1:-}
+case "$command" in
+    prepare) [[ $# -eq 2 ]] || fail "usage: $0 prepare true|false"; prepare "$2" ;;
+    identity) [[ $# -eq 3 ]] || fail "usage: $0 identity RELEASE_DIR PACKAGED"; identity "$2" "$3" ;;
+    metadata) [[ $# -ge 2 ]] || fail "usage: $0 metadata PACKAGED..."; shift; metadata "$@" ;;
+    mode) [[ $# -eq 1 ]] || fail "usage: $0 mode"; mode ;;
+    prerelease) [[ $# -eq 3 ]] || fail "usage: $0 prerelease REF COUNT"; prerelease "$2" "$3" ;;
+    stamp) [[ $# -ge 2 && $# -le 3 ]] || fail "usage: $0 stamp VERSION [ROOT]"; stamp "$2" "${3:-.}" ;;
+    *) fail "usage: $0 identity|metadata|mode|prerelease|stamp ..." ;;
+esac
diff --git a/.github/workflows/crate.yml b/.github/workflows/crate.yml
@@ -0,0 +1,165 @@
+# The lexlean crate on crates.io (#260): what must hold before anyone uploads it,
+# and the upload of a development pre-release of a release line.
+#
+# `release.yml` calls this workflow for every run, so a rehearsal and a tag both
+# prove the crate: it packages twice to the same bytes, the bytes `cargo publish
+# --dry-run` would send are those bytes, they meet what crates.io needs from an
+# archive, and they are the `lexlean.crate` that `cargo xtask release-artifacts`
+# attaches, with the SHA-256 its `checksums.txt` lists. A tag's upload is the
+# `publish` job of release.yml.
+#
+# Dispatched on a release line (`release/vX.Y`) with `prerelease`, it does the
+# same for `X.Y.0-dev.<n>`, n being the number of first-parent commits of the
+# line at the dispatched commit, and uploads that version when a credential
+# exists. The upload needs a `CARGO_REGISTRY_TOKEN` secret in the crates.io
+# environment, or the repository variable CRATES_IO_TRUSTED_PUBLISHING set to
+# `true` once the owner has configured trusted publishing for the crate. With
+# neither, nothing is uploaded and the run says so. The first upload of a name
+# is the owner's: trusted publishing cannot be configured for a crate that does
+# not exist.
+name: crate
+
+on:
+  workflow_call:
+    inputs:
+      prerelease:
+        description: Package a development pre-release of the release line instead of the workspace version
+        type: boolean
+        default: false
+    outputs:
+      sha256:
+        description: The SHA-256 of the crate every check agreed on
+        value: ${{ jobs.readiness.outputs.sha256 }}
+      version:
+        description: The crate version
+        value: ${{ jobs.readiness.outputs.version }}
+  workflow_dispatch:
+    inputs:
+      prerelease:
+        description: Package, and upload when authorised, X.Y.0-dev.<n> of the release line this is dispatched on
+        type: boolean
+        default: true
+
+permissions:
+  contents: read
+
+env:
+  CARGO_TERM_COLOR: never
+
+jobs:
+  readiness:
+    name: crate readiness
+    runs-on: ubuntu-24.04
+    timeout-minutes: 90
+    outputs:
+      sha256: ${{ steps.prove.outputs.sha256 }}
+      version: ${{ steps.prove.outputs.version }}
+    steps:
+      # The whole history: a pre-release is named by its commit count.
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          fetch-depth: 0
+      - name: Install the pinned Rust toolchain
+        run: rustup toolchain install
+      - id: prove
+        shell: bash
+        env:
+          PRERELEASE: ${{ inputs.prerelease }}
+        run: |
+          set -euo pipefail
+          version="$(.github/crate-publication.sh prepare "$PRERELEASE")"
+          a="${RUNNER_TEMP}/package-a" b="${RUNNER_TEMP}/package-b" dry="${RUNNER_TEMP}/dry"
+          crate="lexlean-${version}.crate"
+          # A pre-release is packaged from a stamped copy of the commit, which
+          # cargo calls dirty; the crate records the commit it was cut from
+          # and that it was stamped (`.cargo_vcs_info.json`).
+          dirty=()
+          if [ "$PRERELEASE" = true ]; then dirty=(--allow-dirty); fi
+          cargo package --locked "${dirty[@]}" --package lexlean --target-dir "$a"
+          cargo package --locked --no-verify "${dirty[@]}" --package lexlean --target-dir "$b"
+          cmp "$a/package/$crate" "$b/package/$crate"
+          cargo publish --dry-run --locked "${dirty[@]}" --package lexlean --target-dir "$dry"
+          cmp "$a/package/$crate" "$dry/package/$crate"
+          .github/crate-publication.sh metadata "$dry/package/$crate"
+          if [ "$PRERELEASE" = true ]; then
+            sha256="$(sha256sum "$dry/package/$crate" | cut -d' ' -f1)"
+            agreed="three packagings of the same commit"
+          else
+            # The crate the release attaches and the checksum it lists for it.
+            cargo xtask release-artifacts
+            sha256="$(.github/crate-publication.sh identity release "$dry/package/$crate")"
+            agreed="the crate release-artifacts attaches and the checksum checksums.txt lists"
+          fi
+          echo "sha256=$sha256" >> "$GITHUB_OUTPUT"
+          echo "version=$version" >> "$GITHUB_OUTPUT"
+          {
+            echo "## lexlean ${version}"
+            echo
+            echo "Packaged, dry-run, and checked against crates.io's metadata; ${agreed} agree:"
+            echo
+            echo '```text'
+            echo "${sha256}  ${crate}"
+            echo '```'
+          } >> "$GITHUB_STEP_SUMMARY"
+
+  prerelease:
+    name: upload the development pre-release
+    needs: readiness
+    # Only a dispatch uploads from here; a call from release.yml proves the
+    # crate and uploads nothing.
+    if: ${{ github.event_name == 'workflow_dispatch' && inputs.prerelease }}
+    runs-on: ubuntu-24.04
+    timeout-minutes: 45
+    environment: crates.io
+    env:
+      HAS_CARGO_REGISTRY_TOKEN: ${{ secrets.CARGO_REGISTRY_TOKEN != '' }}
+      TRUSTED_PUBLISHING: ${{ vars.CRATES_IO_TRUSTED_PUBLISHING == 'true' }}
+    permissions:
+      contents: read
+      id-token: write
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          fetch-depth: 0
+      - name: Install the pinned Rust toolchain
+        run: rustup toolchain install
+      - name: Decide how the upload is authorised
+        id: upload
+        shell: bash
+        run: echo "mode=$(.github/crate-publication.sh mode)" >> "$GITHUB_OUTPUT"
+      - name: Acquire crates.io trusted-publisher token
+        if: ${{ steps.upload.outputs.mode == 'trusted' }}
+        uses: rust-lang/crates-io-auth-action@c6f97d42243bad5fab37ca0427f495c86d5b1a18
+        id: crates-auth
+      - name: No upload credential
+        if: ${{ steps.upload.outputs.mode == 'none' }}
+        env:
+          VERSION: ${{ needs.readiness.outputs.version }}
+          CRATE_SHA256: ${{ needs.readiness.outputs.sha256 }}
+        run: echo "::notice::lexlean ${VERSION} (sha256 ${CRATE_SHA256}) was packaged and dry-run; no CARGO_REGISTRY_TOKEN and no trusted publishing, so nothing was uploaded"
+      - name: Upload the exact checked crate
+        if: ${{ steps.upload.outputs.mode != 'none' }}
+        env:
+          CARGO_REGISTRY_TOKEN: ${{ secrets.CARGO_REGISTRY_TOKEN || steps.crates-auth.outputs.token }}
+          VERSION: ${{ needs.readiness.outputs.version }}
+          CRATE_SHA256: ${{ needs.readiness.outputs.sha256 }}
+        shell: bash
+        run: |
+          set -euo pipefail
+          [ "$(.github/crate-publication.sh prepare true)" = "$VERSION" ]
+          cargo package --locked --no-verify --allow-dirty --package lexlean --target-dir "${RUNNER_TEMP}/upload"
+          test "$(sha256sum "${RUNNER_TEMP}/upload/package/lexlean-${VERSION}.crate" | cut -d' ' -f1)" = "$CRATE_SHA256"
+          cargo publish --locked --allow-dirty --package lexlean --target-dir "${RUNNER_TEMP}/upload"
+          for attempt in $(seq 1 30); do
+            printf 'checking crates.io visibility (attempt %s/30)\n' "$attempt"
+            if curl --fail --location --silent --show-error \
+                "https://crates.io/api/v1/crates/lexlean/${VERSION}/download" \
+                --output "${RUNNER_TEMP}/lexlean-public.crate"; then
+              test "$(sha256sum "${RUNNER_TEMP}/lexlean-public.crate" | cut -d' ' -f1)" = "$CRATE_SHA256"
+              echo "lexlean ${VERSION} is on crates.io with sha256 ${CRATE_SHA256}"
+              exit 0
+            fi
+            sleep 2
+          done
+          echo "::error::lexlean ${VERSION} did not become publicly downloadable" >&2
+          exit 1