aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coq_makefile.ml
blob: ef4428755a90574c2b177d83634423c07ba29bae (plain)
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
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \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)         *)
(************************************************************************)

(* Coq_makefile: automatically create a Makefile for a Coq development *)

open CoqProject_file
open Printf

let output_channel = ref stdout
let makefile_name = ref "Makefile"
let make_name = ref ""

let print x = output_string !output_channel x
let printf x = Printf.fprintf !output_channel x

let rec print_list sep = function
  | [ x ] -> print x
  | x :: l -> print x; print sep; print_list sep l
  | [] -> ()

let rec print_prefix_list sep = function
  | x :: l -> print sep; print x; print_prefix_list sep l
  | [] -> ()

let usage_common () =
  output_string stderr "\
\n[file.v]: Coq file to be compiled\
\n[file.ml[i4]?]: Objective Caml file to be compiled\
\n[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml\
\n  library/module\
\n[any] : subdirectory that should be \"made\" and has a Makefile itself\
\n  to do so. Very fragile and discouraged.\
\n[-extra result dependencies command]: add target \"result\" with command\
\n  \"command\" and dependencies \"dependencies\". If \"result\" is not\
\n  generic (do not contains a %), \"result\" is built by _make all_ and\
\n  deleted by _make clean_.\
\n[-extra-phony result dependencies command]: add a PHONY target \"result\"\
\n with command \"command\" and dependencies \"dependencies\". Note that\
\n _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as\
\n as a dependencies of an already defined target \"foo\".\
\n[-I dir]: look for Objective Caml dependencies in \"dir\"\
\n[-R physicalpath logicalpath]: look for Coq dependencies resursively\
\n  starting from \"physicalpath\". The logical path associated to the\
\n  physical path is \"logicalpath\".\
\n[-Q physicalpath logicalpath]: look for Coq dependencies starting from\
\n  \"physicalpath\". The logical path associated to the physical path\
\n  is \"logicalpath\".\
\n[VARIABLE = value]: Add the variable definition \"VARIABLE=value\"\
\n[-byte]: compile with byte-code version of coq\
\n[-opt]: compile with native-code version of coq\
\n[-arg opt]: send option \"opt\" to coqc\
\n[-install opt]: where opt is \"user\" to force install into user directory,\
\n  \"none\" to build a makefile with no install target or\
\n  \"global\" to force install in $COQLIB directory\
\n"

let usage_coq_project () =
  output_string stderr "Available arguments:";
  usage_common ();
  exit 1

let usage_coq_makefile () =
  output_string stderr "Usage summary:\
\n\
\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\
\n  ... [any] ... [-extra[-phony] result dependencies command]\
\n  ... [-I dir] ... [-R physicalpath logicalpath]\
\n  ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\
\n  ...  [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\
\n  [-h] [--help]\
\n";
  usage_common ();
  output_string stderr "\
\n[-f file]: take the contents of file as arguments\
\n[-o file]: output should go in file file (recommended)\
\n	Output file outside the current directory is forbidden.\
\n[-h]: print this usage summary\
\n[--help]: equivalent to [-h]\n";
  exit 1

let is_genrule r = (* generic rule (like bar%foo: ...) *)
    let genrule = Str.regexp("%") in
      Str.string_match genrule r 0

let is_prefix dir1 dir2 =
  let l1 = String.length dir1 in
  let l2 = String.length dir2 in
  let sep = Filename.dir_sep in
  if dir1 = dir2 then true
  else if l1 + String.length sep <= l2 then
    let dir1' = String.sub dir2 0 l1 in
    let sep' = String.sub dir2 l1 (String.length sep) in
    dir1' = dir1 && sep' = sep
  else false

let physical_dir_of_logical_dir ldir =
  let ldir = Bytes.of_string ldir in
  let le = Bytes.length ldir - 1 in
  let pdir =
    if le >= 0 && Bytes.get ldir le = '.' then Bytes.sub ldir 0 (le - 1)
    else Bytes.copy ldir
  in
  for i = 0 to le - 1 do
    if Bytes.get pdir i = '.' then Bytes.set pdir i '/';
  done;
  Bytes.to_string pdir

let read_whole_file s =
  let ic = open_in s in
  let b = Buffer.create (1 lsl 12) in
  try
     while true do
       let s = input_line ic in
       Buffer.add_string b s;
       Buffer.add_char b '\n';
     done;
     assert false;
  with End_of_file ->
    close_in ic;
    Buffer.contents b

