From 169f4c322c304eddc243fd86b7823c1f3a9d9746 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 10 Nov 2023 15:42:36 +0100 Subject: [PATCH] [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`. The generation of the test-suite configuration is implemented by either a regular `dune` rule, or by taking advantage of automake. cc #7149 --- .github/workflows/ci-macos.yml | 2 +- .gitignore | 1 + .gitlab-ci.yml | 4 +-- config/coq_config.mli | 1 + config/dune | 2 +- test-suite/Makefile | 40 ++++++++++++--------- test-suite/dune | 8 +++-- test-suite/tools/coq_config_to_make.ml | 46 +++++++++++++++++++++++++ test-suite/tools/coq_config_to_make.mli | 0 test-suite/tools/dune | 3 ++ tools/configure/cmdArgs.ml | 11 +++--- tools/configure/cmdArgs.mli | 2 -- tools/configure/configure.ml | 42 +++------------------- 13 files changed, 95 insertions(+), 67 deletions(-) create mode 100644 test-suite/tools/coq_config_to_make.ml create mode 100644 test-suite/tools/coq_config_to_make.mli create mode 100644 test-suite/tools/dune diff --git a/.github/workflows/ci-macos.yml b/.github/workflows/ci-macos.yml index 14c34a5ec86b..75c2412be3eb 100644 --- a/.github/workflows/ci-macos.yml +++ b/.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: diff --git a/.gitignore b/.gitignore index 2a7a2f4da098..771ec2250dc0 100644 --- a/.gitignore +++ b/.gitignore @@ -155,3 +155,4 @@ bin .dune-stamp theories/dune user-contrib/Ltac2/dune +/test-suite/test_suite_config.inc diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index b4e32942eb05..88678b60dab1 100644 --- a/.gitlab-ci.yml +++ b/.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 @@ -915,7 +915,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: diff --git a/config/coq_config.mli b/config/coq_config.mli index 4122f02d2844..53a8e7980bea 100644 --- a/config/coq_config.mli +++ b/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 *) diff --git a/config/dune b/config/dune index a5c233b52837..07a8ea8b4104 100644 --- a/config/dune +++ b/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 diff --git a/test-suite/Makefile b/test-suite/Makefile index 28748802ae91..03652f82c370 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -21,18 +21,23 @@ # 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 +# Generate test-suite, when INSIDE_DUNE the file is guaranteed to +# exist, when called directly by make we need to look into the build +# directory. +DUNE_CONTEXT:=default +TEST_SUITE_CONFIG_FILE:=test_suite_config.inc + +ifeq ($(INSIDE_DUNE),) +TEST_SUITE_CONFIG_PATH:=../_build/$(DUNE_CONTEXT)/test-suite/$(TEST_SUITE_CONFIG_FILE) else - COQ_NOT_CONFIGURED:=true +TEST_SUITE_CONFIG_PATH:=$(TEST_SUITE_CONFIG_FILE) endif +include $(TEST_SUITE_CONFIG_PATH) + ####################################################################### # Variables ####################################################################### @@ -144,6 +149,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 $@ @@ -157,15 +163,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 "" @@ -177,7 +174,6 @@ else all: run $(MAKE) report endif -endif # do nothing .PHONY: noop @@ -260,6 +256,16 @@ summary.log: report: summary.log $(HIDE)bash report.sh +####################################################################### +# Test suite configuration, to eventually go away +####################################################################### + +# Not inside Dune, build by hand, note the shuffling +ifeq ($(INSIDE_DUNE),) +$(TEST_SUITE_CONFIG_PATH): $(TESTCONFIGURE) + dune build $(TEST_SUITE_CONFIG_FILE) +endif + ####################################################################### # Unit tests ####################################################################### diff --git a/test-suite/dune b/test-suite/dune index d862763531a5..c60e3bd6a667 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -7,13 +7,17 @@ (env (dev (flags :standard -w -70))) +(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 diff --git a/test-suite/tools/coq_config_to_make.ml b/test-suite/tools/coq_config_to_make.ml new file mode 100644 index 000000000000..b3648c18d75e --- /dev/null +++ b/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 () diff --git a/test-suite/tools/coq_config_to_make.mli b/test-suite/tools/coq_config_to_make.mli new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test-suite/tools/dune b/test-suite/tools/dune new file mode 100644 index 000000000000..b701a05a8958 --- /dev/null +++ b/test-suite/tools/dune @@ -0,0 +1,3 @@ +(executable + (name coq_config_to_make) + (libraries coq-core.config)) diff --git a/tools/configure/cmdArgs.ml b/tools/configure/cmdArgs.ml index e62736dacec0..6d090c609e29 100644 --- a/tools/configure/cmdArgs.ml +++ b/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; } @@ -80,6 +78,11 @@ let arg_native f = Arg.String (fun s -> prefs := f !prefs (get_native s)) (* TODO : earlier any option -foo was also available as --foo *) +let warn_warn_error () = + Format.eprintf "****** the -warn-error option is deprecated, \ + warnings are not set in the config section of the \ + corresponding build tool [coq_makefile, dune]@\n%!" + let check_absolute = function | None -> () | Some path -> @@ -115,10 +118,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 -> warn_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" ] diff --git a/tools/configure/cmdArgs.mli b/tools/configure/cmdArgs.mli index 8f5aa2da2c8a..fae1afe2a72d 100644 --- a/tools/configure/cmdArgs.mli +++ b/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 *) } diff --git a/tools/configure/configure.ml b/tools/configure/configure.ml index 5c00e6ecc267..67d2877de982 100644 --- a/tools/configure/configure.ml +++ b/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; ()