はじめる

ひな形は、そのままで監査に合格します。

最初のサイトをビルドする

  1. 用意するもの

    elan（Lean のバージョンは NoGoals が固定します）、Node（22 系なら 22.22 以上、または 24.8 以上）、jq。初回のビルドは Mathlib を取得するので時間がかかります。

  2. ひな形をコピーする

    NoGoals をチェックアウトしたディレクトリの隣に、最小構成のサイトを置きます。このサイトは、そのままで監査に合格します。

    Shell
    cp -R nogoals/skills/nogoals/assets my-site
cd my-site && npm ci

  3. 最初の監査を実行する

    新しいサイトには公開済みの URL がまだないので、最初の一回だけパーマリンクのベースラインを作ります。ベースラインがすでにあるとき、このフラグは警告を出すだけで、ベースラインには触れません。--offline は外部リンクのリンク切れチェックだけを省きます。

    Shell
    ./scripts/build.sh --audit --offline --update-baseline
✓ AUDIT PASSED — every publisher gate is green.

  4. ページを追加する

    PageId にコンストラクタを一つ追加します。コンパイラは、スラッグ、本文、ページ定義の match 式で分岐の追加が必要な箇所をすべて報告します。必要な分岐が一つでも欠けていると、ビルドは失敗します。

    Site/Blocks.lean
    inductive PageId
  | index
  | about
  | pricing

  5. エージェントを使う

    NoGoals には、モデルの説明、ひな形、ビルドが失敗したときの出力の読み方をまとめたエージェント用のスキルが付属しています。スキルへのリンクを作成してから、エージェントに「料金ページを追加して」と依頼してください。

    Claude Code
    mkdir -p ~/.claude/skills
ln -s "$PWD/../nogoals/skills/nogoals" ~/.claude/skills/nogoals

制限事項

  • Markdown の入力機能はありません

    内容は Lean のデータとして表現され、証明の基礎になります。長い文章は、サイト側のスクリプトを使ってファイルから Lean のデータに変換できます。

  • 対応言語は日本語と英語のみ

    文言の型には ja と en の二つのフィールドがあります。言語構成を変えるには、ジェネレーターの変更が必要です。

  • Cloudflare Pages を前提とするホスティングモデル

    このモデルは、/x/ で x/index.html を配信することや、_headers と _redirects の扱いについて、Cloudflare Pages の仕様を前提にしています。成果物はほかのホストでも配信できますが、リンク解決のモデルは Pages のものです。

  • デザインは形式化の対象外

    検証の対象は構造です。グラデーションやグリッドは形式化の対象に含まれません。