0

I understand what I believe is the essence of the official utilties doc https://coq.inria.fr/refman/practical-tools/utilities.html#building-a-coq-project:

  • one creates a _CoqProject with arguments to coqc and the file names to compile (hopefully in an order that takes into account dependencies)
  • then one make an automatic CoqMakefile with coq_makefile -f _CoqProject -o CoqMakefile
  • Then you use their recommended Makefile to run the automatically generated make file.

But then if we need other dependencies, it doesn't say how to install them (or uninstall) them. What is the standard way to do that?

My guess is that one likely adds a target to your Makefile at the end of it and do some sort of opam install?

e.g.

# KNOWNTARGETS will not be passed along to CoqMakefile
KNOWNTARGETS := CoqMakefile
# KNOWNFILES will not get implicit targets from the final rule, and so
# depending on them won't invoke the submake. TODO: Not sure what this means
# Warning: These files get declared as PHONY, so any targets depending
# on them always get rebuilt -- or better said, any rules which those names will have their cmds be re-ran (which is
# usually rebuilding functions since that is what make files are for)
KNOWNFILES := Makefile _CoqProject

# Runs invoke-coqmakefile rule if you do run make by itself. Sets the default goal to be used if no targets were specified on the command line.
.DEFAULT_GOAL := invoke-coqmakefile

# Depends on two files to run this, itself and our _CoqProject
CoqMakefile: Makefile _CoqProject
    $(COQBIN)coq_makefile -f _CoqProject -o CoqMakefile

# Note make knows what is the make file in this case thanks to -f CoqMakefile
invoke-coqmakefile: CoqMakefile install_external_dependencies
    $(MAKE) --no-print-directory -f CoqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))

#
.PHONY: invoke-coqmakefile $(KNOWNFILES)

####################################################################
##                      Your targets here                         ##
####################################################################

# This should be the last rule, to handle any targets not declared above
%: invoke-coqmakefile
    @true

# I know this is not a good coq dependency example but just to make it concrete wrote some opam command
install_external_dependencies:
    opam install coq-serapi

I think I wrote the install_external_dependencies in the right place but I'm not sure. Is that correct? Anyone has a real example?

For all the code see: https://github.com/brando90/ultimate-utils/tree/master/tutorials_for_myself/my_makefile_playground/beginner_coq_project_with_makefiles/debug_proj

related: question on official tutorial for building coq projects https://coq.discourse.group/t/official-place-to-learn-how-to-setup-coq-make-files-for-beginner/1682

Btw, I don't understand the last like in the makefile yet.

# This should be the last rule, to handle any targets not declared above
%: invoke-coqmakefile
    @true

i.e.

  • %true in the make file template coq gave us.
  • % in the name of the rule.
  • What does that line do?

Update

I'm seeking an end-to-end small demo of how to install all dependencies with whatever the recommended approach when using _CoqProject and coq_makefile as shown in the utilities doc https://coq.inria.fr/refman/practical-tools/utilities.html. The ideal answer would contain a single script to install and compile everything in one go -- say in a install_project_name.sh. Including opam switches etc.

Related:

halfer
  • 19,824
  • 17
  • 99
  • 186
Charlie Parker
  • 5,884
  • 57
  • 198
  • 323

1 Answers1

1

The simplest setup is to install external dependencies manually with opam.

opam install packages-needed-by-my-project

Then they will be immediately available to build your own project.

The next level of organization is to package up your project. Refer to the following Coq community resources:

The main thing immediately relevant to your question is to have a *.opam file at the root of your project which lists its dependencies (possibly with version requirements). Then you can install them using opam install . --deps-only.

The Makefile part of your question is about a bit of overengineering for passing options seamlessly to CoqMakefile. I'm not sure how it works off-hand, but it's not important anyway, especially because Dune is superseding make as the recommended build system for Coq project.

Li-yao Xia
  • 31,896
  • 2
  • 33
  • 56
  • So the usual work flow is to run `opam install coq-project-name.opam` as recommended by (https://github.com/coq-community/manifesto/wiki/Recommended-Project-Structure) before I start developing? Assuming I have the right `opam switch` already created for the project I assume? – Charlie Parker Jun 11 '22 at 18:27
  • Also, something I care about is when there are many projects I want to build and one to build them one by one automatically. So I'm not only interested in running the right commands as I develop. Ideally I want to have a perfect install for my project that sets up absolutely everything (including the opam switch) and install everything automatically. Ideally removes it to or at least I can switch to another project easily if wanted. – Charlie Parker Jun 11 '22 at 18:30
  • Once you have opam packages for everything then you can write a simple script to `opam install` everything. For very large projects I would add the advice to rather use opam only for building dependencies, and then build all of your code as one big dune project. Then that's a matter of reading the dune documentation on Coq and looking at how other packages are set up, like https://github.com/mattam82/Coq-Equations or https://github.com/DeepSpec/InteractionTrees/ – Li-yao Xia Jun 11 '22 at 18:57
  • 1
    Note that you can have different [opam switches](https://opam.ocaml.org/doc/Manual.html#Switches) for different projects. Changing projects is then as simple as calling `opam switch SwitchName`, no uninstalling + reinstalling needed. You can even have a directory automatically use a dedicated opam switch with `opam link SwitchName DIR`. – Ana Borges Jun 11 '22 at 20:44
  • @Li-yaoXia ah, but I only know how to use `_CoqProject` and `make` right now :(. Def would appreciate an example or something with dune for the future...but perhaps I will try to focus on one thing at a time -- prioritizing the makefile `_CoqProject` cofnfig for now. On the dune stuff I will like read https://coq.inria.fr/refman/practical-tools/utilities.html in the future. – Charlie Parker Jun 13 '22 at 22:49
  • the issue is that I am trying to automatically compile many projects at once for non-standard uses of Coq. So there might be many ways the Coq project has been installed with. Is it possible to install **with opam** (or in harmony with opam) a Coq project that only has a `make` file or `CoqMakefile`? – Charlie Parker Aug 19 '22 at 23:18
  • You can make a library installable with opam by adding a my-library.opam file to its directory and registering the directory with `opam pin` – Li-yao Xia Aug 20 '22 at 07:45
  • can that be done automatically? e.g. by looping through the hundreds of coq projs I have & automatically making the `*.opam` file? – Charlie Parker Aug 20 '22 at 13:14
  • can a `coq_proj.opam` file be made automatically from a coq project that has a way to install it with make? e.g. coq proj https://github.com/UCSD-PL/proverbot9001/tree/master/coq-projects/Categories or https://github.com/UCSD-PL/proverbot9001/tree/master/coq-projects/additions – Charlie Parker Aug 20 '22 at 13:24
  • perhaps if I could install the coq proj with `make` (the ones without a `*.opam` file) and then create the file like they do in pip for python with `pip freeze > requirements.txt` (https://stackoverflow.com/questions/31684375/automatically-create-requirements-txt). Is that possible in opam if I installed the coq proj though `make`? – Charlie Parker Aug 20 '22 at 14:36