Merge PR coq#18424: [stm] Remove support for .vio files

Reviewed-by: SkySkimmer Reviewed-by: gares Co-authored-by: SkySkimmer <[email protected]>
haansn08 · Apr 17, 2024 · 3964411 · 3964411
2 parents ed7af40 + 066a49c
commit 3964411
Show file tree

Hide file tree

Showing 79 changed files with 140 additions and 1,315 deletions.
diff --git a/.gitignore b/.gitignore
@@ -1,7 +1,6 @@
 *.glob
 *.d
 *.d.raw
-*.vio
 *.vos
 *.vok
 *.vo

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
@@ -105,7 +105,6 @@ before_script:
   extends: .auto-use-tags
   script:
     - make $DUNE_TARGET
-    - find _build -name '*.vio' -exec rm -f {} \;
     - tar cfj _build.tar.bz2 _build
   variables:
     DUNE_TARGET: world
@@ -166,10 +165,7 @@ before_script:
   needs:
     - not-a-real-job
   script:
-    # exit 0: workaround for https://gitlab.com/gitlab-org/gitlab/issues/202505
-    # the validate:vio job is sometimes started before build:vio, without artifacts
-    # we ignore these spurious errors so if the job fails it's a real error
-    - cd _install_ci || exit 0
+    - cd _install_ci
     - find lib/coq/ -name '*.vo' -fprint0 vofiles
     - xargs -0 --arg-file=vofiles bin/coqchk -o -m -coqlib lib/coq/ > ../coqchk.log 2>&1 || touch coqchk.failed
     - tail -n 1000 ../coqchk.log # the log is too big for gitlab so pipe to a file and display the tail
@@ -352,24 +348,6 @@ build:base+async:
       - dmesg.txt
   timeout: 1h 30min
 
-build:vio:
-  extends: .build-template:base:dev
-  variables:
-    COQ_EXTRA_CONF: "-native-compiler no"
-    COQ_DUNE_EXTRA_OPT: "-vio"
-    DUNE_TARGET: "vio world"
-  after_script:
-    - dmesg > dmesg.txt
-  allow_failure: true # See https://github.com/coq/coq/issues/9637
-  only:
-    variables:
-      - ($FULL_CI == "true" && $UNRELIABLE =~ /enabled/)
-  artifacts:
-    when: always
-    paths:
-      - _install_ci
-      - dmesg.txt
-
 lint:
   stage: build
   image: $EDGE_IMAGE
@@ -594,14 +572,6 @@ validate:edge+flambda:
     OPAM_VARIANT: "+flambda"
   only: *full-ci
 
-validate:vio:
-  extends: .validate-template
-  needs:
-    - build:vio
-  only:
-    variables:
-      - ($FULL_CI == "true" && $UNRELIABLE =~ /enabled/)
-
 # Libraries are by convention the projects that depend on Coq
 # but not on its ML API
 

diff --git a/Makefile b/Makefile
@@ -14,7 +14,7 @@
 .PHONY: refman-html refman-pdf stdlib-html apidoc     # Documentation targets
 .PHONY: test-suite dev-targets
 .PHONY: fmt ocheck obuild ireport clean               # Maintenance targets
-.PHONY: dunestrap vio release install                 # Miscellaneous
+.PHONY: dunestrap release install                 # Miscellaneous
 
 # We don't allow parallel build here, this is just a placehoder for
 # dune commands for the most part
@@ -45,8 +45,6 @@ help:
 	@echo "  - test-suite: run Coq's test suite [env NJOBS=N to set job parallelism]"
 	@echo "  - dunestrap: Generate the dune rules for vo files"
 	@echo ""
-	@echo "  use 'COQ_DUNE_EXTRA_OPT=\"-vio\" make target' to do a vio build"
-	@echo ""
 	@echo "  Note: running ./configure is not recommended for developers,"
 	@echo "        see dev/doc/build-system.dune.md for more info"
 	@echo "  Note: these targets produce a developer build, not suitable"
