[configure] Move test-suite configure parts to test-suite/

This removes the `config/Makefile` file, and paves the way for further
cleanups here; hopefully the test suite can soon run on dune or some
other platform that can provide the info now present in
`test-suite/test_suite_config.inc`.

This also makes the test suite Makefile to depend on less files
outside `test-suite`.

cc coq#7149

.github/workflows/ci-macos.yml

@@ -36,7 +36,7 @@ jobs:
       - name: Build Coq
         run: |
           eval $(opam env)
-          ./configure -prefix "$(pwd)/_install_ci" -warn-error yes -native-compiler no
+          ./configure -prefix "$(pwd)/_install_ci" -native-compiler no
           make dunestrap
           dune build -p coq-core,coq-stdlib,coqide-server,coqide,coq
         env:

.gitignore

@@ -155,3 +155,4 @@ bin
 .dune-stamp
 theories/dune
 user-contrib/Ltac2/dune
+/test-suite/test_suite_config.inc

.gitlab-ci.yml

@@ -84,7 +84,7 @@ before_script:
     - dev/ci/gitlab-section.sh end coq.clean
 
     - dev/ci/gitlab-section.sh start coq.config coq.config
-    - ./configure -warn-error yes -prefix "$(pwd)/_install_ci" $COQ_EXTRA_CONF
+    - ./configure -prefix "$(pwd)/_install_ci" $COQ_EXTRA_CONF
     - dev/ci/gitlab-section.sh end coq.config
 
     - dev/ci/gitlab-section.sh start coq.build coq.build
@@ -918,7 +918,7 @@ plugin:plugin-tutorial:
   interruptible: true
   extends: .auto-use-tags
   script:
-    - ./configure -prefix "$(pwd)/_install_ci" -warn-error yes
+    - ./configure -prefix "$(pwd)/_install_ci"
     - make -j "$NJOBS" plugin-tutorial
 
 plugin:ci-quickchick:

config/coq_config.mli

@@ -9,6 +9,7 @@
 (************************************************************************)
 
 (* The fields below are absolute paths *)
+val install_prefix : string   (* Install prefix passed by the user *)
 val coqlib : string     (* where the std library is installed *)
 val configdir : string  (* where configuration files are installed *)
 val datadir : string    (* where extra data files are installed *)

config/dune

