壊れたサイトは、ビルドできない。

NoGoals は Lean 4 で書かれた静的サイトジェネレーターです。型と証明により、ルートの形式が正しいこと、出力パスの一意性、すべてのページに日本語版と英語版が存在することを保証します。監査では、出力ファイルのリンク、CSP、SEO、公開済み URL を検査します。監査に失敗した場合、出力ディレクトリは変更されません。

定理・sorry・ビルド時ゲートの数

定理
167
sorry（未証明の穴）
0
ビルド時ゲート
15

定理と sorry の数は verify.sh が集計します。ソースコードから集計した値と記録済みの値が一致しなければ、検証は失敗します。ゲートの数はこのページをビルドしたコードから読んでいます。これらの数値はすべて自動で取得しています。

仕組み

多くの静的サイトジェネレーターでは、リンク先や画像の参照先を文字列で指定します。任意の文字列を指定できるため、入力ミスがあってもそのまま受け入れられます。

NoGoals は Lean 4 で書かれています。各サイトでは、ページを列挙型として定義します。ひな形にはこの型が含まれています。リンク先には、その型のコンストラクタを指定します。存在しないページへのリンクは、コンパイル時にエラーになります。

監査時には、リンク検査のゲートが、手書きの HTML を含む出力ファイル内のすべての href を解決します。

文字列による参照
href : String
-- "/about"
-- "/prodcuts"             a typo, and it ships
-- "javascript:alert(1)"   ships too
型つきの値
target : PageId     -- a page that exists
src    : AssetPath  -- path syntax checked at the literal
title  : L          -- a Japanese AND an English field
date   : IsoDate    -- a real calendar date
-- a wrong value is a compile error, with a line number

検証方法

  • 型による保証

    不正な状態を表現できません。リンク先には、サイトのページ型のコンストラクタを指定します。スラッグ、アセットのパス、日付は、コンパイル時に書式を検査されるリテラルです。掲載する文言は日本語と英語のフィールドを持つレコードなので、一方のフィールドを省略するとコンパイルが通りません。

  • 定理による保証

    証明は Lean のカーネルで検査されます。ジェネレーターが受け入れるどのサイトでも、出力パスは衝突せず、すべてのページが出力され、すべてのページに日本語版と英語版が存在します。検証済みレンダラーが生成するリンクは、出力されたファイルへの参照として解決されます。

  • ビルド時の検査

    --audit を指定すると、ブラウザと同じ HTML の解析規則に従うパーサーが出力ファイルを読みます。すべてのリンクとアセット参照が解決するか、ページが配信時の CSP に従っているか、canonical と hreflang がルートと一致するかを検査します。HTML の妥当性と、公開済みのすべての URL が引き続き有効か、リダイレクトされているかも検査します。ゲートが一つでも失敗すると、ファイルは出力ディレクトリにコピーされません。

レポートは、それぞれの主張がどの区分に属するかを示します。監査なしのビルドではゲートは走らず、レポートにはそのとおり「未実行」と出ます。実行されなかった検査が「合格」と表示されることはありません。

検査項目の一覧を見る

ビルドが失敗したとき

ページの URL を変えて、手書きの HTML に古い URL へのリンクが一つ残ったとします。

監査つきビルドの出力（例）
$ ./scripts/build.sh --audit
  …
  ✗ links: every internal reference on 12 pages resolves:
      pricing/index.html: <a href="/plans/">: no emitted file at plans/index.html
  ✓ seo: canonical/hreflang/og on 12 route pages
  …
  ✗ permalinks: all 31 obligations live or redirected (permalinks_sound applies); _redirects rendered from the same map:
      previously published URL would 404: plans/index.html (add a redirect or restore the page)

✗ AUDIT FAILED — violations above; the previous build stays in place.
  …
✗ BUILD REJECTED: a gate failed. build/ is UNTOUCHED (last green build).

直前に成功したビルドはそのまま残ります。失敗したビルド成果物は隔離され、検証記録（receipt）には失敗したゲートが記録されます。この記録は機械可読なので、デプロイ用スクリプトでは、完全な監査に合格した記録だけを受け入れるようにできます。

このサイトの検証結果

このサイトは NoGoals でビルドされています。フッターのバッジは、このビルドの検証ページへのリンクです。

このビルドの検証ページ保証の一覧、区分、根拠となる定理

はじめる