Skip to content

fix(ci): exclude k9 contracts from the Nickel gate #985

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 2 commits into from
Sep 22, 2026
Merged

fix(ci): exclude k9 contracts from the Nickel gate #985

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
fa5edc9
fix(ci): exclude k9 contracts from the Nickel gate
hyperpolymath Sep 22, 2026
4d5db63
Merge branch 'main' into fix/nickel-gate-excludes-k9-contracts
hyperpolymath Sep 22, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
79 changes: 72 additions & 7 deletions .github/workflows/ci-pipeline.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 ""
Expand Down Expand Up @@ -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"

# ───────────────────────────────────────────────────────────────────────
Expand Down Expand Up @@ -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})"
Expand Down
Loading