@@ -152,10 +150,6 @@ NONDOC_INSTALL_TARGETS:=coq-core.install coq-stdlib.install coqide-server.instal
 world: dunestrap
 	dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS)
 
-# only useful for CI
-vio: dunestrap
-	dune build $(DUNEOPT) @vio
-
 watch:
 	dune build $(DUNEOPT) $(NONDOC_INSTALL_TARGETS) -w
 

diff --git a/checker/check.ml b/checker/check.ml
@@ -49,7 +49,6 @@ let pr_path sp =
 
 type compilation_unit_name = DirPath.t
 
-type seg_univ = Univ.ContextSet.t * bool
 type seg_proofs = Opaqueproof.opaque_proofterm option array
 
 type library_t = {
@@ -59,7 +58,6 @@ type library_t = {
   library_opaques : seg_proofs;
   library_deps : (compilation_unit_name * Safe_typing.vodigest) array;
   library_digest : Safe_typing.vodigest;
-  library_extra_univs : Univ.ContextSet.t;
   library_vm : Vmlibrary.on_disk;
 }
 
@@ -125,12 +123,12 @@ let check_one_lib admit senv (dir,m) =
     if LibrarySet.mem dir admit then
       (Flags.if_verbose Feedback.msg_notice
          (str "Admitting library: " ++ pr_dirpath dir);
-       Safe_checking.unsafe_import (fst senv) md m.library_extra_univs m.library_vm dig),
+       Safe_checking.unsafe_import (fst senv) md m.library_vm dig),
       (snd senv)
     else
       (Flags.if_verbose Feedback.msg_notice
          (str "Checking library: " ++ pr_dirpath dir);
-       Safe_checking.import (fst senv) (snd senv) md m.library_extra_univs  m.library_vm dig)
+       Safe_checking.import (fst senv) (snd senv) md m.library_vm dig)
   in
     register_loaded_library m; senv
 
@@ -285,14 +283,13 @@ type library_disk = {
   md_objects : library_objects;
 }
 
