Merge branch 'v8.11' into v8.11+coqpath

rocq-archive · Aug 26, 2020 · 5922346 · 5922346
2 parents e0ef104 + 750dd3e
commit 5922346
Show file tree

Hide file tree

Showing 12 changed files with 33 additions and 13 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -25,6 +25,7 @@
  * [sertop ] Forward port sername from 0.7.1 (@ejgallego)
  * [serlib ] Fix #212 "Segfault on universes" (@ejgallego, reported by @cpitclaudel , #214)
  * [serapi ] Fix #221 "Support COQPATH" (@ejgallego, reported by @cpitclaudel , #224)
+ * [sertop ] Fix #222 "Support --indices-matter" (@ejgallego, reported by @cpitclaudel , #223)
 
 ## Version 0.11.0:
 

diff --git a/sertop/sercomp.ml b/sertop/sercomp.ml
@@ -23,7 +23,7 @@ let fatal_exn exn info =
   Format.eprintf "Error: @[%a@]@\n%!" Pp.pp_with msg;
   exit 1
 
-let create_document ~in_file ~stm_flags ~quick ~iload_path ~debug ~allow_sprop =
+let create_document ~in_file ~stm_flags ~quick ~iload_path ~debug ~allow_sprop ~indices_matter =
 
   let open Sertop.Sertop_init in
 
@@ -33,6 +33,7 @@ let create_document ~in_file ~stm_flags ~quick ~iload_path ~debug ~allow_sprop =
     ; ml_load    = None
     ; debug
     ; allow_sprop
+    ; indices_matter
     };
 
   (* document initialization *)
@@ -179,7 +180,7 @@ let sercomp_doc = "sercomp Coq Compiler"
 
 open Cmdliner
 
-let driver input mode debug disallow_sprop printer async async_workers error_recovery quick
+let driver input mode debug disallow_sprop indices_matter printer async async_workers error_recovery quick
     coq_path ml_path load_path rload_path in_file omit_loc omit_att exn_on_opaque =
 
   (* closures *)
@@ -198,7 +199,7 @@ let driver input mode debug disallow_sprop printer async async_workers error_rec
     ; async_workers
     ; error_recovery
     } in
-  let doc, sid = create_document ~in_file ~stm_flags ~quick ~iload_path ~debug ~allow_sprop in
+  let doc, sid = create_document ~in_file ~stm_flags ~quick ~iload_path ~debug ~allow_sprop ~indices_matter in
 
   (* main loop *)
   let in_chan = open_in in_file in
@@ -219,7 +220,7 @@ let main () =
   let sercomp_cmd =
     let open Sertop.Sertop_arg in
     Term.(const driver
-          $ comp_input $ comp_mode $ debug $ disallow_sprop $ printer $ async $ async_workers $ error_recovery $ quick $ prelude
+          $ comp_input $ comp_mode $ debug $ disallow_sprop $ indices_matter $ printer $ async $ async_workers $ error_recovery $ quick $ prelude
           $ ml_include_path $ load_path $ rload_path $ input_file $ omit_loc $ omit_att $ exn_on_opaque
          ),
     Term.info "sercomp" ~version:sercomp_version ~doc:sercomp_doc ~man:sercomp_man

diff --git a/sertop/sername.ml b/sertop/sername.ml
@@ -32,6 +32,7 @@ let create_document ~require_lib ~in_file ~stm_flags ~quick ~iload_path ~debug ~
     ; ml_load    = None
     ; debug
     ; allow_sprop
+    ; indices_matter = false
     };
 
   (* document initialization *)

diff --git a/sertop/sertok.ml b/sertop/sertok.ml
@@ -40,6 +40,7 @@ let create_document ~in_file ~stm_flags ~quick ~iload_path ~debug ~allow_sprop =
     ; ml_load    = None
     ; debug
     ; allow_sprop
+    ; indices_matter = false
     };
 
   (* document initialization *)

diff --git a/sertop/sertop_arg.ml b/sertop/sertop_arg.ml
@@ -90,6 +90,10 @@ let disallow_sprop =
   let doc = "Forbid using the proof irrelevant SProp sort (allowed by default)" in
   Arg.(value & flag & info ["disallow-sprop"] ~doc)
 
+let indices_matter =
+  let doc = "Levels of indices (and nonuniform parameters) contribute to the level of inductives (disabled by default)" in
+  Arg.(value & flag & info ["indices-matter"] ~doc)
+
 let print0 =
   let doc = "End responses with a \\\\0 char." in
   Arg.(value & flag & info ["print0"] ~doc)

diff --git a/sertop/sertop_arg.mli b/sertop/sertop_arg.mli
@@ -32,7 +32,6 @@ val error_recovery  : bool Term.t
 val implicit_stdlib : bool Term.t
 val printer         : Sertop_ser.ser_printer Term.t
 val debug           : bool Term.t
-val disallow_sprop  : bool Term.t
 val print0          : bool Term.t
 val length          : bool Term.t
 val rload_path      : Loadpath.coq_path list Term.t
@@ -42,6 +41,10 @@ val no_init         : bool Term.t
 val topfile         : string option Term.t
 val no_prelude      : bool Term.t
 
