package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type compilation_mode =
  1. | BuildVo
  2. | BuildVio
  3. | Vio2Vo
  4. | BuildVos
  5. | BuildVok

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

When loading the .vos version of a required library, if the file exists but is empty, then we attempt to load the .vo version of that library. 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 t = {
  1. compilation_mode : compilation_mode;
  2. compile_file : (string * bool) option;
  3. compilation_output_name : string option;
  4. vio_checking : bool;
  5. vio_tasks : (int list * string) list;
  6. vio_files : string list;
  7. vio_files_j : int;
  8. echo : bool;
  9. outputstate : string option;
  10. glob_out : Dumpglob.glob_output;
  11. output_context : bool;
}
val default : t
val parse : string list -> t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct