Official place to learn how to setup Coq make files for beginner

I come from interpreted languages, so I have little to no knowledge how the set up for Coq should be so that I can have it in the right project structure and so that it works with make etc.

Is there an official place to learn this? I found a list of a few but didn’t feel they were super beginner friendly (or perhaps they assumed I have experience with make files, compiled languages? not sure). But I am very happy to learn all I need to do it I’m just unsure where to start or what to use. Not sure if trying something unrelated like compiling an ocaml project with make is a good idea first or something else.

Any pointer or advice is welcome!

References I found and was deciding which to go through:

My dummy coq project is very simple:

Require Import Omega.

 Theorem t:
    forall n: nat, 1 + n > n.
 Proof.
 intro.
 omega.
 Qed.

probably is enough for learning?

Thanks!

I think someone was working on writing beginner-friendly documentation for this, perhaps @ejgallego?

In the meantime, this is not really a tutorial but it helped me back in the day: Coq community’s Recomended Project Structure. You don’t need everything described there to start. It is enough to organize the files you already have in the way described there (in particular, place Coq files inside theories), create a Makefile by copying the one described there (no changes needed), and create a _CoqProject by copying the one described there and replacing ModuleN.v with the names of your Coq files. That’s it, you don’t need any of the other files.

Now in order to compile your project just use make on a terminal. You can erase compiled files with make clean (in case weird things are happening and you wish to try the equivalent of “turn it off and on again”).

Once you have some file A.v and you wish to use things defined there in another file, first make sure A.v has been compiled (with make) and then add the following line to the top of the new file:

From ProjectName Require Import A.

where ProjectName is the string you included at the top of your _CoqProject (called ProjectName in the example). Require tells Coq to look for stuff in A and Import makes it so that you don’t need to write A.thing to refer to some thing that was defined in A.


Unrelated, but omega has been deprecated for a while and was removed in Coq version 8.14 (the latest is 8.15.2). If you are using a recent Coq version, which you should be, then omega won’t be available. The recommended alternative is lia, which you can use after Require Import Lia.

3 Likes

I’ve been working on this documentation. While it hasn’t been reviewed and isn’t in the manual yet, you can probably gain something by reading the pull request here.

2 Likes

@ana-borges @jfehrle will check them out!

But yes we def need a tutorial friendly to beginners in compilation for Coq and proj organization/structure. For example I opened up two projects to see an example:

and some don’t even have a _CoqProject folder (which is the main thing this official doc talks about Utilities — Coq 8.15.2 documentation). Also, some the commands in the examples I’ve seen are rather hairy e.g.

all: Makefile.coq
	@+$(MAKE) -f Makefile.coq all

clean: Makefile.coq
	@+$(MAKE) -f Makefile.coq cleanall
	@rm -f Makefile.coq Makefile.coq.conf

Makefile.coq: _CoqProject
	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq

force _CoqProject Makefile: ;

%: Makefile.coq force
	@+$(MAKE) -f Makefile.coq $@

.PHONY: all clean force

for people like me that never have written a make file before. Not sure if these comments are useful but I’m doing my best to go through the links provided. It’s not clear to me what is truly needed and what is not or the simplest best practice way to make a project.

For example one beginner question, that would help ppl like me. Do I need 1. a Make file? or 2. a _CoqProject file or 3. Something in Dune?

Other question like what is the difference between normal make vs coq_makefile? When should we use one or the other?

@brando90 If your Coq code is in a single .v file, you can do your work interactively using CoqIDE or one of the other IDEs. No makefile is necessary. When you need/want multiple files, create a _CoqProject file and run coq_makefile to generate a makefile. Most people don’t need to modify the makefile. If you want to use external packages in your project, you’ll want to install them. The “Coq platform” can install many of them, or you can use opam.

It’s good to state your goal and what you’ve tried so far when you pose a question. I’m guessing that makefiles are likely irrelevant for you at this point.

If you want to learn how to use Coq, many people find Software Foundations helpful.

1 Like

hi Jim! Thanks for the very useful message you sent me. It was helpful (e.g. I didn’t know most ppl didn’t need to modify the make or know it’s contents).

Let me tell you more or less where I am at. I didn’t say that exactly because it seemed to me that the tutorial I was looking for was looking so helping me in my specific issues wasn’t going to solve that (and potentially distract my real question which is a good beginner tutorial for making coq projects with it’s dependencies).

Happy to clarify though.

