Enable --wfail axiom-guard gate once warnings are clean

まず lake build --wfail を実行し、sorry プレースホルダーの発生元である Lck/Regex/Parser.lean と Lck/Regex/Matcher.lean に一覧表示された宣言を確認します。Lck/Regex/Regex.lean と test/Main.lean の推移的なレポートを確認します。これらの警告がなくなり、CI が leanprover/lean-action@v1 で build-args: "--wfail" を使用していれば完了です。

The lean_extensions axiom-guard plugin is now wired into the build (see the feat/axiom-guard PR). It warns when a declaration depends on a non-standard axiom (anything beyond propext, Quot.sound, Classical.choice; sorry included).

CI currently runs a plain lake build (via leanprover/lean-action@v1), so these warnings are surfaced but do not fail the build. We cannot yet enforce the gate with lake build --wfail because the existing regex code uses sorry, which the guard reports as a dependency on the non-standard axiom sorryAx. Running lake build --wfail locally exits 1 on the following pre-existing declarations:

Lck/Regex/Parser.lean:77:0:  `Lck.Regex.parseCharClassContents` depends on non-standard axiom `sorryAx`
Lck/Regex/Parser.lean:107:0: `Lck.Regex.parseCharClass` depends on non-standard axiom `sorryAx`
Lck/Regex/Parser.lean:126:0: `Lck.Regex.parseAtom` depends on non-standard axiom `sorryAx`
Lck/Regex/Parser.lean:147:0: `Lck.Regex.parseRepetition` depends on non-standard axiom `sorryAx`
Lck/Regex/Parser.lean:160:0: `Lck.Regex.collectAtoms` depends on non-standard axiom `sorryAx`
Lck/Regex/Parser.lean:197:0: `Lck.Regex.parseConcat` depends on non-standard axiom `sorryAx`
Lck/Regex/Parser.lean:202:0: `Lck.Regex.collectAlternates` depends on non-standard axiom `sorryAx`
Lck/Regex/Parser.lean:232:0: `Lck.Regex.parseAlternation` depends on non-standard axiom `sorryAx`
Lck/Regex/Parser.lean:237:0: `Lck.Regex.parse` depends on non-standard axiom `sorryAx`
Lck/Regex/Matcher.lean:102:0: `Lck.Regex.epsilonClosure` depends on non-standard axiom `sorryAx`
Lck/Regex/Matcher.lean:138:0: `Lck.Regex.step` depends on non-standard axiom `sorryAx`
Lck/Regex/Matcher.lean:149:0: `Lck.Regex.matchesString` depends on non-standard axiom `sorryAx`
Lck/Regex/Matcher.lean:172:0: `Lck.Regex.matchesAt` depends on non-standard axiom `sorryAx`
Lck/Regex/Matcher.lean:195:0: `Lck.Regex.matchesLine` depends on non-standard axiom `sorryAx`
Lck/Regex/Regex.lean:18:0:   `Lck.Regex.compile` depends on non-standard axiom `sorryAx`
Lck/Regex/Regex.lean:24:0:   `Lck.Regex.matchFull` depends on non-standard axiom `sorryAx`
Lck/Regex/Regex.lean:29:0:   `Lck.Regex.matchCompiled` depends on non-standard axiom `sorryAx`
Lck/Regex/Regex.lean:33:0:   `Lck.Regex.search` depends on non-standard axiom `sorryAx`
Lck/Regex/Regex.lean:38:0:   `Lck.Regex.searchCompiled` depends on non-standard axiom `sorryAx`
test/Main.lean:6:0:          `main` depends on non-standard axiom `sorryAx` (transitive, via the regex lib under test)

These all stem from the sorry placeholders in Lck/Regex/Parser.lean and Lck/Regex/Matcher.lean; Regex.lean and test/Main.lean inherit them transitively.

Once these sorrys are discharged (or otherwise removed), switch CI from the plain lake build to lake build --wfail to turn the axiom guard into a hard gate. With leanprover/lean-action@v1 this is build-args: "--wfail".