Add support for CoqMakefile.local-late

This allows users to write rules that depend on variables such as
VOFILES and VDFILE, which is essential in some of my use-cases (for
example, to properly handle seamless version switching, I need to make
all of the .vo files depend on a file where I record the version of Coq
being used).

Fixes #10912

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 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).

doc/sphinx/practical-tools/utilities.rst

@@ -100,11 +100,14 @@ 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`.
+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.
 
 The extensions of the files listed in ``_CoqProject`` is used in order to
 decide how to build them. In particular:
@@ -136,8 +139,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.
-Here we describe only few of them.
+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.
 
 :CAMLPKGS:
    can be used to specify third party findlib packages, and is

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,2 @@
+echo 'foo.vo'
+foo.vo

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

@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+. ../template/path-init.sh
+
+set -x
+coq_makefile -Q . Top foo.v -o Makefile
+make printvo >make-printvo.log 2>&1
+diff -u make-printvo.log.expected make-printvo.log || exit $?

tools/CoqMakefile.in

@@ -861,6 +861,11 @@ 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
+# 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 coqlib = Envars.coqlib () in
   let makefile_template =
     let template = Filename.concat "tools" "CoqMakefile.in" in
@@ -133,6 +133,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);
@@ -413,6 +414,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
@@ -436,10 +438,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
-