+(* Kernel checking options *)
+val disallow_sprop  : bool Term.t
+val indices_matter  : bool Term.t
+
 (* sertop options *)
 type comp_mode = | C_parse | C_stats | C_print | C_sexp | C_check | C_vo | C_env
 val comp_mode : comp_mode Term.t

diff --git a/sertop/sertop_async.ml b/sertop/sertop_async.ml
@@ -38,10 +38,11 @@ let sertop_init ~(fb_out : Sexp.t -> unit) ~iload_path ~require_libs ~debug ~all
   let fb_handler fb = Sertop.Sertop_ser.sexp_of_answer (Feedback (Sertop.Sertop_util.feedback_tr fb)) |> fb_out in
 
   coq_init {
-    fb_handler;
-    ml_load = None;
-    debug;
-    allow_sprop;
+    fb_handler
+  ; ml_load = None
+  ; debug
+  ; allow_sprop
+  ; indices_matter = false
   };
 
   let stm_options = process_stm_flags

diff --git a/sertop/sertop_bin.ml b/sertop/sertop_bin.ml
@@ -20,7 +20,7 @@ open Cmdliner
 
 let sertop_version = Sertop.Ser_version.ser_git_version
 
-let sertop printer print0 debug disallow_sprop lheader coq_path ml_path no_init topfile no_prelude lp1 lp2 _std_impl async deep_edits async_workers error_recovery omit_loc omit_att exn_on_opaque =
+let sertop printer print0 debug disallow_sprop indices_matter lheader coq_path ml_path no_init topfile no_prelude lp1 lp2 _std_impl async deep_edits async_workers error_recovery omit_loc omit_att exn_on_opaque =
 
   let open  Sertop.Sertop_init         in
   let open! Sertop.Sertop_sexp         in
@@ -38,6 +38,7 @@ let sertop printer print0 debug disallow_sprop lheader coq_path ml_path no_init
 
        debug;
        allow_sprop;
+       indices_matter;
        printer;
        print0;
        lheader;
@@ -76,7 +77,7 @@ let sertop_cmd =
   ]
   in
   Term.(const sertop
-        $ printer $ print0 $ debug $ disallow_sprop $ length $ prelude $ ml_include_path $ no_init $topfile $ no_prelude $ load_path $ rload_path $ implicit_stdlib
+        $ printer $ print0 $ debug $ disallow_sprop $ indices_matter $ length $ prelude $ ml_include_path $ no_init $topfile $ no_prelude $ load_path $ rload_path $ implicit_stdlib
         $ async $ deep_edits $ async_workers $ error_recovery $ omit_loc $ omit_att $ exn_on_opaque ),
   Term.info "sertop" ~version:sertop_version ~doc ~man
 

diff --git a/sertop/sertop_init.ml b/sertop/sertop_init.ml
@@ -36,6 +36,7 @@ type coq_opts = {
 
   (* Allow SProp *)
   allow_sprop  : bool;
+  indices_matter : bool;
 }
 
 (**************************************************************************)
@@ -68,7 +69,7 @@ let coq_init opts =
 
   (* This should be configurable somehow. *)
   Global.set_engagement Declarations.PredicativeSet;
-  Global.set_indices_matter false;
+  Global.set_indices_matter opts.indices_matter;
 
   (* --allow-sprop in agreement with coq v8.11  *)
   Global.set_allow_sprop opts.allow_sprop;

diff --git a/sertop/sertop_init.mli b/sertop/sertop_init.mli
@@ -39,6 +39,9 @@ type coq_opts =
 
   ; allow_sprop  : bool
   (** allow using the proof irrelevant SProp sort (default=true) *)
+
+  ; indices_matter : bool
+  (** Levels of indices (and nonuniform parameters) contribute to the level of inductives *)
 }
 
 val coq_init : coq_opts -> unit

diff --git a/sertop/sertop_sexp.ml b/sertop/sertop_sexp.ml
@@ -32,7 +32,8 @@ type ser_opts =
 ; printer  : Sertop_ser.ser_printer
 
 ; debug    : bool
-; allow_sprop: bool
+; allow_sprop : bool
+; indices_matter : bool
 ; print0   : bool
 ; lheader  : bool                (* Print lenght header (deprecated)           *)
 
@@ -132,6 +133,7 @@ let ser_loop ser_opts =
         ; ml_load      = None
         ; debug        = ser_opts.debug
         ; allow_sprop  = ser_opts.allow_sprop
+        ; indices_matter = ser_opts.indices_matter
         })
   in
 

diff --git a/sertop/sertop_sexp.mli b/sertop/sertop_sexp.mli
@@ -29,6 +29,7 @@ type ser_opts =
 
 ; debug    : bool                (** Enable Coq debug mode                    *)
 ; allow_sprop: bool              (** Allow using the proof irrelevant SProp sort *)
+; indices_matter : bool          (** Indices of indexes contribute to inductive level *)
 ; print0   : bool                (** End every answer with [\0]               *)
 ; lheader  : bool                (** Print lenght header (deprecated)         *)