diff options
37 files changed, 142 insertions, 21 deletions
diff --git a/config/coq_config.mli b/config/coq_config.mli index 12856cb6e6..809fa3d758 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -57,4 +57,5 @@ val wwwstdlib : string val localwwwrefman : string val bytecode_compiler : bool -val native_compiler : bool +type native_compiler = NativeOff | NativeOn of { ondemand : bool } +val native_compiler : native_compiler diff --git a/configure.ml b/configure.ml index 6a4b1f9a75..e32f780a3d 100644 --- a/configure.ml +++ b/configure.ml @@ -225,6 +225,8 @@ let short_date, full_date = get_date () type ide = Opt | Byte | No +type nativecompiler = NativeYes | NativeNo | NativeOndemand + type preferences = { prefix : string option; local : bool; @@ -252,7 +254,7 @@ type preferences = { bin_annot : bool; annot : bool; bytecodecompiler : bool; - nativecompiler : bool; + nativecompiler : nativecompiler; coqwebsite : string; force_caml_version : bool; force_findlib_version : bool; @@ -288,7 +290,8 @@ let default = { bin_annot = false; annot = false; bytecodecompiler = true; - nativecompiler = not (os_type_win32 || os_type_cygwin); + nativecompiler = + if os_type_win32 || os_type_cygwin then NativeNo else NativeOndemand; coqwebsite = "http://coq.inria.fr/"; force_caml_version = false; force_findlib_version = false; @@ -332,6 +335,12 @@ let get_ide = function | "no" -> No | s -> raise (Arg.Bad ("(opt|byte|no) argument expected instead of "^s)) +let get_native = function + | "yes" -> NativeYes + | "no" -> NativeNo + | "ondemand" -> NativeOndemand + | s -> raise (Arg.Bad ("(yes|no|ondemand) argument expected instead of "^s)) + let arg_bool f = Arg.String (fun s -> prefs := f !prefs (get_bool s)) let arg_string f = Arg.String (fun s -> prefs := f !prefs s) @@ -346,6 +355,8 @@ let arg_clear_option f = Arg.Unit (fun () -> prefs := f !prefs (Some false)) let arg_ide f = Arg.String (fun s -> prefs := f !prefs (Some (get_ide s))) +let arg_native f = Arg.String (fun s -> prefs := f !prefs (get_native s)) + let arg_profile = Arg.String (fun s -> prefs := Profiles.get s !prefs) (* TODO : earlier any option -foo was also available as --foo *) @@ -407,8 +418,11 @@ let args_options = Arg.align [ " Dumps ml binary annotation files while compiling Coq (e.g. for Merlin)"; "-bytecode-compiler", arg_bool (fun p bytecodecompiler -> { p with bytecodecompiler }), "(yes|no) Enable Coq's bytecode reduction machine (VM)"; - "-native-compiler", arg_bool (fun p nativecompiler -> { p with nativecompiler }), - "(yes|no) Compilation to native code for conversion and normalization"; + "-native-compiler", arg_native (fun p nativecompiler -> { p with nativecompiler }), + "(yes|no|ondemand) Compilation to native code for conversion and normalization + yes: -native-compiler option of coqc will default to 'yes', stdlib will be precompiled + no: no native compilation available at all + ondemand (default): -native-compiler option of coqc will default to 'ondemand', stdlib will not be precompiled"; "-coqwebsite", arg_string (fun p coqwebsite -> { p with coqwebsite }), " URL of the coq website"; "-force-caml-version", arg_set (fun p force_caml_version -> { p with force_caml_version }), @@ -991,6 +1005,9 @@ let esc s = if String.contains s ' ' then "\"" ^ s ^ "\"" else s (** * Summary of the configuration *) +let pr_native = function + | NativeYes -> "yes" | NativeNo -> "no" | NativeOndemand -> "ondemand" + let print_summary () = let pr s = printf s in pr "\n"; @@ -1016,7 +1033,7 @@ let print_summary () = pr " Web browser : %s\n" browser; pr " Coq web site : %s\n" !prefs.coqwebsite; pr " Bytecode VM enabled : %B\n" !prefs.bytecodecompiler; - pr " Native Compiler enabled : %B\n\n" !prefs.nativecompiler; + pr " Native Compiler enabled : %s\n\n" (pr_native !prefs.nativecompiler); if !prefs.local then pr " Local build, no installation...\n" else @@ -1095,7 +1112,11 @@ let write_configml f = pr_s "wwwstdlib" (!prefs.coqwebsite ^ "distrib/V" ^ coq_version ^ "/stdlib/"); pr_s "localwwwrefman" ("file:/" ^ docdir ^ "/html/refman"); pr_b "bytecode_compiler" !prefs.bytecodecompiler; - pr_b "native_compiler" !prefs.nativecompiler; + pr "type native_compiler = NativeOff | NativeOn of { ondemand : bool }\n"; + pr "let native_compiler = %s\n" + (match !prefs.nativecompiler with + | NativeYes -> "NativeOn {ondemand=false}" | NativeNo -> "NativeOff" + | NativeOndemand -> "NativeOn {ondemand=true}"); let core_src_dirs = [ "config"; "lib"; "clib"; "kernel"; "library"; "engine"; "pretyping"; "interp"; "gramlib"; "gramlib/.pack"; "parsing"; "proofs"; @@ -1217,7 +1238,7 @@ let write_makefile f = pr "# Option to control compilation and installation of the documentation\n"; pr "WITHDOC=%s\n\n" (if !prefs.withdoc then "all" else "no"); pr "# Option to produce precompiled files for native_compute\n"; - pr "NATIVECOMPUTE=%s\n" (if !prefs.nativecompiler then "-native-compiler yes" else ""); + pr "NATIVECOMPUTE=%s\n" (if !prefs.nativecompiler = NativeYes then "-native-compiler yes" else ""); pr "COQWARNERROR=%s\n" (if !prefs.warn_error then "-w +default" else ""); close_out o; Unix.chmod f 0o444 diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh index 8570c34194..524555b69c 100755 --- a/dev/ci/ci-bedrock2.sh +++ b/dev/ci/ci-bedrock2.sh @@ -6,4 +6,5 @@ ci_dir="$(dirname "$0")" FORCE_GIT=1 git_download bedrock2 +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make && make install ) diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index a0094b1006..72fc613c43 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")" git_download color +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/color" && make ) diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 9cb7a65ab5..6b09726606 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -5,6 +5,7 @@ ci_dir="$(dirname "$0")" git_download compcert +export COQCOPTS='-native-compiler no -w -undeclared-scope -w -omega-is-deprecated' ( cd "${CI_BUILD_DIR}/compcert" && \ ./configure -ignore-coq-version x86_32-linux && \ make && \ diff --git a/dev/ci/ci-coqprime.sh b/dev/ci/ci-coqprime.sh index a4fd296896..e12c36e6a7 100755 --- a/dev/ci/ci-coqprime.sh +++ b/dev/ci/ci-coqprime.sh @@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")" git_download coqprime +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/coqprime" && make && make install) diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh index ac3978dc8d..785ff4c2ad 100755 --- a/dev/ci/ci-corn.sh +++ b/dev/ci/ci-corn.sh @@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")" git_download corn +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/corn" && ./configure.sh && make && make install ) diff --git a/dev/ci/ci-engine_bench.sh b/dev/ci/ci-engine_bench.sh index fda7649f88..d976356dd4 100755 --- a/dev/ci/ci-engine_bench.sh +++ b/dev/ci/ci-engine_bench.sh @@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")" git_download engine_bench +export COQEXTRAFLAGS='-native-compiler ondemand' ( cd "${CI_BUILD_DIR}/engine_bench" && make coq && make coq-perf-Sanity ) diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh index 30047e624b..3eda7161c1 100755 --- a/dev/ci/ci-equations.sh +++ b/dev/ci/ci-equations.sh @@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")" git_download equations +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci && make install ) diff --git a/dev/ci/ci-fiat_crypto.sh b/dev/ci/ci-fiat_crypto.sh index 3ecdb32a51..e8fa8c0be4 100755 --- a/dev/ci/ci-fiat_crypto.sh +++ b/dev/ci/ci-fiat_crypto.sh @@ -18,6 +18,7 @@ fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1" fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} pre-standalone-extracted printlite lite" fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all-except-compiled" +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ ulimit -s ${fiat_crypto_CI_STACKSIZE} && \ make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} ) diff --git a/dev/ci/ci-fiat_crypto_legacy.sh b/dev/ci/ci-fiat_crypto_legacy.sh index 6d0a803401..57cc121bb4 100755 --- a/dev/ci/ci-fiat_crypto_legacy.sh +++ b/dev/ci/ci-fiat_crypto_legacy.sh @@ -9,5 +9,6 @@ git_download fiat_crypto_legacy fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite-hardcoded old-pipeline-lite-hardcoded lite-display-hardcoded" fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem-hardcoded old-pipeline-nobigmem-hardcoded nonautogenerated-specific nonautogenerated-specific-display selected-specific selected-specific-display" +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \ make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} ) diff --git a/dev/ci/ci-fiat_crypto_ocaml.sh b/dev/ci/ci-fiat_crypto_ocaml.sh index 20d3deb14f..c63690d5c9 100755 --- a/dev/ci/ci-fiat_crypto_ocaml.sh +++ b/dev/ci/ci-fiat_crypto_ocaml.sh @@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")" fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1" +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/fiat_crypto" && make ${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml lite-generated-files ) diff --git a/dev/ci/ci-fiat_parsers.sh b/dev/ci/ci-fiat_parsers.sh index ac74ebf667..8409e25bdc 100755 --- a/dev/ci/ci-fiat_parsers.sh +++ b/dev/ci/ci-fiat_parsers.sh @@ -6,4 +6,5 @@ ci_dir="$(dirname "$0")" FORCE_GIT=1 git_download fiat_parsers +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/fiat_parsers" && make parsers parsers-examples && make fiat-core ) diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 4b92c8cb4d..679bef3b5e 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -5,4 +5,6 @@ ci_dir="$(dirname "$0")" git_download hott -( cd "${CI_BUILD_DIR}/hott" && ./autogen.sh -skip-submodules && ./configure && make && make validate ) +( cd "${CI_BUILD_DIR}/hott" && ./autogen.sh -skip-submodules && ./configure \ + && sed -i.bak 's/\(HOQC =.*\)/\1 -native-compiler no/' Makefile \ + && make && make validate ) diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh index 27876d68de..813ea9b07a 100755 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-metacoq.sh @@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")" git_download metacoq +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/metacoq" && ./configure.sh local && make .merlin && make ci-local && make install ) diff --git a/dev/ci/ci-perennial.sh b/dev/ci/ci-perennial.sh index 306cbdf63c..43add8254a 100755 --- a/dev/ci/ci-perennial.sh +++ b/dev/ci/ci-perennial.sh @@ -6,4 +6,5 @@ ci_dir="$(dirname "$0")" FORCE_GIT=1 git_download perennial +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/perennial" && git submodule update --init --recursive && make TIMED=false lite ) diff --git a/dev/ci/ci-rewriter.sh b/dev/ci/ci-rewriter.sh index 235482ffeb..ec7ac5bddc 100755 --- a/dev/ci/ci-rewriter.sh +++ b/dev/ci/ci-rewriter.sh @@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")" git_download rewriter +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/rewriter" && make && make install) diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh index 704e278a4b..3d320617f2 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")" git_download unimath +export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/unimath" && make BUILD_COQ=no ) diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 4a332406a2..a151cf0ba6 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -7,4 +7,5 @@ git_download vst export COMPCERT=bundled +sed -i.bak 's/\(COQC=.*\)/\1 -native-compiler no/' ${CI_BUILD_DIR}/vst/Makefile ( cd "${CI_BUILD_DIR}/vst" && make IGNORECOQVERSION=true ) diff --git a/doc/changelog/07-commands-and-options/13352-cep-48.rst b/doc/changelog/07-commands-and-options/13352-cep-48.rst new file mode 100644 index 0000000000..cb2eeea74b --- /dev/null +++ b/doc/changelog/07-commands-and-options/13352-cep-48.rst @@ -0,0 +1,12 @@ +- **Changed:** + Option -native-compiler of the configure script now impacts the + default value of the option -native-compiler of coqc. The + -native-compiler option of the configure script is added an ondemand + value, which becomes the default, thus preserving the previous default + behavior. + The stdlib is still precompiled when configuring with -native-compiler + yes. It is not precompiled otherwise. + This an implementation of point 2 of + `CEP #48 <https://github.com/coq/ceps/pull/48>`_ + (`#13352 <https://github.com/coq/coq/pull/13352>`_, + by Pierre Roux). diff --git a/lib/envars.ml b/lib/envars.ml index c9c97eaa97..585d5185b4 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -181,5 +181,9 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs = fprintf f "%sWARN=%s\n" prefix_var_name "-warn-error +a-3"; fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name (if Coq_config.has_natdynlink then "true" else "false"); - fprintf f "%sCOQ_SRC_SUBDIRS=%s\n" prefix_var_name (String.concat " " coq_src_subdirs) - + fprintf f "%sCOQ_SRC_SUBDIRS=%s\n" prefix_var_name (String.concat " " coq_src_subdirs); + fprintf f "%sCOQ_NATIVE_COMPILER_DEFAULT=%s\n" prefix_var_name + (match Coq_config.native_compiler with + | Coq_config.NativeOn {ondemand=false} -> "yes" + | Coq_config.NativeOff -> "no" + | Coq_config.NativeOn {ondemand=true} -> "ondemand") diff --git a/test-suite/Makefile b/test-suite/Makefile index 279f32c903..6a7cc0428c 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -252,7 +252,12 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ + (echo "\ + bugs/closed/bug_3783.v \ + bugs/closed/bug_4157.v \ + bugs/closed/bug_5127.v \ + " | grep -q "$<") && no_native="-native-compiler no"; \ + $(coqc) $$no_native "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index 88237815b1..d878b13ce6 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -21,6 +21,10 @@ make install-doc DSTROOT="$PWD/tmp" sort -u > desired <<EOT . ./test +./test/.coq-native +./test/.coq-native/Ntest_test.cmi +./test/.coq-native/Ntest_test.cmx +./test/.coq-native/Ntest_test.cmxs ./test/test_plugin.cmi ./test/test_plugin.cmx ./test/test_plugin.cmxa @@ -29,6 +33,10 @@ sort -u > desired <<EOT ./test/test.v ./test/test.vo ./test/sub +./test/sub/.coq-native +./test/sub/.coq-native/Ntest_sub_testsub.cmi +./test/sub/.coq-native/Ntest_sub_testsub.cmx +./test/sub/.coq-native/Ntest_sub_testsub.cmxs ./test/sub/testsub.glob ./test/sub/testsub.v ./test/sub/testsub.vo @@ -56,4 +64,5 @@ sort -u > desired <<EOT ./test/html/coqdoc.css ./test/html/test.test.html EOT +(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired exec diff -u desired actual diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh index 5811dd17e4..757667e8bd 100755 --- a/test-suite/coq-makefile/coqdoc2/run.sh +++ b/test-suite/coq-makefile/coqdoc2/run.sh @@ -19,6 +19,10 @@ make install-doc DSTROOT="$PWD/tmp" sort -u > desired <<EOT . ./test +./test/.coq-native +./test/.coq-native/Ntest_test.cmi +./test/.coq-native/Ntest_test.cmx +./test/.coq-native/Ntest_test.cmxs ./test/test_plugin.cmi ./test/test_plugin.cmx ./test/test_plugin.cmxa @@ -27,6 +31,10 @@ sort -u > desired <<EOT ./test/test.v ./test/test.vo ./test/sub +./test/sub/.coq-native +./test/sub/.coq-native/Ntest_sub_testsub.cmi +./test/sub/.coq-native/Ntest_sub_testsub.cmx +./test/sub/.coq-native/Ntest_sub_testsub.cmxs ./test/sub/testsub.glob ./test/sub/testsub.v ./test/sub/testsub.vo @@ -54,4 +62,5 @@ sort -u > desired <<EOT ./test/html/coqdoc.css ./test/html/test.test.html EOT +(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired exec diff -u desired actual diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh index bbd2fc460c..113a862d97 100755 --- a/test-suite/coq-makefile/mlpack1/run.sh +++ b/test-suite/coq-makefile/mlpack1/run.sh @@ -12,6 +12,10 @@ make install DSTROOT="$PWD/tmp" sort > desired <<EOT . ./test +./test/.coq-native +./test/.coq-native/Ntest_test.cmi +./test/.coq-native/Ntest_test.cmx +./test/.coq-native/Ntest_test.cmxs ./test/test.glob ./test/test_plugin.cmi ./test/test_plugin.cmx @@ -20,4 +24,5 @@ sort > desired <<EOT ./test/test.v ./test/test.vo EOT +(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired exec diff -u desired actual diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh index bbd2fc460c..113a862d97 100755 --- a/test-suite/coq-makefile/mlpack2/run.sh +++ b/test-suite/coq-makefile/mlpack2/run.sh @@ -12,6 +12,10 @@ make install DSTROOT="$PWD/tmp" sort > desired <<EOT . ./test +./test/.coq-native +./test/.coq-native/Ntest_test.cmi +./test/.coq-native/Ntest_test.cmx +./test/.coq-native/Ntest_test.cmxs ./test/test.glob ./test/test_plugin.cmi ./test/test_plugin.cmx @@ -20,4 +24,5 @@ sort > desired <<EOT ./test/test.v ./test/test.vo EOT +(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired exec diff -u desired actual diff --git a/test-suite/coq-makefile/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh index 45bf1481df..be0d04f93d 100755 --- a/test-suite/coq-makefile/multiroot/run.sh +++ b/test-suite/coq-makefile/multiroot/run.sh @@ -20,6 +20,10 @@ make install-doc DSTROOT="$PWD/tmp" sort > desired <<EOT . ./test +./test/.coq-native +./test/.coq-native/Ntest_test.cmi +./test/.coq-native/Ntest_test.cmx +./test/.coq-native/Ntest_test.cmxs ./test/test.glob ./test/test.cmi ./test/test.cmx @@ -30,6 +34,10 @@ sort > desired <<EOT ./test/test.v ./test/test.vo ./test2 +./test2/.coq-native +./test2/.coq-native/Ntest2_test.cmi +./test2/.coq-native/Ntest2_test.cmx +./test2/.coq-native/Ntest2_test.cmxs ./test2/test.glob ./test2/test.v ./test2/test.vo @@ -58,4 +66,5 @@ sort > desired <<EOT ./orphan_test_test2_test/mlihtml/type_Test_aux.html ./orphan_test_test2_test/mlihtml/type_Test.html EOT +(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired exec diff -u desired actual diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index 3ffe831b3c..5dd36757be 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -1,6 +1,6 @@ #!/usr/bin/env bash -NONATIVECOMP=$(grep "let native_compiler = false" ../../../config/coq_config.ml)||true +NONATIVECOMP=$(grep "let native_compiler = NativeOff" ../../../config/coq_config.ml)||true if [[ $(which ocamlopt) && ! $NONATIVECOMP ]]; then . ../template/init.sh diff --git a/test-suite/coq-makefile/native2/run.sh b/test-suite/coq-makefile/native2/run.sh index aaae81630f..47befc50c3 100755 --- a/test-suite/coq-makefile/native2/run.sh +++ b/test-suite/coq-makefile/native2/run.sh @@ -1,6 +1,6 @@ #!/usr/bin/env bash -NONATIVECOMP=$(grep "let native_compiler = false" ../../../config/coq_config.ml)||true +NONATIVECOMP=$(grep "let native_compiler = NativeOff" ../../../config/coq_config.ml)||true if [[ $(which ocamlopt) && ! $NONATIVECOMP ]]; then . ../template/init.sh diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh index 1e2bd979b3..f69e8c1b8c 100755 --- a/test-suite/coq-makefile/plugin1/run.sh +++ b/test-suite/coq-makefile/plugin1/run.sh @@ -13,6 +13,10 @@ make install DSTROOT="$PWD/tmp" sort > desired <<EOT . ./test +./test/.coq-native +./test/.coq-native/Ntest_test.cmi +./test/.coq-native/Ntest_test.cmx +./test/.coq-native/Ntest_test.cmxs ./test/test.glob ./test/test.cmi ./test/test.cmx @@ -23,4 +27,5 @@ sort > desired <<EOT ./test/test.v ./test/test.vo EOT +(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired exec diff -u desired actual diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh index 1e2bd979b3..f69e8c1b8c 100755 --- a/test-suite/coq-makefile/plugin2/run.sh +++ b/test-suite/coq-makefile/plugin2/run.sh @@ -13,6 +13,10 @@ make install DSTROOT="$PWD/tmp" sort > desired <<EOT . ./test +./test/.coq-native +./test/.coq-native/Ntest_test.cmi +./test/.coq-native/Ntest_test.cmx +./test/.coq-native/Ntest_test.cmxs ./test/test.glob ./test/test.cmi ./test/test.cmx @@ -23,4 +27,5 @@ sort > desired <<EOT ./test/test.v ./test/test.vo EOT +(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired exec diff -u desired actual diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh index 1e2bd979b3..f69e8c1b8c 100755 --- a/test-suite/coq-makefile/plugin3/run.sh +++ b/test-suite/coq-makefile/plugin3/run.sh @@ -13,6 +13,10 @@ make install DSTROOT="$PWD/tmp" sort > desired <<EOT . ./test +./test/.coq-native +./test/.coq-native/Ntest_test.cmi +./test/.coq-native/Ntest_test.cmx +./test/.coq-native/Ntest_test.cmxs ./test/test.glob ./test/test.cmi ./test/test.cmx @@ -23,4 +27,5 @@ sort > desired <<EOT ./test/test.v ./test/test.vo EOT +(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/\.coq-native/d' desired exec diff -u desired actual diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index ed5a4f93f5..426c9ea53f 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -3,6 +3,9 @@ #set -x set -e +NONATIVECOMP=$(grep "let native_compiler = NativeOff" ../../../config/coq_config.ml)||true +if [[ ! $NONATIVECOMP ]]; then exit 0 ; fi + . ../template/path-init.sh # reset MAKEFLAGS so that, e.g., `make -C test-suite -B coq-makefile` doesn't give us issues diff --git a/test-suite/coq-makefile/uninstall1/run.sh b/test-suite/coq-makefile/uninstall1/run.sh index fc95d84b9a..0f05acd072 100755 --- a/test-suite/coq-makefile/uninstall1/run.sh +++ b/test-suite/coq-makefile/uninstall1/run.sh @@ -19,5 +19,8 @@ make uninstall-doc DSTROOT="$PWD/tmp" ) | sort -u > actual sort -u > desired <<EOT . +./test +./test/sub EOT +(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/test/d' desired exec diff -u desired actual diff --git a/test-suite/coq-makefile/uninstall2/run.sh b/test-suite/coq-makefile/uninstall2/run.sh index fc95d84b9a..0f05acd072 100755 --- a/test-suite/coq-makefile/uninstall2/run.sh +++ b/test-suite/coq-makefile/uninstall2/run.sh @@ -19,5 +19,8 @@ make uninstall-doc DSTROOT="$PWD/tmp" ) | sort -u > actual sort -u > desired <<EOT . +./test +./test/sub EOT +(coqc -config | grep -q "NATIVE_COMPILER_DEFAULT=yes") || sed -i.bak '/test/d' desired exec diff -u desired actual diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index c6ccf2a427..ec339c69c6 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -36,7 +36,8 @@ let set_type_in_type () = type color = [`ON | `AUTO | `EMACS | `OFF] -type native_compiler = NativeOff | NativeOn of { ondemand : bool } +type native_compiler = Coq_config.native_compiler = + NativeOff | NativeOn of { ondemand : bool } type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; @@ -96,10 +97,7 @@ type t = { let default_toplevel = Names.(DirPath.make [Id.of_string "Top"]) -let default_native = - if Coq_config.native_compiler - then NativeOn {ondemand=true} - else NativeOff +let default_native = Coq_config.native_compiler let default_logic_config = { impredicative_set = Declarations.PredicativeSet; @@ -301,7 +299,7 @@ let get_native_compiler s = | ("no" | "off") -> NativeOff | _ -> error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler") in - if not Coq_config.native_compiler && n <> NativeOff then + if Coq_config.native_compiler = NativeOff && n <> NativeOff then let () = warn_no_native_compiler s in NativeOff else diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index c8634b7847..f6222e4ec4 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -12,7 +12,8 @@ type color = [`ON | `AUTO | `EMACS | `OFF] val default_toplevel : Names.DirPath.t -type native_compiler = NativeOff | NativeOn of { ondemand : bool } +type native_compiler = Coq_config.native_compiler = + NativeOff | NativeOn of { ondemand : bool } type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; |