开发者

包注册指南

如何注册新的 Lean 数学包，并将审计证书提交到 NPA registry。

为保持 verified math registry 的完整性，新包必须提供密码学签名，并通过配置规则验证。请按照本指南准备要注册的包。

1. 设置 package manifest

每个数学仓库根目录都必须包含 npa-package.toml 文件。该文件定义包版本、依赖、许可证和 module 路径。

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 compiler tool 构建 Lean 文件并编译验证证书。将 .npcert 签名放入生成的 build 目录。

npa package compile --manifest npa-package.toml

在本地环境运行 verify-certs 命令，确保提交前所有签名和 hash 与文件完全一致。

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

将 package 配置添加到本网站仓库的 repositories.yaml，并提交 Pull Request。CI gate 会在合并前自动审计证书。