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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
|
(************************************************************************)
(* This file is licensed under The MIT License *)
(* See LICENSE for more information *)
(* (c) MINES ParisTech 2018-2019 *)
(* (c) INRIA 2020-2022 *)
(* Written by: Emilio Jesús Gallego Arias *)
(* Written by: Rudi Grinberg *)
(************************************************************************)
module Theory : sig
(** A theory binding; directories should be relative to Coq's
sources root *)
type t =
{ directory : Path.t
(** Directory of the theory *)
; dirname: string list
(** Coq's logical path *)
; implicit : bool
(** Use -R or -Q *)
; deps : string list
(** Adds as -Q user-contrib/X X *)
}
end
(** theory kind *)
module Boot_type : sig
type t =
Corelib
(** Standard library *)
| NoInit
(** Standalone library (without Coq's core lib, for example the prelude) *)
| Regular of { corelib : Theory.t; noinit : bool }
(** Regular library, qualified with -Q, [corelib] controls where
the Corelib is.
[noinit = true] only means there is no implicit dep on the
prelude, it may still depend on Corelib (unlike [NoInit]). *)
end
module Context : sig
type t
(** *)
val make :
root_lvl:int
-> theory:Theory.t
-> user_flags:Arg.t list
-> boot:Boot_type.t
-> rule:Coq_module.Rule_type.t (* quick, native, etc... *)
-> async:bool
-> dir_info:Coq_module.t Dir_info.t (* contents of the directory scan *)
-> split:bool (* whether we are building rocq-runtime + rocq-core or only rocq-core *)
-> t
end
(** [gen_vo_rules root_lvl rule flags tname boot] Builds dune rules
for the *current* directory, assuming that we will do [-R
. tname]. The parameter [boot] controls the kind of the current
theory. [root_lvl] tells the rule generator how many levels up the
root Coq sources are. [flags] add extra flags to coqc, such as
`-async on` *)
val vo_rules :
dir_info :Coq_module.t Dir_info.t
-> cctx:Context.t
-> Dune_file.Rule.t list Dune_file.Subdir.t list
val coqnative_rules :
dir_info :Coq_module.t Dir_info.t
-> cctx:Context.t
-> Dune_file.Rule.t list Dune_file.Subdir.t list
val install_rules :
dir_info :Coq_module.t Dir_info.t
-> cctx:Context.t
-> Dune_file.Install.t list Dune_file.Subdir.t list
|
