Merge pull request #1968 from ejgallego/coq+recursive

[lang] Preliminary Coq support, core part with recursively qualified modules.

.travis-ci.sh

@@ -94,14 +94,15 @@ case "$TARGET" in
       fi
       opam list
       opam pin add dune . --no-action
-      opam install ocamlfind utop ppxlib $ODOC ocaml-migrate-parsetree js_of_ocaml-ppx js_of_ocaml-compiler
+      opam install ocamlfind utop ppxlib $ODOC ocaml-migrate-parsetree js_of_ocaml-ppx js_of_ocaml-compiler coq
       echo -en "travis_fold:end:opam.deps\r"
     fi
     echo -en "travis_fold:end:dune.boot\r"
     if [ $WITH_OPAM -eq 1 ] ; then
       cat $RUNTEST_NO_DEPS;
       _boot/install/default/bin/dune runtest && \
       _boot/install/default/bin/dune build @test/blackbox-tests/runtest-js && \
+      _boot/install/default/bin/dune build @test/blackbox-tests/runtest-coq && \
       ! _boot/install/default/bin/dune build @test/fail-with-background-jobs-running
       RESULT=$?
       if [ $UPDATE_OPAM -eq 0 ] ; then

CHANGES.md

@@ -17,6 +17,8 @@ unreleased
 - Add experimental `$ dune init` command. This command is used to create or
   update project boilerplate. (#1448, fixes #159, @shonfeder)
 
+- Experimental Coq support (1466, @ejgallego)
+
 1.8.2 (10/03/2019)
 ------------------
 

Makefile

@@ -28,8 +28,11 @@ test:
 test-js:
 	$(BIN) build @runtest-js
 
+test-coq:
+	$(BIN) build @runtest-coq
+
 test-all:
-	$(BIN) build @runtest @runtest-js
+	$(BIN) build @runtest @runtest-js @runtest-coq
 
 check:
 	$(BIN) build @check

doc/coq.rst

@@ -0,0 +1,63 @@
+.. _coq-main:
+
+******
+Coq
+******
+
+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:
+
+.. code:: scheme
+
+    (using coq 0.1)
+
+This will enable support for the ``coqlib`` stanza in the current project. If the
+language version is absent, dune will automatically add this line with the
+latest Coq version to the project file once a ``(coqlib ...)`` stanza is used anywhere.
+
+
+Basic Usage
+===========
+
+The basic form for defining Coq libraries is very similar to the OCaml form:
+
+.. code:: scheme
+
+    (coqlib
+     (name <module_prefix>)
+     (synopsis <text>)
+     (modules <ordered_set_lang>)
+     (flags <coq_flags>))
+
+The stanza will build all `.v` files on the given directory.
+The semantics of fields is:
+- ``<module_prefix>>`` 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
+- ``<coq_flags>`` will be passed to ``coqc``.
+
+Library Composition and Handling
+===================
+
+The ``coqlib`` stanza does not yet support composition of Coq
+libraries. In the 0.1 version of the language, libraries are located
+using Coq's built-in library management, thus Coq will always resort
+to the installed version of a particular library.
+
+This will be fixed in the future.
+
+Recursive modules
+===================
+
+Adding:
+
+.. code:: scheme
+    (include_subdirs qualified)
+
+to the ``dune`` file will make Dune to consider all the modules in the
+current directory and sub-directories, qualified in the current Coq
+style.

doc/index.rst

@@ -24,6 +24,7 @@ Welcome to dune's documentation!
    jsoo
    variants
    formatting
+   coq
    faq
    known-issues
    migration

src/coq_module.ml

@@ -0,0 +1,60 @@
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2018-2019               *)
+(*     Written by: Emilio Jesús Gallego Arias  *)
+
+open! Stdune
+
+module Name = struct
+
+  type t = string
+
+  let make x = x
+  let compare = String.compare
+  let pp = Fmt.text
+
+end
+
+(* We keep prefix and name separated as the handling of
+  `From Foo Require Bar.` may benefit from it. *)
+type t =
+  { source: Path.t
+  ; prefix : string list
+  ; name : string
+  }
+
+let make ~source ~prefix ~name =
+  { source
+  ; prefix
+  ; name
+  }
+
+let source x = x.source
+let prefix x = x.prefix
+let name x = x.name
+let obj_file ~obj_dir ~ext x =
+  let vo_dir = List.fold_left x.prefix ~init:obj_dir ~f:Path.relative in
+  Path.relative vo_dir (x.name ^ ext)
+let pp fmt x =
+  let open Format in
+  let pp_sep fmt () = pp_print_string fmt "." in
+  fprintf fmt "{ prefix = %a; name = %s; source = %a }"
+    (pp_print_list ~pp_sep pp_print_string) x.prefix x.name Path.pp x.source
+
+let parse ~dir ~loc s =
+  let clist = List.rev @@ String.split s ~on:'.' in
+  match clist with
+  | [] ->
+    Errors.fail loc "invalid coq module"
+  | name :: prefix ->
+    let prefix = List.rev prefix in
+    let source = List.fold_left prefix ~init:dir ~f:Path.relative in
+    let source = Path.relative source (name ^ ".v") in
+    make ~name ~source ~prefix
+
+module Value = struct
+  type nonrec t = t
+  type key = string
+  let key x = String.concat ~sep:"." (x.prefix @ [x.name])
+end
+
+module Eval = Ordered_set_lang.Make(String)(Value)

