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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* Makefile's escaping rules are awful: $ is escaped by doubling and
other special characters are escaped by backslash prefixing while
backslashes themselves must be escaped only if part of a sequence
followed by a special character (i.e. in case of ambiguity with a
use of it as escaping character). Moreover (even if not crucial)
it is apparently not possible to directly escape ';' and leading '\t'. *)
let escape =
let s' = Buffer.create 10 in
fun s ->
Buffer.clear s';
for i = 0 to String.length s - 1 do
let c = s.[i] in
if c = ' ' || c = '#' || c = ':' (* separators and comments *)
|| c = '%' (* pattern *)
|| c = '?' || c = '[' || c = ']' || c = '*' (* expansion in filenames *)
|| i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' ||
'A' <= s.[1] && s.[1] <= 'Z' ||
'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *)
then begin
let j = ref (i-1) in
while !j >= 0 && s.[!j] = '\\' do
Buffer.add_char s' '\\'; decr j (* escape all preceding '\' *)
done;
Buffer.add_char s' '\\';
end;
if c = '$' then Buffer.add_char s' '$';
Buffer.add_char s' c
done;
Buffer.contents s'
open Format
type dynlink = Opt | Byte | Both | No | Variable
let option_dynlink = ref Both
let set_dyndep = function
| "no" -> option_dynlink := No
| "opt" -> option_dynlink := Opt
| "byte" -> option_dynlink := Byte
| "both" -> option_dynlink := Both
| "var" -> option_dynlink := Variable
| o -> CErrors.user_err Pp.(str "Incorrect -dyndep option: " ++ str o)
let mldep_to_make (base, suff) =
match !option_dynlink with
| No -> []
| Byte -> [sprintf "%s%s" base suff]
| Opt -> [sprintf "%s.cmxs" base]
| Both ->
[sprintf "%s%s" base suff ; sprintf "%s.cmxs" base]
| Variable ->
[sprintf "%s%s" base (if suff=".cmo" then "$(DYNOBJ)" else "$(DYNLIB)")]
let string_of_dep ~suffix = let open Dep_info.Dep in
function
| Require basename -> [escape basename ^ suffix]
| Ml (base,suff) -> mldep_to_make (escape base,suff)
| Other s -> [escape s]
let string_of_dependency_list ~suffix deps =
List.map (string_of_dep ~suffix) deps
|> List.concat |> String.concat " "
let option_noglob = ref false
let option_write_vos = ref false
let set_noglob glob = option_noglob := glob
let set_write_vos vos = option_write_vos := vos
let print_dep fmt { Dep_info.name; deps } =
let ename = escape name in
let glob = if !option_noglob then "" else ename^".glob " in
fprintf fmt "%s.vo %s%s.v.beautified %s.required_vo: %s.v %s\n" ename glob ename ename ename
(string_of_dependency_list ~suffix:".vo" deps);
if !option_write_vos then
fprintf fmt "%s.vos %s.vok %s.required_vos: %s.v %s\n" ename ename ename ename
(string_of_dependency_list ~suffix:".vos" deps);
fprintf fmt "%!"
|
