diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 8 | ||||
| -rw-r--r-- | tools/coq_dune.ml | 283 | ||||
| -rw-r--r-- | tools/coq_makefile.ml | 34 | ||||
| -rw-r--r-- | tools/coqdoc/index.ml | 14 | ||||
| -rw-r--r-- | tools/dune | 31 |
5 files changed, 340 insertions, 30 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 8b6822a4ed..403ad61798 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -343,19 +343,19 @@ make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: print-pretty-timed:: $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) print-pretty-timed-diff:: - $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) ifeq (,$(BEFORE)) print-pretty-single-time-diff:: - @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' $(HIDE)false else ifeq (,$(AFTER)) print-pretty-single-time-diff:: - @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' $(HIDE)false else print-pretty-single-time-diff:: - $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) endif endif pretty-timed: diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml new file mode 100644 index 0000000000..c89c78c8ec --- /dev/null +++ b/tools/coq_dune.ml @@ -0,0 +1,283 @@ +(************************************************************************) +(* * 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 "@;" + + 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 *) + module Legacy = struct + + (* 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 + + (* Available in OCaml >= 4.04 *) + let split_on_char sep s = + let open String in + let r = ref [] in + let j = ref (length s) in + for i = length s - 1 downto 0 do + if unsafe_get s i = sep then begin + r := sub s (i + 1) (!j - i - 1) :: !r; + j := i + end + done; + sub s 0 !j :: !r + 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 + +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"; } + ] + + 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 | ML4 of string | 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 *) + +(* 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 + +let gen_sub n = + (* Move to List.init once we can depend on OCaml >= 4.06.0 *) + String.concat "/" (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 + +(* 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 "", ["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 -> sdir ^ s) (edep @ vo.deps) in + (* The source file is also corrected as we will call coqtop from the top dir *) + let source = String.concat "/" dir ^ "/" ^ Filename.(remove_extension vo.target) ^ ".v" in + (* The final build rule *) + let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s -compile %s))" eflag cflag source in + pp_rule fmt [vo.target] deps action + +let pp_ml4_dep _dir fmt ml = + let target = Filename.(remove_extension ml) ^ ".ml" in + let ml4_rule = "(run coqp5 -loc loc -impl %{pp-file} -o %{targets})" in + pp_rule fmt [target] [ml] ml4_rule + +let pp_mlg_dep _dir fmt ml = + let target = Filename.(remove_extension ml) ^ ".ml" in + let ml4_rule = "(run coqpp %{pp-file})" in + pp_rule fmt [target] [ml] ml4_rule + +let pp_dep dir fmt oo = match oo with + | VO vo -> pp_vo_dep dir fmt vo + | ML4 f -> pp_ml4_dep dir fmt f + | MLG f -> pp_mlg_dep dir fmt f + +let out_install fmt dir ff = + let itarget = String.concat "/" dir in + let ff = pmap (function | VO vo -> Some vo.target | _ -> None) ff in + let pp_ispec fmt tg = fprintf fmt "(%s as %s)" tg (itarget^"/"^tg) in + fprintf fmt "(install@\n @[(section lib)@\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 = String.concat "/" d in + if Sys.file_exists sd && Sys.is_directory sd then + let out = open_out (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 choose_ml4g_form f = + if Filename.check_suffix f ".ml4" then ML4 f + else MLG f + +let scan_mlg4 m d = + let dir = ["plugins"; d] in + let m = DirMap.add dir [] m in + let ml4 = Sys.(List.filter (fun f -> Filename.(check_suffix f ".ml4" || check_suffix f ".mlg")) + Array.(to_list @@ readdir String.(concat "/" dir))) in + List.fold_left (fun m f -> add_map_list ["plugins"; d] (choose_ml4g_form f) m) m ml4 + +let scan_plugins m = + let dirs = Sys.(List.filter (fun f -> is_directory @@ "plugins/"^f) Array.(to_list @@ readdir "plugins/")) in + List.fold_left scan_mlg4 m dirs + +(* 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 + Some (Legacy.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 ic = open_in Sys.argv.(1) in + (try f ic with _ -> close_in ic) + | _ -> 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) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index ad489da822..c3bdf656d1 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -31,8 +31,19 @@ let rec print_prefix_list sep = function | x :: l -> print sep; print x; print_prefix_list sep l | [] -> () -let usage_common () = +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 file that describes a Objective Caml\ @@ -61,25 +72,6 @@ let usage_common () = \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.\ @@ -405,7 +397,7 @@ let _ = let project = try cmdline_args_to_project ~curdir:Filename.current_dir_name args - with Parsing_error s -> prerr_endline s; usage_coq_project () in + with Parsing_error s -> prerr_endline s; usage_coq_makefile () in if only_destination <> None then begin destination_of project (Option.get only_destination); diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index 885324aa02..724d3838b0 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -185,7 +185,8 @@ let type_name = function let prepare_entry s = function | Notation -> (* We decode the encoding done in Dumpglob.cook_notation of coqtop *) - (* Encoded notations have the form section:sc:x_'++'_x where: *) + (* Encoded notations have the form section:entry:sc:x_'++'_x *) + (* where: *) (* - the section, if any, ends with a "." *) (* - the scope can be empty *) (* - tokens are separated with "_" *) @@ -202,10 +203,12 @@ let prepare_entry s = function let err () = eprintf "Invalid notation in globalization file\n"; exit 1 in let h = try String.index_from s 0 ':' with _ -> err () in let i = try String.index_from s (h+1) ':' with _ -> err () in - let sc = String.sub s (h+1) (i-h-1) in - let ntn = Bytes.make (String.length s - i) ' ' in + let m = try String.index_from s (i+1) ':' with _ -> err () in + let entry = String.sub s (h+1) (i-h-1) in + let sc = String.sub s (i+1) (m-i-1) in + let ntn = Bytes.make (String.length s - m) ' ' in let k = ref 0 in - let j = ref (i+1) in + let j = ref (m+1) in let quoted = ref false in let l = String.length s - 1 in while !j <= l do @@ -227,7 +230,8 @@ let prepare_entry s = function incr j done; let ntn = Bytes.sub_string ntn 0 !k in - if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")" + let ntn = if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")" in + if entry = "" then ntn else entry ^ ":" ^ ntn | _ -> s diff --git a/tools/dune b/tools/dune new file mode 100644 index 0000000000..2ba0e3fe8a --- /dev/null +++ b/tools/dune @@ -0,0 +1,31 @@ +(executable + (name coqc) + (public_name coqc) + (modules coqc) + (libraries coq.toplevel)) + +(executable + (name coq_makefile) + (public_name coq_makefile) + (modules coq_makefile) + (libraries coq.lib)) + +(executable + (name coqdep) + (public_name coqdep) + (modules coqdep_lexer coqdep_common coqdep) + (libraries coq.lib)) + +(ocamllex coqdep_lexer) + +(executable + (name coq_tex) + (public_name coq_tex) + (modules coq_tex) + (libraries str)) + +(executable + (name coq_dune) + (public_name coq_dune) + (modules coq_dune) + (libraries str)) |