Improved handling of disabled VM

checker/coqchk_main.ml

@@ -146,11 +146,22 @@ let indices_matter = ref false
 
 let enable_vm = ref false
 
+let warn_no_bytecode =
+  CWarnings.create ~name:"bytecode-compiler-disabled" ~category:CWarnings.CoreCategories.bytecode_compiler
+    Pp.(fun () ->
+        str "Bytecode compiler is disabled," ++ spc() ++
+        str "-bytecode-compiler option ignored.")
+
 let make_senv () =
   let senv = Safe_typing.empty_environment in
   let senv = Safe_typing.set_impredicative_set !impredicative_set senv in
   let senv = Safe_typing.set_indices_matter !indices_matter senv in
-  let senv = Safe_typing.set_VM !enable_vm senv in
+  let senv =
+    if !enable_vm && not Coq_config.bytecode_compiler then begin
+      warn_no_bytecode ();
+      senv
+    end else Safe_typing.set_VM !enable_vm senv
+  in
   let senv = Safe_typing.set_allow_sprop true senv in (* be smarter later *)
   Safe_typing.set_native_compiler false senv
 

engine/evd.ml

@@ -814,11 +814,10 @@ let evar_handler sigma =
     | Def _ | Undef _ | Primitive _ | Symbol _ as body -> body
     in
     let drop_code = function
-    | None -> Vmemitcodes.BCconstant
-    | Some (Vmemitcodes.BCdefined (mask, idx, patch)) ->
+    | Vmemitcodes.BCdefined (mask, idx, patch) ->
       let code () = Environ.lookup_vm_code idx env in
       Vmemitcodes.BCdefined (mask, code, patch)
-    | Some (BCalias _ | BCconstant as code) -> code
+    | BCalias _ | BCconstant | BCuncompiled as code -> code
     in
     { cb with const_body = drop_opaque cb.const_body; const_body_code = drop_code cb.const_body_code }
   in

kernel/cClosure.ml

@@ -148,11 +148,10 @@ let drop_opaque = function
 | Def _ | Undef _ | Primitive _ | Symbol _ as body -> body
 
 let drop_code env = function
-| None -> Vmemitcodes.BCconstant
-| Some (Vmemitcodes.BCdefined (mask, idx, patch)) ->
+| Vmemitcodes.BCdefined (mask, idx, patch) ->
   let code () = Environ.lookup_vm_code idx env in
   Vmemitcodes.BCdefined (mask, code, patch)
-| Some (BCalias _ | BCconstant as code) -> code
+| (BCalias _ | BCconstant | BCuncompiled as code) -> code
 
 let lookup_constant_handler env sigma cst = match lookup_constant_opt cst env with
 | None -> sigma.abstr_const cst
@@ -430,7 +429,7 @@ end = struct
         if TransparentState.is_transparent_constant ts cst then match cb.const_body with
         | Undef _ | Def _ | OpaqueDef _ | Primitive _ ->
           let mask = match cb.const_body_code with
-          | (Vmemitcodes.BCalias _ | Vmemitcodes.BCconstant) -> [||]
+          | (Vmemitcodes.BCalias _ | Vmemitcodes.BCconstant | BCuncompiled) -> [||]
           | (Vmemitcodes.BCdefined (mask, _, _)) -> mask
           in
           Def (constant_value_in u cb.const_body, mask)

kernel/declarations.mli

@@ -128,7 +128,7 @@ type ('opaque, 'bytecode) pconstant_body = {
                                            type-checking. *)
 }
 
-type constant_body = (Opaqueproof.opaque, Vmlibrary.indirect_code option) pconstant_body
+type constant_body = (Opaqueproof.opaque, Vmlibrary.indirect_code) pconstant_body
 
 (** {6 Representation of mutual inductive types in the kernel } *)
 

kernel/declareops.ml

