diff --git a/.github/workflows/ci-pipeline.yml b/.github/workflows/ci-pipeline.yml index d2583657..8bcdeaf2 100644 --- a/.github/workflows/ci-pipeline.yml +++ b/.github/workflows/ci-pipeline.yml @@ -129,7 +129,14 @@ jobs: # Every probe here has a CONSUMING job later in this file. That is # the entry requirement for this list, not a coincidence. N_RUST=$(count 'Cargo.toml' '*/Cargo.toml') - N_NICKEL=$(count '*.ncl') + # A suffix is not a format. `*.k9.ncl` files open with a `K9!` sentinel on + # line 1 and are k9 contracts, not Nickel source — `nickel typecheck` dies + # at 1:3 on the `!`. They are excluded here so `has_nickel` cannot go true + # on a repo holding no Nickel at all, and excluded by the SAME pathspec in + # the `nickel` job: a guard that counts a different set than its consumer + # checks is how a gate comes to fail over files the repo cannot fix. + N_NICKEL=$(count '*.ncl' ':!*.k9.ncl') + N_K9=$(count '*.k9.ncl') N_RESCRIPT=$(count 'rescript.json' '*/rescript.json' 'bsconfig.json' '*/bsconfig.json' '*.res') # V is gated on `v.mod` ALONE. The `.v` extension is shared with Coq # proof scripts and Verilog sources, so globbing `*.v` would install @@ -224,13 +231,17 @@ jobs: echo "| Ecosystem | Marker | Tracked files matched |" echo "|---|---|---|" echo "| Rust | \`Cargo.toml\` | ${N_RUST} |" - echo "| Nickel | \`*.ncl\` | ${N_NICKEL} |" + echo "| Nickel | \`*.ncl\` excluding \`*.k9.ncl\` | ${N_NICKEL} |" echo "| ReScript | \`rescript.json\`, \`bsconfig.json\`, \`*.res\` | ${N_RESCRIPT} |" echo "| V | \`v.mod\` only | ${N_V} |" echo "| Haskell | \`*.cabal\`, \`stack.yaml\`, \`*.hs\` | ${N_HASKELL} |" echo "| Deno | \`deno.json(c)\` | ${N_DENO} |" echo "| **Total checkable** | | **${TOTAL}** |" echo "" + if [ "$N_K9" -gt 0 ]; then + echo "> **${N_K9} \`*.k9.ncl\` excluded.** These are k9 contracts (a \`K9!\` sentinel on line 1), not Nickel source. They are neither typechecked nor counted above, and they cannot raise the Total." + echo "" + fi if [ "$N_UNSUPPORTED" -gt 0 ]; then echo "#### Detected, but this pipeline has no gate for it" echo "" @@ -437,25 +448,79 @@ jobs: shell: bash run: | set -euo pipefail - mapfile -d '' FILES < <(git ls-files -z -- '*.ncl') - echo "Nickel files: ${#FILES[@]}" + + # Same pathspec as `detect`. k9 contracts are a DIFFERENT format that + # merely shares the suffix; typechecking them reports a parse error the + # repo has no way to fix. + mapfile -d '' FILES < <(git ls-files -z -- '*.ncl' ':!*.k9.ncl') + N_K9=$(git ls-files -z -- '*.k9.ncl' | tr -cd '\0' | wc -c) + + echo "Nickel files: ${#FILES[@]} (k9 contracts excluded: ${N_K9})" if [ "${#FILES[@]}" -eq 0 ]; then - echo "::error::detect said Nickel was present but zero .ncl files are tracked here. Refusing to report a pass over an empty set." + echo "::error::detect said Nickel was present but zero Nickel files are tracked here (${N_K9} *.k9.ncl were excluded as k9 contracts). Refusing to report a pass over an empty set." exit 1 fi + FAILED=0 + TYPECHECKED=0 + SKIPPED=() + for f in "${FILES[@]}"; do # --check is read-only: it reports, it does not rewrite the file. + # Format is checked over EVERY genuine Nickel file, with no exemption. nickel format --check "$f" || { echo "::error file=$f::not formatted (nickel format --check)"; FAILED=1; } + + # A file importing a build artefact cannot be typechecked standalone: + # the input is generated immediately before use and is correctly + # uncommitted. Detect that by asking git whether the import target is + # tracked, and DISCLOSE every skip by name. A skip is not a pass. + MISSING="" + while IFS= read -r imp; do + [ -n "$imp" ] || continue + cand="$(dirname "$f")/$imp" + cand="$(realpath -m --relative-to=. "$cand" 2>/dev/null || echo "$cand")" + git ls-files --error-unmatch -- "$cand" >/dev/null 2>&1 \ + || MISSING="${MISSING}${MISSING:+, }${imp}" + # Comments are stripped first: `_base.ncl` documents its own usage + # in a `#` comment containing a literal `import "../_base.ncl"`, and + # matching that would skip a file that typechecks perfectly well. + done < <(sed 's/#.*//' "$f" | grep -oE 'import[[:space:]]+"[^"]+"' | sed -E 's/.*"([^"]+)".*/\1/' || true) + + if [ -n "$MISSING" ]; then + echo "::notice file=$f::nickel typecheck skipped - import target not tracked in git: ${MISSING}" + SKIPPED+=("$f (${MISSING})") + continue + fi + nickel typecheck "$f" || { echo "::error file=$f::failed nickel typecheck"; FAILED=1; } + TYPECHECKED=$((TYPECHECKED + 1)) done + + # Narrowing a file set must never be able to manufacture a pass. + if [ "$TYPECHECKED" -eq 0 ]; then + echo "::error::all ${#FILES[@]} Nickel files were skipped for untracked imports, so nothing was typechecked. Refusing to report a pass over an empty set." + FAILED=1 + fi + { echo "### Nickel" echo "" - echo "- files checked: **${#FILES[@]}**" + echo "- format checked: **${#FILES[@]}**" + echo "- typechecked: **${TYPECHECKED}**" + echo "- typecheck skipped (untracked import): **${#SKIPPED[@]}**" + echo "- k9 contracts excluded (\`*.k9.ncl\`, not Nickel): **${N_K9}**" + if [ "${#SKIPPED[@]}" -gt 0 ]; then + echo "" + echo "Skipped, and why:" + echo "" + for s in "${SKIPPED[@]}"; do echo "- \`${s}\`"; done + fi + echo "" echo "- result: $( [ "$FAILED" -eq 0 ] && echo 'pass' || echo '**FAIL**' )" echo "" } >> "$GITHUB_STEP_SUMMARY" + + exit "$FAILED" exit "$FAILED" # ─────────────────────────────────────────────────────────────────────── @@ -833,7 +898,7 @@ jobs: row "Secret scanning" "$R_SECRET" "n/a" row "SAST (semgrep)" "$R_SAST" "disabled via enable_sast: false" row "Rust" "$R_RUST" "no Cargo.toml tracked (has_rust=${H_RUST})" - row "Nickel" "$R_NICKEL" "no *.ncl tracked (has_nickel=${H_NICKEL})" + row "Nickel" "$R_NICKEL" "no Nickel tracked, *.k9.ncl excluded (has_nickel=${H_NICKEL})" row "Deno" "$R_DENO" "BANNED — refusal gate; skipped means no deno.json(c) tracked (has_deno=${H_DENO})" row "ReScript" "$R_RESCRIPT" "no rescript.json/bsconfig.json/*.res tracked (has_rescript=${H_RESCRIPT})" row "V" "$R_V" "no v.mod tracked (has_v=${H_V})"