From 066a49c99ddf1ac7297e90b6a43d5b299dffc938 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 20 Dec 2023 16:33:14 +0100 Subject: [PATCH] [stm] Remove support for `.vio` files As discussed in https://github.com/coq/coq/wiki/Coq-Call-2023-07-11 , we do this PR as a first step to evaluate what are the gains when removing `.vio` files. Due to #4123, it is not likely that `.vio` files are useful in practice, and `.vos` files provide a viable alternative (as outlined in the original vos PR) Moreover, we have no plans to address the remaining vio bugs in the issue tracker. This PR: - closes #4007 - closes #4013 - closes #4123 - closes #5223 - closes #5308 - closes #6720 - closes #8402 - closes #9637 - closes #11471 - closes #18380 Related: #5388 #6710 See also the previous attempt: #8767 #8783 --- .gitignore | 1 - .gitlab-ci.yml | 32 +-- Makefile | 8 +- checker/check.ml | 38 +-- checker/safe_checking.ml | 9 +- checker/safe_checking.mli | 15 +- dev/doc/build-system.dune.md | 13 +- .../18424-HEAD.rst | 16 ++ .../addendum/parallel-proof-processing.rst | 88 ------- kernel/safe_typing.ml | 21 +- kernel/safe_typing.mli | 4 +- library/global.ml | 3 +- library/global.mli | 2 +- man/coqdep.1 | 3 - stm/asyncTaskQueue.ml | 2 +- stm/stm.ml | 224 ++---------------- stm/stm.mli | 27 +-- stm/vio_checking.ml | 143 ----------- stm/vio_checking.mli | 15 -- sysinit/coqargs.ml | 2 +- test-suite/Makefile | 28 +-- test-suite/bugs-nocoqchk/bug_6165.v | 3 +- test-suite/coq-makefile/quick2vo/_CoqProject | 11 - test-suite/coq-makefile/quick2vo/run.sh | 12 - test-suite/coq-makefile/vio2vo/_CoqProject | 11 - test-suite/coq-makefile/vio2vo/run.sh | 13 - test-suite/misc/coqc_dash_vok.sh | 13 +- .../stdout.ref | 7 - test-suite/misc/deps/DistinctRootDeps.out | 3 - test-suite/misc/deps/Theory1Deps.out | 8 - test-suite/misc/deps/Theory2Deps.out | 7 - test-suite/misc/deps/Theory3Deps.out | 5 - test-suite/misc/deps/deps-from.out | 2 - .../misc/external-deps/file1.ambiguous.deps | 1 - .../misc/external-deps/file1.found.deps | 1 - .../misc/external-deps/file1.notfound.deps | 1 - .../misc/external-deps/file2.ambiguous.deps | 1 - .../misc/external-deps/file2.found.deps | 1 - .../misc/external-deps/file2.notfound.deps | 1 - test-suite/misc/quick-include.sh | 5 - test-suite/misc/quick-include/file1.v | 18 -- test-suite/misc/quick-include/file2.v | 6 - test-suite/misc/vio_checking.sh | 32 --- test-suite/misc/vio_checking.v | 9 - test-suite/misc/vio_checking_bad.v | 4 - test-suite/output/ErrorInModule.v | 2 +- test-suite/output/ErrorInSection.v | 2 +- test-suite/vio/numeral.v | 21 -- test-suite/vio/print.v | 10 - test-suite/vio/section.v | 12 - test-suite/vio/seff.v | 10 - test-suite/vio/simple.v | 2 - test-suite/vio/univ_constraints_statements.v | 2 - .../vio/univ_constraints_statements_body.v | 7 - tools/CoqMakefile.in | 36 --- tools/coqdep/lib/common.ml | 2 +- tools/coqdep/lib/dep_info.ml | 2 +- tools/coqdep/lib/dep_info.mli | 2 +- tools/coqdep/lib/loadpath.ml | 8 +- tools/coqdep/lib/makefile.ml | 2 - tools/dune_rule_gen/coq_module.ml | 42 +--- tools/dune_rule_gen/coq_module.mli | 3 - tools/dune_rule_gen/coq_rules.ml | 42 +--- tools/dune_rule_gen/coq_rules.mli | 5 - tools/dune_rule_gen/gen_rules.ml | 10 - topbin/coqnative_bin.ml | 15 +- toplevel/ccompile.ml | 25 +- toplevel/coqc.ml | 19 +- toplevel/coqcargs.ml | 95 +------- toplevel/coqcargs.mli | 9 +- toplevel/vio_compile.ml | 41 ---- toplevel/vio_compile.mli | 12 - vernac/declaremods.ml | 4 +- vernac/declaremods.mli | 2 +- vernac/future.ml | 3 - vernac/future.mli | 3 - vernac/library.ml | 71 +----- vernac/library.mli | 18 +- vernac/loadpath.ml | 47 +--- 79 files changed, 140 insertions(+), 1315 deletions(-) create mode 100644 doc/changelog/12-infrastructure-and-dependencies/18424-HEAD.rst delete mode 100644 stm/vio_checking.ml delete mode 100644 stm/vio_checking.mli delete mode 100644 test-suite/coq-makefile/quick2vo/_CoqProject delete mode 100755 test-suite/coq-makefile/quick2vo/run.sh delete mode 100644 test-suite/coq-makefile/vio2vo/_CoqProject delete mode 100755 test-suite/coq-makefile/vio2vo/run.sh delete mode 100755 test-suite/misc/quick-include.sh delete mode 100644 test-suite/misc/quick-include/file1.v delete mode 100644 test-suite/misc/quick-include/file2.v delete mode 100755 test-suite/misc/vio_checking.sh delete mode 100644 test-suite/misc/vio_checking.v delete mode 100644 test-suite/misc/vio_checking_bad.v delete mode 100644 test-suite/vio/numeral.v delete mode 100644 test-suite/vio/print.v delete mode 100644 test-suite/vio/section.v delete mode 100644 test-suite/vio/seff.v delete mode 100644 test-suite/vio/simple.v delete mode 100644 test-suite/vio/univ_constraints_statements.v delete mode 100644 test-suite/vio/univ_constraints_statements_body.v delete mode 100644 toplevel/vio_compile.ml delete mode 100644 toplevel/vio_compile.mli diff --git a/.gitignore b/.gitignore index 755eea138f06..97b27e1bf00a 100644 --- 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 index 0b47715f24c1..1d0684f3edb9 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -104,7 +104,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 @@ -165,10 +164,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 @@ -334,24 +330,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 @@ -576,14 +554,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 index 9b0e42ca1048..a6a5ba9689a0 100644 --- 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 index a1e2d5482e80..853e6aed9a9c 100644 --- 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 index e92e2aa7ba5d..e1da76e6e0e5 100644 --- 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 index a6ca53b104e1..774631552b27 100644 --- 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 index 51953f3f510e..d8475967e826 100644 --- 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 new file mode 100644 index 000000000000..53ec331a1878 --- /dev/null +++ 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 `_, + fixes `#4007 `_ + and `#4013 `_ + and `#4123 `_ + and `#5308 `_ + and `#5223 `_ + and `#6720 `_ + and `#8402 `_ + and `#9637 `_ + and `#11471 `_ + and `#18380 `_, + by Emilio Jesus Gallego Arias). diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index 2baa48921486..cc5b78da86ce 100644 --- 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. diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 8bf4f3da6fb5..a2ff14ed9b59 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -101,14 +101,10 @@ module NamedDecl = Context.Named.Declaration type vodigest = | Dvo_or_vi of Digest.t (* The digest of the seg_lib part *) - | Dvivo of Digest.t * Digest.t (* The digest of the seg_lib + seg_univ part *) let digest_match ~actual ~required = match actual, required with - | Dvo_or_vi d1, Dvo_or_vi d2 - | Dvivo (d1,_), Dvo_or_vi d2 -> String.equal d1 d2 - | Dvivo (d1,e1), Dvivo (d2,e2) -> String.equal d1 d2 && String.equal e1 e2 - | Dvo_or_vi _, Dvivo _ -> false + | Dvo_or_vi d1, Dvo_or_vi d2 -> String.equal d1 d2 type library_info = DirPath.t * vodigest @@ -127,7 +123,7 @@ type compiled_library = { comp_flags : permanent_flags; } -type reimport = compiled_library * Univ.ContextSet.t * Vmlibrary.on_disk * vodigest +type reimport = compiled_library * Vmlibrary.on_disk * vodigest (** Part of the safe_env at a section opening time to be backtracked *) type section_data = { @@ -1418,9 +1414,7 @@ let export ~output_native_objects senv dir = let vmlib = Vmlibrary.export @@ Environ.vm_library senv.env in mp, lib, vmlib, (ast, symbols) -(* cst are the constraints that were computed by the vi2vo step and hence are - * not part of the [lib.comp_univs] field (but morally should be) *) -let import lib cst vmtab vodigest senv = +let import lib vmtab vodigest senv = let senv = check_flags_for_library lib senv in check_required senv.required lib.comp_deps; if DirPath.equal (ModPath.dp senv.modpath) lib.comp_name then @@ -1429,10 +1423,7 @@ let import lib cst vmtab vodigest senv = ++ DirPath.print lib.comp_name ++ str")."); let mp = MPfile lib.comp_name in let mb = lib.comp_mod in - let env = Environ.push_context_set ~strict:true - (Univ.ContextSet.union lib.comp_univs cst) - senv.env - in + let env = Environ.push_context_set ~strict:true lib.comp_univs senv.env in let env = Environ.link_vm_library vmtab env in let env = let linkinfo = Nativecode.link_info_of_dirpath lib.comp_name in @@ -1440,7 +1431,7 @@ let import lib cst vmtab vodigest senv = in let sections = Option.map (Section.map_custom (fun custom -> - {custom with rev_reimport = (lib,cst,vmtab,vodigest) :: custom.rev_reimport})) + {custom with rev_reimport = (lib,vmtab,vodigest) :: custom.rev_reimport})) senv.sections in mp, @@ -1482,7 +1473,7 @@ let close_section senv = let env = if Environ.rewrite_rules_allowed env0 then Environ.allow_rewrite_rules env else env in let senv = { senv with env; revstruct; sections; univ; objlabels; } in (* Second phase: replay Requires *) - let senv = List.fold_left (fun senv (lib,cst,vmtab,vodigest) -> snd (import lib cst vmtab vodigest senv)) + let senv = List.fold_left (fun senv (lib,vmtab,vodigest) -> snd (import lib vmtab vodigest senv)) senv (List.rev rev_reimport) in (* Third phase: replay the discharged section contents *) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 37a294bffde1..cdaaab944885 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -12,7 +12,6 @@ open Names type vodigest = | Dvo_or_vi of Digest.t (* The digest of the seg_lib part *) - | Dvivo of Digest.t * Digest.t (* The digest of the seg_lib + seg_univ part *) val digest_match : actual:vodigest -> required:vodigest -> bool @@ -244,8 +243,7 @@ val export : safe_environment -> DirPath.t -> ModPath.t * compiled_library * Vmlibrary.compiled_library * Nativelib.native_library -(* Constraints are non empty iff the file is a vi2vo *) -val import : compiled_library -> Univ.ContextSet.t -> Vmlibrary.on_disk -> vodigest -> +val import : compiled_library -> Vmlibrary.on_disk -> vodigest -> ModPath.t safe_transformer (** {6 Safe typing judgments } *) diff --git a/library/global.ml b/library/global.ml index 51f7adcde60c..ee2b43703687 100644 --- a/library/global.ml +++ b/library/global.ml @@ -179,8 +179,7 @@ let mind_of_delta_kn kn = let start_library dir = globalize (Safe_typing.start_library dir) let export ~output_native_objects s = Safe_typing.export ~output_native_objects (safe_env ()) s -let import c u t d = globalize (Safe_typing.import c u t d) - +let import c t d = globalize (Safe_typing.import c t d) (** Function to get an environment from the constants part of the global environment and a given context. *) diff --git a/library/global.mli b/library/global.mli index 7e662d594d34..5eb267ad0374 100644 --- a/library/global.mli +++ b/library/global.mli @@ -144,7 +144,7 @@ val start_library : DirPath.t -> ModPath.t val export : output_native_objects:bool -> DirPath.t -> ModPath.t * Safe_typing.compiled_library * Vmlibrary.compiled_library * Nativelib.native_library val import : - Safe_typing.compiled_library -> Univ.ContextSet.t -> Vmlibrary.on_disk -> Safe_typing.vodigest -> + Safe_typing.compiled_library -> Vmlibrary.on_disk -> Safe_typing.vodigest -> ModPath.t (** {6 Misc } *) diff --git a/man/coqdep.1 b/man/coqdep.1 index 673c93dde7a1..0734ab61ae94 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -147,11 +147,8 @@ example% coqdep \-I . -Q . Foo *.v .sp .5 .nf .B X.vo X.glob X.v.beautified X.required_vo: X.v -.B X.vio: X.v .B Y.vo Y.glob Y.v.beautified Y.required_vo: Y.v X.vo -.B Y.vio: Y.v X.vio .B Z.vo Z.glob Z.v.beautified Z.required_vo: Z.v X.vo ./a.cma ./a.cmxs -.B Z.vio: Z.v X.vio ./a.cma ./a.cmxs .fi .RE .br diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index c4014ef24838..c9c8e18e8037 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -117,7 +117,7 @@ module Make(T : Task) () = struct | ("-emacs" | "--xml_format=Ppcmds" | "-batch" | "-vok" | "-vos") :: tl -> set_slave_opt tl (* Options to discard: 1 argument *) - | ( "-async-proofs" | "-vio2vo" | "-o" + | ( "-async-proofs" | "-o" | "-load-vernac-source" | "-l" | "-load-vernac-source-verbose" | "-lv" | "-require-import" | "-require-export" | "-ri" | "-re" | "-load-vernac-object" diff --git a/stm/stm.ml b/stm/stm.ml index 3dcd63f42952..9b3f978a00e3 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -279,7 +279,7 @@ end (* }}} *) (* The main document type associated to a VCS *) type stm_doc_type = | VoDoc of string - | VioDoc of string + | VosDoc of string | Interactive of Coqargs.top (* Dummy until we land the functional interp patch + fixed start_library *) @@ -315,7 +315,7 @@ module VCS : sig val get_ldir : unit -> Names.DirPath.t val is_interactive : unit -> bool - val is_vio_doc : unit -> bool + val is_vos_doc : unit -> bool val current_branch : unit -> Branch.t val checkout : Branch.t -> unit @@ -537,9 +537,9 @@ end = struct (* {{{ *) | Interactive _ -> true | _ -> false - let is_vio_doc () = + let is_vos_doc () = match !doc_type with - | VioDoc _ -> true + | VosDoc _ -> true | _ -> false let current_branch () = current_branch !vcs @@ -1334,9 +1334,6 @@ module rec ProofTask : sig Stateid.exn_info -> Stateid.t -> Declare.Proof.closed_proof_output Future.computation - (* If set, only tasks overlapping with this list are processed *) - val set_perspective : Stateid.t list -> unit - end = struct (* {{{ *) let forward_feedback msg = !Hooks.forward_feedback msg @@ -1378,17 +1375,9 @@ end = struct (* {{{ *) let name = "proof" let extra_env () = !async_proofs_workers_extra_env - let perspective = ref [] - let set_perspective l = perspective := l - - let is_inside_perspective st = true - (* This code is now disabled. If an IDE needs this feature, make it accessible again. - List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) st - *) - let task_match age t = match age, t with - | Fresh, BuildProof { t_states } -> is_inside_perspective t_states + | Fresh, BuildProof { t_states } -> true | Old my_states, States l -> List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l | _ -> false @@ -1601,19 +1590,11 @@ and Slaves : sig type 'a tasks = (('a,VCS.vcs) Stateid.request * bool) list val dump_snapshot : unit -> Future.UUID.t tasks - val check_task : string -> 'a tasks -> int -> bool - val info_tasks : 'a tasks -> (string * float * int) list - val finish_task : - string -> - Library.seg_univ -> Library.seg_proofs -> - Opaqueproof.opaque_handle option tasks -> int -> Library.seg_univ val cancel_worker : WorkerPool.worker_id -> unit val reset_task_queue : unit -> unit - val set_perspective : Stateid.t list -> unit - end = struct (* {{{ *) module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask) () @@ -1625,147 +1606,10 @@ end = struct (* {{{ *) else queue := Some (TaskQueue.create 0 priority) - type check_result = - | OK of Id.t - | OK_ADMITTED - | ERROR - | ERROR_ADMITTED - - let check_task_aux extra name l i = - let { Stateid.stop; document; loc; name = r_name }, drop = List.nth l i in - Flags.if_verbose msg_info - Pp.(str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name)); - VCS.restore document; - let start = - let rec aux cur = - try aux (VCS.visit cur).next - with VCS.Expired -> cur in - aux stop in - try - Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false stop; - if drop then - let _proof = PG_compat.return_partial_proof () in - OK_ADMITTED - else begin - let opaque = Opaque in - - let proof = - PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true in - - (* We jump at the beginning since the kernel handles side effects by also - * looking at the ones that happen to be present in the current env *) - - Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false start; - (* STATE SPEC: - * - start: First non-expired state! [This looks very fishy] - * - end : start + qed - * => takes nothing from the itermediate states. - *) - (* STATE We use the state resulting from reaching start. *) - let st = Vernacstate.freeze_full_state () in - ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~loc ~control:[] (Proved (opaque,None))); - (* Is this name the same than the one in scope? *) - let name = Declare.Proof.get_po_name proof in - OK name - end - with e -> - let (e, info) = Exninfo.capture e in - (try match Stateid.get info with - | None -> - msg_warning Pp.( - str"File " ++ str name ++ str ": proof of " ++ str r_name ++ - spc () ++ iprint (e, info)) - | Some (_, cur) -> - match VCS.visit cur with - | { step = SCmd { cast } } - | { step = SFork (( cast, _, _, _), _) } - | { step = SQed ( { qast = cast }, _) } - | { step = SSideff (ReplayCommand cast, _) } -> - let loc = cast.expr.CAst.loc in - let start, stop = Option.cata Loc.unloc (0,0) loc in - msg_warning Pp.( - str"File " ++ str name ++ str ": proof of " ++ str r_name ++ - str ": chars " ++ int start ++ str "-" ++ int stop ++ - spc () ++ iprint (e, info)) - | _ -> - msg_warning Pp.( - str"File " ++ str name ++ str ": proof of " ++ str r_name ++ - spc () ++ iprint (e, info)) - with e -> - msg_warning Pp.(str"unable to print error message: " ++ - str (Printexc.to_string e))); - if drop then ERROR_ADMITTED else ERROR - - let finish_task name (cst,_) p l i = - let { Stateid.uuid = bucket }, drop = List.nth l i in - let bucket_name = match bucket with - | None -> (assert drop; ", no bucket") - | Some bucket -> Printf.sprintf ", bucket %d" (Opaqueproof.repr_handle bucket) in - match check_task_aux bucket_name name l i with - | ERROR -> exit 1 - | ERROR_ADMITTED -> cst, false - | OK_ADMITTED -> cst, false - | OK name -> - let con = Nametab.locate_constant (Libnames.qualid_of_ident name) in - let c = Global.lookup_constant con in - let () = match c.Declarations.const_body with - | Declarations.OpaqueDef _ -> () - | _ -> assert false in - (* No need to delay the computation, the future has been forced by - the call to [check_task_aux] above. *) - let uc = Option.get @@ Opaques.get_current_constraints (Option.get bucket) in - let uc = Univ.hcons_universe_context_set uc in - let access = - (* this is only used to access the local opaque (Opaques.get_current_opaque) *) - Library.indirect_accessor[@@warning "-3"] - in - let (pr, priv, ctx) = Option.get (Global.body_of_constant_body access c) in - (* We only manipulate monomorphic terms here. *) - let () = assert (UVars.AbstractContext.is_empty ctx) in - let () = match priv with - | Opaqueproof.PrivateMonomorphic () -> () - | Opaqueproof.PrivatePolymorphic uctx -> - assert (Univ.ContextSet.is_empty uctx) - in - let () = Opaques.set_opaque_disk (Option.get bucket) (pr, priv) p in - Univ.ContextSet.union cst uc, false - - let check_task name l i = - match check_task_aux "" name l i with - | OK _ | OK_ADMITTED -> true - | ERROR | ERROR_ADMITTED -> false - - let info_tasks l = - CList.map_i (fun i ({ Stateid.loc; name }, _) -> - let time1 = - try float_of_string (Aux_file.get ?loc !hints "proof_build_time") - with Not_found -> 0.0 in - let time2 = - try float_of_string (Aux_file.get ?loc !hints "proof_check_time") - with Not_found -> 0.0 in - name, max (time1 +. time2) 0.0001,i) 0 l - - let set_perspective idl = - ProofTask.set_perspective idl; - TaskQueue.broadcast (Option.get !queue); - let open ProofTask in - let overlap s1 s2 = - List.exists (fun x -> CList.mem_f Stateid.equal x s2) s1 in - let overlap_rel s1 s2 = - match overlap s1 idl, overlap s2 idl with - | true, true | false, false -> 0 - | true, false -> -1 - | false, true -> 1 in - TaskQueue.set_order (Option.get !queue) (fun task1 task2 -> - match task1, task2 with - | BuildProof { t_states = s1 }, - BuildProof { t_states = s2 } -> overlap_rel s1 s2 - | _ -> 0) - let build_proof ~doc ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name:pname () = let cancel_switch = ref false in let n_workers = TaskQueue.n_workers (Option.get !queue) in - if Int.equal n_workers 0 && not (VCS.is_vio_doc ()) then + if Int.equal n_workers 0 && not (VCS.is_vos_doc ()) then ProofTask.build_proof_here ~doc ?loc ~drop_pt exn_info block_stop, cancel_switch else let f, t_assign = Future.create_delegate ~name:pname (Some exn_info) in @@ -1890,11 +1734,11 @@ let async_policy () = else if VCS.is_interactive () then (async_proofs_is_master (cur_opt()) || (cur_opt()).async_proofs_mode = APonLazy) else - (VCS.is_vio_doc () || (cur_opt()).async_proofs_mode <> APoff) + (VCS.is_vos_doc () || (cur_opt()).async_proofs_mode <> APoff) let delegate name = get_hint_bp_time name >= (cur_opt()).async_proofs_delegation_threshold - || VCS.is_vio_doc () + || VCS.is_vos_doc () type reason = | Aborted @@ -1984,7 +1828,7 @@ let collect_proof keep cur hd brkind id = ASync (parent last,accn,name,delegate name) | SFork((_, hd', GuaranteesOpacity, ids), _) when has_proof_no_using last && not (State.is_cached_and_valid (parent last)) && - VCS.is_vio_doc () -> + VCS.is_vos_doc () -> assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch); (try let name, hint = name ids, get_hint_ctx loc in @@ -2347,15 +2191,6 @@ type stm_init_options = } - (* fb_handler : Feedback.feedback -> unit; *) - -(* -let doc_type_module_name (std : stm_doc_type) = - match std with - | VoDoc mn | VioDoc mn | Vio2Vo mn -> mn - | Interactive mn -> Names.DirPath.to_string mn -*) - let init_process stm_flags = Spawned.init_channels (); set_cur_opt stm_flags; @@ -2386,7 +2221,7 @@ let new_doc { doc_type ; injections } = set_compilation_hints f; ldir - | VioDoc f -> + | VosDoc f -> let ldir = Coqargs.(dirpath_of_top (TopPhysical f)) in VCS.set_ldir ldir; set_compilation_hints f; @@ -2478,31 +2313,6 @@ let join ~doc = CErrors.anomaly Pp.(str "Stm.join: tip not cached"); VCS.print () -type tasks = Opaqueproof.opaque_handle option Slaves.tasks -let check_task name tasks i = - let vcs = VCS.backup () in - try - let rc = State.purify (Slaves.check_task name tasks) i in - VCS.restore vcs; - rc - with e when CErrors.noncritical e -> VCS.restore vcs; false - -let info_tasks = Slaves.info_tasks - -let finish_tasks name u p tasks = - let finish_task u (_,_,i) = - let vcs = VCS.backup () in - let u = State.purify (Slaves.finish_task name u p tasks) i in - VCS.restore vcs; - u in - try - let a, _ = List.fold_left finish_task u (info_tasks tasks) in - (a,true), p - with e -> - let e = Exninfo.capture e in - msg_warning (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); - exit 1 - type branch_result = Ok | Unfocus of Stateid.t let merge_proof_branch ~valid ?id qast keep brname = @@ -2539,20 +2349,16 @@ let handle_failure (e, info) vcs = VCS.print (); Exninfo.iraise (e, info) -let snapshot_vio ~create_vos ~doc ~output_native_objects ldir long_f_dot_vo = +let snapshot_vos ~doc ~output_native_objects ldir long_f_dot_vo = let _ : Vernacstate.t = finish ~doc in if List.length (VCS.branches ()) > 1 then - CErrors.user_err (str"Cannot dump a vio with open proofs."); + CErrors.user_err (str"Cannot dump a vos with open proofs."); (* LATER: when create_vos is true, it could be more efficient to not allocate the futures; but for now it seems useful for synchronization of the workers, below, [snapshot] gets computed even if [create_vos] is true. *) let tasks = Slaves.dump_snapshot() in let except = List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty tasks in - let todo_proofs = - if create_vos - then Library.ProofsTodoSomeEmpty except - else Library.ProofsTodoSome (except,tasks) - in + let todo_proofs = Library.ProofsTodoSomeEmpty except in Library.save_library_to todo_proofs ~output_native_objects ldir long_f_dot_vo let reset_task_queue = Slaves.reset_task_queue @@ -2615,7 +2421,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) x c = | VtQuery -> let id = VCS.new_node ~id:newtip proof_mode () in let queue = - if VCS.is_vio_doc () && + if VCS.is_vos_doc () && VCS.((get_branch head).kind = Master) && may_pierce_opaque x.expr.CAst.v.expr then SkipQueue @@ -2795,8 +2601,6 @@ let add ~doc ~ontop ?newtip verb ast = | Ok -> doc, VCS.cur_tip (), NewAddTip | Unfocus qed_id -> doc, qed_id, Unfocus (VCS.cur_tip ()) -let set_perspective ~doc id_list = Slaves.set_perspective id_list - type focus = { start : Stateid.t; stop : Stateid.t; diff --git a/stm/stm.mli b/stm/stm.mli index 9c78a61a7870..0a52b5b0811d 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -47,7 +47,7 @@ end to aux files. *) type stm_doc_type = | VoDoc of string (* file path *) - | VioDoc of string (* file path *) + | VosDoc of string (* file path *) | Interactive of Coqargs.top (* module path *) (** STM initialization options: *) @@ -69,7 +69,7 @@ type doc (** [init_process] performs some low-level initialization, call early *) val init_process : AsyncOpts.stm_opt -> unit -(** [init_core] snapshorts the initial system state *) +(** [init_core] snapshots the initial system state *) val init_core : unit -> unit (** [new_doc opt] Creates a new document with options [opt] *) @@ -138,29 +138,15 @@ val stop_worker : string -> unit (* Joins the entire document. Implies finish, but also checks proofs *) val join : doc:doc -> unit -(* Saves on the disk a .vio corresponding to the current status: - - if the worker pool is empty, all tasks are saved - - if the worker proof is not empty, then it waits until all workers - are done with their current jobs and then dumps (or fails if one - of the completed tasks is a failure). - Note: the create_vos argument is used in the "-vos" mode, where the - proof tasks are not dumped into the output file. *) -val snapshot_vio : create_vos:bool -> doc:doc -> output_native_objects:bool -> DirPath.t -> string -> unit +(* Saves on the disk a .vos file. *) +val snapshot_vos : doc:doc -> output_native_objects:bool -> DirPath.t -> string -> unit (* Empties the task queue, can be used only if the worker pool is empty (E.g. - * after having built a .vio in batch mode *) + * after having built a .vos in batch mode *) val reset_task_queue : unit -> unit type document -(* A .vio contains tasks to be completed *) -type tasks = (Opaqueproof.opaque_handle option, document) Library.tasks -val check_task : string -> tasks -> int -> bool -val info_tasks : tasks -> (string * float * int) list -val finish_tasks : string -> - Library.seg_univ -> Library.seg_proofs -> - tasks -> Library.seg_univ * Library.seg_proofs - (* Id of the tip of the current branch *) val get_current_state : doc:doc -> Stateid.t val get_ldir : doc:doc -> Names.DirPath.t @@ -171,9 +157,6 @@ val get_ast : doc:doc -> Stateid.t -> Vernacexpr.vernac_control option (* Filename *) val set_compilation_hints : string -> unit -(* Reorders the task queue putting forward what is in the perspective *) -val set_perspective : doc:doc -> Stateid.t list -> unit - (** workers **************************************************************** **) module ProofTask : AsyncTaskQueue.Task diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml deleted file mode 100644 index b74e2d000bac..000000000000 --- a/stm/vio_checking.ml +++ /dev/null @@ -1,143 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* Stm.check_task f_in tasks ids && acc) true ts - -module Worker = Spawn.Sync () - -module IntOT = struct - type t = int - let compare = compare -end - -module Pool = Map.Make(IntOT) - -let schedule_vio_checking j fs = - if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0"); - let jobs = ref [] in - List.iter (fun long_f_dot_vio -> - let _,_,_, tasks, _, _ = Library.load_library_todo long_f_dot_vio in - Stm.set_compilation_hints long_f_dot_vio; - let infos = Stm.info_tasks tasks in - let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in - if infos <> [] then jobs := (long_f_dot_vio, eta, infos) :: !jobs) - fs; - let cmp_job (_,t1,_) (_,t2,_) = compare t2 t1 in - jobs := List.sort cmp_job !jobs; - let eta = ref (List.fold_left (fun a j -> a +. pi2 j) 0.0 !jobs) in - let pool : Worker.process Pool.t ref = ref Pool.empty in - let rec filter_argv b = function - | [] -> [] - | "-schedule-vio-checking" :: rest -> filter_argv true rest - | s :: rest when String.length s > 0 && s.[0] = '-' && b -> filter_argv false (s :: rest) - | _ :: rest when b -> filter_argv b rest - | s :: rest -> s :: filter_argv b rest in - let pack = function - | [] -> [] - | ((f,_),_,_) :: _ as l -> - let rec aux last acc = function - | [] -> [last,acc] - | ((f',id),_,_) :: tl when last = f' -> aux last (id::acc) tl - | ((f',id),_,_) :: _ as l -> (last,acc) :: aux f' [] l in - aux f [] l in - let prog = Sys.argv.(0) in - let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in - let make_job () = - let cur = ref 0.0 in - let what = ref [] in - let j_left = j - Pool.cardinal !pool in - let take_next_file () = - let f, t, tasks = List.hd !jobs in - jobs := List.tl !jobs; - cur := !cur +. t; - what := (List.map (fun (n,t,id) -> (f,id),n,t) tasks) @ !what in - if List.length !jobs >= j_left then take_next_file () - else while !jobs <> [] && - !cur < max 0.0 (min 60.0 (!eta /. float_of_int j_left)) do - let f, t, tasks = List.hd !jobs in - jobs := List.tl !jobs; - let n, tt, id = List.hd tasks in - if List.length tasks > 1 then - jobs := (f, t -. tt, List.tl tasks) :: !jobs; - cur := !cur +. tt; - what := ((f,id),n,tt) :: !what; - done; - if !what = [] then take_next_file (); - eta := !eta -. !cur; - let cmp_job (f1,_,_) (f2,_,_) = compare f1 f2 in - List.flatten - (List.map (fun (f, tl) -> - "-check-vio-tasks" :: - String.concat "," (List.map string_of_int tl) :: [f]) - (pack (List.sort cmp_job !what))) in - let rc = ref 0 in - while !jobs <> [] || Pool.cardinal !pool > 0 do - while Pool.cardinal !pool < j && !jobs <> [] do - let args = Array.of_list (stdargs @ make_job ()) in - let proc, _, _ = Worker.spawn prog args in - pool := Pool.add (Worker.unixpid proc) proc !pool; - done; - let pid, ret = Unix.wait () in - if ret <> Unix.WEXITED 0 then rc := 1; - Worker.kill (Pool.find pid !pool); - pool := Pool.remove pid !pool; - done; - exit !rc - -let schedule_vio_compilation j fs = - if j < 1 then CErrors.user_err Pp.(str "The number of workers must be bigger than 0"); - let jobs = ref [] in - List.iter (fun long_f_dot_vio -> - let aux = Aux_file.load_aux_file_for long_f_dot_vio in - let eta = - try float_of_string (Aux_file.get aux "vo_compile_time") - with Not_found -> 0.0 in - jobs := (long_f_dot_vio, eta) :: !jobs) - fs; - let cmp_job (_,t1) (_,t2) = compare t2 t1 in - jobs := List.sort cmp_job !jobs; - let pool : Worker.process Pool.t ref = ref Pool.empty in - let rec filter_argv b = function - | [] -> [] - | "-schedule-vio2vo" :: rest -> filter_argv true rest - | s :: rest when String.length s > 0 && s.[0] = '-' && b -> filter_argv false (s :: rest) - | _ :: rest when b -> filter_argv b rest - | s :: rest -> s :: filter_argv b rest in - let prog = Sys.argv.(0) in - let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in - let all_jobs = !jobs in - let make_job () = - let f, t = List.hd !jobs in - jobs := List.tl !jobs; - [ "-vio2vo"; f ] in - let rc = ref 0 in - while !jobs <> [] || Pool.cardinal !pool > 0 do - while Pool.cardinal !pool < j && !jobs <> [] do - let args = Array.of_list (stdargs @ make_job ()) in - let proc, _, _ = Worker.spawn prog args in - pool := Pool.add (Worker.unixpid proc) proc !pool; - done; - let pid, ret = Unix.wait () in - if ret <> Unix.WEXITED 0 then rc := 1; - Worker.kill (Pool.find pid !pool); - pool := Pool.remove pid !pool; - done; - if !rc = 0 then begin - (* set the access and last modification time of all files to the same t - * not to confuse make into thinking that some of them are outdated *) - let t = Unix.gettimeofday () in - List.iter (fun (f,_) -> Unix.utimes (Filename.chop_extension f^".vo") t t) all_jobs; - end; - exit !rc diff --git a/stm/vio_checking.mli b/stm/vio_checking.mli deleted file mode 100644 index 73036762a390..000000000000 --- a/stm/vio_checking.mli +++ /dev/null @@ -1,15 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* bool -val schedule_vio_checking : int -> string list -> unit - -val schedule_vio_compilation : int -> string list -> unit diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index 0c2dd1af607d..0a786da129df 100644 --- a/sysinit/coqargs.ml +++ b/sysinit/coqargs.ml @@ -263,7 +263,7 @@ let parse_option_set opt = 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 + produced artifact(s) (`.vo`, `.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 diff --git a/test-suite/Makefile b/test-suite/Makefile index 36fd292f8d21..e6059b94bb62 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -172,7 +172,7 @@ VSUBSYSTEMS := prerequisite success failure bugs bugs-nocoqchk output output-coq coqdoc ssr $(wildcard primitive/*) ltac2 coqchk # All subsystems -SUBSYSTEMS := $(VSUBSYSTEMS) misc ide ide vio coqchk output-coqchk coqwc coq-makefile precomputed-time-tests tools $(UNIT_TESTS) +SUBSYSTEMS := $(VSUBSYSTEMS) misc ide ide coqchk output-coqchk coqwc coq-makefile precomputed-time-tests tools $(UNIT_TESTS) # EJGA: This seems dangerous as first target... .csdp.cache: .csdp.cache.test-suite @@ -216,9 +216,9 @@ run: $(SUBSYSTEMS) clean: rm -f trace .csdp.cache .nia.cache .lia.cache output/MExtraction.out rm -f misc/universes/all_stdlib.v - $(SHOW) 'RM <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob> <**/*.time>' + $(SHOW) 'RM <**/*.stamp> <**/*.vo> <**/*.log> <**/*.glob> <**/*.time>' $(HIDE)find . \( \ - -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.vos' -o -name '*.vok' -o -name '*.log' -o -name '*.glob' -o -name '*.time' \ + -name '*.stamp' -o -name '*.vo' -o -name '*.vos' -o -name '*.vok' -o -name '*.log' -o -name '*.glob' -o -name '*.time' \ \) -exec rm -f {} + $(SHOW) 'RM <**/*.cmx> <**/*.cmi> <**/*.o> <**/*.test>' $(HIDE)find unit-tests \( \ @@ -264,7 +264,6 @@ summary: $(call summary_dir, "STM tests", stm); \ $(call summary_dir, "SSR tests", ssr); \ $(call summary_dir, "IDE tests", ide); \ - $(call summary_dir, "VI tests", vio); \ $(call summary_dir, "Coqchk tests", coqchk); \ $(call summary_dir, "Output tests with coqchk", output-coqchk); \ $(call summary_dir, "Coqwc tests", coqwc); \ @@ -707,27 +706,6 @@ ide/fake_ide.exe : ide/fake_ide.ml } > "$@" $(HIDE)$(call REPORT_TIMER,$@) -# vio compilation - -vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v)) - -%.vio.log:%.v - @echo "TEST $<" - $(HIDE){ \ - $(call WITH_TIMER,$*.vio,$(coqc) -vio -R vio vio $* 2>&1) && \ - $(call WITH_TIMER,$*.vo,$(coqc) -R vio vio -vio2vo $*.vio 2>&1) && \ - $(call WITH_TIMER,$*.chk,$(coqchk) -R vio vio -norec $(subst /,.,$*) 2>&1); \ - if [ $$? = 0 ]; then \ - echo $(log_success); \ - echo " $<...Ok"; \ - else \ - echo $(log_failure); \ - echo " $<...Error!"; \ - $(FAIL); \ - fi; \ - } > "$@" - $(HIDE)$(call REPORT_TIMER,$*.vio $*.vo $*.chk) - # coqwc : test output coqwc : $(patsubst %.v,%.v.log,$(wildcard coqwc/*.v)) diff --git a/test-suite/bugs-nocoqchk/bug_6165.v b/test-suite/bugs-nocoqchk/bug_6165.v index b87a7caaf266..ecf29bb0325d 100644 --- a/test-suite/bugs-nocoqchk/bug_6165.v +++ b/test-suite/bugs-nocoqchk/bug_6165.v @@ -1,5 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-quick") -*- *) - +(* -*- mode: coq; coq-prog-args: ("-vos") -*- *) Goal True. abstract exact I. Timeout 1 Defined. diff --git a/test-suite/coq-makefile/quick2vo/_CoqProject b/test-suite/coq-makefile/quick2vo/_CoqProject deleted file mode 100644 index 81b3f60e6d2f..000000000000 --- a/test-suite/coq-makefile/quick2vo/_CoqProject +++ /dev/null @@ -1,11 +0,0 @@ -src/META.coq-test-suite --R src test --R theories test --I src - -src/test_plugin.mlpack -src/test.mlg -src/test.mli -src/test_aux.ml -src/test_aux.mli -theories/test.v diff --git a/test-suite/coq-makefile/quick2vo/run.sh b/test-suite/coq-makefile/quick2vo/run.sh deleted file mode 100755 index dda51dd2e4c5..000000000000 --- a/test-suite/coq-makefile/quick2vo/run.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/usr/bin/env bash -a=$(uname) - -. ../template/init.sh - -coq_makefile -f _CoqProject -o Makefile -# vio2vo is broken on Windows (#6720) -if [ "$a" = "Darwin" ] || [ "$a" = "Linux" ]; then - make quick2vo J=2 - test -f theories/test.vo - make validate -fi diff --git a/test-suite/coq-makefile/vio2vo/_CoqProject b/test-suite/coq-makefile/vio2vo/_CoqProject deleted file mode 100644 index 81b3f60e6d2f..000000000000 --- a/test-suite/coq-makefile/vio2vo/_CoqProject +++ /dev/null @@ -1,11 +0,0 @@ -src/META.coq-test-suite --R src test --R theories test --I src - -src/test_plugin.mlpack -src/test.mlg -src/test.mli -src/test_aux.ml -src/test_aux.mli -theories/test.v diff --git a/test-suite/coq-makefile/vio2vo/run.sh b/test-suite/coq-makefile/vio2vo/run.sh deleted file mode 100755 index e555d62f35de..000000000000 --- a/test-suite/coq-makefile/vio2vo/run.sh +++ /dev/null @@ -1,13 +0,0 @@ -#!/usr/bin/env bash -a=$(uname) - -. ../template/init.sh - -coq_makefile -f _CoqProject -o Makefile -make quick -# vio2vo is broken on Windows (#6720) -if [ "$a" = "Darwin" ] || [ "$a" = "Linux" ]; then - make vio2vo J=2 - test -f theories/test.vo - make validate -fi diff --git a/test-suite/misc/coqc_dash_vok.sh b/test-suite/misc/coqc_dash_vok.sh index f945afa1f84d..5e4e7f2ff075 100755 --- a/test-suite/misc/coqc_dash_vok.sh +++ b/test-suite/misc/coqc_dash_vok.sh @@ -2,11 +2,10 @@ IN_V=misc/coqc_cmdline.v OUT_VO=misc/coqc_cmdline.vo -OUT_VIO=misc/coqc_cmdline.vio OUT_VOS=misc/coqc_cmdline.vos OUT_VOK=misc/coqc_cmdline.vok OUT_GLOB=misc/coqc_cmdline.glob -OUT="${OUT_VO} ${OUT_VIO} ${OUT_VOS} ${OUT_VOK} ${OUT_GLOB}" +OUT="${OUT_VO} ${OUT_VOS} ${OUT_VOK} ${OUT_GLOB}" rm -f ${OUT} @@ -29,15 +28,5 @@ if [ ! -f ${OUT_VOK} ]; then exit 1 fi -rm -f ${OUT} - -$coqc ${IN_V} -vio -$coqc -vio2vo ${OUT_VIO} -if [ ! -f ${OUT_VOK} ]; then - echo "vok not produced in -vio2vo mode" - rm -f ${OUT} - exit 1 -fi - rm -f ${OUT} exit 0 diff --git a/test-suite/misc/coqdep-require-filter-categories/stdout.ref b/test-suite/misc/coqdep-require-filter-categories/stdout.ref index 34e05b51c0ff..d460cf4c824f 100644 --- a/test-suite/misc/coqdep-require-filter-categories/stdout.ref +++ b/test-suite/misc/coqdep-require-filter-categories/stdout.ref @@ -1,14 +1,7 @@ fA.vo fA.glob fA.v.beautified fA.required_vo: fA.v -fA.vio: fA.v fB.vo fB.glob fB.v.beautified fB.required_vo: fB.v fA.vo -fB.vio: fB.v fA.vio fC.vo fC.glob fC.v.beautified fC.required_vo: fC.v fB.vo -fC.vio: fC.v fB.vio fD.vo fD.glob fD.v.beautified fD.required_vo: fD.v fA.vo -fD.vio: fD.v fA.vio fE.vo fE.glob fE.v.beautified fE.required_vo: fE.v fA.vo -fE.vio: fE.v fA.vio fF.vo fF.glob fF.v.beautified fF.required_vo: fF.v fA.vo -fF.vio: fF.v fA.vio fG.vo fG.glob fG.v.beautified fG.required_vo: fG.v fA.vo -fG.vio: fG.v fA.vio diff --git a/test-suite/misc/deps/DistinctRootDeps.out b/test-suite/misc/deps/DistinctRootDeps.out index 66f9539b7e1a..2801128c14c2 100644 --- a/test-suite/misc/deps/DistinctRootDeps.out +++ b/test-suite/misc/deps/DistinctRootDeps.out @@ -1,6 +1,3 @@ DistinctRoot/A/File1.vo DistinctRoot/A/File1.glob DistinctRoot/A/File1.v.beautified DistinctRoot/A/File1.required_vo: DistinctRoot/A/File1.v -DistinctRoot/A/File1.vio: DistinctRoot/A/File1.v DistinctRoot/B/File1.vo DistinctRoot/B/File1.glob DistinctRoot/B/File1.v.beautified DistinctRoot/B/File1.required_vo: DistinctRoot/B/File1.v -DistinctRoot/B/File1.vio: DistinctRoot/B/File1.v DistinctRoot/File2.vo DistinctRoot/File2.glob DistinctRoot/File2.v.beautified DistinctRoot/File2.required_vo: DistinctRoot/File2.v DistinctRoot/B/File1.vo -DistinctRoot/File2.vio: DistinctRoot/File2.v DistinctRoot/B/File1.vio diff --git a/test-suite/misc/deps/Theory1Deps.out b/test-suite/misc/deps/Theory1Deps.out index 76c3ab728da5..317488e01506 100644 --- a/test-suite/misc/deps/Theory1Deps.out +++ b/test-suite/misc/deps/Theory1Deps.out @@ -1,16 +1,8 @@ Theory1/File1.vo Theory1/File1.glob Theory1/File1.v.beautified Theory1/File1.required_vo: Theory1/File1.v -Theory1/File1.vio: Theory1/File1.v Theory1/File2.vo Theory1/File2.glob Theory1/File2.v.beautified Theory1/File2.required_vo: Theory1/File2.v Theory1/File1.vo -Theory1/File2.vio: Theory1/File2.v Theory1/File1.vio Theory1/Subtheory1/File1.vo Theory1/Subtheory1/File1.glob Theory1/Subtheory1/File1.v.beautified Theory1/Subtheory1/File1.required_vo: Theory1/Subtheory1/File1.v -Theory1/Subtheory1/File1.vio: Theory1/Subtheory1/File1.v Theory1/Subtheory1/Subsubtheory1/File1.vo Theory1/Subtheory1/Subsubtheory1/File1.glob Theory1/Subtheory1/Subsubtheory1/File1.v.beautified Theory1/Subtheory1/Subsubtheory1/File1.required_vo: Theory1/Subtheory1/Subsubtheory1/File1.v -Theory1/Subtheory1/Subsubtheory1/File1.vio: Theory1/Subtheory1/Subsubtheory1/File1.v Theory1/Subtheory1/Subsubtheory2/File1.vo Theory1/Subtheory1/Subsubtheory2/File1.glob Theory1/Subtheory1/Subsubtheory2/File1.v.beautified Theory1/Subtheory1/Subsubtheory2/File1.required_vo: Theory1/Subtheory1/Subsubtheory2/File1.v -Theory1/Subtheory1/Subsubtheory2/File1.vio: Theory1/Subtheory1/Subsubtheory2/File1.v Theory1/Subtheory2/File1.vo Theory1/Subtheory2/File1.glob Theory1/Subtheory2/File1.v.beautified Theory1/Subtheory2/File1.required_vo: Theory1/Subtheory2/File1.v -Theory1/Subtheory2/File1.vio: Theory1/Subtheory2/File1.v Theory1/Subtheory2/Subsubtheory1/File1.vo Theory1/Subtheory2/Subsubtheory1/File1.glob Theory1/Subtheory2/Subsubtheory1/File1.v.beautified Theory1/Subtheory2/Subsubtheory1/File1.required_vo: Theory1/Subtheory2/Subsubtheory1/File1.v -Theory1/Subtheory2/Subsubtheory1/File1.vio: Theory1/Subtheory2/Subsubtheory1/File1.v Theory1/Subtheory2/Subsubtheory2/File1.vo Theory1/Subtheory2/Subsubtheory2/File1.glob Theory1/Subtheory2/Subsubtheory2/File1.v.beautified Theory1/Subtheory2/Subsubtheory2/File1.required_vo: Theory1/Subtheory2/Subsubtheory2/File1.v -Theory1/Subtheory2/Subsubtheory2/File1.vio: Theory1/Subtheory2/Subsubtheory2/File1.v diff --git a/test-suite/misc/deps/Theory2Deps.out b/test-suite/misc/deps/Theory2Deps.out index 63d299961791..915bdf157a93 100644 --- a/test-suite/misc/deps/Theory2Deps.out +++ b/test-suite/misc/deps/Theory2Deps.out @@ -1,17 +1,10 @@ Theory2/File2.vo Theory2/File2.glob Theory2/File2.v.beautified Theory2/File2.required_vo: Theory2/File2.v Theory2/Subtheory1/File1.vo Theory2/Subtheory1/Subsubtheory1/File1.vo Theory2/Subtheory1/Subsubtheory2/File1.vo Theory2/Subtheory2/File1.vo Theory2/Subtheory2/Subsubtheory1/File1.vo Theory2/Subtheory2/Subsubtheory2/File1.vo -Theory2/File2.vio: Theory2/File2.v Theory2/Subtheory1/File1.vio Theory2/Subtheory1/Subsubtheory1/File1.vio Theory2/Subtheory1/Subsubtheory2/File1.vio Theory2/Subtheory2/File1.vio Theory2/Subtheory2/Subsubtheory1/File1.vio Theory2/Subtheory2/Subsubtheory2/File1.vio Theory2/Subtheory1/File1.vo Theory2/Subtheory1/File1.glob Theory2/Subtheory1/File1.v.beautified Theory2/Subtheory1/File1.required_vo: Theory2/Subtheory1/File1.v -Theory2/Subtheory1/File1.vio: Theory2/Subtheory1/File1.v Theory2/Subtheory1/Subsubtheory1/File1.vo Theory2/Subtheory1/Subsubtheory1/File1.glob Theory2/Subtheory1/Subsubtheory1/File1.v.beautified Theory2/Subtheory1/Subsubtheory1/File1.required_vo: Theory2/Subtheory1/Subsubtheory1/File1.v -Theory2/Subtheory1/Subsubtheory1/File1.vio: Theory2/Subtheory1/Subsubtheory1/File1.v Theory2/Subtheory1/Subsubtheory2/File1.vo Theory2/Subtheory1/Subsubtheory2/File1.glob Theory2/Subtheory1/Subsubtheory2/File1.v.beautified Theory2/Subtheory1/Subsubtheory2/File1.required_vo: Theory2/Subtheory1/Subsubtheory2/File1.v -Theory2/Subtheory1/Subsubtheory2/File1.vio: Theory2/Subtheory1/Subsubtheory2/File1.v Theory2/Subtheory2/File1.vo Theory2/Subtheory2/File1.glob Theory2/Subtheory2/File1.v.beautified Theory2/Subtheory2/File1.required_vo: Theory2/Subtheory2/File1.v -Theory2/Subtheory2/File1.vio: Theory2/Subtheory2/File1.v Theory2/Subtheory2/Subsubtheory1/File1.vo Theory2/Subtheory2/Subsubtheory1/File1.glob Theory2/Subtheory2/Subsubtheory1/File1.v.beautified Theory2/Subtheory2/Subsubtheory1/File1.required_vo: Theory2/Subtheory2/Subsubtheory1/File1.v -Theory2/Subtheory2/Subsubtheory1/File1.vio: Theory2/Subtheory2/Subsubtheory1/File1.v Theory2/Subtheory2/Subsubtheory2/File1.vo Theory2/Subtheory2/Subsubtheory2/File1.glob Theory2/Subtheory2/Subsubtheory2/File1.v.beautified Theory2/Subtheory2/Subsubtheory2/File1.required_vo: Theory2/Subtheory2/Subsubtheory2/File1.v -Theory2/Subtheory2/Subsubtheory2/File1.vio: Theory2/Subtheory2/Subsubtheory2/File1.v *** Warning: in file Theory2/File2.v, required library File1 matches several files in path (found File1.v in Theory2/Subtheory2/Subsubtheory2, Theory2/Subtheory2/Subsubtheory1, Theory2/Subtheory2, Theory2/Subtheory1/Subsubtheory2, Theory2/Subtheory1/Subsubtheory1 and Theory2/Subtheory1; Require will fail). diff --git a/test-suite/misc/deps/Theory3Deps.out b/test-suite/misc/deps/Theory3Deps.out index df86906aa5ab..f531218378de 100644 --- a/test-suite/misc/deps/Theory3Deps.out +++ b/test-suite/misc/deps/Theory3Deps.out @@ -1,13 +1,8 @@ Theory3/File2.vo Theory3/File2.glob Theory3/File2.v.beautified Theory3/File2.required_vo: Theory3/File2.v Theory3/Subtheory1/File1.vo Theory3/Subtheory1/Subsubtheory1/File1.vo Theory3/Subtheory1/Subsubtheory2/File1.vo Theory3/Subtheory2/File1.vo -Theory3/File2.vio: Theory3/File2.v Theory3/Subtheory1/File1.vio Theory3/Subtheory1/Subsubtheory1/File1.vio Theory3/Subtheory1/Subsubtheory2/File1.vio Theory3/Subtheory2/File1.vio Theory3/Subtheory1/File1.vo Theory3/Subtheory1/File1.glob Theory3/Subtheory1/File1.v.beautified Theory3/Subtheory1/File1.required_vo: Theory3/Subtheory1/File1.v -Theory3/Subtheory1/File1.vio: Theory3/Subtheory1/File1.v Theory3/Subtheory1/Subsubtheory1/File1.vo Theory3/Subtheory1/Subsubtheory1/File1.glob Theory3/Subtheory1/Subsubtheory1/File1.v.beautified Theory3/Subtheory1/Subsubtheory1/File1.required_vo: Theory3/Subtheory1/Subsubtheory1/File1.v -Theory3/Subtheory1/Subsubtheory1/File1.vio: Theory3/Subtheory1/Subsubtheory1/File1.v Theory3/Subtheory1/Subsubtheory2/File1.vo Theory3/Subtheory1/Subsubtheory2/File1.glob Theory3/Subtheory1/Subsubtheory2/File1.v.beautified Theory3/Subtheory1/Subsubtheory2/File1.required_vo: Theory3/Subtheory1/Subsubtheory2/File1.v -Theory3/Subtheory1/Subsubtheory2/File1.vio: Theory3/Subtheory1/Subsubtheory2/File1.v Theory3/Subtheory2/File1.vo Theory3/Subtheory2/File1.glob Theory3/Subtheory2/File1.v.beautified Theory3/Subtheory2/File1.required_vo: Theory3/Subtheory2/File1.v -Theory3/Subtheory2/File1.vio: Theory3/Subtheory2/File1.v *** Warning: in file Theory3/File2.v, required library File1 matches several files in path (found File1.v in Theory3/Subtheory2, Theory3/Subtheory1/Subsubtheory2, Theory3/Subtheory1/Subsubtheory1 and Theory3/Subtheory1; Require will fail). diff --git a/test-suite/misc/deps/deps-from.out b/test-suite/misc/deps/deps-from.out index 5951ea54b35d..fbf53a634873 100644 --- a/test-suite/misc/deps/deps-from.out +++ b/test-suite/misc/deps/deps-from.out @@ -1,4 +1,2 @@ misc/deps/test-from/D.vo misc/deps/test-from/D.glob misc/deps/test-from/D.v.beautified misc/deps/test-from/D.required_vo: misc/deps/test-from/D.v misc/deps/test-from/A/C.vo -misc/deps/test-from/D.vio: misc/deps/test-from/D.v misc/deps/test-from/A/C.vio misc/deps/test-from/E.vo misc/deps/test-from/E.glob misc/deps/test-from/E.v.beautified misc/deps/test-from/E.required_vo: misc/deps/test-from/E.v misc/deps/test-from/B/C.vo -misc/deps/test-from/E.vio: misc/deps/test-from/E.v misc/deps/test-from/B/C.vio diff --git a/test-suite/misc/external-deps/file1.ambiguous.deps b/test-suite/misc/external-deps/file1.ambiguous.deps index 832b978ecd78..6b3e61482afb 100644 --- a/test-suite/misc/external-deps/file1.ambiguous.deps +++ b/test-suite/misc/external-deps/file1.ambiguous.deps @@ -1,5 +1,4 @@ misc/external-deps/file1.vo misc/external-deps/file1.glob misc/external-deps/file1.v.beautified misc/external-deps/file1.required_vo: misc/external-deps/file1.v misc/external-deps/more/d1 -misc/external-deps/file1.vio: misc/external-deps/file1.v misc/external-deps/more/d1 *** Warning: in file misc/external-deps/file1.v, required external file d1 exactly matches several files in path (found d1 in misc/external-deps/deps and misc/external-deps/more; used the latter). diff --git a/test-suite/misc/external-deps/file1.found.deps b/test-suite/misc/external-deps/file1.found.deps index 379206edac3b..366d600ea352 100644 --- a/test-suite/misc/external-deps/file1.found.deps +++ b/test-suite/misc/external-deps/file1.found.deps @@ -1,2 +1 @@ misc/external-deps/file1.vo misc/external-deps/file1.glob misc/external-deps/file1.v.beautified misc/external-deps/file1.required_vo: misc/external-deps/file1.v misc/external-deps/deps/d1 -misc/external-deps/file1.vio: misc/external-deps/file1.v misc/external-deps/deps/d1 diff --git a/test-suite/misc/external-deps/file1.notfound.deps b/test-suite/misc/external-deps/file1.notfound.deps index 5985cbc7b335..e3b4329d793b 100644 --- a/test-suite/misc/external-deps/file1.notfound.deps +++ b/test-suite/misc/external-deps/file1.notfound.deps @@ -2,4 +2,3 @@ Warning: in file misc/external-deps/file1.v, external file d1 is required from root foo.bar and has not been found in the loadpath! [module-not-found,filesystem,default] misc/external-deps/file1.vo misc/external-deps/file1.glob misc/external-deps/file1.v.beautified misc/external-deps/file1.required_vo: misc/external-deps/file1.v -misc/external-deps/file1.vio: misc/external-deps/file1.v diff --git a/test-suite/misc/external-deps/file2.ambiguous.deps b/test-suite/misc/external-deps/file2.ambiguous.deps index da8d2996d83f..00634e604176 100644 --- a/test-suite/misc/external-deps/file2.ambiguous.deps +++ b/test-suite/misc/external-deps/file2.ambiguous.deps @@ -1,5 +1,4 @@ misc/external-deps/file2.vo misc/external-deps/file2.glob misc/external-deps/file2.v.beautified misc/external-deps/file2.required_vo: misc/external-deps/file2.v misc/external-deps/more/d1 -misc/external-deps/file2.vio: misc/external-deps/file2.v misc/external-deps/more/d1 *** Warning: in file misc/external-deps/file2.v, required external file d1 exactly matches several files in path (found d1 in misc/external-deps/deps and misc/external-deps/more; used the latter). diff --git a/test-suite/misc/external-deps/file2.found.deps b/test-suite/misc/external-deps/file2.found.deps index 9ab7d347ab2d..8b62bdfe6aba 100644 --- a/test-suite/misc/external-deps/file2.found.deps +++ b/test-suite/misc/external-deps/file2.found.deps @@ -1,2 +1 @@ misc/external-deps/file2.vo misc/external-deps/file2.glob misc/external-deps/file2.v.beautified misc/external-deps/file2.required_vo: misc/external-deps/file2.v misc/external-deps/deps/d1 -misc/external-deps/file2.vio: misc/external-deps/file2.v misc/external-deps/deps/d1 diff --git a/test-suite/misc/external-deps/file2.notfound.deps b/test-suite/misc/external-deps/file2.notfound.deps index ae49c0228372..c8b67c1c1fdb 100644 --- a/test-suite/misc/external-deps/file2.notfound.deps +++ b/test-suite/misc/external-deps/file2.notfound.deps @@ -2,4 +2,3 @@ Warning: in file misc/external-deps/file2.v, external file d1 is required from root foo.bar and has not been found in the loadpath! [module-not-found,filesystem,default] misc/external-deps/file2.vo misc/external-deps/file2.glob misc/external-deps/file2.v.beautified misc/external-deps/file2.required_vo: misc/external-deps/file2.v -misc/external-deps/file2.vio: misc/external-deps/file2.v diff --git a/test-suite/misc/quick-include.sh b/test-suite/misc/quick-include.sh deleted file mode 100755 index e60fb48bca8f..000000000000 --- a/test-suite/misc/quick-include.sh +++ /dev/null @@ -1,5 +0,0 @@ -#!/bin/sh -set -e - -$coqc -R misc/quick-include/ QuickInclude -vio misc/quick-include/file1.v -$coqc -R misc/quick-include/ QuickInclude -vio misc/quick-include/file2.v diff --git a/test-suite/misc/quick-include/file1.v b/test-suite/misc/quick-include/file1.v deleted file mode 100644 index fa48e240cb05..000000000000 --- a/test-suite/misc/quick-include/file1.v +++ /dev/null @@ -1,18 +0,0 @@ - -Module Type E. End E. - -Module M. - Lemma x : True. - Proof. trivial. Qed. -End M. - - -Module Type T. - Lemma x : True. - Proof. trivial. Qed. -End T. - -Module F(A:E). - Lemma x : True. - Proof. trivial. Qed. -End F. diff --git a/test-suite/misc/quick-include/file2.v b/test-suite/misc/quick-include/file2.v deleted file mode 100644 index ab10dfd8de2a..000000000000 --- a/test-suite/misc/quick-include/file2.v +++ /dev/null @@ -1,6 +0,0 @@ - -From QuickInclude Require file1. - -Module M. Include file1.M. End M. -Module T. Include file1.T. End T. -Module F. Include file1.F. End F. diff --git a/test-suite/misc/vio_checking.sh b/test-suite/misc/vio_checking.sh deleted file mode 100755 index c2863a0b3e6c..000000000000 --- a/test-suite/misc/vio_checking.sh +++ /dev/null @@ -1,32 +0,0 @@ -#!/usr/bin/env bash - -set -ex - -export COQBIN=$BIN -export PATH=$COQBIN:$PATH - -cd misc - -rm -f vio_checking{,_bad}.{vo,vio} - -coqc -vio vio_checking.v -coqc -vio vio_checking_bad.v - -coqc -schedule-vio-checking 2 vio_checking.vio - -if coqc -schedule-vio-checking 2 vio_checking_bad.vio; then - echo 'vio-checking on vio_checking_bad.vio should have failed!' - exit 1 -fi -if coqc -schedule-vio-checking 2 vio_checking.vio vio_checking_bad.vio; then - echo 'vio-checking on vio_checking vio_checking_bad.vio should have failed!' - exit 1 -fi - -coqc -vio2vo vio_checking.vio -coqchk -silent vio_checking.vo - -if coqc -vio2vo vio_checking_bad.vio; then - echo 'vio2vo on vio_checking_bad.vio should have failed!' - exit 1 -fi diff --git a/test-suite/misc/vio_checking.v b/test-suite/misc/vio_checking.v deleted file mode 100644 index 8dd5e47383eb..000000000000 --- a/test-suite/misc/vio_checking.v +++ /dev/null @@ -1,9 +0,0 @@ - -Lemma foo : Type. -Proof. exact Type. Qed. - -Lemma foo1 : Type. -Proof. exact Type. Qed. - -Lemma foo2 : Type. -Proof. exact foo1. Qed. diff --git a/test-suite/misc/vio_checking_bad.v b/test-suite/misc/vio_checking_bad.v deleted file mode 100644 index f32d06f34a94..000000000000 --- a/test-suite/misc/vio_checking_bad.v +++ /dev/null @@ -1,4 +0,0 @@ -(* a file to check that vio-checking is not a noop *) - -Lemma foo : Type. -Proof. match goal with |- ?G => exact G end. Qed. diff --git a/test-suite/output/ErrorInModule.v b/test-suite/output/ErrorInModule.v index ead6e8727a3f..3e1aae914ceb 100644 --- a/test-suite/output/ErrorInModule.v +++ b/test-suite/output/ErrorInModule.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-vio") -*- *) +(* -*- mode: coq; coq-prog-args: ("-vos") -*- *) Module M. Fail Definition foo := nonexistent. End M. diff --git a/test-suite/output/ErrorInSection.v b/test-suite/output/ErrorInSection.v index 4c62b01a2cf0..3968adef0f36 100644 --- a/test-suite/output/ErrorInSection.v +++ b/test-suite/output/ErrorInSection.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-vio") -*- *) +(* -*- mode: coq; coq-prog-args: ("-vos") -*- *) Section S. Fail Definition foo := nonexistent. End S. diff --git a/test-suite/vio/numeral.v b/test-suite/vio/numeral.v deleted file mode 100644 index f28355bb29d0..000000000000 --- a/test-suite/vio/numeral.v +++ /dev/null @@ -1,21 +0,0 @@ -Lemma foo : True. -Proof. -Check 0 : nat. -Check 0 : nat. -exact I. -Qed. - -Lemma bar : True. -Proof. -pose (0 : nat). -exact I. -Qed. - -Require Import Coq.Strings.Ascii. -Open Scope char_scope. - -Lemma baz : True. -Proof. -pose "s". -exact I. -Qed. diff --git a/test-suite/vio/print.v b/test-suite/vio/print.v deleted file mode 100644 index 9c36a463c974..000000000000 --- a/test-suite/vio/print.v +++ /dev/null @@ -1,10 +0,0 @@ -Lemma a : True. -Proof. -idtac. -exact I. -Qed. - -Print a. - -Lemma b : False. -Admitted. diff --git a/test-suite/vio/section.v b/test-suite/vio/section.v deleted file mode 100644 index 0e7722516a8c..000000000000 --- a/test-suite/vio/section.v +++ /dev/null @@ -1,12 +0,0 @@ -Section Foo. - Variable A : Type. - - Definition bla := A. - - Variable B : bla. - - Lemma blu : {X:Type & X}. - Proof using A B. - exists bla;exact B. - Qed. -End Foo. diff --git a/test-suite/vio/seff.v b/test-suite/vio/seff.v deleted file mode 100644 index 447e7798336a..000000000000 --- a/test-suite/vio/seff.v +++ /dev/null @@ -1,10 +0,0 @@ -Inductive equal T (x : T) : T -> Type := Equal : equal T x x. - -Module bla. - -Lemma test n : equal nat n (n + n) -> equal nat (n + n + n) n. -Proof using. -intro H. rewrite <- H. rewrite <- H. exact (Equal nat n). -Qed. - -End bla. diff --git a/test-suite/vio/simple.v b/test-suite/vio/simple.v deleted file mode 100644 index 407074c1e7af..000000000000 --- a/test-suite/vio/simple.v +++ /dev/null @@ -1,2 +0,0 @@ -Lemma simple : True. -Proof using. trivial. Qed. diff --git a/test-suite/vio/univ_constraints_statements.v b/test-suite/vio/univ_constraints_statements.v deleted file mode 100644 index bb6b95957d05..000000000000 --- a/test-suite/vio/univ_constraints_statements.v +++ /dev/null @@ -1,2 +0,0 @@ -Lemma ssr_congr_arrow Plemma Pgoal : Plemma = Pgoal -> Plemma -> Pgoal. -Proof using. intro H; rewrite H; trivial. Qed. diff --git a/test-suite/vio/univ_constraints_statements_body.v b/test-suite/vio/univ_constraints_statements_body.v deleted file mode 100644 index 6302adefc2f1..000000000000 --- a/test-suite/vio/univ_constraints_statements_body.v +++ /dev/null @@ -1,7 +0,0 @@ -Definition T := Type. -Definition T1 : T := Type. - -Lemma x : True. -Proof. -exact (let a : T := Type in I). -Qed. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 8114355535f9..d56d1146db34 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -503,37 +503,6 @@ bytefiles: $(CMOFILES) $(CMAFILES) optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) .PHONY: optfiles -# FIXME, see Ralf's bugreport -# quick is deprecated, now renamed vio -vio: $(VOFILES:.vo=.vio) -.PHONY: vio -quick: vio - $(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files") -.PHONY: quick - -vio2vo: - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ - -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) -.PHONY: vio2vo - -# quick2vo is undocumented -quick2vo: - $(HIDE)make -j $(J) vio - $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \ - viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \ - if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \ - done); \ - echo "VIO2VO: $$VIOFILES"; \ - if [ -n "$$VIOFILES" ]; then \ - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \ - fi -.PHONY: quick2vo - -checkproofs: - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ - -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) -.PHONY: checkproofs - vos: $(VOFILES:%.vo=%.vos) .PHONY: vos @@ -711,7 +680,6 @@ clean:: $(HIDE)rm -f $(NATIVEFILES) $(HIDE)find . -name .coq-native -type d -empty -delete $(HIDE)rm -f $(VOFILES) - $(HIDE)rm -f $(VOFILES:.vo=.vio) $(HIDE)rm -f $(VOFILES:.vo=.vos) $(HIDE)rm -f $(VOFILES:.vo=.vok) $(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old) @@ -846,10 +814,6 @@ endif $(foreach vfile,$(VFILES:.v=),$(eval $(call globvorule,$(vfile)))) -$(VFILES:.v=.vio): %.vio: %.v - $(SHOW)COQC -vio $< - $(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< - $(VFILES:.v=.vos): %.vos: %.v $(SHOW)COQC -vos $< $(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< diff --git a/tools/coqdep/lib/common.ml b/tools/coqdep/lib/common.ml index aa95547d08af..954954071689 100644 --- a/tools/coqdep/lib/common.ml +++ b/tools/coqdep/lib/common.ml @@ -120,7 +120,7 @@ end module VCache = Set.Make(VData) (** To avoid reading .v files several times for computing dependencies, - once for .vo, once for .vio, and once for .vos extensions, the + once for .vo, and once for .vos extensions, the following code performs a single pass and produces a structured list of dependencies, separating dependencies on compiled Coq files (those loaded by [Require]) from other dependencies, e.g. dependencies diff --git a/tools/coqdep/lib/dep_info.ml b/tools/coqdep/lib/dep_info.ml index 1bc3dc09e366..65eb4928d9f7 100644 --- a/tools/coqdep/lib/dep_info.ml +++ b/tools/coqdep/lib/dep_info.ml @@ -10,7 +10,7 @@ module Dep = struct type t = - | Require of string (* one basename, to which we later append .vo or .vio or .vos *) + | Require of string (* one basename, to which we later append .vo or .vos *) | Ml of string * string | Other of string (* filenames of dependencies, separated by spaces *) end diff --git a/tools/coqdep/lib/dep_info.mli b/tools/coqdep/lib/dep_info.mli index 2fac5a05c442..10e361bd13e4 100644 --- a/tools/coqdep/lib/dep_info.mli +++ b/tools/coqdep/lib/dep_info.mli @@ -11,7 +11,7 @@ module Dep : sig type t = | Require of string - (** module basename, to which we later append .vo or .vio or .vos *) + (** module basename, to which we later append .vo or .vos *) | Ml of string * string (** plugin basename and byte extension, resolved from Declare Ml Module *) | Other of string diff --git a/tools/coqdep/lib/loadpath.ml b/tools/coqdep/lib/loadpath.ml index d4c48a77075d..4b0541dfc664 100644 --- a/tools/coqdep/lib/loadpath.ml +++ b/tools/coqdep/lib/loadpath.ml @@ -262,16 +262,16 @@ let add_paths recur root table phys_dir log_dir basename = let add_coqlib_known st recur root phys_dir log_dir f = let root = (phys_dir, log_dir) in - match get_extension f [".vo"; ".vio"; ".vos"] with - | (basename, (".vo" | ".vio" | ".vos")) -> + match get_extension f [".vo"; ".vos"] with + | (basename, (".vo" | ".vos")) -> add_paths recur root st.State.coqlib phys_dir log_dir basename | _ -> () let add_known st recur root phys_dir log_dir f = - match get_extension f [".v"; ".vo"; ".vio"; ".vos"] with + match get_extension f [".v"; ".vo"; ".vos"] with | (basename,".v") -> add_paths recur root st.State.vfiles phys_dir log_dir basename - | (basename, (".vo" | ".vio" | ".vos")) when not st.State.boot -> + | (basename, (".vo" | ".vos")) when not st.State.boot -> add_paths recur root st.State.vfiles phys_dir log_dir basename | (f,_) -> add_paths recur root st.State.other phys_dir log_dir f diff --git a/tools/coqdep/lib/makefile.ml b/tools/coqdep/lib/makefile.ml index 6803bc3e4afa..663b5803280b 100644 --- a/tools/coqdep/lib/makefile.ml +++ b/tools/coqdep/lib/makefile.ml @@ -82,8 +82,6 @@ let print_dep fmt { Dep_info.name; deps } = let glob = if !option_noglob then "" else ename^".glob " in fprintf fmt "%s.vo %s%s.v.beautified %s.required_vo: %s.v %s\n" ename glob ename ename ename (string_of_dependency_list ~suffix:".vo" deps); - fprintf fmt "%s.vio: %s.v %s\n" ename ename - (string_of_dependency_list ~suffix:".vio" deps); if !option_write_vos then fprintf fmt "%s.vos %s.vok %s.required_vos: %s.v %s\n" ename ename ename ename (string_of_dependency_list ~suffix:".vos" deps); diff --git a/tools/dune_rule_gen/coq_module.ml b/tools/dune_rule_gen/coq_module.ml index 797d219d89e6..f6a7bbc07a67 100644 --- a/tools/dune_rule_gen/coq_module.ml +++ b/tools/dune_rule_gen/coq_module.ml @@ -29,16 +29,11 @@ module Rule_type = struct type native = Disabled | Coqc | CoqNative type t = | Regular of { native : native } - | Quick - (** build / depend on .vio instead of .vo *) let native_coqc = function | Regular { native = Coqc } -> true | Regular { native = CoqNative } - | Regular { native = Disabled } - | Quick -> false - let quick = function Regular _ -> false | Quick -> true - let vo_ext = function Regular _ -> ".vo" | Quick -> ".vio" + | Regular { native = Disabled } -> false end @@ -48,25 +43,17 @@ let native_obj_files ~install ~tname { prefix; name; _ } = let prefix file = if install then Filename.concat ".coq-native" file else file in [ prefix @@ native_base ^ ".cmi"; prefix @@ native_base ^ ".cmxs" ] -let base_obj_files ~rule coq_module = - let quick = Rule_type.quick rule in - let vo_ext = Rule_type.vo_ext rule in - - let aux_objs = if quick then [] - else - [ mod_to_obj coq_module ~ext:".glob" - ; mod_to_obj coq_module ~ext:".vos" - ] - in - aux_objs @ - [ mod_to_obj coq_module ~ext:vo_ext +let base_obj_files coq_module = + [ mod_to_obj coq_module ~ext:".glob" + ; mod_to_obj coq_module ~ext:".vos" + ; mod_to_obj coq_module ~ext:".vo" ] let obj_files ~tname ~rule coq_module = let native = Rule_type.native_coqc rule in let native_objs = if native then native_obj_files ~tname ~install:false coq_module else [] in let timing_objs = if with_timing then [ mod_to_obj coq_module ~ext:".timing" ] else [] in - timing_objs @ native_objs @ base_obj_files ~rule coq_module + timing_objs @ native_objs @ base_obj_files coq_module let prefix_to_dir = String.concat Filename.dir_sep @@ -76,24 +63,15 @@ let native_install_files ~tname ~rule coq_module = | Regular { native = Coqc } -> native_obj_files ~tname ~install:false coq_module , native_obj_files ~tname ~install:true coq_module - | Regular { native = Disabled } - | Quick -> - [], [] + | Regular { native = Disabled } -> [], [] (* quick/vio woes... it does produce a different set of targets than regular compilation *) -let base_install_files ~rule coq_module = - [ mod_to_obj coq_module ~ext:".v" ] - @ match rule with - | Rule_type.Quick -> - [ mod_to_obj coq_module ~ext:".vo" - ; mod_to_obj coq_module ~ext:".vos" - ] - | Rule_type.Regular _ as rule -> - base_obj_files ~rule coq_module +let base_install_files coq_module = + mod_to_obj coq_module ~ext:".v" :: base_obj_files coq_module let install_files ~tname ~rule coq_module = - let src_base = base_install_files ~rule coq_module in + let src_base = base_install_files coq_module in let src_native, dst_native = native_install_files ~tname ~rule coq_module in let src = src_base @ src_native in let ppath = prefix_to_dir (prefix coq_module) in diff --git a/tools/dune_rule_gen/coq_module.mli b/tools/dune_rule_gen/coq_module.mli index a00f4357390f..07a0e40b357c 100644 --- a/tools/dune_rule_gen/coq_module.mli +++ b/tools/dune_rule_gen/coq_module.mli @@ -21,11 +21,8 @@ module Rule_type : sig type native = Disabled | Coqc | CoqNative type t = | Regular of { native : native } - | Quick - (** build / depend on .vio instead of .vo *) val native_coqc : t -> bool - val vo_ext : t -> string end (** Return the native object files for a module *) diff --git a/tools/dune_rule_gen/coq_rules.ml b/tools/dune_rule_gen/coq_rules.ml index e2cd32302cb9..094ceb628682 100644 --- a/tools/dune_rule_gen/coq_rules.ml +++ b/tools/dune_rule_gen/coq_rules.ml @@ -213,7 +213,7 @@ module Context = struct end (* Return flags and deps to inject *) -let prelude_path ~ext = "Init/Prelude" ^ ext +let prelude_path = "Init/Prelude.vo" (* Return extra flags and deps for a concrete file; the case of interest is to determine when a file needs [-nonit]. If it @@ -221,8 +221,6 @@ let prelude_path ~ext = "Init/Prelude" ^ ext we can't compute this in Context.make due to the per-file check for "Init" *) let boot_module_setup ~cctx coq_module = - let ext = Coq_module.Rule_type.vo_ext cctx.Context.rule in - let prelude_path = prelude_path ~ext in match cctx.Context.boot with | Boot_type.NoInit -> [Arg.A "-noinit"], [] | Stdlib -> @@ -237,7 +235,7 @@ let module_rule ~(cctx : Context.t) coq_module = let tname, rule = cctx.theory.dirname, cctx.rule in (* retrieve deps *) let vfile = Coq_module.source coq_module in - let vo_ext = Coq_module.Rule_type.vo_ext rule in + let vo_ext = ".vo" in let vfile_deps = Dep_info.lookup ~dep_info:cctx.dep_info vfile |> List.map (path_of_dep ~vo_ext) in (* handle -noinit, inject prelude.vo if needed *) let boot_flags, boot_deps = boot_module_setup ~cctx coq_module in @@ -258,41 +256,8 @@ let module_rule ~(cctx : Context.t) coq_module = let updir = Path.(to_string (adjust ~lvl (make "."))) in let action = Format.asprintf "(chdir %s (run coqc %s %%{dep:%s}))" updir flags vfile_base in let targets = Coq_module.obj_files ~tname ~rule coq_module in - let alias = if rule = Coq_module.Rule_type.Quick then Some "vio" else None in - { Dune_file.Rule.targets; deps; action; alias } - -let vio2vo_rule ~(cctx : Context.t) coq_module = - let vfile = Coq_module.source coq_module in - let viofile = Path.replace_ext ~ext:".vio" vfile in - - let boot_flags, _boot_deps = boot_module_setup ~cctx coq_module in - let flags = Arg.A "-vio2vo" :: boot_flags @ cctx.flags.loadpath in - - (* Non deterministic code in loadpath to pick .vio vs .vo means that - we can't really do a parallel build of .v to .vio and .vio to .vo - - We have a race condition due to transitive dependencies not - agreeing on the module chosen, it may happen that a module is - upgraded to .vo and hence the compilation will boom. - - There are four possible remedies: remove vio, make the vio - require deterministic, use a `@vio` alias before the main - build, insert a barrier on which all .vio to .vo depend. - - I guess an alias looks fine for CI for the moment. - *) - (* Adjust paths *) - let lvl = cctx.root_lvl + (Coq_module.prefix coq_module |> List.length) in - let flags = (* flags are relative to the root path *) Arg.List.to_string flags in - (* vio2vo doesn't follow normal convention... so we can't use Coq_module.obj_files *) - let vofile_base = Path.replace_ext ~ext:".vo" vfile |> Path.basename in - let vosfile_base = Path.replace_ext ~ext:".vos" vfile |> Path.basename in - let targets = [vofile_base; vosfile_base] in - let viofile_base = Path.basename viofile in - let updir = Path.(to_string (adjust ~lvl (make "."))) in - let action = Format.asprintf "(chdir %s (run coqc %s %%{dep:%s}))" updir flags viofile_base in let alias = None in - { Dune_file.Rule.targets; deps=[]; action; alias } + { Dune_file.Rule.targets; deps; action; alias } (* Helper for Dir_info to Subdir *) let gen_rules ~dir_info ~cctx ~f = @@ -305,7 +270,6 @@ let gen_rules ~dir_info ~cctx ~f = (* Has to be called in the current dir *) let vo_rules ~dir_info ~cctx = gen_rules ~dir_info ~cctx ~f:module_rule -let vio2vo_rules ~dir_info ~cctx = gen_rules ~dir_info ~cctx ~f:vio2vo_rule (* rule generation for .vo -> .{cmi,cmxs} *) let coqnative_module_rule ~(cctx: Context.t) coq_module = diff --git a/tools/dune_rule_gen/coq_rules.mli b/tools/dune_rule_gen/coq_rules.mli index 67a56d9ab4d0..42c04b485955 100644 --- a/tools/dune_rule_gen/coq_rules.mli +++ b/tools/dune_rule_gen/coq_rules.mli @@ -71,8 +71,3 @@ val install_rules : dir_info :Coq_module.t Dir_info.t -> cctx:Context.t -> Dune_file.Install.t list Dune_file.Subdir.t list - -val vio2vo_rules : - dir_info :Coq_module.t Dir_info.t - -> cctx:Context.t - -> Dune_file.Rule.t list Dune_file.Subdir.t list diff --git a/tools/dune_rule_gen/gen_rules.ml b/tools/dune_rule_gen/gen_rules.ml index 244c665eeecd..0051b970e59f 100644 --- a/tools/dune_rule_gen/gen_rules.ml +++ b/tools/dune_rule_gen/gen_rules.ml @@ -41,7 +41,6 @@ let parse_args () = let default = false, false, Coq_module.Rule_type.Regular { native }, [] in let split, async, rule, user_flags = if Array.length Sys.argv > 3 then match Sys.argv.(3) with - | "-vio" -> false, false, Coq_module.Rule_type.Quick, Arg.[A "-vio"] | "-async" -> false, true, Coq_module.Rule_type.Regular { native }, Arg.[A "-async-proofs"; A "on"] | "-split" -> true, false, Coq_module.Rule_type.Regular { native }, [] (* Dune will sometimes pass this option as "" *) @@ -86,15 +85,6 @@ let main () = List.iter (Dune_file.Subdir.pp ppr fmt) vo_rules; List.iter (Dune_file.Subdir.pp ppi fmt) install_rules; - (* Rules for vio2vo *) - begin - match rule with - | Coq_module.Rule_type.Quick -> - let vio2vo_rules = Coq_rules.vio2vo_rules ~dir_info ~cctx in - List.iter (Dune_file.Subdir.pp ppr fmt) vio2vo_rules - | Coq_module.Rule_type.Regular _ -> () - end; - (* Rules for coqnative (not always setup for now, need to think about this) *) begin match native_mode with diff --git a/topbin/coqnative_bin.ml b/topbin/coqnative_bin.ml index e88929af747f..e16966bd2b56 100644 --- a/topbin/coqnative_bin.ml +++ b/topbin/coqnative_bin.ml @@ -110,7 +110,6 @@ type library_t = { library_data : Safe_typing.compiled_library; library_deps : (compilation_unit_name * Safe_typing.vodigest) array; library_digests : Safe_typing.vodigest; - library_extra_univs : Univ.ContextSet.t; library_vm : Vmlibrary.on_disk; } @@ -123,36 +122,28 @@ let register_loaded_library senv libname file = let () = Nativecode.register_native_file prefix in senv -let mk_library sd f md digests univs vm = +let mk_library sd f md digests vm = { library_name = sd.md_name; library_file = f; library_data = md; library_deps = sd.md_deps; library_digests = digests; - library_extra_univs = univs; library_vm = vm; } 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 : (Univ.ContextSet.t * bool) option ObjFile.id = ObjFile.make_id "universes" let intern_from_file f = let ch = System.with_magic_number_check (fun file -> ObjFile.open_in ~file) f in let lsd, digest_lsd = ObjFile.marshal_in_segment ch ~segment:summary_seg in let lmd, digest_lmd = ObjFile.marshal_in_segment ch ~segment:library_seg in - let univs, digest_u = ObjFile.marshal_in_segment ch ~segment:universes_seg in let vmlib = Vmlibrary.load ~file:f lsd.md_name ch in ObjFile.close_in ch; System.check_caml_version ~caml:lsd.md_ocaml ~file:f; let open Safe_typing in - match univs with - | None -> mk_library lsd f lmd.md_compiled (Dvo_or_vi digest_lmd) Univ.ContextSet.empty vmlib - | Some (uall,true) -> - mk_library lsd f lmd.md_compiled (Dvivo (digest_lmd,digest_u)) uall vmlib - | Some (_,false) -> - mk_library lsd f lmd.md_compiled (Dvo_or_vi digest_lmd) Univ.ContextSet.empty vmlib + mk_library lsd f lmd.md_compiled (Dvo_or_vi digest_lmd) vmlib let rec intern_library (needed, contents) dir = (* Look if already listed and consequently its dependencies too *) @@ -182,7 +173,7 @@ and intern_mandatory_library caller from libs (dir,d) = let register_library senv m = let mp = MPfile m.library_name in - let mp', senv = Safe_typing.import m.library_data m.library_extra_univs m.library_vm m.library_digests senv in + let mp', senv = Safe_typing.import m.library_data m.library_vm m.library_digests senv in let () = if not (ModPath.equal mp mp') then anomaly (Pp.str "Unexpected disk module name.") diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index 8007c58ef394..479e7f8da34e 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -35,8 +35,6 @@ let compile opts stm_options injections copts ~echo ~f_in ~f_out = let ext_in, ext_out = match mode with | BuildVo -> ".v", ".vo" - | BuildVio -> ".v", ".vio" - | Vio2Vo -> ".vio", ".vo" | BuildVos -> ".v", ".vos" | BuildVok -> ".v", ".vok" in @@ -87,10 +85,10 @@ let compile opts stm_options injections copts ~echo ~f_in ~f_out = dump_empty_vok(); Dumpglob.end_dump_glob () - | BuildVio | BuildVos -> + | BuildVos -> let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) Stm.new_doc - Stm.{ doc_type = VioDoc long_f_dot_out; injections; + Stm.{ doc_type = VosDoc long_f_dot_out; injections; } in let state = { doc; sid; proof = None; time = Option.map Vernac.make_time_output opts.config.time } in @@ -100,27 +98,10 @@ let compile opts stm_options injections copts ~echo ~f_in ~f_out = let state = Vernac.load_vernac ~echo ~check:false ~source ~state long_f_dot_in in let state = Stm.finish ~doc:state.doc in ensure_no_pending_proofs state ~filename:long_f_dot_in; - let create_vos = (mode = BuildVos) in - (* In .vos production, the output .vos file contains compiled statements. - In .vio production, the output .vio file contains compiled statements and suspended proofs. *) - let () = Stm.snapshot_vio ~create_vos ~doc ~output_native_objects ldir long_f_dot_out in + let () = Stm.snapshot_vos ~doc ~output_native_objects ldir long_f_dot_out in Stm.reset_task_queue (); - (* In .vio production, dump an empty .vos file to indicate that the .vio should be loaded. *) - (* EJGA: This is problematic in a vio + vio2vo run, as there is - a race with target generation *) - if mode = BuildVio then dump_empty_vos(); () - | Vio2Vo -> - Flags.async_proofs_worker_id := "Vio2Vo"; - let sum, lib, univs, tasks, proofs, vmlib = - Library.load_library_todo long_f_dot_in in - let univs, proofs = Stm.finish_tasks long_f_dot_out univs proofs tasks in - Library.save_library_raw long_f_dot_out sum lib univs proofs vmlib; - (* Like in direct .vo production, dump an empty .vok file and an empty .vos file. *) - dump_empty_vos(); - create_empty_file (long_f_dot_out ^ "k") - let compile opts stm_opts copts injections ~echo ~f_in ~f_out = ignore(CoqworkmgrApi.get 1); compile opts stm_opts injections copts ~echo ~f_in ~f_out; diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 1a1e1614b117..c1baa4d5353b 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -28,19 +28,9 @@ coqc specific options:\ \n -verbose compile and output the input file\ \n -noglob do not dump globalizations\ \n -dump-glob f dump globalizations in file f (to be used by coqdoc)\ -\n -schedule-vio2vo j f1..fn run up to j instances of Coq to turn each fi.vio\ -\n into fi.vo\ -\n -schedule-vio-checking j f1..fn run up to j instances of Coq to check all\ -\n proofs in each fi.vio\ \n -vos process statements but ignore opaque proofs, and produce a .vos file\ \n -vok process the file by loading .vos instead of .vo files for\ \n dependencies, and produce an empty .vok file on success\ -\n -vio process statements and suspend opaque proofs, and produce a .vio file\ -\n\ -\nUndocumented:\ -\n -quick (deprecated) alias for -vio\ -\n -vio2vo [see manual]\ -\n -check-vio-tasks [see manual]\ \n" } @@ -48,11 +38,6 @@ let coqc_main ((copts,_),stm_opts) injections ~opts = Topfmt.(in_phase ~phase:CompilationPhase) Ccompile.compile_file opts stm_opts copts injections; - (* Careful this will modify the load-path and state so after this - point some stuff may not be safe anymore. *) - Topfmt.(in_phase ~phase:CompilationPhase) - Vio_compile.do_vio opts copts injections; - flush_all(); if copts.Coqcargs.output_context then begin @@ -76,7 +61,7 @@ let coqc_run copts ~opts injections = exit exit_code let fix_stm_opts opts stm_opts = match opts.Coqcargs.compilation_mode with - | BuildVio | BuildVos -> + | BuildVos -> (* We need to disable error resiliency, otherwise some errors will be ignored in batch mode. c.f. #6707 @@ -89,7 +74,7 @@ let fix_stm_opts opts stm_opts = match opts.Coqcargs.compilation_mode with async_proofs_cmd_error_resilience = false; async_proofs_tac_error_resilience = FNone; } - | BuildVo | BuildVok | Vio2Vo -> stm_opts + | BuildVo | BuildVok -> stm_opts let custom_coqc : ((Coqcargs.t * Colors.color) * Stm.AsyncOpts.stm_opt, 'b) Coqtop.custom_toplevel = Coqtop.{ diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml index eac7303118a0..6871d18df97d 100644 --- a/toplevel/coqcargs.ml +++ b/toplevel/coqcargs.ml @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -type compilation_mode = BuildVo | BuildVio | Vio2Vo | BuildVos | BuildVok +type compilation_mode = BuildVo | BuildVos | BuildVok type t = { compilation_mode : compilation_mode @@ -16,11 +16,6 @@ type t = ; compile_file: (string * bool) option (* bool is verbosity *) ; compilation_output_name : string option - ; vio_checking : bool - ; vio_tasks : (int list * string) list - ; vio_files : string list - ; vio_files_j : int - ; echo : bool ; glob_out : Dumpglob.glob_output @@ -34,11 +29,6 @@ let default = ; compile_file = None ; compilation_output_name = None - ; vio_checking = false - ; vio_tasks = [] - ; vio_files = [] - ; vio_files_j = 0 - ; echo = false ; glob_out = Dumpglob.MultFiles @@ -84,53 +74,6 @@ let add_compile ?echo copts v_file = | None -> add_compile ?echo copts v_file -let add_vio_task opts f = - { opts with vio_tasks = f :: opts.vio_tasks } - -let add_vio_file opts f = - { opts with vio_files = f :: opts.vio_files } - -let set_vio_checking_j opts opt j = - try { opts with vio_files_j = int_of_string j } - with Failure _ -> - prerr_endline ("The first argument of " ^ opt ^ " must the number"); - prerr_endline "of concurrent workers to be used (a positive integer)."; - prerr_endline "Makefiles generated by coq_makefile should be called"; - prerr_endline "setting the J variable like in 'make vio2vo J=3'"; - exit 1 - -let set_compilation_mode opts mode = - match opts.compilation_mode with - | BuildVo -> { opts with compilation_mode = mode } - | mode' when mode <> mode' -> - prerr_endline "Options -vio and -vio2vo are exclusive"; - exit 1 - | _ -> opts - -let get_task_list s = - List.map (fun s -> - try int_of_string s - with Failure _ -> - prerr_endline "Option -check-vio-tasks expects a comma-separated list"; - prerr_endline "of integers followed by a list of files"; - exit 1) - (Str.split (Str.regexp ",") s) - -let is_not_dash_option = function - | Some f when String.length f > 0 && f.[0] <> '-' -> true - | _ -> false - -let rec add_vio_args peek next oval = - if is_not_dash_option (peek ()) then - let oval = add_vio_file oval (next ()) in - add_vio_args peek next oval - else oval - -let warn_deprecated_quick = - CWarnings.create ~name:"deprecated-quick" ~category:Deprecation.Version.v8_11 - (fun () -> - Pp.strbrk "The -quick option is renamed -vio. Please consider using the -vos feature instead.") - let parse arglist : t = let echo = ref false in let args = ref arglist in @@ -144,10 +87,6 @@ let parse arglist : t = | x::rem -> args := rem; x | [] -> error_missing_arg opt in - let peek_next () = match !args with - | x::_ -> Some x - | [] -> None - in let noval : t = begin match opt with (* Deprecated options *) | "-opt" @@ -169,11 +108,6 @@ let parse arglist : t = (* Output filename *) | "-o" -> { oval with compilation_output_name = Some (next ()) } - | "-quick" -> - warn_deprecated_quick(); - set_compilation_mode oval BuildVio - | "-vio" -> - set_compilation_mode oval BuildVio |"-vos" -> Flags.load_vos_libraries := true; { oval with compilation_mode = BuildVos } @@ -181,26 +115,6 @@ let parse arglist : t = Flags.load_vos_libraries := true; { oval with compilation_mode = BuildVok } - | "-check-vio-tasks" -> - let tno = get_task_list (next ()) in - let tfile = next () in - add_vio_task oval (tno,tfile) - - | "-schedule-vio-checking" -> - let oval = { oval with vio_checking = true } in - let oval = set_vio_checking_j oval opt (next ()) in - let oval = add_vio_file oval (next ()) in - add_vio_args peek_next next oval - - | "-schedule-vio2vo" -> - let oval = set_vio_checking_j oval opt (next ()) in - let oval = add_vio_file oval (next ()) in - add_vio_args peek_next next oval - - | "-vio2vo" -> - let oval = add_compile ~echo:false oval (next ()) in - set_compilation_mode oval Vio2Vo - (* Glob options *) |"-no-glob" | "-noglob" -> { oval with glob_out = Dumpglob.NoGlob } @@ -221,10 +135,3 @@ let parse arglist : t = let args = List.fold_left add_compile opts extra in args with any -> fatal_error any - -let parse args = - let opts = parse args in - { opts with - vio_tasks = List.rev opts.vio_tasks - ; vio_files = List.rev opts.vio_files - } diff --git a/toplevel/coqcargs.mli b/toplevel/coqcargs.mli index c4be67963cee..c43b7a3f14a9 100644 --- a/toplevel/coqcargs.mli +++ b/toplevel/coqcargs.mli @@ -11,8 +11,6 @@ (** Compilation modes: - BuildVo : process statements and proofs (standard compilation), and also output an empty .vos file and .vok file - - BuildVio : process statements, delay proofs in futures - - Vio2Vo : load delayed proofs and process them - BuildVos : process statements, and discard proofs, and load .vos files for required libraries - BuildVok : like BuildVo, but load .vos files for required libraries @@ -22,7 +20,7 @@ This trick is useful to avoid the need for the user to compile .vos version when an up to date .vo version is already available. *) -type compilation_mode = BuildVo | BuildVio | Vio2Vo | BuildVos | BuildVok +type compilation_mode = BuildVo | BuildVos | BuildVok type t = { compilation_mode : compilation_mode @@ -30,11 +28,6 @@ type t = ; compile_file: (string * bool) option (* bool is verbosity *) ; compilation_output_name : string option - ; vio_checking : bool - ; vio_tasks : (int list * string) list - ; vio_files : string list - ; vio_files_j : int - ; echo : bool ; glob_out : Dumpglob.glob_output diff --git a/toplevel/vio_compile.ml b/toplevel/vio_compile.ml deleted file mode 100644 index dacef879cdf8..000000000000 --- a/toplevel/vio_compile.ml +++ /dev/null @@ -1,41 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* - let f_in = ensure ~ext:".vio" ~src:f ~tgt:f in - ensure_exists f_in; - Vio_checking.check_vio (n,f_in) && acc) - true copts.vio_tasks in - if not rc then fatal_error Pp.(str "VIO Task Check failed") - -(* vio files *) -let schedule_vio copts = - let l = - List.map (fun f -> let f_in = ensure ~ext:".vio" ~src:f ~tgt:f in ensure_exists f_in; f_in) - copts.vio_files in - if copts.vio_checking then - Vio_checking.schedule_vio_checking copts.vio_files_j l - else - Vio_checking.schedule_vio_compilation copts.vio_files_j l - -let do_vio opts copts _injections = - (* Vio compile pass *) - if copts.vio_files <> [] then schedule_vio copts; - (* Vio task pass *) - if copts.vio_tasks <> [] then check_vio_tasks copts diff --git a/toplevel/vio_compile.mli b/toplevel/vio_compile.mli deleted file mode 100644 index e003842f725c..000000000000 --- a/toplevel/vio_compile.mli +++ /dev/null @@ -1,12 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* Coqcargs.t -> Coqargs.injection_command list -> unit diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml index f8659297c0e2..6ffc1268d529 100644 --- a/vernac/declaremods.ml +++ b/vernac/declaremods.ml @@ -1544,7 +1544,7 @@ let declare_include me_asts = RawIncludeOps.Interp.declare_include me_asts (** For the native compiler, we cache the library values *) -let register_library dir cenv (objs:library_objects) digest univ vmtab = +let register_library dir cenv (objs:library_objects) digest vmtab = let mp = MPfile dir in let () = try @@ -1553,7 +1553,7 @@ let register_library dir cenv (objs:library_objects) digest univ vmtab = with Not_found -> begin (* If not, let's do it now ... *) - let mp' = Global.import cenv univ vmtab digest in + let mp' = Global.import cenv vmtab digest in if not (ModPath.equal mp mp') then anomaly (Pp.str "Unexpected disk module name.") end diff --git a/vernac/declaremods.mli b/vernac/declaremods.mli index bb8ce9039c36..962e861cea4c 100644 --- a/vernac/declaremods.mli +++ b/vernac/declaremods.mli @@ -130,7 +130,7 @@ val end_modtype : unit -> ModPath.t val register_library : library_name -> Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest -> - Univ.ContextSet.t -> Vmlibrary.on_disk -> + Vmlibrary.on_disk -> unit (** [import_module export mp] imports the module [mp]. diff --git a/vernac/future.ml b/vernac/future.ml index 934b9438e17b..4b598375c48c 100644 --- a/vernac/future.ml +++ b/vernac/future.ml @@ -21,9 +21,6 @@ let not_here_msg = ref (fun name -> "asynchronous script processing and don't pass \"-vio\" to "^ "coqc.")) -let customize_not_ready_msg f = not_ready_msg := f -let customize_not_here_msg f = not_here_msg := f - exception NotReady of string exception NotHere of string diff --git a/vernac/future.mli b/vernac/future.mli index bf97558fbebf..9c90aa0e62ef 100644 --- a/vernac/future.mli +++ b/vernac/future.mli @@ -83,6 +83,3 @@ val compute : 'a computation -> 'a value (** Debug: print a computation given an inner printing function. *) val print : ('a -> Pp.t) -> 'a computation -> Pp.t - -val customize_not_ready_msg : (string -> Pp.t) -> unit -val customize_not_here_msg : (string -> Pp.t) -> unit diff --git a/vernac/library.ml b/vernac/library.ml index 25ad73d234d9..c17b2ade014d 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -101,7 +101,6 @@ type library_t = { library_data : library_disk; library_deps : (compilation_unit_name * Safe_typing.vodigest) array; library_digests : Safe_typing.vodigest; - library_extra_univs : Univ.ContextSet.t; library_info : Library_info.t; library_vm : Vmlibrary.on_disk; } @@ -230,18 +229,15 @@ let indirect_accessor = { type seg_sum = summary_disk type seg_lib = library_disk -type seg_univ = (* true = vivo, false = vi *) - Univ.ContextSet.t * bool type seg_proofs = Opaques.opaque_disk type seg_vm = Vmlibrary.compiled_library -let mk_library sd md digests univs vm = +let mk_library sd md digests vm = { library_name = sd.md_name; library_data = md; library_deps = sd.md_deps; library_digests = digests; - library_extra_univs = univs; library_info = sd.md_info; library_vm = vm; } @@ -252,22 +248,13 @@ let mk_summary m = { libsum_info = m.library_info; } -let mk_intern_library sum lib digest_lib univs digest_univs proofs = +let mk_intern_library sum lib digest_lib proofs = add_opaque_table sum.md_name (ToFetch proofs); let open Safe_typing in - match univs with - | None -> mk_library sum lib (Dvo_or_vi digest_lib) Univ.ContextSet.empty - | Some (uall,true) -> - mk_library sum lib (Dvivo (digest_lib, digest_univs)) uall - | Some (_,false) -> - mk_library sum lib (Dvo_or_vi digest_lib) Univ.ContextSet.empty - -type ('uid, 'doc) tasks = (('uid, 'doc) Stateid.request * bool) list + mk_library sum lib (Dvo_or_vi digest_lib) let summary_seg : seg_sum ObjFile.id = ObjFile.make_id "summary" let library_seg : seg_lib ObjFile.id = ObjFile.make_id "library" -let universes_seg : seg_univ option ObjFile.id = ObjFile.make_id "universes" -let tasks_seg () : (Opaqueproof.opaque_handle option, 'doc) tasks option ObjFile.id = ObjFile.make_id "tasks" let opaques_seg : seg_proofs ObjFile.id = ObjFile.make_id "opaques" let vm_seg : seg_vm ObjFile.id = Vmlibrary.vm_segment @@ -277,7 +264,6 @@ let intern_from_file ?loc lib_resolver dir = let ch = raw_intern_library f ?loc in let lsd, digest_lsd = ObjFile.marshal_in_segment ch ~segment:summary_seg in let lmd, digest_lmd = ObjFile.marshal_in_segment ch ~segment:library_seg in - let univs, digest_u = ObjFile.marshal_in_segment ch ~segment:universes_seg in let del_opaque, _ = in_delayed f ch ~segment:opaques_seg in let vmlib = Vmlibrary.load dir ~file:f ch in ObjFile.close_in ch; @@ -291,7 +277,7 @@ let intern_from_file ?loc lib_resolver dir = spc() ++ DirPath.print dir ++ str "."); Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f)); Library_info.warn_library_info ~transitive:true lsd.md_name lsd.md_info; - lsd, lmd, digest_lmd, univs, digest_u, del_opaque, vmlib + lsd, lmd, digest_lmd, del_opaque, vmlib let rec intern_library ~intern (needed, contents as acc) dir = (* Look if in the current logical environment *) @@ -300,8 +286,8 @@ let rec intern_library ~intern (needed, contents as acc) dir = (* Look if already listed and consequently its dependencies too *) try mk_summary (DPmap.find dir contents), acc with Not_found -> - let lsd, lmd, digest_lmd, univs, digest_u, del_opaque, vmlib = intern dir in - let m = mk_intern_library lsd lmd digest_lmd univs digest_u del_opaque vmlib in + let lsd, lmd, digest_lmd, del_opaque, vmlib = intern dir in + let m = mk_intern_library lsd lmd digest_lmd del_opaque vmlib in mk_summary m, intern_library_deps ~intern acc dir m and intern_library_deps ~intern libs dir m = @@ -358,7 +344,6 @@ let register_library m = l.md_compiled l.md_objects m.library_digests - m.library_extra_univs m.library_vm ; register_native_library m.library_name @@ -436,24 +421,6 @@ let require_library_syntax_from_dirpath ~lib_resolver modrefl = Lib.add_leaf (in_require_syntax needed); needed -(************************************************************************) -(*s Initializing the compilation of a library. *) - -let load_library_todo f = - let ch = raw_intern_library f in - let s0, _ = ObjFile.marshal_in_segment ch ~segment:summary_seg in - let s1, _ = ObjFile.marshal_in_segment ch ~segment:library_seg in - let s2, _ = ObjFile.marshal_in_segment ch ~segment:universes_seg in - let tasks, _ = ObjFile.marshal_in_segment ch ~segment:(tasks_seg ()) in - let s4, _ = ObjFile.marshal_in_segment ch ~segment:opaques_seg in - let s5, _ = ObjFile.marshal_in_segment ch ~segment:vm_seg in - ObjFile.close_in ch; - System.check_caml_version ~caml:s0.md_ocaml ~file:f; - if tasks = None then user_err (str "Not a .vio file."); - if s2 = None then user_err (str "Not a .vio file."); - if snd (Option.get s2) then user_err (str "Not a .vio file."); - s0, s1, Option.get s2, Option.get tasks, s4, s5 - (************************************************************************) (*s [save_library dir] ends library [dir] and save it to the disk. *) @@ -473,7 +440,6 @@ let error_recursively_dependent_library dir = type 'doc todo_proofs = | ProofsTodoNone (* for .vo *) | ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *) - | ProofsTodoSome of Future.UUIDSet.t * (Future.UUID.t, 'doc) tasks (* for .vio *) (* We now use two different digests in a .vo file. The first one only covers half of the file, without the opaque table. It is @@ -486,13 +452,11 @@ type 'doc todo_proofs = (* Security weakness: file might have been changed on disk between writing the content and computing the checksum... *) -let save_library_base f sum lib univs tasks proofs vmlib = +let save_library_base f sum lib proofs vmlib = let ch = raw_extern_library f in try ObjFile.marshal_out_segment ch ~segment:summary_seg sum; ObjFile.marshal_out_segment ch ~segment:library_seg lib; - ObjFile.marshal_out_segment ch ~segment:universes_seg univs; - ObjFile.marshal_out_segment ch ~segment:(tasks_seg ()) tasks; ObjFile.marshal_out_segment ch ~segment:opaques_seg proofs; ObjFile.marshal_out_segment ch ~segment:vm_seg vmlib; ObjFile.close_out ch @@ -527,13 +491,11 @@ let save_library_to todo_proofs ~output_native_objects dir f = let expected_extension = match todo_proofs with | ProofsTodoNone -> ".vo" | ProofsTodoSomeEmpty _ -> ".vos" - | ProofsTodoSome _ -> ".vio" in Filename.check_suffix f expected_extension); let except = match todo_proofs with | ProofsTodoNone -> Future.UUIDSet.empty | ProofsTodoSomeEmpty except -> except - | ProofsTodoSome (except,l) -> except in (* Ensure that the call below is performed with all opaques joined *) let () = Opaques.Summary.join ~except () in @@ -541,30 +503,15 @@ let save_library_to todo_proofs ~output_native_objects dir f = let () = assert (not (Future.UUIDSet.is_empty except) || Safe_typing.is_joined_environment (Global.safe_env ())) in - let tasks, utab = - match todo_proofs with - | ProofsTodoNone -> None, None - | ProofsTodoSomeEmpty _except -> - None, Some (Univ.ContextSet.empty,false) - | ProofsTodoSome (_except, tasks) -> - let tasks = - List.map Stateid.(fun (r,b) -> - try { r with uuid = Some (Future.UUIDMap.find r.uuid f2t_map) }, b - with Not_found -> assert b; { r with uuid = None }, b) - tasks in - Some tasks, - Some (Univ.ContextSet.empty,false) - in let sd, md, vmlib, ast = save_library_struct ~output_native_objects dir in (* Writing vo payload *) - save_library_base f sd md utab tasks opaque_table vmlib; + save_library_base f sd md opaque_table vmlib; (* Writing native code files *) if output_native_objects then let fn = Filename.dirname f ^"/"^ Nativecode.mod_uid_of_dirpath dir in Nativelib.compile_library ast fn -let save_library_raw f sum lib univs proofs = - save_library_base f sum lib (Some univs) None proofs +let save_library_raw f sum lib proofs = save_library_base f sum lib proofs let get_used_load_paths () = String.Set.elements diff --git a/vernac/library.mli b/vernac/library.mli index 0fef6cca51ab..19bd4337bd68 100644 --- a/vernac/library.mli +++ b/vernac/library.mli @@ -35,33 +35,25 @@ val require_library_syntax_from_dirpath (** Segments of a library *) type seg_sum type seg_lib -type seg_univ = (* all_cst, finished? *) - Univ.ContextSet.t * bool type seg_proofs = Opaques.opaque_disk type seg_vm = Vmlibrary.compiled_library -(** End the compilation of a library and save it to a ".vo" file, - a ".vio" file, or a ".vos" file, depending on the todo_proofs - argument. - [output_native_objects]: when producing vo objects, also compile the native-code version. *) +(** End the compilation of a library and save it to a ".vo" file, or a + ".vos" file, depending on the todo_proofs argument. -type ('uid, 'doc) tasks = (('uid, 'doc) Stateid.request * bool) list + [output_native_objects]: when producing vo objects, also compile + the native-code version. *) type 'doc todo_proofs = | ProofsTodoNone (* for .vo *) | ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *) - | ProofsTodoSome of Future.UUIDSet.t * (Future.UUID.t, 'doc) tasks (* for .vio *) val save_library_to : 'document todo_proofs -> output_native_objects:bool -> DirPath.t -> string -> unit -val load_library_todo - : CUnix.physical_path - -> seg_sum * seg_lib * seg_univ * (Opaqueproof.opaque_handle option, 'doc) tasks * seg_proofs * seg_vm - -val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> seg_vm -> unit +val save_library_raw : string -> seg_sum -> seg_lib -> seg_proofs -> seg_vm -> unit (** {6 Interrogate the status of libraries } *) diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml index 20107735b7de..74f4de47f3c7 100644 --- a/vernac/loadpath.ml +++ b/vernac/loadpath.ml @@ -179,46 +179,25 @@ let locate_file fname = type locate_error = LibUnmappedDir | LibNotFound type 'a locate_result = ('a, locate_error) result -let warn_several_object_files = - CWarnings.create ~name:"several-object-files" ~category:CWarnings.CoreCategories.filesystem - Pp.(fun (vi, vo) -> - seq [ str "Loading"; spc (); str vi - ; strbrk " instead of "; str vo - ; strbrk " because it is more recent." - ]) - +(* If [!Flags.load_vos_libraries] + and the .vos file exists + and this file is not empty + Then load this library + Else load the .vo file or raise error if both are missing *) let select_vo_file ~find base = let find ext = try let name = Names.Id.to_string base ^ ext in let lpath, file = find name in - Some (lpath, file) - with Not_found -> None in - (* If [!Flags.load_vos_libraries] - and the .vos file exists - and this file is not empty - Then load this library - Else load the most recent between the .vo file and the .vio file, - or if there is only of the two files, take this one, - or raise an error if both are missing. *) - let load_most_recent_of_vo_and_vio () = - match find ".vo", find ".vio" with - | None, None -> - Error LibNotFound - | Some res, None | None, Some res -> - Ok res - | Some (_, vo), Some (_, vi as resvi) - when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - warn_several_object_files (vi, vo); - Ok resvi - | Some resvo, Some _ -> - Ok resvo - in - if !Flags.load_vos_libraries then begin + Ok (lpath, file) + with Not_found -> Error LibNotFound in + if !Flags.load_vos_libraries + then begin match find ".vos" with - | Some (_, vos as resvos) when (Unix.stat vos).Unix.st_size > 0 -> Ok resvos - | _ -> load_most_recent_of_vo_and_vio() - end else load_most_recent_of_vo_and_vio() + | Ok (_, vos as resvos) when (Unix.stat vos).Unix.st_size > 0 -> Ok resvos + | _ -> find ".vo" + end + else find ".vo" let find_first loadpath base = match System.all_in_path loadpath base with