CI: audit every declaration, broader source checks, pinned elan

[MarcIlunga]

Follow-up to #23. Its review found that the gates let through constructs they were meant to reject; each of these compiled silently and passed CI on main:

• a sorry under set_option warn.sorry false (or a #guard_msgs that drops the warning);
• noncomputable axiom … and @[simp] axiom …;
• decide (config := { native := true }).

Changes

Axiom audit of every declaration. scripts/check-axioms.sh now runs scripts/AxiomAudit.lean, which imports every module under src and checks every declaration they define (9,973 today, in about 30 s) against propext, Classical.choice and Quot.sound. It no longer depends on #print axioms lines, so nothing has to be listed and a swallowed message cannot lower a count. A module that is not built fails the import, so every file under src is covered.

The only exemptions are the four DSL diagnostics that check an elaboration error with #guard_msgs (Infinite, Growing, Uninitialized, WrongReply in Tests/DSL/Diagnostics.lean); after the error Lean still adds their generated declarations, with sorryAx in place of the part that failed. They are exempt by name, for sorryAx only.

Broader source check. scripts/check-sources.sh stays as a quick first check and now also matches:

• axioms after attributes, modifiers or a docstring;
• native :=, +native, reduceBool, trustCompiler;
• implemented_by and extern in any attribute position, and csimp;
• warn.sorry, debug.skipKernelTC, addDeclCore and doCheck.

A grep error now fails the check instead of passing it.

Workflow.

• elan is installed from a pinned release (v4.2.4), checked against its published SHA-256. lean-action fetched the installer from elan's master branch.
• The build cache is saved only by pushes to main. Pull requests restore it but no longer evict it.
• Superseded runs are cancelled only on pull requests; runs on main finish.

Checks

Check	Result
audit on main	9,973 declarations in 206 modules, none outside the envelope
audit with a planted module	catches the hidden sorry, the #guard_msgs-dropped sorry, noncomputable axiom and native := true
check-sources.sh on main	passes
check-sources.sh with planted lines	all 16 flagged (axiom forms, native forms, binding forms, options, limits)
shellcheck, actionlint	clean
zizmor 1.30.1 (regular, pedantic, auditor)	no findings
elan v4.2.4 tarball	SHA-256 matches the release digest

Dependabot keeps the action pins current; the elan pin in ci.yml is updated by hand (noted in AGENTS.md).

🤖 Generated with Claude Code

https://claude.ai/code/session_01E7GPy1oUx164NSZsxJT3N9