開発者向け

パッケージ登録ガイド

新しいLean数学パッケージおよび監査証明書をNPAレジストリに登録する方法。

検証済み数学レジストリの整合性を維持するため、新しいパッケージは暗号署名を提供し、設定ルールを検証する必要があります。このガイドに従って、パッケージの登録準備を行ってください。

1. パッケージマニフェストのセットアップ

すべての数学リポジトリのルートに npa-package.toml ファイルを含める必要があります。これにより、パッケージバージョン、依存関係、ライセンス、およびモジュールパスが定義されます。

schema = "0.1.0"
package = "my-math-library"
version = "0.1.0"
license = "Apache-2.0"
description = "Verified theorems for group actions and rings."

NPA CLIコンパイラツールを使用してLeanファイルをビルドし、検証証明書をコンパイルします。生成されたビルドフォルダーに .npcert 署名を配置します。

npa package compile --manifest npa-package.toml

提出前に、ローカル環境で verify-certs コマンドを実行し、すべての署名とハッシュがファイルと完全に一致することを確認します。

npa package verify-certs --root . --checker reference

本ウェブサイトのリポジトリにある repositories.yaml にあなたのパッケージ設定を追加し、プルリクエストを送信します。マージ前に、CIゲートが自動的に証明書を監査します。