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
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
type worker = {
package : string;
basename : string;
}
let get_worker_path {package; basename} =
let dir = try Findlib.package_directory package
with Findlib.No_such_package _ ->
Printf.eprintf "Error: Could not find package %s.\n%!" package;
exit 1
in
let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in
Filename.concat dir (basename^exe)
type init_opts = {
boot : bool;
coqlib : string option;
ml_includes : string list;
queries : Boot.Usage.query list;
}
let default_opts = {
boot = false;
coqlib = None;
ml_includes = [];
queries = [];
}
let add_query q opts = { opts with queries = q :: opts.queries }
let parse_query = let open Boot.Usage in function
| "-config"|"--config" -> Some PrintConfig
| "-where" -> Some PrintWhere
| "-v"|"-version"|"--version" -> Some PrintVersion
| "-print-version"|"--print-version" -> Some PrintMachineReadableVersion
| _ -> None
let rec parse_args opts = function
| [] -> opts
| "-boot" :: rest -> parse_args {opts with boot = true} rest
| "-coqlib" :: lib :: rest -> parse_args {opts with coqlib = Some lib} rest
| "-I" :: ml :: rest -> parse_args {opts with ml_includes = ml :: opts.ml_includes} rest
| arg :: rest ->
match parse_query arg with
| Some q -> parse_args (add_query q opts) rest
| None -> parse_args opts rest
let parse_args args =
let opts = parse_args default_opts args in
let opts = {
opts with
ml_includes = List.rev opts.ml_includes;
queries = List.rev opts.queries;
}
in
opts
let with_ic file f =
let ic = open_in file in
try
let rc = f ic in
close_in ic;
rc
with e -> close_in ic; raise e
let parse_env_line l =
try Scanf.sscanf l "%[^=]=%S" (fun name value -> Some(name,value))
with Scanf.Scan_failure _ | End_of_file -> None
(** We [putenv] instead of wrapping [getenv] calls because the
subprocess also needs the updated env, and usually doesn't have
the env file next to its binary. *)
let putenv_from_file ~debug () =
let base = Filename.dirname Sys.executable_name in
let f = base ^ "/coq_environment.txt" in
try
with_ic f (fun ic ->
let () = if debug then Printf.eprintf "using env vars from %s\n%!" f in
let rec iter () =
match input_line ic with
| exception End_of_file -> ()
| l ->
let () = match parse_env_line l with
| Some(n,v) ->
begin match Sys.getenv_opt n with
| None -> Unix.putenv n v
| Some _ -> ()
end
| None -> ()
in
iter ()
in
iter ())
with
| Sys_error s -> ()
let make_ocamlpath envopt opts =
let boot_ml_path = match envopt with
| Boot.Env.Boot -> []
| Boot.Env.Env coqenv ->
Boot.Env.Path.[to_string (relative (Boot.Env.runtimelib coqenv) "..")]
in
let env_ocamlpath =
try [Sys.getenv "OCAMLPATH"]
with Not_found -> []
in
let path = List.concat [opts.ml_includes; boot_ml_path; env_ocamlpath] in
let ocamlpathsep = if Sys.unix then ":" else ";" in
String.concat ocamlpathsep path
let exec_or_create_process prog argv =
if Sys.os_type <> "Win32" then
Unix.execv prog argv
else
let pid = Unix.create_process prog argv Unix.stdin Unix.stdout Unix.stderr in
if pid = 0 then begin
Printf.eprintf "coqc shim: create_process failed\n%!";
exit 127
end;
let _, status = Unix.waitpid [] pid in
match status with
| WEXITED n | WSIGNALED n -> exit n
| WSTOPPED _ ->
assert false
type opts = { debug_shim : bool }
let parse_opts = function
| "-debug-shim" :: rest -> { debug_shim = true }, rest
| args -> { debug_shim = false }, args
let warn_ignored_coqlib () = ()
let boot_env opts =
match Boot.Env.print_queries_maybe_init ~boot:opts.boot ~coqlib:opts.coqlib
~warn_ignored_coqlib
None opts.queries
with
| Ok env -> env
| Error msg -> Printf.eprintf "%s\n%!" msg; exit 1
let init { debug_shim=debug } args =
let () = putenv_from_file ~debug () in
let opts = parse_args args in
let coqenv = boot_env opts in
let () = match opts.queries with [] -> () | _ :: _ -> exit 0 in
let env_ocamlpath = make_ocamlpath coqenv opts in
let () = if debug then Printf.eprintf "OCAMLPATH = %s\n%!" env_ocamlpath in
Findlib.init ~env_ocamlpath ()
let try_run_queries { debug_shim=debug } args =
let () = putenv_from_file ~debug () in
let opts = parse_args args in
match opts.queries with
| [] -> false
| _ :: _ ->
let _coqenv = boot_env opts in
true