[coq_makefile] Move down local, no local-late

As per coq#12411 (comment),
instead of using a local-late file, we just move the local file down.
This means that we need to replace all the relevant := assignments with
= so that users can still override variables, and this mandates that we
split up CAMLFLAGS.

doc/changelog/08-tools/12411-makefile-local-late.rst

@@ -1,5 +1,10 @@
 - **Added:**
-  ``coq_makefile``\-made ``Makefile``\s now support inclusion of a
-  ``.local-late`` file at the very end, in case the user wants to have access
-  to more variables (`#12411 <https://github.com/coq/coq/pull/12411>`_, fixes
-  `#10912 <https://github.com/coq/coq/issues/10912>`_, by Jason Gross).
+  ``coq_makefile``\-made ``Makefile``\s now include the ``.local``
+  file at the very end, in case the user wants to have access to more
+  variables.  Note that this may break some very rare use-cases where
+  the ``.local`` file was used to override some variables in the
+  ``Makefile``; if you are making use of this, please open an issue on
+  the bug tracker and we can add back support for overriding variables
+  with inclusion of an local file earlier on (`#12411
+  <https://github.com/coq/coq/pull/12411>`_, fixes `#10912
+  <https://github.com/coq/coq/issues/10912>`_, by Jason Gross).

doc/sphinx/practical-tools/utilities.rst

@@ -100,14 +100,11 @@ CoqMakefile.conf
   |Coq|.
 
 
-An optional file ``CoqMakefile.local`` can be provided by the user in
-order to extend ``CoqMakefile``.  In particular one can declare custom
-actions to be performed before or after the build process. Similarly
-one can customize the install target or even provide new
-targets. Extension points are documented in paragraph
-:ref:`coqmakefilelocal`.  If the user needs to access variables
-defined in the ``Makefile``, the optional file
-``CoqMakefile.local-late`` can be used.
+An optional file ``CoqMakefile.local`` can be provided by the user in order to
+extend ``CoqMakefile``. In particular one can declare custom actions to be
+performed before or after the build process. Similarly one can customize the
+install target or even provide new targets. Extension points are documented in
+paragraph :ref:`coqmakefilelocal`.
 
 The extensions of the files listed in ``_CoqProject`` is used in order to
 decide how to build them. In particular:
@@ -138,10 +135,9 @@ file ``CoqMakefile``. It can contain two kinds of directives.
 
 **Variable assignment**
 
-The variable must belong to the variables listed in the ``Parameters``
-section of the generated makefile.  If access to more variables are
-needed, ``CoqMakefile.local-late`` can be used instead. Here we
-describe only few of the variables.
+The variable may belong to the variables listed in the ``Parameters``
+section of the generated makefile.
+Here we describe only few of them.
 
 :CAMLPKGS:
    can be used to specify third party findlib packages, and is

test-suite/coq-makefile/local-late-extension/make-printvo.log.expected

@@ -1,2 +1,3 @@
+COQDEP VFILES
 echo 'foo.vo'
 foo.vo

test-suite/coq-makefile/local-late-extension/run.sh

@@ -4,5 +4,6 @@
 
 set -x
 coq_makefile -Q . Top foo.v -o Makefile
-make printvo >make-printvo.log 2>&1
+rm -f .*.d *.d
+make --no-print-directory -j1 printvo 2>&1 | grep -v 'make[^:]*: warning: -jN forced in submake: disabling jobserver mode.' | grep -v 'coq_makefile -Q . Top foo.v -o Makefile' > make-printvo.log
 diff -u make-printvo.log.expected make-printvo.log || exit $?

tools/CoqMakefile.in

@@ -46,10 +46,6 @@ OCAMLWARN         := $(COQMF_WARN)
 @CONF_FILE@: @PROJECT_FILE@
 	@COQ_MAKEFILE_INVOCATION@
 
-# This file can be created by the user to hook into double colon rules or
-# add any other Makefile code he may need
--include @LOCAL_FILE@
-
 # Parameters ##################################################################
 #
 # Parameters are make variable assignments.
@@ -224,8 +220,7 @@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)")
 
 CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS)
 # ocamldoc fails with unknown argument otherwise
-CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS)))
-CAMLFLAGS+=$(OCAMLWARN)
+CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS)))
 
 ifneq (,$(TIMING))
 TIMING_ARG=-time
@@ -651,7 +646,7 @@ archclean::
 
 $(MLIFILES:.mli=.cmi): %.cmi: %.mli
 	$(SHOW)'CAMLC -c $<'
