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
79
80
81
|
(************************************************************************)
(* 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 *)
(************************************************************************)
let with_timing = true
type t =
{ source : Path.t
; prefix : string list
; name : string
}
let pp fmt { source; prefix; name } =
Format.fprintf fmt "@[{%s : %a}@]" (String.concat "." (prefix@[name]) ) Path.pp source
let make ~source ~prefix ~name = { source; prefix; name }
let source { source; _ } = source
let prefix { prefix; _ } = prefix
let mod_to_obj ~ext { name; _ } = name ^ ext
module Rule_type = struct
type native = Disabled | Coqc | CoqNative
type t =
| Regular of { native : native }
let native_coqc = function
| Regular { native = Coqc } -> true
| Regular { native = CoqNative }
| Regular { native = Disabled } -> false
end
let native_obj_files ~install ~tname { prefix; name; _ } =
let base_theory = tname in
let native_base = "N" ^ String.concat "_" (base_theory @ prefix @ [name]) in
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 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 coq_module
let prefix_to_dir = String.concat Filename.dir_sep
let native_install_files ~tname ~rule coq_module =
match rule with
| Rule_type.Regular { native = CoqNative }
| Regular { native = Coqc } ->
native_obj_files ~tname ~install:false coq_module
, native_obj_files ~tname ~install:true coq_module
| Regular { native = Disabled } -> [], []
(* quick/vio woes... it does produce a different set of targets than
regular compilation *)
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 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
let dst = List.map (Filename.concat ppath) (src_base @ dst_native) in
List.combine src dst
let native_obj_files = native_obj_files ~install:false
|