let quote s = if String.contains s ' ' || CString.is_empty s then "'" ^ s ^ "'" else s

let generate_makefile oc conf_file local_file args project =
  let makefile_template =
    let template = "/tools/CoqMakefile.in" in
    Envars.coqlib () ^ template in
  let s = read_whole_file makefile_template in
  let s = List.fold_left
    (* We use global_substitute to avoid running into backslash issues due to \1 etc. *)
    (fun s (k,v) -> Str.global_substitute (Str.regexp_string k) (fun _ -> v) s) s
    [ "@CONF_FILE@", conf_file;
      "@LOCAL_FILE@", local_file;
      "@COQ_VERSION@", Coq_config.version;
      "@PROJECT_FILE@", (Option.default "" project.project_file);
      "@COQ_MAKEFILE_INVOCATION@",String.concat " " (List.map quote args);
    ] in
  output_string oc s
;;

let section oc s =
  let pad = String.make (76 - String.length s) ' ' in
  let sharps = String.make 79 '#' in
  let spaces = "#" ^ String.make 77 ' ' ^ "#" in
  fprintf oc "\n%s\n" sharps;
  fprintf oc "%s\n" spaces;
  fprintf oc "# %s%s#\n" s pad;
  fprintf oc "%s\n" spaces;
  fprintf oc "%s\n\n" sharps
;;

let clean_tgts = ["clean"; "cleanall"; "archclean"]

let generate_conf_extra_target oc sps =
  let pr_path { target; dependencies; phony; command } =
    let target = if target = "all" then "custom-all" else target in
    if phony then fprintf oc ".PHONY: %s\n" target;
    if not (is_genrule target) && not phony then begin
      fprintf oc "post-all::\n\t$(MAKE) -f $(SELF) %s\n" target;
      if not phony then
        fprintf oc "clean::\n\trm -f %s\n" target;
    end;
    fprintf oc "%s %s %s\n\t%s\n\n"
       target
       (if List.mem target clean_tgts then ":: " else ": ")
       dependencies
       command
  in
    if sps <> [] then
      section oc "Extra targets. (-extra and -extra-phony, DEPRECATED)";
    List.iter pr_path sps

let generate_conf_subdirs oc sds =
  if sds <> [] then section oc "Subdirectories. (DEPRECATED)";
  List.iter (fprintf oc ".PHONY:%s\n") sds;
  List.iter (fprintf oc "post-all::\n\tcd \"%s\" && $(MAKE) all\n") sds;
  List.iter (fprintf oc "clean::\n\tcd \"%s\" && $(MAKE) clean\n") sds;
  List.iter (fprintf oc "archclean::\n\tcd \"%s\" && $(MAKE) archclean\n") sds;
  List.iter (fprintf oc "install-extra::\n\tcd \"%s\" && $(MAKE) install\n") sds
   

let generate_conf_includes oc { ml_includes; r_includes; q_includes } =
  section oc "Path directives (-I, -R, -Q).";
  let module S = String in
  let open List in
  let dash1 opt v = sprintf "-%s %s" opt (quote v) in
  let dash2 opt v1 v2 = sprintf "-%s %s %s" opt (quote v1) (quote v2) in
  fprintf oc "COQMF_OCAMLLIBS = %s\n"
    (S.concat " " (map (fun { path } -> dash1 "I" path) ml_includes));
  fprintf oc "COQMF_SRC_SUBDIRS = %s\n"
    (S.concat " " (map (fun { path } -> quote path) ml_includes));
  fprintf oc "COQMF_COQLIBS = %s %s %s\n"
    (S.concat " " (map (fun { path } -> dash1 "I" path) ml_includes))
    (S.concat " " (map (fun ({ path },l) -> dash2 "Q" path l) q_includes))
    (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes));
  fprintf oc "COQMF_COQLIBS_NOML = %s %s\n"
    (S.concat " " (map (fun ({ path },l) -> dash2 "Q" path l) q_includes))
    (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes))
;;

let windrive s =
  if Coq_config.arch_is_win32 && Str.(string_match (regexp "^[a-zA-Z]:") s 0)
  then Str.matched_string s
  else s
;;

let generate_conf_coq_config oc args =
  section oc "Coq configuration.";
  let src_dirs = Coq_config.all_src_dirs in
  Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs;
  fprintf oc "COQMF_WINDRIVE=%s\n" (windrive Coq_config.coqlib)
;;

