Merge pull request #838 from ejgallego/vm_init

[coq] [init] Allow init to tweak VM mode and warnings.
ejgallego · Sep 28, 2024 · 01cb796 · 01cb796
2 parents afaac46 + 9760248
commit 01cb796
Show file tree

Hide file tree

Showing 5 changed files with 14 additions and 4 deletions.
diff --git a/compiler/driver.ml b/compiler/driver.ml
@@ -2,7 +2,8 @@
 let coq_init ~debug =
   let load_module = Dynlink.loadfile in
   let load_plugin = Coq.Loader.plugin_handler None in
-  Coq.Init.(coq_init { debug; load_module; load_plugin })
+  let vm, warnings = (true, None) in
+  Coq.Init.(coq_init { debug; load_module; load_plugin; vm; warnings })
 
 let replace_test_path exp message =
   let home_re = Str.regexp (exp ^ ".*$") in

diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml
@@ -63,7 +63,8 @@ let concise_cb ofn =
 let coq_init ~debug =
   let load_module = Dynlink.loadfile in
   let load_plugin = Coq.Loader.plugin_handler None in
-  Coq.Init.(coq_init { debug; load_module; load_plugin })
+  let vm, warnings = (true, None) in
+  Coq.Init.(coq_init { debug; load_module; load_plugin; vm; warnings })
 
 let exit_notification =
   Lsp.Base.Message.(Notification { method_ = "exit"; params = [] })

diff --git a/coq/init.ml b/coq/init.ml
@@ -23,6 +23,8 @@ type coq_opts =
   ; load_plugin : Mltop.PluginSpec.t -> unit
         (** callback to load findlib packages *)
   ; debug : bool  (** Enable Coq Debug mode *)
+  ; vm : bool  (** Enable Coq's VM *)
+  ; warnings : string option  (** Coq's Warnings *)
   }
 
 let coq_lvl_to_severity (lvl : Feedback.level) =
@@ -46,7 +48,7 @@ let mk_fb_handler q Feedback.{ contents; _ } =
 let coq_init opts =
   (* Core Coq initialization *)
   Lib.init ();
-  Global.set_impredicative_set false;
+  Global.set_VM opts.vm;
   Global.set_native_compiler false;
 
   if opts.debug then CDebug.set_flags "backtrace";
@@ -70,6 +72,9 @@ let coq_init opts =
   in
   Mltop.set_top ser_mltop;
 
+  (* Maybe set warnings *)
+  Option.iter CWarnings.set_flags opts.warnings;
+
   (* This should go away in Coq itself *)
   Safe_typing.allow_delayed_constants := true;
 

diff --git a/coq/init.mli b/coq/init.mli
@@ -23,6 +23,8 @@ type coq_opts =
   ; load_plugin : Mltop.PluginSpec.t -> unit
         (** callback to load findlib packages *)
   ; debug : bool  (** Enable Coq Debug mode *)
+  ; vm : bool  (** Enable Coq's VM *)
+  ; warnings : string option  (** Coq's Warnings *)
   }
 
 val coq_init : coq_opts -> State.t

diff --git a/petanque/json_shell/shell.ml b/petanque/json_shell/shell.ml
@@ -1,7 +1,8 @@
 let init_coq ~debug =
   let load_module = Dynlink.loadfile in
   let load_plugin = Coq.Loader.plugin_handler None in
-  Coq.Init.(coq_init { debug; load_module; load_plugin })
+  let vm, warnings = (true, None) in
+  Coq.Init.(coq_init { debug; load_module; load_plugin; vm; warnings })
 
 let cmdline : Coq.Workspace.CmdLine.t =
   { coqlib = Coq_config.coqlib