@@ -19,6 +19,10 @@ let noh hcons x = snd (hcons x)
 (** Operations concernings types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
 
+let configure_enabled_native = match Coq_config.native_compiler with
+  | NativeOff -> false
+  | NativeOn _ -> true
+
 let safe_flags oracle = {
   check_guarded = true;
   check_positive = true;
@@ -27,8 +31,8 @@ let safe_flags oracle = {
   conv_oracle = oracle;
   share_reduction = true;
   unfold_dep_heuristic = false;
-  enable_VM = true;
-  enable_native_compiler = true;
+  enable_VM = Coq_config.bytecode_compiler;
+  enable_native_compiler = configure_enabled_native;
   indices_matter = true;
   impredicative_set = false;
   sprop_allowed = true;
@@ -107,8 +111,7 @@ let subst_const_body subst cb =
         const_univ_hyps = UVars.Instance.empty;
         const_body = body';
         const_type = type';
-        const_body_code =
-          Option.map (Vmemitcodes.subst_body_code subst) cb.const_body_code;
+        const_body_code = Vmemitcodes.subst_body_code subst cb.const_body_code;
         const_universes = cb.const_universes;
         const_relevance = cb.const_relevance;
         const_inline_code = cb.const_inline_code;

kernel/environ.ml

@@ -598,11 +598,18 @@ let same_flags {
   allow_uip == alt.allow_uip
 [@warning "+9"]
 
+let check_flags c =
+  assert (Coq_config.bytecode_compiler || not c.enable_VM);
+  assert (match Coq_config.native_compiler with
+      | NativeOff -> not c.enable_native_compiler
+      | NativeOn _ -> true)
+
 let set_type_in_type b = map_universes (UGraph.set_type_in_type b)
 
 let set_typing_flags c env =
   if same_flags env.env_typing_flags c then env
   else
+    let () = check_flags c in
     let env = { env with env_typing_flags = c } in
     let env = set_type_in_type (not c.check_universes) env in
     let env = { env with env_qualities = QGraph.set_ignore_constraints (not c.check_eliminations) env.env_qualities } in

kernel/genlambda.ml

@@ -543,7 +543,7 @@ let rec get_alias env sigma kn =
   let tps = cb.const_body_code in
   match tps with
   | Vmemitcodes.BCalias kn' -> get_alias env sigma kn'
-  | Vmemitcodes.BCconstant -> kn, [||]
+  | Vmemitcodes.BCconstant | BCuncompiled -> kn, [||]
   | Vmemitcodes.BCdefined (mask, _, _) -> kn, mask
 
 (* Translation of constructors *)

kernel/mod_typing.ml

@@ -61,7 +61,7 @@ let infer_gen_conv_leq state env c1 c2 =
 type with_body = {
   w_def : Constr.t;
   w_univs : universes;
-  w_bytecode : Vmlibrary.indirect_code option;
+  w_bytecode : Vmlibrary.indirect_code;
 }
 
 let rec check_with_def (cst, ustate) env struc (idl, wth) mp reso =
@@ -239,7 +239,7 @@ let rec check_with_mod (cst, ustate) env struc (idl,new_mp) mp reso =
   with
   | Not_found -> error_no_such_label lab mp
 
-type 'a vm_handler = { vm_handler : env -> universes -> Constr.t -> 'a -> 'a * Vmlibrary.indirect_code option }
+type 'a vm_handler = { vm_handler : env -> universes -> Constr.t -> 'a -> 'a * Vmlibrary.indirect_code }
 type 'a vm_state = 'a * 'a vm_handler
 
 let check_with ustate vmstate env mp (sign,reso,cst,vm) = function

kernel/mod_typing.mli

@@ -17,7 +17,7 @@ open Names
 
 (** Main functions for translating module entries *)
 
-type 'a vm_handler = { vm_handler : env -> universes -> Constr.t -> 'a -> 'a * Vmlibrary.indirect_code option }
+type 'a vm_handler = { vm_handler : env -> universes -> Constr.t -> 'a -> 'a * Vmlibrary.indirect_code }
 type 'a vm_state = 'a * 'a vm_handler
 
 (** [translate_module] produces a [module_body] out of a [module_entry].

kernel/modops.ml

@@ -219,7 +219,7 @@ let strengthen_const mp_from l cb resolver =
     let u = UVars.make_abstract_instance (Declareops.constant_polymorphic_context cb) in
       { cb with
         const_body = Def (mkConstU (con,u));
-        const_body_code = Some (Vmbytegen.compile_alias con) }
+        const_body_code = Vmbytegen.compile_alias con }
 
 let rec strengthen_module mp mb = match mod_type mb with
 | NoFunctor struc ->

kernel/safe_typing.ml

@@ -424,7 +424,7 @@ end
 type side_effect = {
   seff_certif : Certificate.t CEphemeron.key;
   seff_constant : Constant.t;
-  seff_body : HConstr.t option * (Constr.t, Vmemitcodes.body_code option) Declarations.pconstant_body;
+  seff_body : HConstr.t option * (Constr.t, Vmemitcodes.body_code) Declarations.pconstant_body;
   seff_univs : Univ.ContextSet.t;
 }
 (* Invariant: For any senv, if [Certificate.safe_extend senv seff_certif] returns [Some certif'] then
@@ -498,12 +498,10 @@ let lift_constant c =
 let push_bytecode vmtab code =
   let open Vmemitcodes in
   let vmtab, code = match code with
-  | None -> vmtab, None
-  | Some (BCdefined (mask, code, patches)) ->
+  | BCdefined (mask, code, patches) ->
     let vmtab, index = Vmlibrary.add code vmtab in
-    vmtab, Some (BCdefined (mask, index, patches))
-  | Some BCconstant -> vmtab, Some BCconstant
-  | Some (BCalias kn) -> vmtab, Some (BCalias kn)
+    vmtab, BCdefined (mask, index, patches)
+  | BCconstant | BCuncompiled | BCalias _ as code -> vmtab, code
   in
   vmtab, code
 

kernel/vmbytegen.ml

@@ -539,12 +539,9 @@ let rec compile_fv cenv l sz cont =
 let rec get_alias env kn =
   let cb = lookup_constant kn env in
   let tps = cb.const_body_code in
-    match tps with
-    | None -> kn
-    | Some tps ->
-       (match tps with
-        | BCalias kn' -> get_alias env kn'
-        | _ -> kn)
+  match tps with
+   | BCalias kn' -> get_alias env kn'
+   | _ -> kn
 
 (* Some primitives are not implemented natively by the VM, but calling OCaml
    code instead *)
@@ -975,19 +972,20 @@ let warn_compile_error =
     Vmerrors.pr_error
 
 let compile ~fail_on_error ~uinstance env sigma c =
+  if not (typing_flags env).enable_VM then None else
   try NewProfile.profile "vm_compile" (fun () -> Some (compile ~uinstance env sigma c)) ()
   with Vmerrors.CompileError msg as exn ->
     let exn = Exninfo.capture exn in
     if fail_on_error then
       Exninfo.iraise exn
     else begin
       warn_compile_error msg;
-      None
+      assert false
     end
 
 let compile_constant_body ~fail_on_error env univs = function
-  | Undef _ | OpaqueDef _ -> Some BCconstant
-  | Primitive _ | Symbol _ -> None
+  | Undef _ | OpaqueDef _ -> BCconstant
+  | Primitive _ | Symbol _ -> BCuncompiled
   | Def body ->
       let instance_size = UVars.AbstractContext.size (Declareops.universes_context univs) in
       let alias =
@@ -1003,11 +1001,12 @@ let compile_constant_body ~fail_on_error env univs = function
             end
         | _ -> None in
       match alias with
-      | Some kn -> Some (BCalias kn)
-      | _ ->
+      | Some kn -> BCalias kn
+      | None ->
         let uinstance = Bound instance_size in
-        let res = compile ~fail_on_error ~uinstance env (empty_evars env) body in
-        Option.map (fun (mask, code, patch) -> BCdefined (mask, code, patch)) res
+        match compile ~fail_on_error ~uinstance env (empty_evars env) body with
+        | None -> BCuncompiled
+        | Some (mask, code, patch) -> BCdefined (mask, code, patch)
 
 let compile ~fail_on_error env sigma c =
   compile ~fail_on_error ~uinstance:Global env sigma c

kernel/vmbytegen.mli

@@ -20,7 +20,7 @@ val compile :
 
 val compile_constant_body : fail_on_error:bool ->
   env -> universes -> (Constr.t, 'opaque, 'symb) constant_def ->
-  body_code option
+  body_code
 
 (** Shortcut of the previous function used during module strengthening *)
 

kernel/vmemitcodes.ml

@@ -632,13 +632,15 @@ type 'a pbody_code =
   | BCdefined of bool array * 'a * patches
   | BCalias of Names.Constant.t
   | BCconstant
+  | BCuncompiled
 
 type body_code = to_patch pbody_code
 
 let subst_body_code s = function
 | BCdefined (m, x, tp) -> BCdefined (m, x, subst_patches s tp)
 | BCalias cu -> BCalias (subst_constant s cu)
 | BCconstant -> BCconstant
+| BCuncompiled -> BCuncompiled
 
 let to_memory fv code =
   let env = {

kernel/vmemitcodes.mli

@@ -26,6 +26,7 @@ type 'a pbody_code =
   | BCdefined of bool array * 'a * patches
   | BCalias of Constant.t
   | BCconstant
+  | BCuncompiled
 
 type body_code = to_patch pbody_code
 

kernel/vmsymtable.ml

@@ -284,6 +284,8 @@ let rec slot_for_getglobal env sigma kn envcache table =
       set_global v table
     | BCalias kn' -> slot_for_getglobal env sigma kn' envcache table
     | BCconstant -> set_global (val_of_constant kn) table
+    | BCuncompiled ->
+      CErrors.user_err Pp.(str "VM encountered uncompiled constant "++Constant.print kn ++ str ".")
     in
     rk := Some (CEphemeron.create pos);
     pos

plugins/extraction/extract_env.ml

@@ -185,7 +185,7 @@ let factor_fix env sg l cb msb =
 
 let vm_state =
   (* VM bytecode is not needed here *)
-  let vm_handler _ _ _ () = (), None in
+  let vm_handler _ _ _ () = (), Vmemitcodes.BCuncompiled in
   ((), { Mod_typing.vm_handler })
 
 let expand_mexpr env mp me =

sysinit/coqargs.ml

@@ -41,6 +41,7 @@ type require_injection = { lib: string; prefix: string option; export: export_fl
 type injection_command =
   | OptionInjection of (string list * option_command)
   | RequireInjection of require_injection
+  | WarnNoBytecode
   | WarnNoNative of string
   | WarnNativeDeprecated
 
@@ -106,8 +107,6 @@ type t = {
 
 let default_toplevel = "Top"
 
-let default_native = Coq_config.native_compiler
-
 let default_logic_config = {
   impredicative_set = false;
   indices_matter = false;
@@ -120,8 +119,8 @@ let default_config = {
   logic        = default_logic_config;
   rcfile       = None;
   coqlib       = None;
-  enable_VM    = true;
-  native_compiler = default_native;
+  enable_VM    = Coq_config.bytecode_compiler;
+  native_compiler = Coq_config.native_compiler;
   native_output_dir = ".coq-native";
   native_include_dirs = [];
   output_directory = None;
@@ -229,6 +228,10 @@ 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 get_bytecode_compiler_warns b =
+  if b && not Coq_config.bytecode_compiler then [WarnNoBytecode]
+  else []
+
 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
@@ -345,7 +348,10 @@ let parse_args ~init arglist : t * string list =
     |"-w" | "-W" -> add_set_warnings oval (next())
 
     |"-bytecode-compiler" ->
-      { oval with config = { oval.config with enable_VM = get_bool ~opt (next ()) }}
+      let b = get_bool ~opt (next ()) in
+      let warn = get_bytecode_compiler_warns b in
+      { oval with config = { oval.config with enable_VM = b };
+                  pre = { oval.pre with injections = warn @ oval.pre.injections }}
 
     |"-native-compiler" ->
       let native_compiler, warn = get_native_compiler (next ()) in

sysinit/coqargs.mli

@@ -30,6 +30,7 @@ type injection_command =
   | RequireInjection of require_injection
   (** Require libraries before the initial state is
       ready. *)
+  | WarnNoBytecode
   | WarnNoNative of string
   (** Used so that "-w -native-compiler-disabled -native-compiler yes"
      does not cause a warning. The native option must be processed

sysinit/coqinit.ml

@@ -219,6 +219,11 @@ let require_file ~intern ~prefix ~lib ~export ~allow_failure =
   with (Synterp.UnmappedLibrary _ | Synterp.NotFoundLibrary _) when allow_failure ->
     warn_require_not_found (mfrom, mp)
 
+let warn_no_bytecode =
+  CWarnings.create ~name:"bytecode-compiler-disabled" ~category:CWarnings.CoreCategories.bytecode_compiler
+    Pp.(fun () -> str "Bytecode compiler is disabled," ++ spc() ++
+                  str "-bytecode-compiler option ignored.")
+
 let warn_no_native_compiler =
   CWarnings.create_in Nativeconv.w_native_disabled
     Pp.(fun s -> strbrk "Native compiler is disabled," ++
@@ -253,6 +258,7 @@ let handle_injection ~intern = let open Coqargs in function
   | RequireInjection {lib;prefix;export;allow_failure} ->
     require_file ~intern ~lib ~prefix ~export ~allow_failure
   | OptionInjection o -> set_option o
+  | WarnNoBytecode -> warn_no_bytecode ()
   | WarnNoNative s -> warn_no_native_compiler s
   | WarnNativeDeprecated -> warn_deprecated_native_compiler ()
 

theories/Corelib/Numbers/Cyclic/Int63/Sint63Axioms.v

@@ -20,7 +20,7 @@ Local Infix "^" := Z.pow : Z_scope.
 Local Notation "x <= y" := (Z.compare x y <> Gt) : Z_scope.
 Local Notation "x < y" := (Z.compare x y = Lt) : Z_scope.
 
-Definition min_int := Eval vm_compute in (lsl 1 62).
+Definition min_int := Eval lazy in (lsl 1 62).
 
 (** Translation to and from Z *)
 Definition to_Z (i : int) :=

theories/Corelib/Numbers/Cyclic/Int63/Uint63Axioms.v

@@ -32,7 +32,7 @@ Definition size := 63%nat.
 Definition digits := 63%uint63.
 
 (** The biggest int *)
-Definition max_int := Eval vm_compute in sub 0 1.
+Definition max_int := Eval lazy in sub 0 1.
 
 (** Access to the nth digits *)
 Definition get_digit x p := ltb 0 (land x (lsl 1 p)).