let generate_conf_files oc
  { v_files; mli_files; ml4_files; ml_files; mllib_files; mlpack_files }
=
  let module S = String in
  let open List in
  section oc "Project files.";
  fprintf oc "COQMF_VFILES = %s\n"      (S.concat " " (map quote v_files));
  fprintf oc "COQMF_MLIFILES = %s\n"    (S.concat " " (map quote mli_files));
  fprintf oc "COQMF_MLFILES = %s\n"     (S.concat " " (map quote ml_files));
  fprintf oc "COQMF_ML4FILES = %s\n"    (S.concat " " (map quote ml4_files));
  fprintf oc "COQMF_MLPACKFILES = %s\n" (S.concat " " (map quote mlpack_files));
  fprintf oc "COQMF_MLLIBFILES = %s\n"  (S.concat " " (map quote mllib_files));
;;

let rec all_start_with prefix = function
  | [] -> true
  | [] :: _ -> false
  | (x :: _) :: rest -> x = prefix && all_start_with prefix rest

let rec logic_gcd acc = function
  | [] -> acc
  | [] :: _ -> acc
  | (hd :: tl) :: rest ->
      if all_start_with hd rest
      then logic_gcd (acc @ [hd]) (tl :: List.map List.tl rest)
      else acc

let generate_conf_doc oc { defs; q_includes; r_includes } =
  let includes = List.map snd (q_includes @ r_includes) in
  let logpaths = List.map (CString.split '.') includes in
  let gcd = logic_gcd [] logpaths in
  let root =
    if gcd = [] then
      if not (List.mem_assoc "INSTALLDEFAULTROOT" defs) then begin
         let destination = "orphan_" ^ (String.concat "_" includes) in
         eprintf "Warning: no common logical root\n";
         eprintf "Warning: in such case INSTALLDEFAULTROOT must be defined\n";
         eprintf "Warning: the install-doc target is going to install files\n";
         eprintf "Warning: in %s\n" destination;
         destination
      end else "$(INSTALLDEFAULTROOT)"
    else String.concat "/" gcd in
  Printf.fprintf oc "COQMF_INSTALLCOQDOCROOT = %s\n" (quote root)

let generate_conf_defs oc { defs; extra_args } =
  section oc "Extra variables.";
  List.iter (fun (k,v) -> Printf.fprintf oc "%s = %s\n" k v) defs;
  Printf.fprintf oc "COQMF_OTHERFLAGS = %s\n"
    (String.concat " " extra_args)

let generate_conf oc project args  =
  fprintf oc "# This configuration file was generated by running:\n";
  fprintf oc "# %s\n\n" (String.concat " " (List.map quote args));
  generate_conf_files oc project;
  generate_conf_includes oc project;
  generate_conf_coq_config oc args;
  generate_conf_defs oc project;
  generate_conf_doc oc project;
  generate_conf_extra_target oc project.extra_targets;
  generate_conf_subdirs oc project.subdirs;
;;

let ensure_root_dir
  ({ ml_includes; r_includes; q_includes;
     v_files; ml_files; mli_files; ml4_files;
     mllib_files; mlpack_files } as project)
=
  let open List in
  let here = Sys.getcwd () in
  let not_tops = List.for_all (fun s -> s <> Filename.basename s) in
  if exists (fun { canonical_path = x } -> x = here) ml_includes
  || exists (fun ({ canonical_path = x },_) -> is_prefix x here) r_includes
  || exists (fun ({ canonical_path = x },_) -> is_prefix x here) q_includes
  || (not_tops v_files &&
      not_tops mli_files && not_tops ml4_files && not_tops ml_files &&
      not_tops mllib_files && not_tops mlpack_files)
  then
    project
  else
    let here_path = { path = "."; canonical_path = here } in
    { project with
        ml_includes = here_path :: ml_includes;
        r_includes = (here_path, "Top") :: r_includes }
;;

let warn_install_at_root_directory 
  { q_includes; r_includes;
    v_files; ml_files; mli_files; ml4_files;
    mllib_files; mlpack_files }
=
  let open CList in
  let inc_top_p =
    map_filter
      (fun ({ path } ,ldir) -> if ldir = "" then Some path else None)
      (r_includes @ q_includes) in
  let files =
    v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files in
  let bad = filter (fun f -> mem (Filename.dirname f) inc_top_p) files in
  if bad <> [] then begin
    eprintf "Warning: No file should be installed at the root of Coq's library.\n";
    eprintf "Warning: No logical path (-R, -Q) applies to these files:\n";
    List.iter (fun x -> eprintf "Warning:  %s\n" x) bad;
    eprintf "\n";
  end