-	$(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
+	$(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(OCAMLWARN) $(CAMLPKGS) $<
 
 $(MLGFILES:.mlg=.ml): %.ml: %.mlg
 	$(SHOW)'COQPP $<'
@@ -660,53 +655,53 @@ $(MLGFILES:.mlg=.ml): %.ml: %.mlg
 # Stupid hack around a deficient syntax: we cannot concatenate two expansions
 $(filter %.cmo, $(MLFILES:.ml=.cmo) $(MLGFILES:.mlg=.cmo)): %.cmo: %.ml
 	$(SHOW)'CAMLC -c $<'
-	$(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
+	$(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(OCAMLWARN) $(CAMLPKGS) $<
 
 # Same hack
 $(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml
 	$(SHOW)'CAMLOPT -c $(FOR_PACK) $<'
-	$(HIDE)$(TIMER) $(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $<
+	$(HIDE)$(TIMER) $(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(OCAMLWARN) $(CAMLPKGS) $(FOR_PACK) $<
 
 
 $(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa
 	$(SHOW)'CAMLOPT -shared -o $@'
-	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(OCAMLWARN) $(CAMLPKGS) \
 		-linkall -shared -o $@ $<
 
 $(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib
 	$(SHOW)'CAMLC -a -o $@'
-	$(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
+	$(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(OCAMLWARN) $(CAMLPKGS) -a -o $@ $^
 
 $(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib
 	$(SHOW)'CAMLOPT -a -o $@'
-	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^
+	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(OCAMLWARN) -a -o $@ $^
 
 
 $(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa
 	$(SHOW)'CAMLOPT -shared -o $@'
-	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(OCAMLWARN) $(CAMLPKGS) \
 		-shared -linkall -o $@ $<
 
 $(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx
 	$(SHOW)'CAMLOPT -a -o $@'
-	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $<
+	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(OCAMLWARN) -a -o $@ $<
 
 $(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack
 	$(SHOW)'CAMLC -a -o $@'
-	$(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
+	$(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(OCAMLWARN) $(CAMLPKGS) -a -o $@ $^
 
 $(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack
 	$(SHOW)'CAMLC -pack -o $@'
-	$(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
+	$(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(OCAMLWARN) -pack -o $@ $^
 
 $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack
 	$(SHOW)'CAMLOPT -pack -o $@'
-	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
+	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(OCAMLWARN) -pack -o $@ $^
 
 # This rule is for _CoqProject with no .mllib nor .mlpack
 $(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx
 	$(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@'
-	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+	$(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(OCAMLWARN) $(CAMLPKGS) \
 		-shared -o $@ $<
 
 ifneq (,$(TIMING))
@@ -865,10 +860,10 @@ debug:
 
 .DEFAULT_GOAL := all
 
-# This file can be created by the user to hook into double colon rules
-# or add any other Makefile code he may need, making use of defined
+# This file can be created by the user to hook into double colon rules or
+# add any other Makefile code he may need, making use of defined
 # variables if necessary.
--include @LOCAL_LATE_FILE@
+-include @LOCAL_FILE@
 
 # Local Variables:
 # mode: makefile-gmake

tools/coq_makefile.ml

@@ -122,7 +122,7 @@ let read_whole_file s =
 
 let quote s = if String.contains s ' ' || CString.is_empty s then "'" ^ s ^ "'" else s
 
-let generate_makefile oc conf_file local_file local_late_file dep_file args project =
+let generate_makefile oc conf_file local_file dep_file args project =
   let coqlib = Envars.coqlib () in
   let makefile_template =
     let template = Filename.concat "tools" "CoqMakefile.in" in
@@ -133,7 +133,6 @@ let generate_makefile oc conf_file local_file local_late_file dep_file args proj
     (fun s (k,v) -> Str.global_substitute (Str.regexp_string k) (fun _ -> v) s) s
     [ "@CONF_FILE@", conf_file;
       "@LOCAL_FILE@", local_file;
-      "@LOCAL_LATE_FILE@", local_late_file;
       "@DEP_FILE@", dep_file;
       "@COQ_VERSION@", Coq_config.version;
       "@PROJECT_FILE@", (Option.default "" project.project_file);
@@ -414,7 +413,6 @@ let _ =
 
   let conf_file = Option.default "CoqMakefile" project.makefile ^ ".conf" in
   let local_file = Option.default "CoqMakefile" project.makefile ^ ".local" in
-  let local_late_file = Option.default "CoqMakefile" project.makefile ^ ".local-late" in
   let dep_file = "." ^ Option.default "CoqMakefile" project.makefile ^ ".d" in
 
   if project.extra_targets <> [] then begin
@@ -438,7 +436,7 @@ let _ =
   Envars.set_coqlib ~fail:(fun x -> Printf.eprintf "Error: %s\n" x; exit 1);
 
   let ocm = Option.cata open_out stdout project.makefile in
-  generate_makefile ocm conf_file local_file local_late_file dep_file (prog :: args) project;
+  generate_makefile ocm conf_file local_file dep_file (prog :: args) project;
   close_out ocm;
   let occ = open_out conf_file in
   generate_conf occ project (prog :: args);