如何从 Coq 项目/包中自动创建一个“COQ_PROJ.opam”安装脚本？

Question

我有一个很长的 coq 项目列表，我想用opam pin/install. 我想用 opam 安装它们，因为我正在使用这个使用 opam pin/install 的 python 工具（PyCoq）。COQ_PROJ.opam / *.opam给定一个可以使用 make 安装的 coq 项目，如何自动创建一个文件？

例如，适合我的 coq 项目/包 (proj/pkg) 的格式是这样的：https: //github.com/IBM/pycoq/tree/main/pycoq/test/lf

---

一个想法是，在 pip 中，我们可以轻松地从已安装的 python 项目创建 pip 需求文件（自动创建requirements.txt）。因此，一种可能的解决方案是：

1. 使用 make （或其说明）安装 coq 项目
2. pip freeze > requirements.txt运行与 but for coq等效的命令。

如何做到这一点？

---

coq 项目的示例列表：

[
    {
        "project_name": "constructive-geometry",
        "train_files": [
            "problems.v",
            "affinity.v",
            "basis.v",
            "orthogonality.v",
            "part1.v",
            "part3.v",
            "part2.v"
        ],
        "test_files": [],
        "switch": "coq-8.10"
    },
    {
        "project_name": "higman-s",
        "train_files": [
            "inductive_wqo.v",
            "higman_aux.v",
            "higman.v",
            "list_embeding.v",
            "tree.v"
        ],
        "test_files": [],
        "switch": "coq-8.10"
    },
    {
        "project_name": "int-map",
        "train_files": [
            "Mapcanon.v",
            "Mapc.v",
            "Mapaxioms.v",
            "Map.v",
            "Adalloc.v",
            "Fset.v",
            "Mapsubset.v",
            "Mapfold.v",
            "Maplists.v",
            "Lsort.v",
            "Mapcard.v",
            "Allmaps.v",
            "FMapIntMap.v",
            "Mapiter.v"
        ],
...

---

我确实知道，opam switch export/import/create但我怀疑它是否有效，原因如下：

I think opam switch export assumes that everything I've installed so far was already available in your opam switch already: Save the current switch state to a file.. Thus I think it assumes that you've installed everything so far with opam which is not always true for every coq project afaik and if it were I wouldn't have this issue in the first place -- since I would have used opam pin/install in the first place to install the coq proj/pkg. I think some coq projects/packages use a coq_makefile -f _CoqProject -o CoqMakefile followed by a make command (ref: https://coq.inria.fr/refman/practical-tools/utilities.html#building-a-coq-project, /sf/ask/5081044671/). Those that use make are my target. I know make can run arbitrary code but I am hoping there is a standard way to install things in coq that will help me connect it with opam...or python...

虽然我可以尝试运行make，然后opam switch export虽然我不知道opam如何知道如何编译并获取依赖项（如果make仅使用coqc或其他不将其安装到opam的东西）...有什么想法吗？

也许有用的自包含 coq proj/pkg：https://github.com/brando90/pycoq/tree/main/debug_proj尽管它目前不使用外部依赖项:(，为了举例而帮助扩展它，甚至是最简单的依赖关系欢迎！

---

参考：

• Proverbot 的讨论：https://github.com/UCSD-PL/proverbot9001/issues/27
• 原始 coq-gym 存储库中的问题/讨论：https://github.com/princeton-vl/CoqGym/discussions/77
• coq 项目：https://github.com/UCSD-PL/proverbot9001/tree/master/coq-projects
• 安装 coq projs 的有用参考：在 Coq 项目中安装外部依赖项的最佳实践是什么？
• 我的 PyCoq 分支中的 .gitissue：https ://github.com/brando90/pycoq/issues/4
• https://coq.zulipchat.com/#narrow/stream/252087-Machine-learning-and-automation/topic/Installation.20of.20a.20diverse.20set.20of.20Coq.20package.20for.20ML/near/294876190