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
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
|
open! Coq_dune
(* Coqnative overhead is more than 33% in build time :( :( *)
(* in a 16-core system:
- coqnative:
real 2m29,860s
user 19m44,997s
sys 2m19,618s
real 2m30,940s
user 20m6,945s
sys 2m22,057s
- coqc -native-compiler on
real 2m30,567s
user 14m17,062s
sys 1m47,661s
real 2m29,008s
user 14m15,293s
sys 1m48,194s
*)
(* let native_mode = Coq_module.Rule_type.CoqNative *)
let native_mode = Coq_module.Rule_type.Coqc
let native = match Coq_config.native_compiler with
| Coq_config.NativeOff -> Coq_module.Rule_type.Disabled
| Coq_config.NativeOn _ -> native_mode
(** arguments are [gen_rules theory_name dir flags] *)
type args = {
tname : string list;
base_dir : string;
async : bool;
rule : Coq_module.Rule_type.t;
split : bool;
noinit : bool;
user_flags : Arg.t list;
dependencies : string list;
}
let parse_args () : args =
match Array.to_list Sys.argv with
| _ :: tname :: base_dir :: args ->
let tname = String.split_on_char '.' tname in
let _backtrace = [Arg.A "-d"; Arg.A "backtrace"] in
let default = { base_dir; tname;
async = false;
split = false;
noinit = false;
rule = Coq_module.Rule_type.Regular { native };
user_flags = [];
dependencies = [];
}
in
let rec parse a = function
| [] -> a
| "-async" :: rest -> parse { a with async = true; user_flags = Arg.[A "-async-proofs"; A "on"] } rest
| "-split" :: rest -> parse { a with split = true } rest
| "-dep" :: d :: rest -> parse { a with dependencies = d :: a.dependencies } rest
| "-noinit" :: rest -> parse { a with noinit = true } rest
(* Dune will sometimes pass this option as "" *)
| "" :: rest -> parse a rest
| unknown :: _ -> raise (Invalid_argument unknown)
in
parse default args
| _ -> raise (Invalid_argument "usage: gen_rules theory_name directory")
let ppr fmt = List.iter (Dune_file.Rule.pp fmt)
let ppi fmt = List.iter (Dune_file.Install.pp fmt)
let main () =
let { tname; base_dir; async; rule; user_flags; split; noinit; dependencies } = parse_args () in
let root_lvl = List.length (String.split_on_char '/' base_dir) in
let corelib =
let directory = Path.relative (Path.make "theories") "Corelib" in
Coq_rules.Theory.{ directory; dirname = ["Corelib"]; implicit = true; deps = [] }
in
(* usually the else case here is Ltac2, but other libraries could be
handled as well *)
let boot, implicit = if tname = ["Corelib"] then begin
if noinit then CErrors.user_err Pp.(str "Corelib handles -noinit automatically.");
Coq_rules.Boot_type.Corelib, true
end
else Coq_rules.Boot_type.Regular { corelib; noinit }, false
in
(* Rule generation *)
let dir_info = Dir_info.scan ~prefix:[] base_dir in
let directory = Path.make base_dir in
let theory = Coq_rules.Theory.{ directory; dirname = tname; implicit; deps = dependencies } in
let cctx = Coq_rules.Context.make ~root_lvl ~theory ~user_flags ~rule ~boot ~dir_info ~async ~split in
let vo_rules = Coq_rules.vo_rules ~dir_info ~cctx in
let install_rules = Coq_rules.install_rules ~dir_info ~cctx in
(* Rule printing *)
let fmt = Format.std_formatter in
List.iter (Dune_file.Subdir.pp ppr fmt) vo_rules;
List.iter (Dune_file.Subdir.pp ppi fmt) install_rules;
(* Rules for coqnative (not always setup for now, need to think about this) *)
begin
match native_mode with
(* cmxs files are already generated in coqc *)
| Coq_module.Rule_type.Disabled
| Coq_module.Rule_type.Coqc -> ()
| Coq_module.Rule_type.CoqNative ->
let coqnative_rules = Coq_rules.coqnative_rules ~dir_info ~cctx in
List.iter (Dune_file.Subdir.pp ppr fmt) coqnative_rules
end;
Format.pp_print_flush fmt ();
()
let pr_feedback (fb : Feedback.feedback) =
match fb.contents with
| Message (_,_,_,msg) -> Format.eprintf "%a" Pp.pp_with msg
| _ -> () [@@warning "-4"]
let () =
Printexc.record_backtrace true;
let _ : int = Feedback.add_feeder pr_feedback in
try main ()
with exn ->
Format.eprintf "[gen_rules] Fatal error:@ @[<2>%a@]@\n%!" Pp.pp_with (CErrors.print exn);
exit 1
|
