From 9cd1918654b338cb8a229c6ee2f7def8bf8796b0 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 12 Apr 2019 04:32:46 +0200 Subject: [PATCH] [coq] Add coq.pp preprocessing stanza. We add a ``` (coq.pp (modules foo bar)) ```` stanza, that will look for a `foo.mlg` file and produce a pre-processed `foo.ml`; similarly for `bar`. This helps Coq plugin writers to avoid boilerplate and more importantly, to get the right path on error messages. Signed-off-by: Emilio Jesus Gallego Arias --- CHANGES.md | 6 +++++ doc/coq.rst | 20 ++++++++++++++++ src/coq_rules.ml | 14 +++++++++++ src/coq_rules.mli | 6 +++++ src/dir_contents.ml | 6 ++--- src/dune_file.ml | 24 ++++++++++++++++++- src/dune_file.mli | 10 ++++++++ src/gen_rules.ml | 4 ++++ src/stdune/path.ml | 4 ++-- .../test-cases/coq/ml_lib/src/dune | 3 +++ .../test-cases/coq/ml_lib/src/gram.mlg | 9 +++++++ .../test-cases/coq/ml_lib/src/gram.mli | 1 + test/blackbox-tests/test-cases/coq/run.t | 6 +++++ 13 files changed, 106 insertions(+), 7 deletions(-) create mode 100644 test/blackbox-tests/test-cases/coq/ml_lib/src/gram.mlg create mode 100644 test/blackbox-tests/test-cases/coq/ml_lib/src/gram.mli diff --git a/CHANGES.md b/CHANGES.md index 0b1346486c8..1835da3d001 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,9 @@ +unreleased +---------- + +- [coq] Add `coq.pp` stanza to help with pre-processing of grammar + files (#2054, @ejgallego, review by @rgrinberg) + 1.9.1 (11/04/2019) ------------------ diff --git a/doc/coq.rst b/doc/coq.rst index c7097ed161d..6f9c8834004 100644 --- a/doc/coq.rst +++ b/doc/coq.rst @@ -49,6 +49,26 @@ The stanza will build all `.v` files on the given directory. The semantics of fi ``coqdep`` and ``coqc`` using Coq's ``-I`` flag; this allows for a Coq library to depend on a ML plugin. +Preprocessing with ``coqpp`` +============================ + +Coq plugin writers usually need to write ``.mlg`` files to extend Coq +grammar. Such files are pre-processed with `coqpp`; to help plugin +writers avoid boilerplate we provide a `(coqpp ...)` stanza: + +.. code:: scheme + + (coq.pp (modules )) + +which for each ``g_mod`` in `````is equivalent to: + +.. code:: scheme + + (rule + (targets g_mod.ml) + (deps (:mlg-file g_mod.mlg)) + (action (run coqpp %{mlg-file}))) + Recursive Qualification of Modules ================================== diff --git a/src/coq_rules.ml b/src/coq_rules.ml index e85272f6525..cecb2dbe2bb 100644 --- a/src/coq_rules.ml +++ b/src/coq_rules.ml @@ -211,3 +211,17 @@ let install_rules ~sctx ~dir s = let dst = Path.to_string dst in None, Install.(Entry.make Section.Lib_root ~dst vofile)) |> List.rev_append (coq_plugins_install_rules ~scope ~package ~dst_dir s) + +let coqpp_rules ~sctx ~dir (s : Dune_file.Coqpp.t) = + + let scope = SC.find_scope_by_dir sctx dir in + let base_dir = Scope.root scope in + let cc = create_ccoq sctx ~dir in + + let mlg_rule m = + let source = Path.relative dir (m ^ ".mlg") in + let target = Path.relative dir (m ^ ".ml") in + let args = Arg_spec.[Dep source; Hidden_targets [target]] in + Build.run ~dir:base_dir cc.coqpp args in + + List.map ~f:mlg_rule s.modules diff --git a/src/coq_rules.mli b/src/coq_rules.mli index dabb0412a5b..08edec8611a 100644 --- a/src/coq_rules.mli +++ b/src/coq_rules.mli @@ -18,3 +18,9 @@ val install_rules -> dir:Path.t -> Dune_file.Coq.t -> (Loc.t option * Install.Entry.t) list + +val coqpp_rules + : sctx:Super_context.t + -> dir:Path.t + -> Dune_file.Coqpp.t + -> (unit, Action.t) Build.t list diff --git a/src/dir_contents.ml b/src/dir_contents.ml index aa958e1661e..3013cd23bdc 100644 --- a/src/dir_contents.ml +++ b/src/dir_contents.ml @@ -266,10 +266,8 @@ let load_text_files sctx ft_dir let generated_files = List.concat_map stanzas ~f:(fun stanza -> match (stanza : Stanza.t) with - | Coq.T _coq -> - (* Format.eprintf "[coq] generated_files called at sctx: %a@\n%!" Path.pp (File_tree.Dir.path ft_dir); *) - (* FIXME: Need to generate ml files from mlg ? *) - [] + | Coqpp.T { modules; _ } -> + List.map modules ~f:(fun m -> m ^ ".ml") | Menhir.T menhir -> Menhir_rules.targets menhir | Rule rule -> diff --git a/src/dune_file.ml b/src/dune_file.ml index b98476028ee..66407de90d5 100644 --- a/src/dune_file.ml +++ b/src/dune_file.ml @@ -1812,6 +1812,25 @@ module Menhir = struct }) end +module Coqpp = struct + + type t = + { modules : string list + ; loc : Loc.t + } + + let decode = + record + (let+ modules = field "modules" (list string) + and+ loc = loc in + { modules + ; loc + }) + + type Stanza.t += T of t + +end + module Coq = struct type t = @@ -1867,8 +1886,11 @@ module Coq = struct let unit_to_sexp () = Sexp.List [] + let coqlib_p = "coqlib", decode >>| fun x -> [T x] + let coqpp_p = "coq.pp", Coqpp.(decode >>| fun x -> [T x]) + let unit_stanzas = - let+ r = return ["coqlib", decode >>| fun x -> [T x]] in + let+ r = return [coqlib_p; coqpp_p] in ((), r) let key = diff --git a/src/dune_file.mli b/src/dune_file.mli index 8b0222c0570..d1c696970e9 100644 --- a/src/dune_file.mli +++ b/src/dune_file.mli @@ -372,6 +372,16 @@ module Coq : sig type Stanza.t += T of t end +module Coqpp : sig + + type t = + { modules : string list + ; loc : Loc.t + } + + type Stanza.t += T of t +end + module Alias_conf : sig type t = { name : string diff --git a/src/gen_rules.ml b/src/gen_rules.ml index 3cfde5870e7..89110c3fbb7 100644 --- a/src/gen_rules.ml +++ b/src/gen_rules.ml @@ -188,6 +188,10 @@ module Gen(P : sig val sctx : Super_context.t end) = struct let dir = ctx_dir in let coq_rules = Coq_rules.setup_rules ~sctx ~dir ~dir_contents m in SC.add_rules ~dir:ctx_dir sctx coq_rules + | Coqpp.T m -> + let dir = ctx_dir in + let coqpp_rules = Coq_rules.coqpp_rules ~sctx ~dir m in + SC.add_rules ~dir:ctx_dir sctx coqpp_rules | _ -> ()); let dyn_deps = let pred = diff --git a/src/stdune/path.ml b/src/stdune/path.ml index 1504af1d4a6..96f73811848 100644 --- a/src/stdune/path.ml +++ b/src/stdune/path.ml @@ -873,8 +873,8 @@ let readdir_unsorted = Exn.protect ~f:(fun () -> match loop dh [] with - | exception (Unix.Unix_error (e, _, _)) -> Error e - | s -> Ok s) + | exception (Unix.Unix_error (e, _, _)) -> Error e + | s -> Result.Ok s) ~finally:(fun () -> Unix.closedir dh) with Unix.Unix_error (e, _, _) -> Error e diff --git a/test/blackbox-tests/test-cases/coq/ml_lib/src/dune b/test/blackbox-tests/test-cases/coq/ml_lib/src/dune index 74f34816a17..d4f874c31be 100644 --- a/test/blackbox-tests/test-cases/coq/ml_lib/src/dune +++ b/test/blackbox-tests/test-cases/coq/ml_lib/src/dune @@ -1,4 +1,7 @@ (library (public_name ml_lib.ml_plugin) (name ml_plugin) + (flags :standard -rectypes) (libraries coq.plugins.ltac)) + +(coq.pp (modules gram)) diff --git a/test/blackbox-tests/test-cases/coq/ml_lib/src/gram.mlg b/test/blackbox-tests/test-cases/coq/ml_lib/src/gram.mlg new file mode 100644 index 00000000000..80481ac4631 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/ml_lib/src/gram.mlg @@ -0,0 +1,9 @@ +DECLARE PLUGIN "gram" + +{ + +(* We don't use any coqpp specific macros as to make the test more + resilient on different Coq versions *) +let foo = 3 + +} diff --git a/test/blackbox-tests/test-cases/coq/ml_lib/src/gram.mli b/test/blackbox-tests/test-cases/coq/ml_lib/src/gram.mli new file mode 100644 index 00000000000..bcc533d2e62 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/ml_lib/src/gram.mli @@ -0,0 +1 @@ +val foo : int diff --git a/test/blackbox-tests/test-cases/coq/run.t b/test/blackbox-tests/test-cases/coq/run.t index 7e1a565b9a7..15df108ad21 100644 --- a/test/blackbox-tests/test-cases/coq/run.t +++ b/test/blackbox-tests/test-cases/coq/run.t @@ -18,12 +18,18 @@ $ dune build --root ml_lib --display short --debug-dependency-path @all Entering directory 'ml_lib' + coqpp src/gram.ml + ocamldep src/.ml_plugin.objs/gram.ml.d ocamlc src/.ml_plugin.objs/byte/ml_plugin.{cmi,cmo,cmt} ocamlopt src/.ml_plugin.objs/native/ml_plugin.{cmx,o} + ocamldep src/.ml_plugin.objs/gram.mli.d + ocamlc src/.ml_plugin.objs/byte/ml_plugin__Gram.{cmi,cmti} + ocamlc src/.ml_plugin.objs/byte/ml_plugin__Gram.{cmo,cmt} ocamldep src/.ml_plugin.objs/simple.ml.d ocamlc src/.ml_plugin.objs/byte/ml_plugin__Simple.{cmi,cmo,cmt} ocamlc src/ml_plugin.cma coqdep theories/a.v.d + ocamlopt src/.ml_plugin.objs/native/ml_plugin__Gram.{cmx,o} ocamlopt src/.ml_plugin.objs/native/ml_plugin__Simple.{cmx,o} ocamlopt src/ml_plugin.{a,cmxa} ocamlopt src/ml_plugin.cmxs