@@ -13,7 +13,7 @@
 ; Dune doesn't use configure's output, but it is still necessary for
 ; some Coq files to work; will be fixed in the future.
 (rule
- (targets coq_config.ml coq_config.py Makefile dune.c_flags)
+ (targets coq_config.ml coq_config.py dune.c_flags)
  (mode fallback)
  (deps
    %{project_root}/dev/ocamldebug-coq.run

test-suite/Makefile

@@ -21,17 +21,12 @@
 # all tests to be run, use the "clean" target.
 
 ###########################################################################
-# Includes
+# Includes, see below for generation
 ###########################################################################
 
-# If Coq is not configured, we can't run the makefile.
-ifneq ($(wildcard ../config/Makefile ../_build/default/config/Makefile),)
--include ../_build/default/config/Makefile
--include ../config/Makefile
-  COQ_NOT_CONFIGURED:=false
-else
-  COQ_NOT_CONFIGURED:=true
-endif
+# Generate test-suite, when INSIDE_DUNE the file is guaranteed to
+# exist
+include test_suite_config.inc
 
 #######################################################################
 # Variables
@@ -146,6 +141,7 @@ VSUBSYSTEMS := prerequisite success failure bugs bugs-nocoqchk output output-coq
 # All subsystems
 SUBSYSTEMS := $(VSUBSYSTEMS) misc ide ide vio coqchk output-coqchk coqwc coq-makefile tools $(UNIT_TESTS)
 
+# EJGA: This seems dangerous as first target...
 .csdp.cache: .csdp.cache.test-suite
 	cp $< $@
 	chmod u+w $@
@@ -159,15 +155,6 @@ PREREQUISITELOG = $(addsuffix .log,$(wildcard prerequisite/*.v)) .csdp.cache
 .DELETE_ON_ERROR:
 .PHONY: all run clean $(SUBSYSTEMS)
 
-ifeq ($(COQ_NOT_CONFIGURED),true)
-all:
-	@echo ""
-	@echo "Coq has not been configured, please run: "
-	@echo "  - make check"
-	@echo "Before running the test suite"
-	@echo ""
-	@false
-else
 ifeq ($(COQLIB_NOT_FOUND),true)
 all:
 	@echo ""
@@ -179,7 +166,6 @@ else
 all: run
 	$(MAKE) report
 endif
-endif
 
 # do nothing
 .PHONY: noop
@@ -188,7 +174,7 @@ noop: ;
 run: $(SUBSYSTEMS)
 
 clean:
-	rm -f trace .csdp.cache .nia.cache .lia.cache output/MExtraction.out
+	rm -f trace .csdp.cache .nia.cache .lia.cache output/MExtraction.out test_suite_config.inc
 	rm -f misc/universes/all_stdlib.v
 	$(SHOW) 'RM        <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>'
 	$(HIDE)find . \( \
@@ -262,6 +248,21 @@ summary.log:
 report: summary.log
 	$(HIDE)bash report.sh
 
+#######################################################################
+# Test suite configuration, to eventually go away
+#######################################################################
+
+# Not inside Dune, build by hand
+ifeq ($(INSIDE_DUNE),)
+# EGJA: using $(ROOT)/_build/default/... here confuses make due to quotes...
+TESTCONFIGURE:=../_build/default/test-suite/tools/coq_config_to_make.exe
+$(TESTCONFIGURE): tools/coq_config_to_make.ml
+	dune build ./tools/coq_config_to_make.exe
+
+test_suite_config.inc: $(TESTCONFIGURE)
+	$(TESTCONFIGURE) > $@
+endif
+
 #######################################################################
 # Unit tests
 #######################################################################

test-suite/dune

@@ -15,13 +15,17 @@
  (targets bin.inc)
  (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted -trailing-slash ../../install/%{context_name}/bin/ ))))
 
+(rule
+ (targets test_suite_config.inc)
+ (action (with-stdout-to %{targets} (run tools/coq_config_to_make.exe))))
+
 (rule
  (targets summary.log)
  (deps
    ; File that should be promoted.
    misc/universes/all_stdlib.v
-   ; Dependencies of the legacy makefile
-   ../config/Makefile
+   ; Configure for test-suite
+   test_suite_config.inc
    ; Stuff for the compat script test
    ../dev/header.ml
    ../dev/tools/update-compat.py

test-suite/tools/coq_config_to_make.ml

@@ -0,0 +1,46 @@
+(* Flags used to compile Coq but _not_ plugins (via coq_makefile) *)
+module Prefs = struct
+  type t = { warn_error : bool }
+  let default = { warn_error = true }
+end
+
+(** This Makefile is only used in the test-suite now, remove eventually. *)
+let write_makefile coqprefix coqlibinstall best_compiler ocamlfind caml_flags coq_caml_flags o () =
+  let pr s = Format.fprintf o s in
+  pr "###### Coq Test suite configuration ##############################\n";
+  pr "#                                                                #\n";
+  pr "# This file is generated by the script \"coq_config_to_make\"      #\n";
+  pr "# DO NOT EDIT IT !! DO NOT EDIT IT !! DO NOT EDIT IT !!          #\n";
+  pr "#                                                                #\n";
+  pr "##################################################################\n\n";
+
+  pr "# Paths where Coq is installed\n";
+  pr "COQPREFIX=%s\n" coqprefix;
+  pr "COQLIBINSTALL=%s\n\n" coqlibinstall;
+  pr "# The best compiler: native (=opt) or bytecode (=byte)\n";
+  pr "BEST=%s\n\n" best_compiler;
+  pr "# Findlib command\n";
+  pr "OCAMLFIND=%S\n" ocamlfind;
+  pr "# Caml flags\n";
+  pr "CAMLFLAGS=%s %s\n" caml_flags coq_caml_flags;
+  ()
+
+let coq_warn_error (prefs : Prefs.t) =
+    if prefs.warn_error
+    then "-warn-error +a"
+    else ""
+
+let main () =
+  let prefs = Prefs.default in
+  let coqprefix = Coq_config.install_prefix in
+  let coqlibinstall = Coq_config.coqlib in
+  (* EJGA: Good enough approximation *)
+  let best_compiler = if Coq_config.has_natdynlink then "opt" else "byte" in
+  let ocamlfind = Coq_config.ocamlfind in
+  let caml_flags = Coq_config.caml_flags in
+  let coq_caml_flags = coq_warn_error prefs in
+  Format.printf "@[%a@]@\n%!"
+    (write_makefile coqprefix coqlibinstall best_compiler ocamlfind caml_flags coq_caml_flags) ();
+  ()
+
+let () = main ()

test-suite/tools/dune

@@ -0,0 +1,3 @@
+(executable
+ (name coq_config_to_make)
+ (libraries coq-core.config))

tools/configure/cmdArgs.ml

@@ -30,7 +30,6 @@ type t = {
   bytecodecompiler : bool;
   nativecompiler : nativecompiler;
   coqwebsite : string;
-  warn_error : bool;
   debug : bool;
 }
 
@@ -52,7 +51,6 @@ let default_prefs = {
   bytecodecompiler = true;
   nativecompiler = NativeNo;
   coqwebsite = "http://coq.inria.fr/";
-  warn_error = false;
   debug = false;
 }
 
@@ -115,10 +113,10 @@ let args_options = Arg.align [
      yes: -native-compiler option of coqc will default to 'yes', stdlib will be precompiled
      no (default): no native compilation available at all
      ondemand: -native-compiler option of coqc will default to 'ondemand', stdlib will not be precompiled";
+  "-warn-error", arg_bool (fun p _warn_error -> p),
+    "Deprecated option: warnings are now adjusted in the corresponding build tool.";
   "-coqwebsite", arg_string (fun p coqwebsite -> { p with coqwebsite }),
     " URL of the coq website";
-  "-warn-error", arg_bool (fun p warn_error -> { p with warn_error }),
-    "(yes|no) Make OCaml warnings into errors (default no)";
   "-debug", arg_set (fun p -> { p with debug = true }), " Enable debug information for package detection"
 ]
 

tools/configure/cmdArgs.mli

@@ -40,8 +40,6 @@ type t =
   (** Enable/disable Coq's native compiler *)
   ; coqwebsite : string
   (** Override Coq's website, used by distributions  *)
-  ; warn_error : bool
-  (** Enable/disable warn-error in makefile build *)
   ; debug : bool
   (** Debug package and environment detection *)
   }

tools/configure/configure.ml

@@ -137,18 +137,11 @@ let check_findlib_version prefs { CamlConf.findlib_version; _ } =
 
 (* Note, we list all warnings to be complete *)
 let coq_warnings = "-w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70"
-let coq_warn_error prefs =
-    if prefs.warn_error
-    then "-warn-error +a"
-    else ""
 
 (* Flags used to compile Coq and plugins (via coq_makefile) *)
 let caml_flags =
   Printf.sprintf "-thread -bin-annot -strict-sequence %s" coq_warnings
 
-(* Flags used to compile Coq but _not_ plugins (via coq_makefile) *)
-let coq_caml_flags = coq_warn_error
-
 (** * Native compiler *)
 
 let msg_byteonly =
@@ -391,7 +384,7 @@ let print_summary prefs arch camlenv install_dirs browser =
 
 (** * Build the config/coq_config.ml file *)
 
-let write_configml camlenv coqenv caml_flags caml_version_nums arch arch_is_win32 hasnatdynlink browser prefs o =
+let write_configml install_prefix camlenv coqenv caml_flags caml_version_nums arch arch_is_win32 hasnatdynlink browser prefs o =
   let { CoqEnv.coqlib; coqlibsuffix; configdir; configdirsuffix; docdir; docdirsuffix; datadir; datadirsuffix } = coqenv in
   let { CamlConf.caml_version; _ } = camlenv in
   let pr s = fprintf o s in
@@ -404,6 +397,7 @@ let write_configml camlenv coqenv caml_flags caml_version_nums arch arch_is_win3
   pr "(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)\n";
   pr "(* Exact command that generated this file: *)\n";
   pr "(* %s *)\n\n" (String.concat " " (Array.to_list Sys.argv));
+  pr_s "install_prefix" install_prefix;
   pr_s "coqlib" coqlib;
   pr_s "configdir" configdir;
   pr_s "datadir" datadir;
@@ -466,32 +460,6 @@ let write_configml camlenv coqenv caml_flags caml_version_nums arch arch_is_win3
 
 (** * Build the config/Makefile file *)
 
-(** This Makefile is only used in the test-suite now, remove eventually. *)
-let write_makefile install_dirs best_compiler caml_flags coq_caml_flags o =
-  let pr s = fprintf o s in
-  pr "###### config/Makefile : Configuration file for Coq ##############\n";
-  pr "#                                                                #\n";
-  pr "# This file is generated by the script \"configure\"               #\n";
-  pr "# DO NOT EDIT IT !! DO NOT EDIT IT !! DO NOT EDIT IT !!          #\n";
-  pr "# If something is wrong below, then rerun the script \"configure\" #\n";
-  pr "# with the good options (see the file INSTALL).                  #\n";
-  pr "#                                                                #\n";
-  pr "##################################################################\n\n";
-
-  (* XXX: Not used anymore, or only in the test suite makefile *)
-  pr "# Paths for true installation\n";
-  List.iter (fun ((v,msg),_) -> pr "# %s: path for %s\n" v msg) install_dirs;
-  List.iter (fun ((v,_),(dir,_)) -> pr "%s=%S\n" v dir) install_dirs;
-
-  (* XXX: Only used in the test suite: BEST OCAMLFIND CAMLFLAGS ARCH *)
-  pr "# The best compiler: native (=opt) or bytecode (=byte)\n";
-  pr "BEST=%s\n\n" best_compiler;
-  pr "# Findlib command\n";
-  pr "OCAMLFIND=%S\n" camlexec.find;
-  pr "# Caml flags\n";
-  pr "CAMLFLAGS=%s %s\n" caml_flags coq_caml_flags;
-  ()
-
 let write_dune_c_flags cflags o =
   let pr s = fprintf o s in
   pr "(%s)\n" cflags
@@ -517,19 +485,17 @@ let main () =
   check_caml_version prefs camlenv.CamlConf.caml_version caml_version_nums;
   check_findlib_version prefs camlenv;
   let best_compiler = best_compiler prefs camlenv in
-  let coq_caml_flags = coq_caml_flags prefs in
   let hasnatdynlink = hasnatdynlink prefs best_compiler in
   check_for_zarith prefs;
   let install_dirs = install_dirs prefs arch in
+  let install_prefix = select "COQPREFIX" install_dirs |> fst in
   let coqenv = resolve_coqenv install_dirs in
   let cflags, sse2_math = compute_cflags () in
   check_fmath sse2_math;
   if prefs.interactive then
     print_summary prefs arch camlenv install_dirs browser;
   write_config_file ~file:"config/coq_config.ml"
-    (write_configml camlenv coqenv caml_flags caml_version_nums arch arch_is_win32 hasnatdynlink browser prefs);
-  write_config_file ~file:"config/Makefile"
-    (write_makefile install_dirs best_compiler caml_flags coq_caml_flags);
+    (write_configml install_prefix camlenv coqenv caml_flags caml_version_nums arch arch_is_win32 hasnatdynlink browser prefs);
   write_config_file ~file:"config/dune.c_flags" (write_dune_c_flags cflags);
   write_config_file ~file:"config/coq_config.py" write_configpy;
   ()