Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: coq_dune.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)         *)
(************************************************************************)

(* LICENSE NOTE: This file is dually MIT/LGPL 2.1+ licensed. MIT license:
*
* Permission is hereby granted, free of charge, to any person obtaining a copy
* of this software and associated documentation files (the "Software"), to deal
* in the Software without restriction, including without limitation the rights
* to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
* copies of the Software, and to permit persons to whom the Software is
* furnished to do so, subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
* AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
* OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
* SOFTWARE.
*)

(* coq_dune: generate dune build rules for .vo files                    *)
(*                                                                      *)
(* At some point this file will become a Dune plugin, so it is very     *)
(* important that this file can be bootstrapped with:                   *)
(*                                                                      *)
(* ocamlfind ocamlopt -linkpkg -package str coq_dune.ml -o coq_dune     *)

open Format

(* Keeping this file self-contained as it is a "bootstrap" utility *)
(* Is OCaml missing these basic functions in the stdlib?           *)
module Aux = struct

  let option_iter f o = match o with
    | Some x -> f x
    | None -> ()

  let option_cata d f o = match o with
    | Some x -> f x
    | None -> d

  let list_compare f = let rec lc x y = match x, y with
      | [], [] -> 0
      | [], _ -> -1
      | _, [] -> 1
      | x::xs, y::ys -> let r = f x y in if r = 0 then lc xs ys else r
    in lc

  let rec pp_list pp sep fmt l = match l with
    | []  -> ()
    | [l] -> fprintf fmt "%a" pp l
    | x::xs -> fprintf fmt "%a%a%a" pp x sep () (pp_list pp sep) xs

  let rec pmap f l = match l with
    | []  -> []
    | x :: xs ->
      begin match f x with
        | None -> pmap f xs
        | Some r -> r :: pmap f xs
      end

  let sep fmt () = fprintf fmt "@;"

  (* Creation of paths, aware of the platform separator. *)
  let bpath l = String.concat Filename.dir_sep l

  module DirOrd = struct
    type t = string list
    let compare = list_compare String.compare
  end

  module DirMap = Map.Make(DirOrd)

  (* Functions available in newer OCaml versions *)
  (* Taken from the OCaml std library (c) INRIA / LGPL-2.1 *)
  module Legacy = struct

    (* Fix once we move to OCaml >= 4.06.0 *)
    let list_init len f =
      let rec init_aux i n f =
        if i >= n then []
        else let r = f i in r :: init_aux (i+1) n f
      in init_aux 0 len f

    (* Slower version of DirMap.update, waiting for OCaml 4.06.0 *)
    let dirmap_update key f map =
      match begin
        try f (Some (DirMap.find key map))
        with Not_found -> f None
      end with
      | None   -> DirMap.remove key map
      | Some x -> DirMap.add key x map

  end

  let add_map_list key elem map =
    (* Move to Dirmap.update once we require OCaml >= 4.06.0 *)
    Legacy.dirmap_update key (fun l -> Some (option_cata [elem] (fun ll -> elem :: ll) l)) map

  let replace_ext ~file ~newext =
    Filename.(remove_extension file) ^ newext

end

open Aux

(* Once this is a Dune plugin the flags will be taken from the env *)
module Options = struct

  type flag = {
    enabled : bool;
    cmd : string;
  }

  let all_opts =
  [ { enabled = false; cmd = "-debug"; }
  ; { enabled = false; cmd = "-native_compiler"; }
  ; { enabled = true; cmd = "-allow-sprop"; }
  ]

  let build_coq_flags () =
    let popt o = if o.enabled then Some o.cmd else None in
    String.concat " " @@ pmap popt all_opts
end

type vodep = {
  target: string;
  deps : string list;
}

type ldep = | VO of vodep | MLG of string
type ddir = ldep list DirMap.t

(* Filter `.vio` etc... *)
let filter_no_vo =
  List.filter (fun f -> Filename.check_suffix f ".vo")

(* We could have coqdep to output dune files directly *)

let gen_sub n =
  (* Move to List.init once we can depend on OCaml >= 4.06.0 *)
  bpath @@ Legacy.list_init n (fun _ -> "..")

let pp_rule fmt targets deps action =
  (* Special printing of the first rule *)
  let ppl = pp_list pp_print_string sep in
  let pp_deps fmt l = match l with
    | [] ->
      ()
    | x :: xs ->
      fprintf fmt "(:pp-file %s)%a" x sep ();
      pp_list pp_print_string sep fmt xs
  in
  fprintf fmt
    "@[(rule@\n @[(targets @[%a@])@\n(deps @[%a@])@\n(action @[%a@])@])@]@\n"
    ppl targets pp_deps deps pp_print_string action

let gen_coqc_targets vo =
  [ vo.target
  ; replace_ext ~file:vo.target ~newext:".glob"
  ; "." ^ replace_ext ~file:vo.target ~newext:".aux"]

