opam publishコマンドを使ってRocqのコードをopamに登録する

Rocqのライブラリやツールは次のリポジトリが広く使われている¹.

• rocq-released: Rocq利用者のための推奨opamリポジトリ
• rocq-extra-dev: 開発者向けリポジトリ，開発中のRocqのライブラリなどがある

両方のリポジトリは coq/opam というgithubプロジェクトで管理されており，ここに自分の開発しているプロジェクトのopamファイルを pull request することで登録申請をする．それを自動的にやってくれるのが opam publish コマンドというわけ．

rocq-released に自分のプロジェクトを登録申請する手順

1. (初回のみ) プロジェクトのopamファイルを作成する

rocq-<PROJ>.opam というような名前で作成する．

2. 自プロジェクトで新しくtagを打つ

git tag X.X.X
git push --tags

3. github上でreleaseする

https://github.com/<name>/<proj>/releases/new から新しいreleaseを上記タグ

4. (初回のみ) github アクセストークンを発行して

「Settings」→「Developpers Tool」→「Personal access tokens」→「Tokens (classic)」から「Generate new token」して，PRを発行できる権限を付けたトークンを発行する．

5. opam publish

opam publish --tag=<GIT_TAG> <OPAM_TAG> --repo=rocq-prover/opam --packages-directory released/packages <OPAMFILE> <SRC_URL>

• --tag: 自プロジェクトでのtag
• -v: opam上でのバージョン番号(tagと同じ場合が多いかも)
• --repo: packageを管理するgithubのリポジトリの場所なので今回は rocq-prover/opam
• --packages-directory: 上記リポジトリ上でのディレクトリの場所，今回は released/packages
• <OPAMFILE> : 手元にある .opam ファイル
• <SRC_URL> : ソースコードのある場所

使用例:

opam publish --tag=rocqnavi.0.3.1 -v 0.3.1 --repo=rocq-prover/opam --packages-directory released/packages rocq-navi.opam https://github.com/affeldt-aist/rocqnavi/archive/refs/tags/rocqnavi.0.3.1.tar.gz

1. https://rocq-prover.org/docs/using-opam#installing-rocq-packages ↩