From 1532e4d57fce07e8a1cd6838853a4a31ea84e453 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 31 May 2016 23:20:21 +0200 Subject: Makefile: restore the use of coqdep_boot for creating .v.d files Coqdep_boot has almost no dependencies, and hence can be compiled very early during the build, without relying on .ml.d files. Some code of system.ml is now in a separate file minisys.ml, which is also included in system.ml for compatibility. --- tools/coqdep_common.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'tools') diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index c63e4aaa64..0f7937d729 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -9,11 +9,11 @@ open Printf open Coqdep_lexer open Unix -open System +open Minisys (** [coqdep_boot] is a stripped-down version of [coqdep], whose behavior is the one of [coqdep -boot]. Its only dependencies - are [Coqdep_lexer] and [Unix], and it should stay so. + are [Coqdep_lexer], [Unix] and [Minisys], and it should stay so. If it need someday some additional information, pass it via options (see for instance [option_natdynlk] below). *) @@ -526,7 +526,7 @@ let rec add_directory recur add_file phys_dir log_dir = | FileRegular f -> add_file phys_dir log_dir f in - System.check_unix_dir (fun s -> eprintf "*** Warning: %s\n" s) phys_dir; + check_unix_dir (fun s -> eprintf "*** Warning: %s\n" s) phys_dir; if exists_dir phys_dir then process_directory f phys_dir else -- cgit v1.2.3 From d0a9edabf59a858625d11516cdb230d223a77aeb Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 31 May 2016 12:14:55 +0200 Subject: Yet another Makefile reform : a unique phase without nasty make tricks We're back to a unique build phase (as before e372b72), but without relying on the awkward include-deps-failed-lets-retry feature of make. Since PMP has made grammar/ self-contained, we could now build grammar.cma in a rather straightforward way, no need for a specific sub-call to $(MAKE) for that. The dependencies between files of grammar/ are stated explicitely, since .d files aren't fully available initially. Some Makefile simplifications, for instance remove the CAMLP4DEPS shell horror. Instead, we generalize the use of two different filename extensions : - a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp) - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo), except coqide_main.ml4 and its specific rule Note that we do not generate .ml4.d anymore (thanks to the .mlp vs. .ml4 dichotomy) --- tools/compat5b.ml | 13 ------------- 1 file changed, 13 deletions(-) delete mode 100644 tools/compat5b.ml (limited to 'tools') diff --git a/tools/compat5b.ml b/tools/compat5b.ml deleted file mode 100644 index 37cb487c59..0000000000 --- a/tools/compat5b.ml +++ /dev/null @@ -1,13 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(*