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! 
But unfortunately doesn’t have a chapter for this less mathy/fun thing like developing the an actually (small dummy) project.
