diff options
| -rw-r--r-- | doc/changelog/07-commands-and-options/12070-native-compiler-disabled.rst | 5 | ||||
| -rw-r--r-- | test-suite/coq-makefile/native1/_CoqProject | 2 | ||||
| -rwxr-xr-x | test-suite/coq-makefile/native2/run.sh | 2 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 39 |
4 files changed, 33 insertions, 15 deletions
diff --git a/doc/changelog/07-commands-and-options/12070-native-compiler-disabled.rst b/doc/changelog/07-commands-and-options/12070-native-compiler-disabled.rst new file mode 100644 index 0000000000..0f30b5f5e8 --- /dev/null +++ b/doc/changelog/07-commands-and-options/12070-native-compiler-disabled.rst @@ -0,0 +1,5 @@ +- **Changed:** + Ignore -native-compiler option when built without native compute + support. + (`#12070 <https://github.com/coq/coq/pull/12070>`_, + by Pierre Roux). diff --git a/test-suite/coq-makefile/native1/_CoqProject b/test-suite/coq-makefile/native1/_CoqProject index 3dfca7ffc0..85276fd9b9 100644 --- a/test-suite/coq-makefile/native1/_CoqProject +++ b/test-suite/coq-makefile/native1/_CoqProject @@ -1,6 +1,8 @@ -R src test -R theories test -I src +-arg -w +-arg +native-compiler-disabled -arg -native-compiler -arg yes diff --git a/test-suite/coq-makefile/native2/run.sh b/test-suite/coq-makefile/native2/run.sh index 857f70fdff..aaae81630f 100755 --- a/test-suite/coq-makefile/native2/run.sh +++ b/test-suite/coq-makefile/native2/run.sh @@ -7,7 +7,7 @@ if [[ $(which ocamlopt) && ! $NONATIVECOMP ]]; then coq_makefile -f _CoqProject -o Makefile cat Makefile.conf -COQEXTRAFLAGS="-native-compiler yes" make +COQEXTRAFLAGS="-w +native-compiler-disabled -native-compiler yes" make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 1988c7cc42..cfc89782a1 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -286,6 +286,30 @@ let parse_option_set opt = let v = String.sub opt (eqi+1) (len - eqi - 1) in to_opt_key (String.sub opt 0 eqi), Some v +let warn_no_native_compiler = + CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler" + Pp.(fun s -> strbrk "Native compiler is disabled," ++ + strbrk " -native-compiler " ++ strbrk s ++ + strbrk " option ignored.") + +let get_native_compiler s = + (* We use two boolean flags because the four states make sense, even if + only three are accessible to the user at the moment. The selection of the + produced artifact(s) (`.vo`, `.vio`, `.coq-native`, ...) should be done by + a separate flag, and the "ondemand" value removed. Once this is done, use + [get_bool] here. *) + let n = match s with + | ("yes" | "on") -> NativeOn {ondemand=false} + | "ondemand" -> NativeOn {ondemand=true} + | ("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 + let () = warn_no_native_compiler s in + NativeOff + else + n + (* Main parsing routine *) (*s Parsing of the command line *) @@ -455,20 +479,7 @@ let parse_args ~help ~init arglist : t * string list = { oval with config = { oval.config with enable_VM = get_bool opt (next ()) }} |"-native-compiler" -> - - (* We use two boolean flags because the four states make sense, even if - only three are accessible to the user at the moment. The selection of the - produced artifact(s) (`.vo`, `.vio`, `.coq-native`, ...) should be done by - a separate flag, and the "ondemand" value removed. Once this is done, use - [get_bool] here. *) - let native_compiler = - match (next ()) with - | ("yes" | "on") -> NativeOn {ondemand=false} - | "ondemand" -> NativeOn {ondemand=true} - | ("no" | "off") -> NativeOff - | _ -> - error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler") - in + let native_compiler = get_native_compiler (next ()) in { oval with config = { oval.config with native_compiler }} | "-set" -> |