Merge PR #12411: Add support for CoqMakefile.local-late

Reviewed-by: gares
Reviewed-by: jfehrle
Co-authored-by: gares <gares@users.noreply.github.com>

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

@@ -0,0 +1,5 @@
+- **Added:**
+  ``coq_makefile``\-made ``Makefile``\s now support inclusion of a
+  ``.local-late`` file at the end, allowing the user to access
+  more variables (`#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

@@ -152,14 +152,27 @@ Including the generated makefile with an include directive is
 discouraged, since the contents of this file, including variable names and
 status of rules, may change in the future.
 
-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:
+Use the optional file ``CoqMakefile.local`` to extend
+``CoqMakefile``. In particular, you can declare custom actions to run
+before or after the build process. Similarly you can customize the
+install target or even provide new targets. See
+:ref:`coqmakefilelocal` for extension-point documentation. Although
+you can use all variables defined in ``CoqMakefile`` in the *recipes*
+of rules that you write and in the definitions of any variables that
+you assign with ``=``, many variables are not available for use if you
+assign variable values with ``:=`` nor to define the *targets* of
+rules nor in top-level conditionals such as ``ifeq``. Additionally,
+you must use `secondary expansion
+<https://www.gnu.org/software/make/manual/html_node/Secondary-Expansion.html>`_
+to make use of such variables in the prerequisites of rules. To access
+variables defined in ``CoqMakefile`` in rule target computation,
+top-level conditionals, and ``:=`` variable assignment, for example to
+add new dependencies to compiled outputs, use the optional file
+``CoqMakefile.local-late``.  See :ref:`coqmakefilelocallate` for a
+non-exhaustive list of variables.
+
+The extensions of files listed in ``_CoqProject`` determine
+how they are built. In particular:
 
 
 + Coq files must use the ``.v`` extension
@@ -188,8 +201,8 @@ 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.
-Here we describe only few of them.
+section of the generated makefile.  Use
+``CoqMakefile.local-late`` instead to access more variables. These include:
 
 :CAMLPKGS:
    can be used to specify third party findlib packages, and is
@@ -273,6 +286,40 @@ The following makefile rules can be extended.
   One can append lines to the generated ``.merlin`` file extending this
   target.
 
+.. _coqmakefilelocallate:
+
+CoqMakefile.local-late
+++++++++++++++++++++++
+
+The optional file ``CoqMakefile.local-late`` is included at the end of the generated
+file ``CoqMakefile``.  The following is a partial list of accessible variables:
+
+:COQ_VERSION:
+   the version of ``coqc`` being used, which can be used to
+   provide different behavior depending on the Coq version
+:COQMAKEFILE_VERSION:
+   the version of Coq used to generate the
+   Makefile, which can be used to detect version mismatches
+:ALLDFILES:
+   the list of generated dependency files, which can be used,
+   for example, to cause ``make`` to recompute dependencies
+   when files change by writing ``$(ALLDFILES): myfiles`` or to
+   indicate that files must be generated before dependencies can
+   be computed by writing ``$(ALLDFILES): | mygeneratedfiles``
+:VOFILES, GLOBFILES, CMOFILES, CMXFILES, OFILES, CMAFILES, CMXAFILES, CMIFILES, CMXSFILES:
+   lists of files that are generated by various invocations of the compilers
+
+In addition, the following variables may be useful for
+deciding what targets to present via ``$(shell ...)``; these
+variables are already accessible in recipes for rules added in
+``CoqMakefile.local``, but are only accessible from top-level ``$(shell
+...)`` invocations in ``CoqMakefile.local-late``:
+
+:COQC, COQDEP, COQDOC, CAMLC, CAMLOPTC:
+   compiler binaries
+:COQFLAGS, CAMLFLAGS, COQLIBS, COQDEBUG, OCAMLLIBS:
+   flags passed to the Coq or OCaml compilers
+
 Timing targets and performance testing
 ++++++++++++++++++++++++++++++++++++++
 

test-suite/coq-makefile/local-late-extension/Makefile.local-late

@@ -0,0 +1,4 @@
+MYVOFILES := $(VOFILES)
+
+printvo::
+	@echo '$(MYVOFILES)'

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

@@ -0,0 +1 @@
+foo.vo

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

@@ -0,0 +1,15 @@
+#!/usr/bin/env bash
+
+. ../template/path-init.sh
+
+set -x
+coq_makefile -Q . Top foo.v -o Makefile
+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' \
+    | grep -v 'make[^:]*: Entering directory' \
+    | grep -v 'make[^:]*: Leaving directory' \
+    | grep -v 'exit 1' \
+           > make-printvo.log
+diff -u make-printvo.log.expected make-printvo.log || exit $?

tools/CoqMakefile.in

@@ -913,6 +913,11 @@ debug:
 
 .DEFAULT_GOAL := all
 
+# Users can create @LOCAL_LATE_FILE@ to hook into double-colon rules
+# or add other needed Makefile code, using defined
+# variables if necessary.
+-include @LOCAL_LATE_FILE@
+
 # Local Variables:
 # mode: makefile-gmake
 # End:

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 dep_file args project =
+let generate_makefile oc conf_file local_file local_late_file dep_file args project =
   let coqcorelib = Envars.coqcorelib () in
   let makefile_template = Filename.concat coqcorelib "tools/CoqMakefile.in" in
   if not (Sys.file_exists makefile_template) then
@@ -134,6 +134,7 @@ let generate_makefile oc conf_file local_file dep_file args project =
     (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);
@@ -434,6 +435,7 @@ 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
@@ -459,10 +461,9 @@ 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 dep_file (prog :: args) project;
+  generate_makefile ocm conf_file local_file local_late_file dep_file (prog :: args) project;
   close_out ocm;
   let occ = open_out conf_file in
   generate_conf occ project (prog :: args);
   close_out occ;
   exit 0
-