blob: 905250e3638791f9c43dce713384b5c003570671 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** 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 compilation_mode = BuildVo | BuildVio | Vio2Vo | BuildVos | BuildVok
type t =
{ compilation_mode : compilation_mode
; compile_list: (string * bool) list (* 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
; outputstate : string option
; glob_out : Dumpglob.glob_output
; output_context : bool
}
val default : t
val parse : string list -> t
|
