6

I have a very long list of coq projects I want to automatically install with opam pin/install. I'd like to install them with opam because I am using this python tool (PyCoq) that uses opam pin/install. How can I automatically create a COQ_PROJ.opam / *.opam file given a coq project that I can install with make?

For example, a format of a coq project/package (proj/pkg) that works for me is this: https://github.com/IBM/pycoq/tree/main/pycoq/test/lf

An idea is that in pip one can easily create a pip requirements file from a python project that is already installed (Automatically create requirements.txt). Thus, one possible solution could be:

  1. install the coq project with make (or it's instructions)
  2. run the equivalent of pip freeze > requirements.txt but for coq.

How does one do that?

sample list of coq projs:

[
    {
        "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"
        ],
...

I do know about opam switch export/import/create but I doubt it works due to this reason:

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, https://stackoverflow.com/questions/72586352/what-is-the-best-practice-for-installing-external-dependencies-in-a-coq-project). 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...

though I could try running make and then opam switch export though I don't know how opam would know how make compiled and got dependencies if make uses only coqc or something else that doesn't install it to opam...any ideas?

Perhaps useful self contained coq proj/pkg: https://github.com/brando90/pycoq/tree/main/debug_proj though it uses no external dependencies for now :(, help extending it for even the simplest depedency for the sake of example is welcomed!

references:

Charlie Parker
  • 5,884
  • 57
  • 198
  • 323
  • How do you know the dependencies of your projects so you can install them with make in the first place? – Li-yao Xia Aug 21 '22 at 08:56
  • @Li-yaoXia great question! I think the assumption I am making is that when `opam` is not used to install things in coq but only `make` there is some sort of common structure to most/many coq projects/packages that we can leverage. So as described in the question https://stackoverflow.com/questions/72586352/what-is-the-best-practice-for-installing-external-dependencies-in-a-coq-project the `coq_makefile -f _CoqProject -o CoqMakefile` followed by `make` might help us locate where the dependencies have been compiled to (plus user standard ways to use coq). I assume `coqc` might also be helpful. – Charlie Parker Aug 21 '22 at 15:32
  • yes, `make` can run arbitrary code which makes this question in principle impossible, but what makes it trackable is that I that I'm assuming there must be some structure to have coq projects are installed when only `make` (or `coqc`) are used that one can use to create the `coq_pkg_proj.opam` I want to make. – Charlie Parker Aug 21 '22 at 15:34
  • @Li-yaoXia would they be in the `_CoqProject` file? see a small debug demo I made: https://github.com/brando90/pycoq/blob/main/debug_proj/_CoqProject (though my proj/pkg is so simple it uses no dependencies and it lists only the `*.v` filenames for my proj/pkg. – Charlie Parker Aug 21 '22 at 15:54
  • 1
    In the pre-opam era (which most academic coq projects are stuck in), it's usually up to users to install dependencies, and `coqc` will automatically find installed packages as their modules are `Require`-d. This means dependencies are not recorded anywhere for non-opam users, and `opam` files are precisely where that's done nowadays. – Li-yao Xia Aug 21 '22 at 16:15
  • It might be that most of your packages don't have any dependencies beyond coq and perhaps some widely used packages that you somehow have already installed, in which case the simplest `opam` file would suffice for all of them. – Li-yao Xia Aug 21 '22 at 16:17

0 Answers0