Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: coq_makefile.ml Sprache: SML

Original von: Coq^©

(************************************************************************)
(*         *   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 (>) f g = fun x -> g (f x)

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_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";
  output_string stderr "\
\nFull list of options:\
\n\
\n[file.v]: Coq file to be compiled\
\n[file.ml[i4]?]: Objective Caml file to be compiled\
\n[file.ml{lib,pack}]: ocamlbuild-style 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 recursively\
\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[-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 coqlib = Envars.coqlib () in
  let makefile_template =
    let template = Filename.concat "tools" "CoqMakefile.in" in
    Filename.concat 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 (forget_source > pr_path) sps

let generate_conf_subdirs oc sds =
  if sds <> [] then section oc "Subdirectories. (DEPRECATED)";
  let iter f = List.iter (forget_source > f) in
  iter (fprintf oc ".PHONY:%s\n") sds;
  iter (fprintf oc "post-all::\n\tcd \"%s\" && $(MAKE) all\n") sds;
  iter (fprintf oc "clean::\n\tcd \"%s\" && $(MAKE) clean\n") sds;
  iter (fprintf oc "archclean::\n\tcd \"%s\" && $(MAKE) archclean\n") sds;
  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 map = map_sourced_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));
  fprintf oc "COQMF_CMDLINE_COQLIBS = %s %s %s\n"
    (S.concat " " (map_cmdline (fun { path } -> dash1 "I" path) ml_includes))
    (S.concat " " (map_cmdline (fun ({ path },l) -> dash2 "Q" path l) q_includes))
    (S.concat " " (map_cmdline (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 ""
;;

let generate_conf_coq_config oc =
  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; mlg_files; ml_files; mllib_files; mlpack_files; }
=
  let module S = String in
  let map = map_sourced_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_MLGFILES = %s\n"    (S.concat " " (map quote mlg_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 cmdline_vfiles = filter_cmdline v_files in
  fprintf oc "COQMF_CMDLINE_VFILES = %s\n" (S.concat " " (List.map quote cmdline_vfiles));
;;

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 (forget_source > snd) (q_includes @ r_includes) in
  let logpaths = List.map (String.split_on_char '.') includes in
  let gcd = logic_gcd [] logpaths in
  let root =
    if gcd = [] then
      if not (List.exists (fun x -> fst x.thing = "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 Filename.dir_sep 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 (forget_source > (fun (k,v) -> Printf.fprintf oc "%s = %s\n" k v)) defs;
  Printf.fprintf oc "COQMF_OTHERFLAGS = %s\n"
    (String.concat " " (List.map forget_source 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;
  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; mlg_files;
     mllib_files; mlpack_files } as project)
  =
  let exists f = List.exists (forget_source > f) in
  let here = Sys.getcwd () in
  let not_tops = List.for_all (fun s -> s.thing <> Filename.basename s.thing) 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 mlg_files &&
      not_tops ml_files && not_tops mllib_files && not_tops mlpack_files)
  then
    project
  else
    let source x = {thing=x; source=CmdLine} in
    let here_path = { path = "."; canonical_path = here } in
    { project with
        ml_includes = source here_path :: ml_includes;
        r_includes = source (here_path, "Top") :: r_includes }
;;

let warn_install_at_root_directory
  ({ q_includes; r_includes; } as project)
=
  let open CList in
  let inc_top_p =
    map_filter
      (fun {thing=({ path } ,ldir)} -> if ldir = "" then Some path else None)
      (r_includes @ q_includes) in
  let files = all_files project in
  let bad = filter (fun f -> mem (Filename.dirname f.thing) 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.thing) bad;
    eprintf "\n";
  end
;;

let check_overlapping_include { q_includes; r_includes } =
  let pwd = Sys.getcwd () in
  let aux = function
    | [] -> ()
    | {thing = { 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 {thing={ 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 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 =
    Filename.concat
      (physical_dir_of_logical_dir logic)
      (chop_prefix canonical_path file_dir) in
  let candidates =
    CList.map_filter (fun {thing={ 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 {thing={ canonical_path = p }} -> is_prefix p file_dir)
          ml_includes
     with
        | [{thing={ canonical_path }, logic}], {thing={ canonical_path = p }} ->
            let destination =
              Filename.concat
                (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 = String.split_on_char '.' s1 in
  let s2 = String.split_on_char '.' 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 =
    let warning_fn x = Format.eprintf "%s@\n%!" x in
    try cmdline_args_to_project ~warning_fn ~curdir:Filename.current_dir_name args
    with Parsing_error s -> prerr_endline s; usage_coq_makefile () 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

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.