From 6b1ad8e11ca2c0437560d0f3730207be5fe2a1a7 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 1 Jul 2026 02:01:21 +0000 Subject: [PATCH 1/2] =?UTF-8?q?fix(ci):=20check-spdx=20prose=20licence=20v?= =?UTF-8?q?ariable=20=E2=86=92=20CC-BY-SA-4.0?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit check-spdx.sh set the prose SPDX variable to MPL-2.0, which contradicted the repo's own machine-readable declaration (licensing-policy.toml: prose = CC-BY-SA-4.0) and the checker's own failure label. Every prose file already carries CC-BY-SA-4.0, so the checker was failing `just license-check` on a pristine tree. Point the variable at the declared policy and exclude the canonical LICENSES/ REUSE texts (mirrored in licensing-policy.toml). No licence header on any file is changed — this only corrects the enforcer to accept the headers that are already present and declared. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7 --- .machine_readable/licensing-policy.toml | 1 + scripts/check-spdx.sh | 5 +++-- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/.machine_readable/licensing-policy.toml b/.machine_readable/licensing-policy.toml index ecc0e3c..6b93aa7 100644 --- a/.machine_readable/licensing-policy.toml +++ b/.machine_readable/licensing-policy.toml @@ -22,6 +22,7 @@ prose = "CC-BY-SA-4.0" # *.adoc, *.md narrative paths = [ "Cargo.lock", # generated by cargo; enumerates third-party dependencies "LICENSE", # the MPL-2.0 licence text itself + "LICENSES/", # canonical SPDX licence texts (REUSE dir: MPL-2.0 + CC-BY-SA-4.0) "target/", # cargo build output (gitignored) "tests/fixtures/", # Agda test-input data (some deliberately malformed) ] diff --git a/scripts/check-spdx.sh b/scripts/check-spdx.sh index cd559c0..9106e13 100755 --- a/scripts/check-spdx.sh +++ b/scripts/check-spdx.sh @@ -5,7 +5,7 @@ # Licence invariant for arghda-core (enforced by `just check` + Rust CI). # # code / config / scripts / state -> SPDX-License-Identifier: MPL-2.0 -# prose documentation (*.adoc, *.md) -> SPDX-License-Identifier: MPL-2.0 +# prose documentation (*.adoc, *.md) -> SPDX-License-Identifier: CC-BY-SA-4.0 # # Files that are NOT ours, generated, or test-input data are EXCLUDED and must # never carry the repo's licence choices. The machine-readable declaration of @@ -20,13 +20,14 @@ set -euo pipefail cd "$(git rev-parse --show-toplevel)" MPL='SPDX-License-Identifier: MPL-2.0' -CC='SPDX-License-Identifier: MPL-2.0' +CC='SPDX-License-Identifier: CC-BY-SA-4.0' fail=0 # Not ours / generated / test-input data — see [excluded] in the policy file. excluded() { case "$1" in Cargo.lock | LICENSE) return 0 ;; # generated lockfile / the licence text itself + LICENSES/*) return 0 ;; # canonical SPDX licence texts (REUSE dir) target/* | tests/fixtures/*) return 0 ;; # build output / Agda test-input data *) return 1 ;; esac From 7631cd555083001587166c1ee45776b3bd41ba21 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 1 Jul 2026 02:01:35 +0000 Subject: [PATCH 2/2] feat(provision): pinned multi-prover/solver toolchain provisioning + doctor MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds scripts/provision-provers.sh: an idempotent, version-pinned installer for the prover/solver backends ArghDA drives, modelled on echo-types' provision-agda.sh and widened to the full set. Tractable tier (installed by default): agda 2.6.3 + stdlib v2.3 + the agda/cubical library, zig 0.15.2, idris2 v0.7.0 (chez bootstrap), lean4 v4.13.0 (elan), and the SMT solvers z3 + cvc5 1.2.0. Heavy tier behind --heavy (coq via opam, isabelle) and --mizar. Honesty contract: a backend is only ever reported OK when its own --version returned 0 in the run; anything else is MISSING/FAILED with the command tried. Third-party sources are fetched as curl tarballs rather than `git clone`, because this environment's proxy 403s git-relay access to non-scoped repos (and tarballs are more portable anyway). Justfile gains `provision` / `provision-heavy` / `doctor` recipes (the interim doctor shells the script's --verify-only table until the `arghda doctor` subcommand lands). STATE.a2ml records M0 and the Flying-Logic multi-prover epic (M1–M11). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7 --- .machine_readable/6a2/STATE.a2ml | 43 ++++- Justfile | 16 ++ scripts/provision-provers.sh | 280 +++++++++++++++++++++++++++++++ 3 files changed, 334 insertions(+), 5 deletions(-) create mode 100644 scripts/provision-provers.sh diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index e8aa259..2393c32 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -6,7 +6,7 @@ [metadata] project = "arghda-core" version = "0.1.0" -last-updated = "2026-06-20" +last-updated = "2026-07-01" status = "active" # active | paused | archived [project-context] @@ -33,17 +33,50 @@ milestones = [ { name = "Groove service manifest (/.well-known/groove) for PanLL discovery", completion = 0 }, ] +# "Flying Logic for provers/solvers" epic (v0.2+): generalise the Agda-only +# engine into a multi-backend reasoning-graph workspace. Two backend kinds: +# proof-assistants (typecheck a file -> exit code) and solvers (SMT-LIB2 -> +# sat/unsat/unknown). Backends shell out to real binaries; a node is only +# "proven" on a real exit-0 (never embed a prover). See the plan doc. +[route-to-flying-logic] +milestones = [ + { name = "M0: provision-provers.sh (pinned, honest --version verification) + `just provision/doctor` recipes", completion = 80 }, + { name = "M1: Backend trait (Assistant|Solver kinds; Outcome/Verdict); agda.rs -> prover/agda.rs; graph/dag take &dyn Backend (pure refactor, 50 tests stay green)", completion = 0 }, + { name = "M2: Cubical-Agda variant (Agda::cubical(), --cubical --safe island)", completion = 0 }, + { name = "M3: Flying-Logic reasoning graph (src/reason: And|Or juncts, demote-only cycle-safe Verdict propagation, additive studio JSON)", completion = 0 }, + { name = "M4: Idris2 adapter (core/ABI language: .ipkg/--check/totality; escape-hatches)", completion = 0 }, + { name = "M5: SMT solver backends (Z3, CVC5): SMT-LIB2 -> sat/unsat/unknown -> Verdict", completion = 0 }, + { name = "M6: Lean4 adapter (lake build + #print axioms audit)", completion = 0 }, + { name = "M7: Echidna dispatch seam (optional route to orchestrator :8090, same Outcome)", completion = 0 }, + { name = "M8: Coq/Rocq adapter (--heavy provisioning; Section-aware postulate classifier)", completion = 0 }, + { name = "M9: Isabelle adapter (--heavy; dogfood tropical-resource-typing .thy)", completion = 0 }, + { name = "M10: Mizar adapter (detect-only first; highest uncertainty)", completion = 0 }, + { name = "M11: studio JSON freeze (reason/0.1) + Groove manifest", completion = 0 }, +] +# M0 provisioning verified in-container 2026-07-01: agda 2.6.3 (+stdlib v2.3 +# +cubical lib), zig 0.15.2, z3 4.8.12, cvc5 1.2.0, lean 4.13.0 all report +# real --version. idris2 v0.7.0 builds via chez bootstrap. Coq/Isabelle/Mizar +# are scripted (behind --heavy/--mizar) but not installed this session. +# Remaining M0: `arghda doctor` Rust subcommand (interim: `just doctor` shells +# the script's --verify-only table). + [blockers-and-issues] # No active blockers. v0.1 lint set + DAG schema (arghda-spec.adoc) are # complete. The SPDX licence invariant is applied and enforced # (scripts/check-spdx.sh; .machine_readable/licensing-policy.toml). +# 2026-07-01: fixed a pre-existing checker bug — check-spdx.sh's prose variable +# was set to MPL-2.0, contradicting the declared policy (prose = CC-BY-SA-4.0 in +# licensing-policy.toml) and the checker's own failure label; it now matches +# the declaration. NO licence header on any file changed; the LICENSES/ REUSE +# dir is now excluded (canonical texts). This was blocking `just license-check`. [critical-next-actions] actions = [ - "Template-applicability: rsr-profile.a2ml declares capabilities (landed); estate policy + gate model + reference checker landed in hyperpolymath/standards#391 + #392 (pure capability-gating). Follow-up: wire the standards rsr-profile check into CI.", - "Transitive-import closure hashing landed (workspace [proven] include_root); follow-up: also expose it as a --include-root CLI flag on promote/stale.", - "Serve /.well-known/groove for PanLL discovery (Groove protocol)", - "Scaffold arghda-studio (AffineScript visual layer consuming the dag JSON)", + "Flying-Logic epic M1: introduce the Backend trait (Assistant|Solver) and move agda.rs to prover/agda.rs as a PURE REFACTOR — the 50 existing tests are the oracle, they must stay green with no behaviour change. This is the keystone everything else rides on.", + "Flying-Logic epic M3: src/reason reasoning graph (And|Or juncts + demote-only cycle-safe Verdict propagation) — independent of new backends, lands the headline capability early.", + "Finish M0: add the `arghda doctor` Rust subcommand and repoint `just doctor` at it (interim shells provision-provers.sh --verify-only).", + "Transitive-import closure hashing landed; follow-up: expose it as a --include-root CLI flag on promote/stale.", + "Serve /.well-known/groove for PanLL discovery (Groove protocol) — folds into M11.", ] [maintenance-status] diff --git a/Justfile b/Justfile index 150f8b0..4f9c88e 100644 --- a/Justfile +++ b/Justfile @@ -55,6 +55,22 @@ dag path: agda-check file: cargo run -- check "{{file}}" +# Provision the prover/solver toolchains ArghDA drives (tractable set: +# agda+cubical, zig, idris2, lean4, z3, cvc5). Honest: a backend is reported +# OK only if its own --version actually returned 0 in the run. +provision: + bash scripts/provision-provers.sh + +# As `provision`, plus the heavy backends (Coq via opam, Isabelle ~4 GB). +provision-heavy: + bash scripts/provision-provers.sh --heavy + +# Report which prover/solver backends are actually runnable, no installs. +# (Interim: shells the provision script's --verify-only table until the +# `arghda doctor` subcommand lands.) +doctor: + bash scripts/provision-provers.sh --verify-only + # RSR: the mandated machine-readable artefacts are present and well-formed. validate-rsr: @for f in STATE META ECOSYSTEM AGENTIC NEUROSYM PLAYBOOK; do \ diff --git a/scripts/provision-provers.sh b/scripts/provision-provers.sh new file mode 100644 index 0000000..eb0818d --- /dev/null +++ b/scripts/provision-provers.sh @@ -0,0 +1,280 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# On-demand provisioning of the prover / solver toolchains ArghDA drives. +# Companion to hyperpolymath/echo-types scripts/provision-agda.sh, widened to +# the full multi-backend set. Idempotent: safe to re-run; skips anything already +# present. +# +# HONESTY CONTRACT (load-bearing — see arghda-core AGENTIC.a2ml): +# A tool is only ever reported "OK" if its own `--version` (or equivalent) +# actually returned exit 0 in THIS run. Anything else is reported MISSING or +# FAILED with the command that was tried. The script never claims an install +# it did not verify. +# +# Tiers: +# default (tractable, installed now): agda(+stdlib +cubical lib), zig, +# idris2, lean4, z3, cvc5 +# --heavy (adds): coq/rocq (opam), isabelle (~4 GB) +# --mizar (adds): mizar (niche; distribution uncertain) +# --all: everything above +# --verify-only: skip installs, just run the doctor table +# +# Usage: bash scripts/provision-provers.sh [--heavy] [--mizar] [--all] [--verify-only] +set -uo pipefail # NB: no -e; we tolerate per-tool failure and report it. + +log() { echo "[provision] $*"; } +warn() { echo "[provision] WARN: $*" >&2; } +have() { command -v "$1" >/dev/null 2>&1; } + +# ---- Pinned versions (reused from the estate where a precedent exists) ------- +STDLIB_TAG="v2.3" # echo-types pin +ZIG_VER="0.15.2" # boj-server setup-zig pin +IDRIS2_TAG="v0.7.0" # standards/a2ml CI pin +LEAN_VER="v4.13.0" # tropical-resource-typing lean-toolchain +CVC5_VER="1.2.0" # cvc5 static-binary release +COQ_VER="8.18.0" # opam (with --heavy) +ISABELLE_VER="Isabelle2024" # TUM tarball (with --heavy) + +STDLIB_DIR=/opt/agda-stdlib +CUBICAL_DIR=/opt/agda-cubical +ZIG_DIR=/opt/zig +IDRIS2_SRC=/opt/Idris2 +AGDA_HOME="${HOME}/.agda" + +WANT_HEAVY=0; WANT_MIZAR=0; VERIFY_ONLY=0 +for a in "$@"; do case "$a" in + --heavy) WANT_HEAVY=1 ;; + --mizar) WANT_MIZAR=1 ;; + --all) WANT_HEAVY=1; WANT_MIZAR=1 ;; + --verify-only) VERIFY_ONLY=1 ;; + *) warn "unknown flag: $a" ;; +esac; done + +apt_get() { DEBIAN_FRONTEND=noninteractive apt-get "$@"; } + +# ============================================================================= +# Installers — each best-effort, never aborts the script. +# ============================================================================= + +install_agda() { + have agda && { log "agda present: $(agda --version 2>&1 | head -1)"; return; } + log "installing agda (apt agda-bin)…" + apt_get update -qq || true + apt_get install -y agda-bin >/dev/null 2>&1 || apt_get install -y agda >/dev/null 2>&1 || \ + warn "apt could not install agda" +} + +# NB: this environment's proxy routes `git clone` through a git-relay that only +# permits the session's scoped repos (third-party clones return HTTP 403), but +# plain `curl` to GitHub archive tarballs works. So all third-party sources are +# fetched as release/branch tarballs, which is also more portable than a clone. +fetch_tarball() { # fetch_tarball + local url="$1" dest="$2" tmp="/tmp/arghda-fetch-$$.tar.gz" + curl -fsSL "$url" -o "$tmp" 2>/dev/null && [ -s "$tmp" ] || { rm -f "$tmp"; return 1; } + rm -rf "$dest"; mkdir -p "$dest" + tar -xzf "$tmp" -C "$dest" --strip-components=1; local rc=$? + rm -f "$tmp"; return $rc +} + +install_agda_stdlib() { + if [ -f "${STDLIB_DIR}/standard-library.agda-lib" ]; then + log "agda-stdlib present at ${STDLIB_DIR}"; return + fi + log "fetching agda-stdlib ${STDLIB_TAG} tarball…" + if fetch_tarball "https://github.com/agda/agda-stdlib/archive/refs/tags/${STDLIB_TAG}.tar.gz" "${STDLIB_DIR}"; then + sed -i 's/^name: standard-library-.*/name: standard-library/' \ + "${STDLIB_DIR}/standard-library.agda-lib" || true + log "agda-stdlib ${STDLIB_TAG} ready" + else + warn "agda-stdlib tarball fetch failed" + fi +} + +# Cubical Agda is the `--cubical` FLAG (ships with the agda binary — free). +# The agda/cubical LIBRARY (HIT stdlib) is optional and version-sensitive; +# best-effort fetch, never fatal. +install_agda_cubical() { + [ -d "${CUBICAL_DIR}" ] && { log "agda/cubical library present"; return; } + log "fetching agda/cubical library tarball (best-effort)…" + fetch_tarball "https://github.com/agda/cubical/archive/refs/heads/master.tar.gz" "${CUBICAL_DIR}" \ + || warn "agda/cubical fetch failed (the --cubical flag still works without the library)" +} + +register_agda_libraries() { + mkdir -p "${AGDA_HOME}" + { + [ -f "${STDLIB_DIR}/standard-library.agda-lib" ] && echo "${STDLIB_DIR}/standard-library.agda-lib" + [ -f "${CUBICAL_DIR}/cubical.agda-lib" ] && echo "${CUBICAL_DIR}/cubical.agda-lib" + for cand in /home/user/absolute-zero/absolute-zero.agda-lib \ + "${HOME}/absolute-zero/absolute-zero.agda-lib"; do + [ -f "$cand" ] && echo "$cand" + done + } > "${AGDA_HOME}/libraries" + echo "standard-library" > "${AGDA_HOME}/defaults" + log "registered ~/.agda/libraries:"; sed 's/^/ /' "${AGDA_HOME}/libraries" +} + +install_zig() { + have zig && { log "zig present: $(zig version 2>&1)"; return; } + log "installing zig ${ZIG_VER}…" + local base="https://ziglang.org/download/${ZIG_VER}" + # Asset naming flipped arch/os around 0.14; try both. + for name in "zig-x86_64-linux-${ZIG_VER}" "zig-linux-x86_64-${ZIG_VER}"; do + if curl -fsSL "${base}/${name}.tar.xz" -o /tmp/zig.tar.xz 2>/dev/null; then + rm -rf "${ZIG_DIR}"; mkdir -p "${ZIG_DIR}" + tar -xJf /tmp/zig.tar.xz -C "${ZIG_DIR}" --strip-components=1 \ + && ln -sf "${ZIG_DIR}/zig" /usr/local/bin/zig && { log "zig unpacked (${name})"; return; } + fi + done + warn "zig download failed for both asset-name patterns at ${base}" +} + +install_lean() { + export PATH="${HOME}/.elan/bin:${PATH}" + have lean && { log "lean present: $(lean --version 2>&1)"; return; } + log "installing lean ${LEAN_VER} via elan…" + if curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o /tmp/elan.sh 2>/dev/null; then + sh /tmp/elan.sh -y --default-toolchain "leanprover/lean4:${LEAN_VER}" >/dev/null 2>&1 \ + || warn "elan install failed" + else + warn "could not fetch elan-init.sh" + fi +} + +# Idris2 is a CORE estate language (owns ABIs) — install via Chez bootstrap. +install_idris2() { + export PATH="${HOME}/.idris2/bin:${PATH}" + have idris2 && { log "idris2 present: $(idris2 --version 2>&1)"; return; } + log "installing idris2 ${IDRIS2_TAG} (chez bootstrap)…" + have scheme || have chez || have chezscheme || apt_get install -y chezscheme >/dev/null 2>&1 || \ + warn "could not install chezscheme (idris2 bootstrap needs a Chez Scheme)" + local sch="" + for c in chezscheme chez scheme; do have "$c" && { sch="$c"; break; }; done + [ -z "$sch" ] && { warn "no Chez Scheme found; skipping idris2"; return; } + if [ ! -f "${IDRIS2_SRC}/Makefile" ]; then + fetch_tarball "https://github.com/idris-lang/Idris2/archive/refs/tags/${IDRIS2_TAG}.tar.gz" "${IDRIS2_SRC}" \ + || { warn "idris2 tarball fetch failed"; return; } + fi + ( cd "${IDRIS2_SRC}" \ + && make bootstrap SCHEME="${sch}" >/tmp/idris2-build.log 2>&1 \ + && make install PREFIX="${HOME}/.idris2" >>/tmp/idris2-build.log 2>&1 ) \ + || warn "idris2 build failed (see /tmp/idris2-build.log)" +} + +install_z3() { + have z3 && { log "z3 present: $(z3 --version 2>&1)"; return; } + log "installing z3 (apt)…" + apt_get install -y z3 >/dev/null 2>&1 || warn "apt could not install z3" +} + +install_cvc5() { + have cvc5 && { log "cvc5 present: $(cvc5 --version 2>&1 | head -1)"; return; } + log "installing cvc5 ${CVC5_VER}…" + have unzip || apt_get install -y unzip >/dev/null 2>&1 || true + local base="https://github.com/cvc5/cvc5/releases/download/cvc5-${CVC5_VER}" + # Single static binary first, then the zipped variant. + if curl -fsSL "${base}/cvc5-Linux-x86_64-static" -o /usr/local/bin/cvc5 2>/dev/null \ + && [ -s /usr/local/bin/cvc5 ]; then + chmod +x /usr/local/bin/cvc5; log "cvc5 binary installed"; return + fi + for asset in "cvc5-Linux-x86_64-static.zip" "cvc5-Linux-static.zip" "cvc5-Linux.zip"; do + if curl -fsSL "${base}/${asset}" -o /tmp/cvc5.zip 2>/dev/null && [ -s /tmp/cvc5.zip ]; then + rm -rf /tmp/cvc5d; mkdir -p /tmp/cvc5d && unzip -q /tmp/cvc5.zip -d /tmp/cvc5d 2>/dev/null || continue + local bin; bin="$(find /tmp/cvc5d -type f -name cvc5 | head -1)" + [ -n "$bin" ] && { install -m755 "$bin" /usr/local/bin/cvc5; log "cvc5 installed (${asset})"; return; } + fi + done + warn "cvc5 download failed for all known asset names at ${base}" +} + +# ---- Heavy (opt-in) --------------------------------------------------------- +install_coq() { + have coqc && { log "coq present: $(coqc --version 2>&1 | head -1)"; return; } + log "installing coq ${COQ_VER} via opam (heavy)…" + if ! have opam; then + apt_get install -y opam >/dev/null 2>&1 || { warn "opam unavailable"; return; } + fi + opam init --disable-sandboxing -y >/dev/null 2>&1 || true + eval "$(opam env 2>/dev/null)" || true + opam install -y "coq.${COQ_VER}" >/tmp/coq-build.log 2>&1 || warn "opam coq install failed (see /tmp/coq-build.log)" +} + +install_isabelle() { + have isabelle && { log "isabelle present"; return; } + log "installing ${ISABELLE_VER} (heavy, ~4 GB)…" + local url="https://isabelle.in.tum.de/dist/${ISABELLE_VER}_linux.tar.gz" + if curl -fsSL "$url" -o /tmp/isabelle.tar.gz 2>/dev/null && [ -s /tmp/isabelle.tar.gz ]; then + tar -xzf /tmp/isabelle.tar.gz -C /opt \ + && ln -sf "/opt/${ISABELLE_VER}/bin/isabelle" /usr/local/bin/isabelle \ + && log "isabelle unpacked" || warn "isabelle unpack failed" + else + warn "isabelle download failed: ${url}" + fi +} + +install_mizar() { + have mizar && { log "mizar present"; return; } + warn "mizar not auto-installed: distribution is manual (mizar.org). Flagged as UNKNOWN." +} + +# ============================================================================= +# Honest verification / doctor table. +# ============================================================================= +declare -a REPORT +verify() { # verify