From c5caafdaf91924f38cc38854fde078e721308a8d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 1 Apr 2019 13:29:33 +0200 Subject: [PATCH] [wip] [coq] Allow dependencies and composition with local Coq libraries. We support simple composition of Coq libraries using the `(theories ...)` field. This is a work-in-progress and I am submitting to gather feedback; in particular: - Attention: I ignore what is the right way to handle paths for depending libraries. I am using `Path.drop_build_context` however that doesn't feel very clear. - Todo Before Merge: + tests + Error handling. + validation of library names must be adapted to Coq's conventions. - Would be nice to have / next PRs: + Closure of theory dependencies. + Allow to depend on libraries installed globally. Signed-off-by: Emilio Jesus Gallego Arias --- doc/coq.rst | 21 ++++++++--- src/coq_lib.ml | 48 +++++++++++++++++++++++++ src/coq_lib.mli | 27 ++++++++++++++ src/coq_rules.ml | 83 ++++++++++++++++++++++++++++---------------- src/dune_file.ml | 13 ++++++- src/dune_file.mli | 3 ++ src/scope.ml | 14 +++++--- src/scope.mli | 2 ++ src/super_context.ml | 10 ++++++ 9 files changed, 183 insertions(+), 38 deletions(-) create mode 100644 src/coq_lib.ml create mode 100644 src/coq_lib.mli diff --git a/doc/coq.rst b/doc/coq.rst index c7097ed161de..896f09e2705b 100644 --- a/doc/coq.rst +++ b/doc/coq.rst @@ -8,7 +8,8 @@ Dune is also able to build Coq developments. A Coq project is a mix of Coq ``.v`` files and (optionally) OCaml libraries linking to the Coq API (in which case we say the project is a *Coq plugin*). To enable Coq support in a dune project, the language version should be selected -in the ``dune-project`` file. For example: +in the ``dune-project`` file. As of today, the only version supported +is ``0.1`` and is experimental: .. code:: scheme @@ -32,11 +33,12 @@ The basic form for defining Coq libraries is very similar to the OCaml form: (synopsis ) (modules ) (libraries ) + (theories ) (flags )) The stanza will build all `.v` files on the given directory. The semantics of fields is: -- ``>`` will be used as the default Coq library prefix ``-R``, +- ```` will be used as the default Coq library prefix ``-R``, - the ``modules`` field does allow to constraint the set of modules included in the library, similarly to its OCaml counterpart, - ``public_name`` will make Dune generate install rules for the `.vo` @@ -47,7 +49,10 @@ The stanza will build all `.v` files on the given directory. The semantics of fi - ```` will be passed to ``coqc``, - the path to installed locations of ```` will be passed to ``coqdep`` and ``coqc`` using Coq's ``-I`` flag; this allows for a Coq - library to depend on a ML plugin. + library to depend on a ML plugin, +- you can depend on in-tree ````, in this case, Dune + will pass to Coq the the corresponding `-Q` flag for the libraries + and their dependencies. Recursive Qualification of Modules ================================== @@ -62,9 +67,17 @@ to a ``dune`` file, Dune will to consider that all the modules in their directory and sub-directories, adding a prefix to the module name in the usual Coq style for sub-directories. For example, file ``A/b/C.v`` will be module ``A.b.C``. +Composition of Coq libraries +============================ + +For local Coq libraries, composition is possible using the +``theories`` field. Libraries are wrapped, however for their own +compilation the scope is opened so qualification is not necessary. + +TODO: "rules about prefix shadowing" + Limitations =========== -- composition and scoping of Coq libraries is still not possible. For now, libraries are located using Coq's built-in library management, - .v always depend on the native version of a plugin, - a ``foo.mlpack`` file must the present for locally defined plugins to work, this is a limitation of coqdep, diff --git a/src/coq_lib.ml b/src/coq_lib.ml new file mode 100644 index 000000000000..71617289e591 --- /dev/null +++ b/src/coq_lib.ml @@ -0,0 +1,48 @@ +(* This file is licensed under The MIT License *) +(* (c) MINES ParisTech 2018-2019 *) +(* Written by: Emilio Jesús Gallego Arias *) + +open! Stdune + +type t = + { name : Lib_name.t + ; src_dir : Path.t + ; obj_dir : Path.t + ; package : Package.Name.t option + } + +let name l = l.name +let src_dir l = l.src_dir +let obj_dir l = l.obj_dir +let package l = l.package + +module DB = struct + + type lib = t + type t = lib Lib_name.Map.t + + let create_from_stanza (dir, s : Path.t * Dune_file.Coq.t) = + let name = Dune_file.Coq.best_name s in + name, + { name + ; obj_dir = dir + ; src_dir = dir + ; package = Option.map s.public ~f:(fun p -> p.package.name) + } + + (* XXX: Error handling: register errors and printers *) + let create_from_coqlib_stanzas sl = + match Lib_name.Map.of_list_map ~f:create_from_stanza sl with + | Ok m -> m + | Error (name, _w1, w2) -> + let loc = (snd w2).loc in + raise (Errors.exnf loc "Duplicate lib name: %a" Lib_name.pp name) + + let resolve db (loc,name) = + match Lib_name.Map.find db name with + | None -> + Error (Errors.exnf loc "Theory %a not found" Lib_name.pp name) + | Some s -> Ok s + + +end diff --git a/src/coq_lib.mli b/src/coq_lib.mli new file mode 100644 index 000000000000..307cd7516f70 --- /dev/null +++ b/src/coq_lib.mli @@ -0,0 +1,27 @@ +(* This file is licensed under The MIT License *) +(* (c) MINES ParisTech 2018-2019 *) +(* Written by: Emilio Jesús Gallego Arias *) + +open! Stdune + +type t + +val name : t -> Lib_name.t + +val src_dir : t -> Path.t +val obj_dir : t -> Path.t + +val package : t -> Package.Name.t option + +module DB : sig + + type lib = t + type t + + val create_from_coqlib_stanzas + : (Path.t * Dune_file.Coq.t) list + -> t + + val resolve : t -> Loc.t * Lib_name.t -> lib Or_exn.t + +end diff --git a/src/coq_rules.ml b/src/coq_rules.ml index e85272f65251..a55641f2a610 100644 --- a/src/coq_rules.ml +++ b/src/coq_rules.ml @@ -26,7 +26,7 @@ type coq_context = ; coqpp : Action.program } -let parse_coqdep ~coq_module (lines : string list) = +let parse_coqdep ~src_dir ~coq_module (lines : string list) = if coq_debug then Format.eprintf "Parsing coqdep @\n%!"; let source = Coq_module.source coq_module in let invalid p = @@ -45,8 +45,8 @@ let parse_coqdep ~coq_module (lines : string list) = | Some (basename,deps) -> let ff = List.hd @@ String.extract_blank_separated_words basename in let depname, _ = Filename.split_extension ff in - let modname = - Coq_module.(String.concat ~sep:"/" (prefix coq_module @ [name coq_module])) in + let modname = String.concat ~sep:"/" Coq_module.(prefix coq_module @ [name coq_module]) in + let modname = Path.(to_string (relative src_dir modname)) in if coq_debug then Format.eprintf "depname / modname: %s / %s@\n%!" depname modname; if depname <> modname then invalid "basename"; @@ -55,8 +55,13 @@ let parse_coqdep ~coq_module (lines : string list) = then Format.eprintf "deps for %a: %a@\n%!" Path.pp source Fmt.(list text) deps; deps -let setup_rule ~expander ~dir ~cc ~source_rule ~wrapper_name - ~coq_flags ~ml_iflags ~mlpack_rule coq_module = +let setup_theory_flag lib = + let wrapper = Lib_name.to_string (Coq_lib.name lib) in + let dir = Path.drop_build_context_exn (Coq_lib.src_dir lib) in + ["-Q"; Path.to_string dir; wrapper] + +let setup_rule ~expander ~base_dir ~dir ~cc ~source_rule ~wrapper_name + ~coq_flags ~theories_libs ~ml_iflags ~mlpack_rule coq_module = if coq_debug then Format.eprintf "gen_rule coq_module: %a@\n%!" Coq_module.pp coq_module; @@ -66,7 +71,9 @@ let setup_rule ~expander ~dir ~cc ~source_rule ~wrapper_name let stdout_to = Coq_module.obj_file ~obj_dir ~ext:".v.d" coq_module in let object_to = Coq_module.obj_file ~obj_dir ~ext:".vo" coq_module in - let iflags = Arg_spec.As ["-R"; "."; wrapper_name] in + let src_dir = Path.drop_build_context_exn dir in + let th_flags = List.concat_map theories_libs ~f:setup_theory_flag in + let iflags = Arg_spec.As (["-R"; Path.to_string src_dir; wrapper_name] @ th_flags) in let cd_arg : (string list, _) Arg_spec.t list = Arg_spec.[ As ["-dyndep"; "opt"]; iflags; ml_iflags; Dep source ] in @@ -75,14 +82,14 @@ let setup_rule ~expander ~dir ~cc ~source_rule ~wrapper_name (* This is weird stuff in order to adapt the rule so we can reuse ml_iflags :( I wish we had more flexible typing. *) ((fun () -> []) ^>> source_rule &&& mlpack_rule) >>^ fst >>> - Build.run ~dir ~stdout_to cc.coqdep cd_arg + Build.run ~dir:base_dir ~stdout_to cc.coqdep cd_arg in (* Process coqdep and generate rules *) let deps_of = Build.dyn_paths ( Build.lines_of stdout_to >>^ - parse_coqdep ~coq_module >>^ - List.map ~f:(Path.relative dir) + parse_coqdep ~src_dir ~coq_module >>^ + List.map ~f:(Path.relative base_dir) ) in let cc_arg = Arg_spec.[ @@ -96,7 +103,7 @@ let setup_rule ~expander ~dir ~cc ~source_rule ~wrapper_name [coqdep_rule; deps_of >>> Expander.expand_and_eval_set expander coq_flags ~standard:(Build.return []) >>> - Build.run ~dir cc.coqc (Dyn (fun flags -> As flags) :: cc_arg) + Build.run ~dir:base_dir cc.coqc (Dyn (fun flags -> As flags) :: cc_arg) ] (* TODO: remove; rgrinberg points out: @@ -112,14 +119,16 @@ let create_ccoq sctx ~dir = } (* get_libraries from Coq's ML dependencies *) -let libs_of_coq_deps ~loc ~scope libs = +let libs_of_coq_deps ~scope libs = let lib_db = Scope.libs scope in - List.concat_map ~f:Dune_file.Lib_dep.to_lib_names libs - |> Lib.DB.find_many ~loc lib_db + List.map ~f:(fun lib_dep -> + Dune_file.Lib_dep.get_loc lib_dep, + Dune_file.Lib_dep.to_lib_names lib_dep) libs + |> Result.List.concat_map ~f:(fun (loc, ln) -> Lib.DB.find_many ~loc lib_db ln) |> Result.ok_exn (* compute include flags and mlpack rules *) -let setup_ml_deps ~scope ~loc libs = +let setup_ml_deps ~scope libs = (* coqdep expects an mlpack file next to the sources otherwise it * will omit the cmxs deps *) @@ -134,7 +143,7 @@ let setup_ml_deps ~scope ~loc libs = (* Pair of include flags and paths to mlpack *) let ml_iflags, mlpack = - let libs = libs_of_coq_deps ~loc ~scope libs in + let libs = libs_of_coq_deps ~scope libs in Util.include_flags libs, List.concat_map ~f:ml_pack_files libs in @@ -144,40 +153,56 @@ let setup_ml_deps ~scope ~loc libs = let coqlib_wrapper_name (s : Dune_file.Coq.t) = Lib_name.Local.to_string (snd s.name) -let setup_rules ~sctx ~dir ~dir_contents (s : Dune_file.Coq.t) = +let coq_modules_of_dep ~sctx lib = + let name = Coq_lib.name lib in + let dir = Coq_lib.src_dir lib in + let dir_contents = Dir_contents.get_without_rules sctx ~dir in + Dir_contents.coq_modules_of_library dir_contents ~name - let scope = SC.find_scope_by_dir sctx dir in +let coq_theories_of_lib_deps ~lib_db = + List.concat_map ~f:(fun lib_dep -> + let loc = Dune_file.Lib_dep.get_loc lib_dep in + Dune_file.Lib_dep.to_lib_names lib_dep + |> List.map ~f:(fun name -> Result.ok_exn (Coq_lib.DB.resolve lib_db (loc, name)))) - if coq_debug then begin - let scope = SC.find_scope_by_dir sctx dir in - Format.eprintf "[gen_rules] @[dir: %a@\nscope: %a@]@\n%!" - Path.pp dir Path.pp (Scope.root scope) - end; +let setup_rules ~sctx ~dir ~dir_contents (s : Dune_file.Coq.t) = let cc = create_ccoq sctx ~dir in + let scope = SC.find_scope_by_dir sctx dir in + let lib_db = Scope.coq_libs scope in + let name = Dune_file.Coq.best_name s in + let coq_modules = Dir_contents.coq_modules_of_library dir_contents ~name in + let theories_libs = coq_theories_of_lib_deps ~lib_db s.theories in + let theories_modules = + List.concat_map theories_libs ~f:(coq_modules_of_dep ~sctx) in + (* coqdep requires all the files to be in the tree to produce correct - dependencies *) - let source_rule = Build.paths (List.map ~f:Coq_module.source coq_modules) in + dependencies, including those of dependencies *) + let source_rule = + List.map ~f:Coq_module.source theories_modules + |> List.rev_append (List.map ~f:Coq_module.source coq_modules) + |> Build.paths in + let coq_flags = s.flags in let expander = SC.expander sctx ~dir in let wrapper_name = coqlib_wrapper_name s in - let ml_iflags, mlpack_rule = - setup_ml_deps ~scope ~loc:s.loc s.libraries in + let ml_iflags, mlpack_rule = setup_ml_deps ~scope s.libraries in + let base_dir = Scope.root scope in let coq_rules = List.concat_map - ~f:(setup_rule ~expander ~dir ~cc ~source_rule ~wrapper_name ~coq_flags - ~ml_iflags ~mlpack_rule) coq_modules in + ~f:(setup_rule ~expander ~base_dir ~dir ~cc ~source_rule ~wrapper_name ~coq_flags + ~theories_libs ~ml_iflags ~mlpack_rule) coq_modules in coq_rules (* This is here for compatibility with Coq < 8.11, which expects plugin files to be in the folder containing the `.vo` files *) let coq_plugins_install_rules ~scope ~package ~dst_dir (s : Dune_file.Coq.t) = - let ml_libs = libs_of_coq_deps ~scope ~loc:s.loc s.libraries in + let ml_libs = libs_of_coq_deps ~scope s.libraries in let rules_for_lib lib = (* Don't install libraries that don't belong to this package *) if Option.equal Package.Name.equal diff --git a/src/dune_file.ml b/src/dune_file.ml index b98476028ee4..088da6bfc40a 100644 --- a/src/dune_file.ml +++ b/src/dune_file.ml @@ -509,6 +509,11 @@ module Lib_dep = struct let direct x = Direct x let of_lib_name (loc, pp) = Direct (loc, pp) + + let get_loc = function + | Direct (loc,_) -> loc + | Select s -> s.loc + end module Lib_deps = struct @@ -1823,6 +1828,8 @@ module Coq = struct ; flags : Ordered_set_lang.Unexpanded.t ; libraries : Lib_dep.t list (** ocaml libraries *) + ; theories : Lib_dep.t list + (** coq libraries *) ; loc : Loc.t ; enabled_if : Blang.t } @@ -1842,11 +1849,14 @@ module Coq = struct and+ flags = field_oslu "flags" and+ modules = modules_field "modules" and+ libraries = field "libraries" Lib_deps.decode ~default:[] + and+ theories = field "theories" Lib_deps.decode ~default:[] and+ enabled_if = enabled_if in let name = let (loc, res) = name in - (loc, Lib_name.Local.validate (loc, res) ~wrapped:None) + match res with + | Ok t | Warn t -> (loc, t) + | Invalid -> Errors.fail loc "%s" Lib_name.Local.invalid_message in { name ; public @@ -1854,6 +1864,7 @@ module Coq = struct ; modules ; flags ; libraries + ; theories ; loc ; enabled_if }) diff --git a/src/dune_file.mli b/src/dune_file.mli index 8b0222c0570d..31f6034d3af9 100644 --- a/src/dune_file.mli +++ b/src/dune_file.mli @@ -78,6 +78,7 @@ module Lib_dep : sig val to_lib_names : t -> Lib_name.t list val direct : Loc.t * Lib_name.t -> t val of_lib_name : Loc.t * Lib_name.t -> t + val get_loc : t -> Loc.t end module Lib_deps : sig @@ -363,6 +364,8 @@ module Coq : sig ; flags : Ordered_set_lang.Unexpanded.t ; libraries : Lib_dep.t list (** ocaml libraries *) + ; theories : Lib_dep.t list + (** coq libraries *) ; loc : Loc.t ; enabled_if : Blang.t } diff --git a/src/scope.ml b/src/scope.ml index 95dfd8efad8a..6bb3e1747a8d 100644 --- a/src/scope.ml +++ b/src/scope.ml @@ -4,6 +4,7 @@ open Import type t = { project : Dune_project.t ; db : Lib.DB.t + ; coq_db : Coq_lib.DB.t ; root : Path.t (* Path inside the build directory *) } @@ -11,6 +12,7 @@ let root t = t.root let name t = Dune_project.name t.project let project t = t.project let libs t = t.db +let coq_libs t = t.coq_db module DB = struct type scope = t @@ -101,7 +103,7 @@ module DB = struct ~all:(fun () -> Lib_name.Map.keys public_libs) let sccopes_by_name ~context ~projects ~lib_config ~public_libs - internal_libs = + internal_libs coq_internal_libs = let build_context_dir = Path.relative Path.build_dir context in let projects_by_name = List.map projects ~f:(fun (project : Dune_project.t) -> @@ -130,15 +132,19 @@ module DB = struct let libs = Option.value libs ~default:[] in let db = Lib.DB.create_from_library_stanzas libs ~parent:public_libs ~lib_config in + let coq_db = + Coq_lib.DB.create_from_coqlib_stanzas coq_internal_libs in let root = Path.append_local build_context_dir (Dune_project.root project) in - Some { project; db; root }) + Some { project; db; coq_db; root }) - let create ~projects ~context ~installed_libs ~lib_config internal_libs = + let create ~projects ~context ~installed_libs ~lib_config + internal_libs coq_internal_libs = let t = Fdecl.create () in let public_libs = public_libs t ~installed_libs internal_libs in let by_name = - sccopes_by_name ~context ~projects ~lib_config ~public_libs internal_libs + sccopes_by_name ~context ~projects ~lib_config ~public_libs + internal_libs coq_internal_libs in let by_dir = Dune_project.Name.Map.values by_name diff --git a/src/scope.mli b/src/scope.mli index 5267c05ad546..d938e5349468 100644 --- a/src/scope.mli +++ b/src/scope.mli @@ -12,6 +12,7 @@ val project : t -> Dune_project.t (** Return the library database associated to this scope *) val libs : t -> Lib.DB.t +val coq_libs : t -> Coq_lib.DB.t (** Scope databases *) module DB : sig @@ -27,6 +28,7 @@ module DB : sig -> installed_libs:Lib.DB.t -> lib_config:Lib_config.t -> (Path.t * Dune_file.Library.t) list + -> (Path.t * Dune_file.Coq.t) list -> t * Lib.DB.t val find_by_dir : t -> Path.t -> scope diff --git a/src/super_context.ml b/src/super_context.ml index d0b2770e35bc..58a6eaa2c878 100644 --- a/src/super_context.ml +++ b/src/super_context.ml @@ -296,6 +296,15 @@ let create | Library lib -> Some (ctx_dir, lib) | _ -> None)) in + let internal_coq_libs = + List.concat_map stanzas + ~f:(fun { Dune_load.Dune_file. dir; stanzas; project = _ ; kind = _ } -> + let ctx_dir = Path.append context.build_dir dir in + List.filter_map stanzas ~f:(fun stanza -> + match (stanza : Stanza.t) with + | Coq.T coq_lib -> Some (ctx_dir, coq_lib) + | _ -> None)) + in let scopes, public_libs = let lib_config = Context.lib_config context in Scope.DB.create @@ -304,6 +313,7 @@ let create ~installed_libs ~lib_config internal_libs + internal_coq_libs in let stanzas = List.map stanzas