-let mk_library sd md f table digest cst vm = {
+let mk_library sd md f table digest vm = {
   library_name = sd.md_name;
   library_filename = f;
   library_compiled = md.md_compiled;
   library_opaques = table;
   library_deps = sd.md_deps;
   library_digest = digest;
-  library_extra_univs = cst;
   library_vm = vm;
 }
 
@@ -326,22 +323,18 @@ let marshal_in_segment (type a) ~validate ~value ~(segment : a ObjFile.segment)
 
 let summary_seg : summary_disk ObjFile.id = ObjFile.make_id "summary"
 let library_seg : library_disk ObjFile.id = ObjFile.make_id "library"
-let universes_seg : seg_univ option ObjFile.id = ObjFile.make_id "universes"
-let tasks_seg : Obj.t option ObjFile.id = ObjFile.make_id "tasks"
 let opaques_seg : seg_proofs ObjFile.id = ObjFile.make_id "opaques"
 let vm_seg = Vmlibrary.vm_segment
 
 let intern_from_file ~intern_mode ~enable_VM (dir, f) =
   let validate = intern_mode <> Dep in
   Flags.if_verbose chk_pp (str"[intern "++str f++str" ...");
-  let (sd,md,table,opaque_csts,vmlib,digest) =
+  let (sd,md,table,vmlib,digest) =
     try
       (* First pass to read the metadata of the file *)
       let ch = System.with_magic_number_check raw_intern_library f in
       let seg_sd = ObjFile.get_segment ch ~segment:summary_seg in
       let seg_md = ObjFile.get_segment ch ~segment:library_seg in
-      let seg_univs = ObjFile.get_segment ch ~segment:universes_seg in
-      let seg_tasks = ObjFile.get_segment ch ~segment:tasks_seg in
       let seg_opaque = ObjFile.get_segment ch ~segment:opaques_seg in
       let seg_vmlib = ObjFile.get_segment ch ~segment:vm_seg in
       let () = ObjFile.close_in ch in
@@ -350,8 +343,6 @@ let intern_from_file ~intern_mode ~enable_VM (dir, f) =
 
       let sd = marshal_in_segment ~validate ~value:Values.v_libsum ~segment:seg_sd f ch in
       let md = marshal_in_segment ~validate ~value:Values.v_lib ~segment:seg_md f ch in
-      let opaque_csts = marshal_in_segment ~validate ~value:Values.v_univopaques ~segment:seg_univs f ch in
-      let tasks = marshal_in_segment ~validate ~value:Values.(Opt Any) ~segment:seg_tasks f ch in
       let table = marshal_in_segment ~validate ~value:Values.v_opaquetable ~segment:seg_opaque f ch in
       let vmlib = if enable_VM
         then marshal_in_segment ~validate ~value:Values.v_vmlib ~segment:seg_vmlib f ch
@@ -365,29 +356,14 @@ let intern_from_file ~intern_mode ~enable_VM (dir, f) =
       if dir <> sd.md_name then
         CErrors.user_err
           (name_clash_message dir sd.md_name f);
-      if tasks <> None then
-        CErrors.user_err
-          (str "The file "++str f++str " contains unfinished tasks");
-      if opaque_csts <> None then begin
-       Flags.if_verbose chk_pp (str " (was a vio file) ");
-      Option.iter (fun (_,b) -> if not b then
-        CErrors.user_err
-          (str "The file "++str f++str " is still a .vio"))
-        opaque_csts;
-      end;
       Flags.if_verbose chk_pp (str" done]" ++ fnl ());
       let digest =
-        let open ObjFile in
-        if opaque_csts <> None then Safe_typing.Dvivo (seg_md.hash, seg_univs.hash)
-        else (Safe_typing.Dvo_or_vi seg_md.hash) in
-      sd,md,table,opaque_csts,vmlib,digest
+        Safe_typing.Dvo_or_vi seg_md.hash in
+      sd,md,table,vmlib,digest
     with e -> Flags.if_verbose chk_pp (str" failed!]" ++ fnl ()); raise e in
   depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph;
   opaque_tables := LibraryMap.add sd.md_name table !opaque_tables;
-  let extra_cst =
-    Option.default Univ.ContextSet.empty
-      (Option.map (fun (cs,_) -> cs) opaque_csts) in
-  mk_library sd md f table digest extra_cst (Vmlibrary.inject vmlib)
+  mk_library sd md f table digest (Vmlibrary.inject vmlib)
 
 (* Read a compiled library and all dependencies, in reverse order.
    Do not include files that are already in the context. *)

diff --git a/checker/safe_checking.ml b/checker/safe_checking.ml
@@ -11,16 +11,15 @@
 open Declarations
 open Environ
 
-let import senv opac clib univs vmtab digest =
+let import senv opac clib vmtab digest =
   let senv = Safe_typing.check_flags_for_library clib senv in
   let mb = Safe_typing.module_of_library clib in
   let env = Safe_typing.env_of_safe_env senv in
   let env = push_context_set ~strict:true (Safe_typing.univs_of_library clib) env in
-  let env = push_context_set ~strict:true univs env in
   let env = Modops.add_retroknowledge mb.mod_retroknowledge env in
   let env = Environ.link_vm_library vmtab env in
   let opac = Mod_checking.check_module env opac mb.mod_mp mb in
-  let (_,senv) = Safe_typing.import clib univs vmtab digest senv in senv, opac
+  let (_,senv) = Safe_typing.import clib vmtab digest senv in senv, opac
 
-let unsafe_import senv clib univs vmtab digest =
-  let (_,senv) = Safe_typing.import clib univs vmtab digest senv in senv
+let unsafe_import senv clib vmtab digest =
+  let (_,senv) = Safe_typing.import clib vmtab digest senv in senv
diff --git a/checker/safe_checking.mli b/checker/safe_checking.mli
@@ -12,5 +12,16 @@
 open Safe_typing
 (*i*)
 
-val import : safe_environment -> Names.Cset.t Names.Cmap.t -> compiled_library -> Univ.ContextSet.t -> Vmlibrary.on_disk -> vodigest -> safe_environment * Names.Cset.t Names.Cmap.t
-val unsafe_import : safe_environment -> compiled_library -> Univ.ContextSet.t -> Vmlibrary.on_disk -> vodigest -> safe_environment
+val import
+  : safe_environment
+  -> Names.Cset.t Names.Cmap.t
+  -> compiled_library
+  -> Vmlibrary.on_disk
+  -> vodigest -> safe_environment * Names.Cset.t Names.Cmap.t
+
+val unsafe_import
+  : safe_environment
+  -> compiled_library
+  -> Vmlibrary.on_disk
+  -> vodigest
+  -> safe_environment
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
@@ -84,21 +84,10 @@ currently `coqnative` incurs a 33% build time overhead on a powerful
 16-core machine.
 
 There are several modes for the rule generation script to work,
-depending on the parameter passed. As of today, it support `-async`
-and `-vio`.
+depending on the parameter passed. As of today, it support `-async`.
 
 `-async` will pass `-async-proofs on` to `coqc`.
 
-`-vio` will have the script setup compilation such that `.vo` files
-are generated first going thru `.vio` files.
-
-In particular, `-vio` mode has several pitfalls, for example, no
-`.glob` files are generated (this is inherited from Coq
-itself). Moreover, it is not possible to do a full parallel build
-doing `.v -> .vio` and `.vio -> .vo`, as it'd be racy, so a barrier
-must be used (the first process must be completed) before running the
-`.vio -> .vo` step.
-
 ## Per-User Custom Settings
 
 Dune will read the file `~/.config/dune/config`; see `man

diff --git a/doc/changelog/12-infrastructure-and-dependencies/18424-HEAD.rst b/doc/changelog/12-infrastructure-and-dependencies/18424-HEAD.rst
@@ -0,0 +1,16 @@
+- **Removed:**
+  Support for ``.vio`` files and for ``.vio2vo`` transformation has
+  been removed, compilation to ``.vos`` is the supported method for
+  quick compilation now
+  (`#18424 <https://github.com/coq/coq/pull/18424>`_,
+  fixes `#4007 <https://github.com/coq/coq/issues/4007>`_
+  and `#4013 <https://github.com/coq/coq/issues/4013>`_
+  and `#4123 <https://github.com/coq/coq/issues/4123>`_
+  and `#5308 <https://github.com/coq/coq/issues/5308>`_
+  and `#5223 <https://github.com/coq/coq/issues/5223>`_
+  and `#6720 <https://github.com/coq/coq/issues/6720>`_
+  and `#8402 <https://github.com/coq/coq/issues/8402>`_
+  and `#9637 <https://github.com/coq/coq/issues/9637>`_
+  and `#11471 <https://github.com/coq/coq/issues/11471>`_
+  and `#18380 <https://github.com/coq/coq/issues/18380>`_,
+  by Emilio Jesus Gallego Arias).
diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst
@@ -181,91 +181,3 @@ default, pass the ``-async-proofs on`` flag to enable it.
 Proofs that are known to take little time to process are not delegated
 to a worker process. The threshold can be configured with
 ``-async-proofs-delegation-threshold``. Default is 0.03 seconds.
