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
|
(************************************************************************)
(* 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 *)
(************************************************************************)
type t
val make : source:Path.t -> prefix:string list -> name:string -> t
val source : t -> Path.t
val prefix : t -> string list
val prefix_to_dir : string list -> string
(** We support two build modes for now *)
module Rule_type : sig
type native = Disabled | Coqc | CoqNative
type t =
| Regular of { native : native }
val native_coqc : t -> bool
end
(** Return the native object files for a module *)
val native_obj_files : tname:string list -> t -> string list
(** Return the object files for a module *)
val obj_files :
tname:string list
-> rule:Rule_type.t
-> t
-> string list
(** Return pairs of object files and install locations *)
val install_files :
tname:string list
-> rule:Rule_type.t
-> t
-> (string * string) list
val pp : Format.formatter -> t -> unit
val with_timing : bool
|
