Rewrite create_makefile.sh as a Makefile

This simplifies the build process. We now only need to type make
to launch the compilation, the Makefile will create the _CoqProject
and Makefile.coq files itself.

.gitignore

@@ -6,7 +6,7 @@
 *.html
 /html
 *.aux
-Makefile*
+Makefile.coq*
 *.crashcoqide
 *.v#
 *.cache

.gitlab-ci.yml

@@ -79,8 +79,7 @@ compile-and-doc:
     - .preferred-stable-version
   script:
     - !reference [.install-dependencies, script]
-    - ./create_makefile.sh
-    - make -j ${NJOBS}
+    - make -j ${NJOBS} all
     - !reference [.make-html, script]
   artifacts:
     name: "prosa-spec-$CI_COMMIT_REF_NAME"
@@ -97,8 +96,7 @@ compile-and-doc-and-validate:
     - .preferred-stable-version
   script:
     - !reference [.install-dependencies, script]
-    - ./create_makefile.sh
-    - make -j ${NJOBS}
+    - make -j ${NJOBS} all
     - !reference [.make-html, script]
     - make validate 2>&1 | tee validation-results.txt
     - scripts/check-validation-output.sh --accept-proof-irrelevance validation-results.txt
@@ -118,7 +116,6 @@ compile-and-validate:
     - .preferred-stable-version
   script:
     - !reference [.install-dependencies, script]
-    - ./create_makefile.sh --without-refinements
     - make -j ${NJOBS}    
     - make validate 2>&1 | tee validation-results.txt
     - scripts/check-validation-output.sh validation-results.txt
@@ -161,7 +158,7 @@ proof-state:
   script:
     - eval $(opam env "--switch=${COMPILER_EDGE}" --set-switch)
     - !reference [.install-dependencies, script]
-    - ./create_makefile.sh
+    - make -j ${NJOBS} all
     - make -j ${NJOBS} alectryon
   artifacts:
     name: "prosa-proof-state-$CI_COMMIT_REF_NAME"

Makefile

+# Makefile for Prosa
+
+COQ_PROJ := _CoqProject
+COQ_MAKEFILE := Makefile.coq
+FIND_OPTS := . -name '*.v' ! -name '*\#*' ! -path './.git/*' ! -path './with-proof-state/*'
+
+default: prosa
+
+all: allCoqProject
+	$(MAKE) $(COQ_MAKEFILE)
+	$(MAKE) -f $(COQ_MAKEFILE)
+
+prosa: prosaCoqProject
+	$(MAKE) $(COQ_MAKEFILE)
+	$(MAKE) -f $(COQ_MAKEFILE)
+
+refinements: refinementsCoqProject
+	$(MAKE) $(COQ_MAKEFILE)
+	$(MAKE) -f $(COQ_MAKEFILE)
+
+commonCoqProject:
+	@$(RM) -f $(COQ_PROJ)
+	@echo "# Automatically created by make, do not edit" > $(COQ_PROJ)
+	@echo "# (edit Makefile instead)" >> $(COQ_PROJ)
+	@echo "" >> $(COQ_PROJ)
+	@echo "-arg \"-w -notation-overriden,-parsing,-projection-no-head-constant\"" >> $(COQ_PROJ)
+	@echo "" >> $(COQ_PROJ)
+
+allCoqProject: commonCoqProject
+	@echo "-R . prosa" >> $(COQ_PROJ)
+	@echo "" >> $(COQ_PROJ)
+	@find $(FIND_OPTS) \
+	  -print | scripts/module-toc-order.py >> $(COQ_PROJ)
+
+prosaCoqProject: commonCoqProject
+	@echo "-R . prosa" >> $(COQ_PROJ)
+	@echo "" >> $(COQ_PROJ)
+	@find $(FIND_OPTS) \
+	  ! -path './implementation/refinements/*' \
+	  -print | scripts/module-toc-order.py >> $(COQ_PROJ)
+
+refinementsCoqProject: commonCoqProject
+	@echo "-R implementation/refinements prosa.implementation.refinements" >> $(COQ_PROJ)
+	@echo "" >> $(COQ_PROJ)
+	@find $(FIND_OPTS) \
+	  -path './implementation/refinements/*' \
+	  -print | scripts/module-toc-order.py >> $(COQ_PROJ)
+
+$(COQ_MAKEFILE): $(COQ_PROJ) scripts/Makefile.coq.patch
+	@coq_makefile -f $< -o $@
+	@# Patch HTML target to switch out color, and 
+	@# so that it parses comments and has links to ssreflect.
+	@# Also include Makefile.coqdocjs for 'htmlpretty' documentation target.
+	@patch -s < scripts/Makefile.coq.patch
+
+install html gallinahtml htmlpretty clean cleanall validate alectryon: $(COQ_MAKEFILE)
+	$(MAKE) -f $(COQ_MAKEFILE) $@
+
+%.vo: %.v
+	$(MAKE) -f $(COQ_MAKEFILE) $@
+
+vacuum: cleanall
+	@echo 'VACUUMING *.vo *.glob .*.aux <empty directories>'
+	@find . -depth \( -iname '*.vo' -or  -iname '*.glob' -or -iname '.*.aux' \)  ! -path './.git/*' -delete
+	@find . -depth -type d -empty ! -path './.git/*' -delete
+
+macos-clean:
+	@echo 'CLEAN .DS_Store'
+	@find . -depth -iname '.DS_Store' ! -path './.git/*' -delete
+
+spell:
+	./scripts/flag-typos-in-comments.sh `find .  -iname '*.v'`
+
+distclean: cleanall
+	$(RM) $(COQ_PROJ)
+
+help:
+	@echo "You can run:"
+	@echo "'make' or 'make prosa' to build Prosa main development"
+	@echo "'make refinements' to build the refinement part only"
+	@echo "    (requires the main development to be installed)"
+	@echo "'make all' to build everything"
+	@echo "'make install' to install previously compiled files"
+	@echo "'make htmlpretty' to build the documentation based on CoqdocJS"
+	@echo "    (can hide/show proofs)"
+	@echo "'make gallinahtml' to build the documentation without proofs"
+	@echo "'make html' to build the documentation with all proofs"
+	@echo "'make clean' to remove generated files"
+	@echo "'make vacumm' to clean .vo .glob .aux files and empty dirs"
+	@echo "'make macos-clean' to clean macos' .DS_Store dirs"
+	@echo "'make distclean' to remove all generated files"
+
+.PHONY: all prosa refinements
+.PHONY: commonCoqProject allCoqProject prosaCoqProject refinementsCoqProject
+.PHONY: install html gallinahtml htmlpretty clean cleanall validate alectryon
+.PHONY: vacuum macos-clean spell distclean help