-
-Batch mode
----------------
-
-   .. warning::
-
-      The ``-vio`` flag is subsumed, for most practical usage, by the
-      the more recent ``-vos`` flag. See :ref:`compiled-interfaces`.
-
-   .. warning::
-
-      When working with ``.vio`` files, do not use the ``-vos`` option at
-      the same time, otherwise stale files might get loaded when executing
-      a ``Require``. Indeed, the loading of a nonempty ``.vos`` file is
-      assigned higher priority than the loading of a ``.vio`` file.
-
-When Coq is used as a batch compiler by running ``coqc``, it produces
-a ``.vo`` file for each ``.v`` file. A ``.vo`` file contains, among other
-things, theorem statements and proofs. Hence to produce a .vo Coq
-need to process all the proofs of the ``.v`` file.
-
-The asynchronous processing of proofs can decouple the generation of a
-compiled file (like the ``.vo`` one) that can be loaded by ``Require`` from the
-generation and checking of the proof objects. The ``-vio`` flag can be
-passed to ``coqc`` to produce, quickly, ``.vio`` files.
-Alternatively, when using a Makefile produced by ``coq_makefile``,
-the ``vio`` target can be used to compile all files using the ``-vio`` flag.
-
-A ``.vio`` file can be loaded using ``Require`` exactly as a ``.vo`` file but
-proofs will not be available (the Print command produces an error).
-Moreover, some universe constraints might be missing, so universes
-inconsistencies might go unnoticed. A ``.vio`` file does not contain proof
-objects, but proof tasks, i.e. what a worker process can transform
-into a proof object.
-
-Compiling a set of files with the ``-vio`` flag allows one to work,
-interactively, on any file without waiting for all the proofs to be
-checked.
-
-When working interactively, one can fully check all the ``.v`` files by
-running ``coqc`` as usual.
-
-Alternatively one can turn each ``.vio`` into the corresponding ``.vo``. All
-.vio files can be processed in parallel, hence this alternative might
-be faster. The command ``coqc -schedule-vio2vo 2 a b c`` can be used to
-obtain a good scheduling for two workers to produce ``a.vo``, ``b.vo``, and
-``c.vo``. When using a Makefile produced by ``coq_makefile``, the ``vio2vo`` target
-can be used for that purpose. Variable ``J`` should be set to the number
-of workers, e.g. ``make vio2vo J=2``. The only caveat is that, while the
-.vo files obtained from ``.vio`` files are complete (they contain all proof
-terms and universe constraints), the satisfiability of all universe
-constraints has not been checked globally (they are checked to be
-consistent for every single proof). Constraints will be checked when
-these ``.vo`` files are (recursively) loaded with ``Require``.
-
-There is an extra, possibly even faster, alternative: just check the
-proof tasks stored in ``.vio`` files without producing the ``.vo`` files. This
-is possibly faster because all the proof tasks are independent, hence
-one can further partition the job to be done between workers. The
-``coqc -schedule-vio-checking 6 a b c`` command can be used to obtain a
-good scheduling for 6 workers to check all the proof tasks of ``a.vio``,
-``b.vio``, and ``c.vio``. Auxiliary files are used to predict how long a proof
-task will take, assuming it will take the same amount of time it took
-last time. When using a Makefile produced by coq_makefile, the
-``checkproofs`` target can be used to check all ``.vio`` files. Variable ``J``
-should be set to the number of workers, e.g. ``make checkproofs J=6``. As
-when converting ``.vio`` files to ``.vo`` files, universe constraints are not
-checked to be globally consistent. Hence this compilation mode is only
-useful for quick regression testing and on developments not making
-heavy use of the ``Type`` hierarchy.
-
-Limiting the number of parallel workers
---------------------------------------------
-
-Many Coq processes may run on the same computer, and each of them may
-start many additional worker processes. The ``coqworkmgr`` utility lets
-one limit the number of workers, globally.
-
-The utility accepts the ``-j`` argument to specify the maximum number of
-workers (defaults to 2). ``coqworkmgr`` automatically starts in the
-background and prints an environment variable assignment
-like ``COQWORKMGR_SOCK=localhost:45634``. The user must set this variable
-in all the shells from which Coq processes will be started. If one
-uses just one terminal running the bash shell, then
-``export ‘coqworkmgr -j 4‘`` will do the job.
-
-After that, all Coq processes, e.g. ``coqide`` and ``coqc``, will respect the
-limit, globally.
-Original file line number
+Diff line change
@@ -1,7 +1,6 @@
     *.glob
     *.d
     *.d.raw
-    *.vio
     *.vos
     *.vok
     *.vo
@@ Expand Down @@