diff --git a/.limen/aqua-registry.yaml b/.limen/aqua-registry.yaml index 81494b2..59dbc17 100644 --- a/.limen/aqua-registry.yaml +++ b/.limen/aqua-registry.yaml @@ -72,3 +72,26 @@ packages: - darwin/arm64 - linux - windows + # Quint (quint.sh): executable formal specifications, the model language of + # the spec-driven testing experiment (traces in ITF, replayed against the + # implementation). Upstream ships one bare Node-bundled binary per platform, + # with no checksums, signatures, or attestations: sourcing-ladder rung 1 on + # trust-on-first-use — aqua pins the checksum on first fetch. No + # windows/arm64 asset upstream. The repo also tags `evaluator/vX.Y.Z` + # releases (the Rust simulator that `quint run` downloads at run time into + # $QUINT_HOME unless told `--backend=typescript`); they are a different + # artifact and are filtered out of version resolution here. + - type: github_release + repo_owner: quint-co + repo_name: quint + description: Executable formal specifications (TLA+ semantics, ITF traces) + asset: quint-{{.OS}}-{{.Arch}} + format: raw + replacements: + darwin: macos + windows: pc + version_filter: not (Version startsWith "evaluator/") + supported_envs: + - darwin + - linux + - windows/amd64 diff --git a/.limen/just/lib.just b/.limen/just/lib.just index 1741ee9..08281ba 100644 --- a/.limen/just/lib.just +++ b/.limen/just/lib.just @@ -44,25 +44,28 @@ _per-platform +cmd: done fi +# The native build of one tools/go.mod tool into build/tools/, shared by +# _go-tool and the tools recipes (`{{ go_tool_build }} `). GOOS/GOARCH +# cleared: a per-platform leg would cross-compile the tool itself (exec format +# error). Directory form of -o: go names the binary itself, which on windows +# means the .exe suffix the loader needs — git-bash then resolves the bare +# build/tools/ the recipes call to it. (go strips a /vN major suffix +# when naming, so github.com/google/go-licenses/v2 lands as go-licenses.) +# -o is resolved relative to -C. +go_tool_build := "mkdir -p build/tools && GOOS='' GOARCH='' go -C tools build -o '../build/tools/'" + # Every Go-built tool the recipes run — the Go-source analyzers and the rest # alike — is a `tool` directive in tools/go.mod, a module of its own, built # natively ONCE into build/tools/ by the pinned go (book/tooling.md, "Go-built -# tools are go.mod tools"). Never `go tool ` from a per-platform leg: it -# honours GOOS/GOARCH and would cross-compile the tool itself (exec format -# error). A tools/go.mod without the directive fails with the command to add -# it. Recipes depend on this with the tool's name and package, then call +# tools are go.mod tools"). Never `go tool ` from a per-platform leg. +# A tools/go.mod without the directive fails with the recipe that adds it. +# Recipes depend on this with the tool's name and package, then call # build/tools/. _go-tool name pkg: #!/usr/bin/env bash set -euo pipefail if ! grep -qE '^(tool[[:space:]]+)?[[:space:]]*{{ pkg }}([[:space:]]|$)' tools/go.mod 2>/dev/null; then - echo "tools/go.mod lacks 'tool {{ pkg }}' — add it: go -C tools get -tool {{ pkg }}@ && go -C tools mod tidy (see book/tooling.md)" >&2 + echo "tools/go.mod lacks 'tool {{ pkg }}' — add it: just do tools add {{ pkg }} (see book/tooling.md)" >&2 exit 1 fi - mkdir -p build/tools - # Directory form of -o: go names the binary itself, which on windows means - # the .exe suffix the loader needs — git-bash then resolves the bare - # build/tools/ the recipes call to it. (go strips a /vN major suffix - # when naming, so github.com/google/go-licenses/v2 lands as go-licenses.) - # -o is resolved relative to -C. - GOOS='' GOARCH='' go -C tools build -o '../build/tools/' '{{ pkg }}' + {{ go_tool_build }} '{{ pkg }}' diff --git a/.limen/just/tools.just b/.limen/just/tools.just index 5bc7e15..cadd6a7 100644 --- a/.limen/just/tools.just +++ b/.limen/just/tools.just @@ -7,30 +7,44 @@ set working-directory := '../..' # Silence just's per-line command echo; recipes announce themselves via _banner. set quiet -# Shared private _banner recipe (see lib.just). +# Shared private _banner recipe and go_tool_build (see lib.just). import 'lib.just' -# --- Project tooling via aqua (see book/tooling.md). Each recipe takes the -# owner/repo exactly as it appears in aqua.yaml, e.g. golangci/golangci-lint. --- +# --- Project tooling (see book/tooling.md). Every recipe takes the tool as it +# is pinned: an aqua slug exactly as in aqua.yaml (golangci/golangci-lint), +# or a Go package path exactly as in tools/go.mod +# (golang.org/x/tools/cmd/deadcode). --- # -# Go-built tools are go.mod `tool` directives in tools/go.mod, not aqua -# packages (book/tooling.md): `go -C tools get -tool @`, then -# `go -C tools mod tidy`. +# The two are told apart by the first path element: a Go module root is a +# host and always carries a dot; a GitHub owner never can. aqua.yaml holds no +# go_install package any more (book/tooling.md), so there is no overlap. # -# The mutating recipes end with a FULL `aqua install`, never `--only-link`: -# links verify nothing (lazy pulls are a CI economy — wrong at the moment a -# pin changes), so only a real install proves the new pin downloads and -# verifies. On a warm machine the full install is incremental — only the -# touched tool downloads. +# The mutating recipes end by really installing the tool, never by linking: +# a FULL `aqua install` for an aqua package (links verify nothing — lazy pulls +# are a CI economy, wrong at the moment a pin changes; on a warm machine the +# full install is incremental), and a native build into build/tools/ for a +# Go tool (the same build _go-tool does before a recipe runs it). Either way a +# bad pin fails here, not at first use. # Add a new tool at its latest version, e.g. `just do tools add junegunn/fzf`. add pkg: (_banner "tools" "add") #!/usr/bin/env bash set -euo pipefail - # Regex-escape the slug: aqua slugs carry dots, and an unescaped '.' would - # match a sibling (`foo/li.r` vs `foo/liar`). ']' and '\' are absent from - # slugs and trip BSD sed. + # Regex-escape the name: slugs and package paths carry dots, and an + # unescaped '.' would match a sibling (`foo/li.r` vs `foo/liar`). ']' and + # '\' are absent from both and trip BSD sed. esc=$(printf '%s' '{{ pkg }}' | sed 's/[.^$*+?()[{}|]/\\&/g') + first='{{ pkg }}'; first=${first%%/*} + if [[ $first == *.* ]]; then + if grep -qE "^(tool[[:space:]]+)?[[:space:]]*${esc}([[:space:]]|$)" tools/go.mod 2>/dev/null; then + echo "{{ pkg }} is already a tool directive in tools/go.mod — use 'just do tools update ' or 'just do tools set {{ pkg }} '." >&2 + exit 1 + fi + go -C tools get -tool '{{ pkg }}@latest' # the directive, at the latest release + go -C tools mod tidy + {{ go_tool_build }} '{{ pkg }}' # REAL build: a bad pin fails here, not at first use + exit 0 + fi if grep -qE "^[[:space:]]*-[[:space:]]*name:[[:space:]]*${esc}([[:space:]]|@|$)" aqua.yaml; then echo "{{ pkg }} is already in aqua.yaml — use 'just do tools update {{ pkg }}' or 'just do tools set {{ pkg }} '." >&2 exit 1 @@ -45,6 +59,17 @@ set pkg version: (_banner "tools" "set") set -euo pipefail # See `add` for the escaping. esc=$(printf '%s' '{{ pkg }}' | sed 's/[.^$*+?()[{}|]/\\&/g') + first='{{ pkg }}'; first=${first%%/*} + if [[ $first == *.* ]]; then + if ! grep -qE "^(tool[[:space:]]+)?[[:space:]]*${esc}([[:space:]]|$)" tools/go.mod 2>/dev/null; then + echo "{{ pkg }} is not a tool directive in tools/go.mod — add it with 'just do tools add {{ pkg }}'." >&2 + exit 1 + fi + go -C tools get -tool '{{ pkg }}@{{ version }}' # moves the pin + go -C tools mod tidy + {{ go_tool_build }} '{{ pkg }}' # REAL build: a bad pin fails here, not at first use + exit 0 + fi if ! grep -qE "^[[:space:]]*-[[:space:]]*name:[[:space:]]*${esc}@" aqua.yaml; then echo "{{ pkg }} is not pinned in aqua.yaml — add it with 'just do tools add {{ pkg }}'." >&2 exit 1 @@ -58,12 +83,54 @@ set pkg version: (_banner "tools" "set") aqua update-checksum --prune # new checksum in, replaced version's out aqua install # REAL install: a bad pin fails here, not at first use -# Update an existing tool to its latest version, e.g. `just do tools update golangci-lint`. -# Takes the COMMAND name (`just`, `limen`), not the package slug: `aqua update` -# resolves a command to its pinned package, local registry included. -update command: (_banner "tools" "update") +# Takes the COMMAND name (`just`, `limen`, `deadcode`), not the package: `aqua +# update` resolves a command to its pinned package, local registry included, +# and a tool directive is found by the command it builds as. With no argument +# every tool moves: each aqua package and the registries (`aqua update`), then +# each directive at its latest — one `go get` for all of them, so the module +# graph is solved once — and every directive is rebuilt. Renovate does this +# one tool at a time; the no-argument form is for moving everything by hand +# and reading one diff. (The blank line below keeps this paragraph out of +# `just --list`; only the line right above the recipe is its doc.) + +# Update one tool to its latest version (`just do tools update golangci-lint`), or every tool with no argument. +update command="": (_banner "tools" "update") #!/usr/bin/env bash set -euo pipefail + # Every directive in tools/go.mod: a `tool` line and a `tool (…)` block are + # both walked; a `//` comment line inside the block is not a directive. + # (A read loop, not mapfile: macOS ships bash 3.) + pkgs=() + while IFS= read -r p; do pkgs+=("$p"); done < <(awk ' + /^tool[[:blank:]]*\(/ { block = 1; next } + block && /^\)/ { block = 0; next } + /^tool[[:blank:]]/ { print $2 } + block && NF && $1 !~ /^\/\// { print $1 } + ' tools/go.mod 2>/dev/null || true) + # A directive builds as its last path element, except that go strips a /vN + # major suffix (github.com/google/go-licenses/v2 builds as go-licenses — + # see _go-tool). + name_of() { local n=${1##*/}; if [[ $n =~ ^v[0-9]+$ ]]; then n=${1%/*}; n=${n##*/}; fi; printf '%s' "$n"; } + if [ -z '{{ command }}' ]; then + aqua update # every package and the registries, to the latest + aqua update-checksum --prune # new checksums in, replaced versions' out + aqua install # REAL install: a bad pin fails here, not at first use + if [ ${#pkgs[@]} -gt 0 ]; then + go -C tools get -tool "${pkgs[@]/%/@latest}" # one solve for all of them + go -C tools mod tidy + {{ go_tool_build }} "${pkgs[@]}" # REAL build of every directive + fi + exit 0 + fi + # ${pkgs[@]+…}: under set -u, bash 3 treats an empty array as unset. + for p in ${pkgs[@]+"${pkgs[@]}"}; do + if [ "$(name_of "$p")" = '{{ command }}' ]; then + go -C tools get -tool "${p}@latest" # bump tools/go.mod to the latest release + go -C tools mod tidy + {{ go_tool_build }} "$p" # REAL build: a bad pin fails here, not at first use + exit 0 + fi + done aqua update "{{ command }}" # bump aqua.yaml to the latest release aqua update-checksum --prune # new checksum in, replaced version's out aqua install # REAL install: a bad pin fails here, not at first use @@ -72,8 +139,22 @@ update command: (_banner "tools" "update") remove pkg: (_banner "tools" "remove") #!/usr/bin/env bash set -euo pipefail - # Regex-escape the slug before grep -E — see `add` for why. + # See `add` for the escaping. esc=$(printf '%s' '{{ pkg }}' | sed 's/[.^$*+?()[{}|]/\\&/g') + first='{{ pkg }}'; first=${first%%/*} + if [[ $first == *.* ]]; then + if ! grep -qE "^(tool[[:space:]]+)?[[:space:]]*${esc}([[:space:]]|$)" tools/go.mod 2>/dev/null; then + echo "{{ pkg }} is not a tool directive in tools/go.mod — nothing to remove." >&2 + exit 1 + fi + go -C tools get -tool '{{ pkg }}@none' # drops the directive + go -C tools mod tidy # and the requirements only it needed + # The built binary, named as go names it: last element, /vN stripped. + pkg='{{ pkg }}'; name=${pkg##*/} + if [[ $name =~ ^v[0-9]+$ ]]; then name=${pkg%/*}; name=${name##*/}; fi + rm -f "build/tools/${name}" "build/tools/${name}.exe" + exit 0 + fi if ! grep -qE "^[[:space:]]*-[[:space:]]*name:[[:space:]]*${esc}([[:space:]]|@|$)" aqua.yaml; then echo "{{ pkg }} is not in aqua.yaml — nothing to remove." >&2 exit 1 diff --git a/aqua-checksums.json b/aqua-checksums.json index 688165d..16378d2 100644 --- a/aqua-checksums.json +++ b/aqua-checksums.json @@ -46,28 +46,28 @@ "algorithm": "sha256" }, { - "id": "github_release/github.com/farcloser/limen/v0.3.0/limen_0.3.0_darwin_arm64.tar.gz", - "checksum": "CEF8FB56B7EEA4462D9D1E9C4B710C097913FC8EF94F5835AF4B594F9EF7F13D", + "id": "github_release/github.com/farcloser/limen/v0.4.0/limen_0.4.0_darwin_arm64.tar.gz", + "checksum": "EDE72BB064E6C67CE13128E7CB0224BCF918D48C0D7592308B4ED92E9B9D0458", "algorithm": "sha256" }, { - "id": "github_release/github.com/farcloser/limen/v0.3.0/limen_0.3.0_linux_amd64.tar.gz", - "checksum": "C88710B7B6E73B6C861B6B2618435DEAC870506AF1145368E2A83C55DCCBBA9C", + "id": "github_release/github.com/farcloser/limen/v0.4.0/limen_0.4.0_linux_amd64.tar.gz", + "checksum": "A7191E1C0469BAE83F28647E0D29BF7A326A2D0E18BE27947D78FFFBE7A9C7B5", "algorithm": "sha256" }, { - "id": "github_release/github.com/farcloser/limen/v0.3.0/limen_0.3.0_linux_arm64.tar.gz", - "checksum": "D5B33269CF12229D5ECBB795372D430FE06950F7845D438568712C45CE28D1DB", + "id": "github_release/github.com/farcloser/limen/v0.4.0/limen_0.4.0_linux_arm64.tar.gz", + "checksum": "AD00BBB630E232C3D383E4EA90B76979ED2B7D9E5CFA16AA154D414606A5AF28", "algorithm": "sha256" }, { - "id": "github_release/github.com/farcloser/limen/v0.3.0/limen_0.3.0_windows_amd64.tar.gz", - "checksum": "F2626F3C3D2B1337EE1963188D4637679D9DC7BA2B657F01D57F40EAD12196A6", + "id": "github_release/github.com/farcloser/limen/v0.4.0/limen_0.4.0_windows_amd64.tar.gz", + "checksum": "17C97515D66B8F3E93CAC797069F65D95DD88CB0AAE99AEC87C345CB1F98D967", "algorithm": "sha256" }, { - "id": "github_release/github.com/farcloser/limen/v0.3.0/limen_0.3.0_windows_arm64.tar.gz", - "checksum": "DBCA070451ECB28EF9DB640D0892DC3DE3ACDBEF570B462B5CB4DB395CFE3F12", + "id": "github_release/github.com/farcloser/limen/v0.4.0/limen_0.4.0_windows_arm64.tar.gz", + "checksum": "520FDBCCA3CDBEE744AD8D92ECCE5781CC603334AAEE1E162DBD75852E8EDA3A", "algorithm": "sha256" }, { @@ -230,6 +230,26 @@ "checksum": "73657A111819A30C47C08352896796F23D64E4EB2B3ED39B6D32149241566FC5", "algorithm": "sha256" }, + { + "id": "github_release/github.com/quint-co/quint/v0.32.0/quint-linux-amd64", + "checksum": "939B64095B706017F2F202C6F99C860C40BE7C31BDDC2B98557316E50F42CD7F", + "algorithm": "sha256" + }, + { + "id": "github_release/github.com/quint-co/quint/v0.32.0/quint-linux-arm64", + "checksum": "5B23E6F7E6F6B9C870C5EA7D38675E8FC709F4578BCF4A236918414157267A35", + "algorithm": "sha256" + }, + { + "id": "github_release/github.com/quint-co/quint/v0.32.0/quint-macos-arm64", + "checksum": "EB038B5E47D9839977053097830EEA386F42081780CA7E6A9B6B4FF5F3DE131F", + "algorithm": "sha256" + }, + { + "id": "github_release/github.com/quint-co/quint/v0.32.0/quint-pc-amd64.exe", + "checksum": "A5197EC8CCFDE5B5AD40F5C62FA7D4CBA2A01D1AFFE1A93B72D41B2385AFF7AC", + "algorithm": "sha256" + }, { "id": "github_release/github.com/sigstore/cosign/v3.1.3/cosign-darwin-arm64", "checksum": "5CF948C2F4DFE59687BDD0B8523709067383E03982CC543475C8A7DC70E92A76", diff --git a/aqua.yaml b/aqua.yaml index c7403f8..c606f52 100644 --- a/aqua.yaml +++ b/aqua.yaml @@ -20,7 +20,7 @@ packages: # --- go install tools (local registry, GOSUMDB-verified) --- # Pseudo-version: the nested cmd/dot module carries no tags upstream. # --- farcloser tools (local registry; standard once registered upstream) --- - - name: farcloser/limen@v0.3.0 # renovate: depName=farcloser/limen + - name: farcloser/limen@v0.4.0 # renovate: depName=farcloser/limen registry: local # --- toolchain + binary-release tools (standard registry, aqua-verified) --- - name: golang/go@go1.27.1 @@ -36,3 +36,5 @@ packages: - name: cli/cli@v2.100.0 - name: uutils/coreutils@0.11.0 registry: local + - name: quint-co/quint@v0.32.0 # renovate: depName=quint-co/quint + registry: local diff --git a/renovate.json b/renovate.json index f1332ac..1fac3e0 100644 --- a/renovate.json +++ b/renovate.json @@ -6,7 +6,7 @@ "gitIgnoredAuthors: the update-aqua-checksum workflow pushes a fix-up commit onto Renovate's branches; without this, Renovate treats the branch as human-modified and stops rebasing it. The org's App identity is the org's, so the array stays here (the `renovate` rule maintains it) rather than in the preset." ], "extends": [ - "github>farcloser/limen#v0.3.0" + "github>farcloser/limen#v0.4.0" ], "forkProcessing": "enabled", "gitIgnoredAuthors": [