(* Generate the dune rule: *)
let pp_vo_dep dir fmt vo =
  let depth = List.length dir in
  let sdir = gen_sub depth in
  (* All files except those in Init implicitly depend on the Prelude, we account for it here. *)
  let eflag, edep = if List.tl dir = ["Init"] then "-noinit -R theories Coq", [] else "", [bpath ["theories";"Init";"Prelude.vo"]] in
  (* Coq flags *)
  let cflag = Options.build_coq_flags () in
  (* Correct path from global to local "theories/Init/Decimal.vo" -> "../../theories/Init/Decimal.vo" *)
  let deps = List.map (fun s -> bpath [sdir;s]) (edep @ vo.deps) in
  (* The source file is also corrected as we will call coqtop from the top dir *)
  let source = bpath (dir @ [replace_ext ~file:vo.target ~newext:".v"]) in
  (* We explicitly include the location of coqlib to avoid tricky issues with coqlib location *)
  let libflag = "-coqlib %{project_root}" in
  (* The final build rule *)
  let action = sprintf "(chdir %%{project_root} (run coqc -q %s %s %s %s))" libflag eflag cflag source in
  let all_targets = gen_coqc_targets vo in
  pp_rule fmt all_targets deps action

let pp_mlg_dep _dir fmt ml =
  let target = Filename.(remove_extension ml) ^ ".ml" in
  let mlg_rule = "(run coqpp %{pp-file})" in
  pp_rule fmt [target] [ml] mlg_rule

let pp_dep dir fmt oo = match oo with
  | VO vo -> pp_vo_dep dir fmt vo
  | MLG f -> pp_mlg_dep dir fmt f

let out_install fmt dir ff =
  let itarget = String.concat "/" dir in
  let ff = List.concat @@ pmap (function | VO vo -> Some (gen_coqc_targets vo) | _ -> None) ff in
  let pp_ispec fmt tg = fprintf fmt "(%s as coq/%s)" tg (bpath [itarget;tg]) in
  fprintf fmt "(install@\n @[(section lib_root)@\n(package coq)@\n(files @[%a@])@])@\n"
    (pp_list pp_ispec sep) ff

(* For each directory, we must record two things, the build rules and
   the install specification. *)
let record_dune d ff =
  let sd = bpath d in
  if Sys.file_exists sd && Sys.is_directory sd then
    let out = open_out (bpath [sd;"dune"]) in
    let fmt = formatter_of_out_channel out in
    if List.nth d 0 = "plugins" then
      fprintf fmt "(include plugin_base.dune)@\n";
    out_install fmt d ff;
    List.iter (pp_dep d fmt) ff;
    fprintf fmt "%!";
    close_out out
  else
    eprintf "error in coq_dune, a directory disappeared: %s@\n%!" sd

(* File Scanning *)
let scan_mlg m d =
  let dir = ["plugins"; d] in
  let m = DirMap.add dir [] m in
  let mlg = Sys.(List.filter (fun f -> Filename.(check_suffix f ".mlg"))
                   Array.(to_list @@ readdir (bpath dir))) in
  List.fold_left (fun m f -> add_map_list ["plugins"; d] (MLG f) m) m mlg

let scan_plugins m =
  let is_plugin_directory dir = Sys.(is_directory dir && file_exists (bpath [dir;"plugin_base.dune"])) in
  let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath ["plugins";f]) Array.(to_list @@ readdir "plugins")) in
  List.fold_left scan_mlg m dirs

(* This will be removed when we drop support for Make *)
let fix_cmo_cma file =
  if String.equal Filename.(extension file) ".cmo"
  then replace_ext ~file ~newext:".cma"
  else file

(* Process .vfiles.d and generate a skeleton for the dune file *)
let parse_coqdep_line l =
  match Str.(split (regexp ":") l) with
  | [targets;deps] ->
    let targets = Str.(split (regexp "[ \t]+") targets) in
    let deps    = Str.(split (regexp "[ \t]+") deps)    in
    let targets = filter_no_vo targets in
    begin match targets with
    | [target] ->
      let dir, target = Filename.(dirname target, basename target) in
      (* coqdep outputs with the '/' directory separator regardless of
         the platform. Anyways, I hope we can link to coqdep instead
         of having to parse its output soon, that should solve this
         kind of issues *)
      let deps = List.map fix_cmo_cma deps in
      Some (String.split_on_char '/' dir, VO { target; deps; })
    (* Otherwise a vio file, we ignore *)
    | _ -> None
    end
  (* Strange rule, we ignore *)
  | _ -> None

let rec read_vfiles ic map =
  try
    let rule = parse_coqdep_line (input_line ic) in
    (* Add vo_entry to its corresponding map entry *)
    let map = option_cata map (fun (dir, vo) -> add_map_list dir vo map) rule in
    read_vfiles ic map
  with End_of_file -> map

let out_map map =
  DirMap.iter record_dune map

let exec_ifile f =
  match Array.length Sys.argv with
  | 1 -> f stdin
  | 2 ->
    let in_file = Sys.argv.(1) in
    begin try
      let ic = open_in in_file in
      (try f ic
       with _ -> eprintf "Error: exec_ifile@\n%!"; close_in ic)
      with _ -> eprintf "Error: cannot open input file %s@\n%!" in_file
    end
  | _ -> eprintf "Error: wrong number of arguments@\n%!"; exit 1

let _ =
  exec_ifile (fun ic ->
      let map = scan_plugins DirMap.empty in
      let map = read_vfiles ic map in
      out_map map)

¤ Dauer der Verarbeitung: 0.17 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.