src/coq_module.mli

@@ -0,0 +1,40 @@
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2018-2019               *)
+(*     Written by: Emilio Jesús Gallego Arias  *)
+
+open! Stdune
+
+module Name : sig
+
+  type t
+
+  val make : string -> t
+  val compare : t -> t -> Ordering.t
+
+  val pp : t Fmt.t
+
+end
+
+type t
+
+(** A Coq module [a.b.foo] defined in file [a/b/foo.v] *)
+val make
+  :  source:Path.t
+  (** file = .v source file; module name has to be the same so far *)
+  -> prefix:string list
+  (** Library-local qualified prefix *)
+  -> name:Name.t
+  (** Name of the module *)
+  -> t
+
+(** Coq does enforce some invariants wrt module vs file names *)
+
+val source : t -> Path.t
+val prefix : t -> string list
+val name : t -> string
+val obj_file : obj_dir:Path.t -> ext:string -> t -> Path.t
+val pp : t Fmt.t
+
+(** Parses a form "a.b.c" to a module *)
+val parse : dir:Path.t -> loc:Loc.t -> string -> t
+module Eval : Ordered_set_lang.S with type value := t

src/coq_rules.ml

@@ -0,0 +1,113 @@
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2018-2019               *)
+(*     Written by: Emilio Jesús Gallego Arias  *)
+
+open! Stdune
+open Build.O
+module SC = Super_context
+
+let coq_debug = false
+
+type coq_context =
+  { coqdep : Action.program
+  ; coqc   : Action.program
+  ; coqpp  : Action.program
+  }
+
+let parse_coqdep ~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 =
+    Errors.die "coqdep returned invalid output for %s / [phase: %s]"
+      (Path.to_string source) p in
+  let line =
+    match lines with
+    | [] | _ :: _ :: _ :: _ -> invalid "line"
+    | [line] -> line
+    | [l1;_l2] ->
+      (* .vo is produced before .vio, this is fragile tho *)
+      l1
+  in
+  match String.lsplit2 line ~on:':' with
+  | None -> invalid "split"
+  | 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
+    if coq_debug
+    then Format.eprintf "depname / modname: %s / %s@\n%!" depname modname;
+    if depname <> modname then invalid "basename";
+    let deps = String.extract_blank_separated_words deps in
+    if coq_debug
+    then Format.eprintf "deps for %a: %a@\n%!" Path.pp source Fmt.(list text) deps;
+    deps
+
+let setup_rule ~expander ~dir ~cc ~source_rule ~name ~cflags coq_module =
+
+  if coq_debug
+  then Format.eprintf "gen_rule coq_module: %a@\n%!" Coq_module.pp coq_module;
+  let obj_dir = dir in
+  let source    = Coq_module.source coq_module in
+  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"; "."; name] in
+  let cd_arg = Arg_spec.[ iflags; Dep source ] in
+
+  (* coqdep needs the full source to be present :( *)
+  let coqdep_rule =
+    source_rule >>>
+    Build.run ~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)
+  ) in
+  let cc_arg = Arg_spec.[
+    iflags;
+    Dep source;
+    Hidden_targets [object_to] ]
+  in
+  [coqdep_rule;
+   deps_of >>>
+   Expander.expand_and_eval_set expander cflags ~standard:(Build.return []) >>>
+   Build.run ~dir cc.coqc (Dyn (fun flags -> As flags) :: cc_arg)
+  ]
+
+(* TODO: remove; rgrinberg points out:
+   - resolve program is actually cached,
+   - better just to ask for values that we actually use.
+ *)
+let create_ccoq sctx ~dir =
+  let rr prg =
+    SC.resolve_program ~dir sctx prg ~loc:None ~hint:"try: opam install coq" in
+  { coqdep = rr "coqdep"
+  ; coqc   = rr "coqc"
+  ; coqpp  = rr "coqpp"
+  }
+
+let setup_rules ~sctx ~dir ~dir_contents (s : Dune_file.Coq.t) =
+
+  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 cc = create_ccoq sctx ~dir in
+  let name = snd s.name in
+  let coq_modules = Dir_contents.coq_modules_of_library dir_contents ~name 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
+  let cflags = s.Dune_file.Coq.flags in
+  let expander = SC.expander sctx ~dir in
+  let coq_rules =
+    List.concat_map
+      ~f:(setup_rule ~expander ~dir ~cc ~source_rule ~name ~cflags) coq_modules in
+  coq_rules

src/coq_rules.mli

@@ -0,0 +1,14 @@
+(* This file is licensed under The MIT License *)
+(* (c) MINES ParisTech 2018-2019               *)
+(*     Written by: Emilio Jesús Gallego Arias  *)
+
+(* Build rules for Coq's .v -> .vo files       *)
+
+open! Stdune
+
+val setup_rules
+  :  sctx:Super_context.t
+  -> dir:Path.t
+  -> dir_contents:Dir_contents.t
+  -> Dune_file.Coq.t
+  -> (unit, Action.t) Build.t list