From 920723ab4c1707c0a98c978cdd7742d47e58582f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 24 May 2018 03:52:06 +0200 Subject: [build] Preliminary support for building Coq with `dune`. [Dune](https://github.com/ocaml/dune) is a compositional declarative build system for OCaml. It provides automatic generation of `version.ml`, `.merlin`, `META`, `opam`, API documentation; install management; easy integration with external libraries, test runners, and modular builds. In particular, Dune uniformly handles components regardless whether they live in, or out-of-tree. This greatly simplifies cases where a plugin [or CoqIde] is checked out in the current working copy but then distributed separately [and vice-versa]. Dune can thus be used as a more flexible `coq_makefile` replacement. For now we provide experimental support for a Dune build. In order to build Coq + the standard library with Dune type: ``` $ make -f Makefile.dune world ``` This PR includes a preliminary, developer-only preview of Dune for Coq. There is still ongoing work, see https://github.com/coq/coq/issues/8052 for tracking status towards full support. ## Technical description. Dune works out of the box with Coq, once we have fixed some modularity issues. The main remaining challenge was to support `.vo` files. As Dune doesn't support custom build rules yet, to properly build `.vo` files we provide a small helper script `tools/coq_dune.ml`. The script will scan the Coq library directories and generate the corresponding rules for `.v -> .vo` and `.ml4 -> .ml` builds. The script uses `coqdep` as to correctly output the dependencies of `.v` files. `coq_dune` is akin to `coq_makefile` and should be able to be used to build Coq projects in the future. Due to this pitfall, the build process has to proceed in three stages: 1) build `coqdep` and `coq_dune`; 2) generate `dune` files for `theories` and `plugins`; 3) perform a regular build with all targets are in scope. ## FAQ ### Why Dune? Coq has a moderately complex build system and it is not a secret that many developer-hours have been spent fighting with `make`. In particular, the current `make`-based system does offer poor support to verify that the current build rules and variables are coherent, and requires significant manual, error-prone. Many variables must be passed by hand, duplicated, etc... Additionally, our make system offers poor integration with now standard OCaml ecosystem tools such as `opam`, `ocamlfind` or `odoc`. Another critical point is build compositionality. Coq is rich in 3rd party contributions, and a big shortcoming of the current make system is that it cannot be used to build these projects; requiring us to maintain a custom tool, `coq_makefile`, with the corresponding cost. In the past, there has been some efforts to migrate Coq to more specialized build systems, however these stalled due to a variety of reasons. Dune, is a declarative, OCaml-specific build tool that is on the path to become the standard build system for the OCaml ecosystem. Dune seems to be a good fit for Coq well: it is well-supported, fast, compositional, and designed for large projects. ### Does Dune replace the make-based build system? The current, make-based build system is unmodified by this PR and kept as the default option. However, Dune has the potential ### Is this PR complete? What does it provide? This PR is ready for developer preview and feedback. The build system is functional, however, more work is necessary in order to make Dune the default for Coq. The main TODOs are tracked at https://github.com/coq/coq/issues/8052 This PR allows developers to use most of the features of Dune today: - Modular organization of the codebase; each component is built only against declared dependencies so components are checked for containment more strictly. - Hygienic builds; Dune places all artifacts under `_build`. - Automatic generation of `.install` files, simplified OPAM workflow. - `utop` support, `-opaque` in developer mode, etc... - `ml4` files are handled using `coqp5`, a native-code customized camlp5 executable which brings much faster `ml4 -> ml` processing. ### What dependencies does Dune require? Dune doesn't depend on any 3rd party package other than the OCaml compiler. ### Some Benchs: ``` $ /usr/bin/time make DUNEOPT="-j 1000" -f Makefile.dune states 59.50user 18.81system 0:29.83elapsed 262%CPU (0avgtext+0avgdata 302996maxresident)k 0inputs+646632outputs (0major+4893811minor)pagefaults 0swaps $ /usr/bin/time sh -c "./configure -local -native-compiler no && make -j states" 88.21user 23.65system 0:32.96elapsed 339%CPU (0avgtext+0avgdata 304992maxresident)k 0inputs+1051680outputs (0major+5300680minor)pagefaults 0swaps ``` --- tools/coq_dune.ml | 283 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ tools/dune | 31 ++++++ 2 files changed, 314 insertions(+) create mode 100644 tools/coq_dune.ml create mode 100644 tools/dune (limited to 'tools') 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 *) +(* 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/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)) -- cgit v1.2.3