From 1596cdbb2e97f2353236e35fb07be05efe6d1a84 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 11 Nov 2020 17:07:14 +0100 Subject: Configure default value of -native-compiler This an implementation of point 2 of CEP coq/ceps#48 https://github.com/coq/ceps/pull/48 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. --- config/coq_config.mli | 3 ++- configure.ml | 35 ++++++++++++++++++++++++++++------- toplevel/coqargs.ml | 10 ++++------ toplevel/coqargs.mli | 3 ++- 4 files changed, 36 insertions(+), 15 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/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; -- cgit v1.2.3 From 04b5b2e8367ab01a2e9a0a1b511f8fa6cdb60a0f Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 13 Nov 2020 11:09:29 +0100 Subject: Add default value of -native-compiler to `coqc -config` --- lib/envars.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) 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") -- cgit v1.2.3 From 146415fb624c182493d46413d738a3c2c3f47e02 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 13 Nov 2020 12:03:19 +0100 Subject: [CI] Update coq_makefile --- test-suite/coq-makefile/coqdoc1/run.sh | 9 +++++++++ test-suite/coq-makefile/coqdoc2/run.sh | 9 +++++++++ test-suite/coq-makefile/mlpack1/run.sh | 5 +++++ test-suite/coq-makefile/mlpack2/run.sh | 5 +++++ test-suite/coq-makefile/multiroot/run.sh | 9 +++++++++ test-suite/coq-makefile/native1/run.sh | 2 +- test-suite/coq-makefile/native2/run.sh | 2 +- test-suite/coq-makefile/plugin1/run.sh | 5 +++++ test-suite/coq-makefile/plugin2/run.sh | 5 +++++ test-suite/coq-makefile/plugin3/run.sh | 5 +++++ test-suite/coq-makefile/timing/run.sh | 3 +++ test-suite/coq-makefile/uninstall1/run.sh | 3 +++ test-suite/coq-makefile/uninstall2/run.sh | 3 +++ 13 files changed, 63 insertions(+), 2 deletions(-) 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 < desired < desired < desired < desired < desired < desired < desired < desired < desired < desired < desired < desired < desired < desired < desired < desired < desired < desired < actual sort -u > desired < actual sort -u > desired <&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"; \ -- cgit v1.2.3 From 673849ed6d0218be566fc9391a77bbed09cb387b Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 13 Nov 2020 17:00:10 +0100 Subject: [CI] Deactivate native-compiler in some jobs A few libraries in the CI don't compile with it (out of memory). --- dev/ci/ci-bedrock2.sh | 1 + dev/ci/ci-color.sh | 1 + dev/ci/ci-compcert.sh | 1 + dev/ci/ci-coqprime.sh | 1 + dev/ci/ci-corn.sh | 1 + dev/ci/ci-engine_bench.sh | 1 + dev/ci/ci-equations.sh | 1 + dev/ci/ci-fiat_crypto.sh | 1 + dev/ci/ci-fiat_crypto_legacy.sh | 1 + dev/ci/ci-fiat_crypto_ocaml.sh | 1 + dev/ci/ci-fiat_parsers.sh | 1 + dev/ci/ci-hott.sh | 4 +++- dev/ci/ci-metacoq.sh | 1 + dev/ci/ci-perennial.sh | 1 + dev/ci/ci-rewriter.sh | 1 + dev/ci/ci-unimath.sh | 1 + dev/ci/ci-vst.sh | 1 + 17 files changed, 19 insertions(+), 1 deletion(-) 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 ) -- cgit v1.2.3 From c95512bc5716fc477948ae5e4947afe9dca2976d Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 15 Nov 2020 12:26:54 +0100 Subject: Add changelog --- doc/changelog/07-commands-and-options/13352-cep-48.rst | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 doc/changelog/07-commands-and-options/13352-cep-48.rst 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 `_ + (`#13352 `_, + by Pierre Roux). -- cgit v1.2.3