;;

let check_overlapping_include { q_includes; r_includes } =
  let pwd = Sys.getcwd () in
  let aux = function
    | [] -> ()
    | ({ path; canonical_path }, _) :: l ->
	if not (is_prefix pwd canonical_path) then
	  eprintf "Warning: %s (used in -R or -Q) is not a subdirectory of the current directory\n\n" path;
	List.iter (fun ({ path = p; canonical_path = cp }, _) ->
	  if is_prefix canonical_path cp  || is_prefix cp canonical_path then
	    eprintf "Warning: %s and %s overlap (used in -R or -Q)\n\n"
              path p) l
  in
    aux (q_includes @ r_includes)
;;

let chop_prefix p f =
  let len_p = String.length p in
  let len_f = String.length f in
  String.sub f len_p (len_f - len_p)

let clean_path p =
  Str.global_replace (Str.regexp_string "//") "/" p

let destination_of { ml_includes; q_includes; r_includes; } file =
  let file_dir = CUnix.canonical_path_name (Filename.dirname file) in
  let includes = q_includes @ r_includes in
  let mk_destination logic canonical_path =
    clean_path (physical_dir_of_logical_dir logic ^ "/" ^
                chop_prefix canonical_path file_dir ^ "/") in
  let candidates =
    CList.map_filter (fun ({ canonical_path }, logic) ->
      if is_prefix canonical_path file_dir then
        Some(mk_destination logic canonical_path)
      else None) includes
  in
  match candidates with
  | [] ->
     (* BACKWARD COMPATIBILITY: -I into the only logical root *)
     begin match
        r_includes,
        List.find (fun { canonical_path = p } -> is_prefix p file_dir)
          ml_includes
     with
        | [{ canonical_path }, logic], { canonical_path = p } ->
            let destination =
              clean_path (physical_dir_of_logical_dir logic ^ "/" ^
                          chop_prefix p file_dir ^ "/") in
            Printf.printf "%s" (quote destination)
        | _ -> () (* skip *)
        | exception Not_found -> () (* skip *)
     end
  | [s] -> Printf.printf "%s" (quote s)
  | _ -> assert false

let share_prefix s1 s2 =
  let s1 = CString.split '.' s1 in
  let s2 = CString.split '.' s2 in
  match s1, s2 with
  | x :: _ , y :: _ -> x = y
  | _ -> false

let _ =
  let _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in
  let prog, args =
    let args = Array.to_list Sys.argv in
    let prog = List.hd args in
    prog, List.tl args in

  let only_destination, args = match args with
    | "-destination-of" :: tgt :: rest -> Some tgt, rest
    | _ -> None, args in

  let project = 
    try cmdline_args_to_project ~curdir:Filename.current_dir_name args
    with Parsing_error s -> prerr_endline s; usage_coq_project () in

  if only_destination <> None then begin
    destination_of project (Option.get only_destination);
    exit 0
  end;

  if project.makefile = None then
    eprintf "Warning: Omitting -o is deprecated\n\n";
    (* We want to know the name of the Makefile (say m) in order to
     * generate m.conf and include m.local *)

  let conf_file = Option.default "CoqMakefile" project.makefile ^ ".conf" in
  let local_file = Option.default "CoqMakefile" project.makefile ^ ".local" in

  if project.extra_targets <> [] then begin
    eprintf "Warning: -extra and -extra-phony are deprecated.\n";
    eprintf "Warning: Write the extra targets in %s.\n\n" local_file;
  end;

  if project.subdirs <> [] then begin
    eprintf "Warning: Subdirectories are deprecated.\n";
    eprintf "Warning: Use double colon rules in %s.\n\n" local_file;
  end;

  let project = ensure_root_dir project in
  
  if project.install_kind <> (Some CoqProject_file.NoInstall) then begin
    warn_install_at_root_directory project;
  end;

  check_overlapping_include project;

  Envars.set_coqlib ~fail:(fun x -> Printf.eprintf "Error: %s\n" x; exit 1);
  
  let ocm = Option.cata open_out stdout project.makefile in
  generate_makefile ocm conf_file local_file (prog :: args) project;
  close_out ocm;
  let occ = open_out conf_file in
  generate_conf occ project (prog :: args);
  close_out occ;
  exit 0