I am currently going through the official utilities docs Utilities — Coq 8.15.2 documentation. I think I understand now that I do not need to worry about the Makefile – which wasn’t obvious to a beginner coq project developer (like me) – since I would have assumed its useful since other languages do use it like C. I think from our conversation and the [utilities docs](https://Utilities — Coq 8.15.2 documentation) I can infer that most of the stuff to build the project seems to go inside the _CoqProject, including the flags for compilation using coqc and the relevant files in the project. Is this true? What if I want to include dependencies outside of Coq e.g. in python we would call pip to install those dependencies. e.g. what if I want to run an old coq version and use the deprecated omega tactic – which to my best understanding needs an installation or something? Do I put all the installation in the _CoqProject?

I was trying to learn to do this by example by I see comp cert doesn’t have a _CoqProject nor does a constructive geometry file. Actually this one only has coqc args:

-R coq FormalML -arg -set -arg "Warnings=+default,-ambiguous-path,-typechecker,-ssr-search-moved,-deprecated"

which threw me off.

Also, in addition, what is really confusing (to me) from the utilities doc is that the path to the folder where the coq project lives is a relative path. e.g.

-R theories/ MyCode
-arg "-w all"
theories/foo.v
theories/bar.v
-I src/
src/baz.mlg
src/bazaux.ml
src/qux_plugin.mlpack

or a real project (ails):

-R . AILS pi_ineq.v trajectory_const.v rrho.v trajectory_def.v constants.v ycngftys.v ycngstys.v ails_def.v math_prop.v tau.v ails.v trajectory.v measure2state.v ails_trajectory.v alarm.v alpha_no_conflict.v correctness.v

the second argument is a . dot. Which seems to imply that whatever tool that is used to compile the project (which now I know the round about way is actually the coq_makefile that makes the make file that then is used to compile the actual project). So in the utilities docs it doesn’t say but I assume that we run

coq_makefile -f _CoqProject -o CoqMakefile

in a special way since the _CoqProject uses relative paths?

In python some people make the root of the github repo the project. Others make a seperate folder or any arbitrary nesting. Either way with the way the current docs are written I can’t for sure know what is going on. But I will continue running commands pseudo-randomly hoping they teach me what I should do?

Also note my current file is really dum/small (for the same of debugging):

Theorem add_easy_0:
forall n:nat,
  0 + n = n.
Proof.
    Show Proof.
    intros.
    Show Proof.
    simpl.
    Show Proof.
    reflexivity.
    Show Proof.
Qed.

attempted _CoqProject:

-Q . debug_proj
-arg "-w all"

debug_0_plus_n_eq_n.v

but since I am only playing with proofs I’m not sure even how to check if the compilation I ran is actually successful. e.g. in C or ocaml I could at least run hello world or something on the executable.

Let’s add the complexity that I want to do this through coq-serapi and eventually python bindings. Which makes it even more confusing.

PS: I am familiar with software foundations…it’s great! :slight_smile: But unfortunately doesn’t have a chapter for this less mathy/fun thing like developing the an actually (small dummy) project.

Since it might be worth to emphasize on it’s own since I made a lot of comments in the previous post.

Where do the external “pip”/opam, dependencies go? do they go in the _CoqProject? How does one install them once they are in the right place? Do I need to have an opam switch for each?

I plan to go through a bunch of projects and build them one at a time. Then throw it away etc. repeatedly. How do this for example for 2 projects as an example. Do I need to “uninstall” the previous projects dependencies or something for things to work properly?

Please read the “Configuration Basics” section in the link I sent you. I think that answers some of your questions.

I was trying to learn to do this by example by I see comp cert doesn’t have a _CoqProject nor does a constructive geometry file.

_CoqProject is the easiest/best practice but not required. The -Q . debug_proj must eventually be passed as arguments to coqc or coqide. It’s also possible to give the contents of _CoqProject as CLI parameters to coq_makefile. The IDEs apply the parameters specificed in _CoqProject when you try to step through a script.

You should run coq_makefile from the directory containing _CoqProject. Then the relative paths will be good.

What if I want to include dependencies outside of Coq e.g. in python we would call pip to install those dependencies.

Please read the material in the link first.

e.g. what if I want to run an old coq version and use the deprecated omega tactic – which to my best understanding needs an installation or something?

omega was bundled into Coq. You need a From ... Require ... to refer to it. The manual covered that.

You should use the IDE and ignore Show Proof for now. Try to do some of the exercises in Software Foundations:

Let’s add the complexity that I want to do this through coq-serapi and eventually python bindings.

What will that accomplish?

I plan to go through a bunch of projects and build them one at a time. Then throw it away etc. repeatedly. How do this for example for 2 projects as an example. Do I need to “uninstall” the previous projects dependencies or something for things to work properly?

Read the link I sent you. It depends on the project and whether the dependencies are compatible. You can install multiple projects at once if they’re compatible Why don’t you look at things that can be installed with Coq platform and/or opam? Among other things, it depends on whether the dependencies are for the

I know how to use CoqIde or vscode in Coq. I don’t really need to step through the proof that’s not my point. What I want is to learn to build coq projects.

Will check the link you sent in a bit. Trying to go through the utilities doc Utilities — Coq 8.15.2 documentation first a bit more.

I’m curious, is there a specific part of the wonderful SF book that you had in mind I should check – related to packaging projects? e.g. using make, coq_makefile, _CoqProject, opam for installing depedencies, opam for managing coq versions and stuff like that? Or was it a general recommendation? (note I’ve been through it and done proofs there, it’s a great book!)

Curious, do people usually put these makefiles etc in the .gitignore? (since they are built automatically)


also, related to what makes things difficult for beginners. Although I am familiar with Coq I’m not familiar with makefiles and opam. So when I see files and vocabulary like target it’s unclear to me if that is a coq or a make file thing. Now that I’ve about make files (sort of randomly unfortunately since I didn’t know what I needed to read nor in what order). Anyway, not really a complaint, just trying to help once this tutorial does get built if it does at all :slight_smile:


Last thing for me to understand the makefile the utilities doc gives:

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

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

TODO:

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

I’m curious, is there a specific part of the wonderful SF book that you had in mind I should check – related to packaging projects? e.g. using make

I’ve not seen that material in SF.

Although I am familiar with Coq I’m not familiar with makefiles and opam.

There are many excellent sources of information on makefiles. It’s much better documented than Coq. You don’t need to know much about opam. Look at the installation instructions for Coq on the Coq website.

Will check the link you sent in a bit.

Please check out the link before asking more questions.