README.md

@@ -110,31 +110,35 @@ Prosa always tracks the latest stable versions of Coq and ssreflect. We do not m
 
 #### Compiling Prosa
 
-Assuming all dependencies are available (either via OPAM or compiled from source, see the [Prosa setup instructions](http://prosa.mpi-sws.org/setup-instructions.html)), compiling Prosa consists of only two steps.
-
-First, create an appropriate `Makefile`.
+Assuming all dependencies are available (either via OPAM or compiled from source, see the [Prosa setup instructions](http://prosa.mpi-sws.org/setup-instructions.html)), compiling Prosa can be done by just typing:
 
 ```bash
-./create_makefile.sh
+make -j
 ```
 
-To avoid compiling the POET-related refinements (which require CoqEAL to be installed and inject a dependency on the *proof irrelevance* axiom), specify the switch `--without-refinements`. For example:
+Depending on how powerful your machine is, this will take a few minutes.
+
+The library can then be installed with:
 
 ```bash
-./create_makefile.sh --without-refinements
+make install
 ```
 
-Second, compile the library.
+To compile the POET-related refinements (which require CoqEAL to be installed and inject a dependency on the *proof irrelevance* axiom), first install the main Prosa library with the two commands above, then type:
 
 ```bash
-make -j
+make refinements
 ```
 
-Depending on how powerful your machine is, this will take a few minutes.
+The newly compiled files can then be installed with:
+
+```bash
+make install
+```
 
 ## Generating HTML Documentation
 
-The Coqdoc documentation (as shown on the [webpage](http://prosa.mpi-sws.org/documentation.html)) can be easily generated with the provided `Makefile`:
+Once the has been library compiled, the Coqdoc documentation (as shown on the [webpage](http://prosa.mpi-sws.org/documentation.html)) can be easily generated with:
 
 - `make htmlpretty -j`  --- pretty documentation based on CoqdocJS (can hide/show proofs),
 - `make gallinahtml -j` --- just the specification, without proofs,

coq-prosa-refinements.opam

@@ -8,8 +8,7 @@ bug-reports: "https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/issues"
 license: "BSD-2-Clause"
 
 build: [
-  ["./create_makefile.sh" "--only-refinements"]
-  [make "-j%{jobs}%"]
+  [make "-j%{jobs}%" "refinements"]
 ]
 install: [make "install"]
 depends: [

coq-prosa.opam

@@ -8,7 +8,6 @@ bug-reports: "https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/issues"
 license: "BSD-2-Clause"
 
 build: [
-  ["./create_makefile.sh" "--without-refinements"]
   [make "-j%{jobs}%"]
 ]
 install: [make "install"]

create_makefile.sh

-#!/bin/bash 
-
-# options passed to `find` for locating relevant source files
-FIND_OPTS=( . -name '*.v' ! -name '*#*' ! -path './.git/*' ! -path './with-proof-state/*' )
-
-CoqProjectR="-R . prosa"
-CoqProjectContent="-arg \"-w -notation-overriden,-parsing,-projection-no-head-constant\""
-
-while ! [ -z "$1" ]
-do
-    case "$1" in
-        --without-refinements)
-            FIND_OPTS+=( ! -path './implementation/refinements/*' )
-            ;;
-        --only-refinements)
-            FIND_OPTS+=( -path './implementation/refinements/*' )
-            CoqProjectR="-R implementation/refinements prosa.implementation.refinements"
-            ;;
-        *)
-            echo "Unrecognized option: $1"
-            exit 1
-            ;;
-    esac
-    shift
-done
-
-rm -f _CoqProject
-echo "# Automatically created by create_makefile.sh, do not edit" > _CoqProject
-echo "${CoqProjectR}" >> _CoqProject
-echo "${CoqProjectContent}" >> _CoqProject
-
-FIND_OPTS+=( -print )
-
-# Compile all relevant *.v files
-coq_makefile -f _CoqProject $(find "${FIND_OPTS[@]}" | scripts/module-toc-order.py ) -o Makefile
-
-# Patch HTML target to switch out color, and 
-# so that it parses comments and has links to ssreflect.
-# Also include Makefile.coqdocjs for 'htmlpretty' documentation target.
-patch -s < scripts/Makefile.patch

scripts/Makefile.patch → scripts/Makefile.coq.patch

---- Makefile.orig	2021-10-04 11:15:22.592822933 +0200
-+++ Makefile	2021-10-04 11:17:18.684584261 +0200
+--- Makefile.coq.orig	2021-10-04 11:15:22.592822933 +0200
++++ Makefile.coq	2021-10-04 11:17:18.684584261 +0200
 @@ -15,6 +15,11 @@
  SELF := $(lastword $(MAKEFILE_LIST))
  PARENT := $(firstword $(MAKEFILE_LIST))
@@ -42,21 +42,3 @@
  # FIXME: not quite right, since the output name is different
  gallinahtml: GAL=-g
  gallinahtml: html
-@@ -646,6 +658,17 @@
- 	$(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx)
- .PHONY: archclean
- 
-+vacuum:: cleanall
-+	$(SHOW)'VACUUMING *.vo *.glob .*.aux <empty directories>'
-+	$(HIDE)find . -depth \( -iname '*.vo' -or  -iname '*.glob' -or -iname '.*.aux' \)  ! -path './.git/*' -delete
-+	$(HIDE)find . -depth -type d -empty ! -path './.git/*' -delete
-+
-+macos-clean::
-+	$(SHOW)'CLEAN .DS_Store'
-+	$(HIDE)find . -depth -iname '.DS_Store' ! -path './.git/*' -delete
-+
-+spell::
-+	./scripts/flag-typos-in-comments.sh `find .  -iname '*.v'`
- 
- # Compilation rules ###########################################################
- 

scripts/check-validation-output.sh

@@ -24,7 +24,7 @@ OBSERVED="/tmp/observed-validation-output"
 EXPECTED="/tmp/expected-validation-output"
 
 # strip the list of files and COQDEP output
-grep -v 'COQDEP VFILES' "$RESULTS" | grep -v '"coqchk" -silent' > "$OBSERVED"
+grep -v 'COQDEP VFILES' "$RESULTS" | grep -v 'make' | grep -v '"coqchk" -silent' > "$OBSERVED"
 
 if [ -z "$ACCEPT_PI" ]
 then
@@ -71,7 +71,7 @@ then
 
     # strip the list of files, COQDEP output, and 
     # filter bogus ltac: axioms (see Coq issue 13324)
-    grep -v 'COQDEP VFILES' "$RESULTS" | grep -v '"coqchk" -silent' | grep -v "ltac_gen_subproof" > "$OBSERVED"
+    grep -v 'COQDEP VFILES' "$RESULTS" | grep -v 'make' | grep -v '"coqchk" -silent' | grep -v "ltac_gen_subproof" > "$OBSERVED"
     # the list of axioms should now be an empty list
     if ! diff --brief  "$EXPECTED" "$OBSERVED" > /dev/null
     then

[Björn Brandenburg]

@proux — I just noticed this doesn't seem to pass on the -j option. As a result, it seems slow-but-parallelizable targets like alectryon don't benefit from multiple cores. Am I missing something?

[Björn Brandenburg]

Mh, nevermind. I guess it's passed implicitly. At least it seems to work on my machine at home. It's just slow in CI.

[Pierre Roux]

Ok, my reading of GNU make documentation was indeed that $(MAKE) should pass the options directly without need for +$(MAKE).