Skip to content

Commit

Permalink
[coq] Allow Coq libraries to depend on ML plugins.
Browse files Browse the repository at this point in the history 
We add a new field `(libraries <ocaml_libraries>)` to the `coqlib`
stanza for specifying dependencies on OCaml libs, such as plugins.

The current implementation has to workaround a couple of `coqdep`
problem:

- `-I` flags to `coqdep` must refer to the build tree as to find the
  `.cmxs` file, this is different from what OCaml needs;
- `coqdep` needs to find the `foo.mlpack` file as to emit the correct
  `cmxs` dependency. However such file won't be available for
  system-installed plugins.

We solve the first one by manually computing the include flags, and
the second one by adding a conditional dependency so we don't fail if
the file is missing.

We should improve `coqdep` so these kind of hacks are not necessary.

Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
  • Loading branch information
@ejgallego
ejgallego committed Mar 29, 2019
1 parent d67969c commit 4651e7c
Show file tree
Hide file tree
Showing 13 changed files with 234 additions and 171 deletions.
39 changes: 21 additions & 18 deletions doc/coq.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,10 +31,10 @@ The basic form for defining Coq libraries is very similar to the OCaml form:
(public_name <package.lib_name>)
(synopsis <text>)
(modules <ordered_set_lang>)
(libraries <ocaml_libraries>)
(flags <coq_flags>))
The stanza will build all `.v` files on the given directory.
The semantics of fields is:
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
Expand All @@ -43,27 +43,30 @@ The semantics of fields is:
files; files will be installed in
``lib/coq/user-contrib/<module_prefix>``, as customary in the
make-based Coq package eco-system,
- ``<coq_flags>`` will be passed to ``coqc``.
- ``<coq_flags>`` will be passed to ``coqc``,
- the path to installed locations of ``<ocaml_libraries>`` 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 Composition and Handling
================================
Recursive Qualification of Modules
==================================

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.
If you add:

This will be fixed in the future.
.. code:: scheme
Recursive modules
=================
(include_subdirs qualified)
Adding:
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``.

.. code:: scheme
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,
- Coq plugins are installed into their regular OCaml library path.

(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.
10 changes: 10 additions & 0 deletions src/build.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -154,6 +154,16 @@ let file_exists_opt p t =
~then_:(t >>^ Option.some)
~else_:(arr (Fn.const None))

let paths_existing paths =
List.fold_left paths
~init:(return true)
~f:(fun acc file ->
if_file_exists file
~then_:(path file)
~else_:(arr Fn.id)
>>>
acc)

let fail ?targets x =
match targets with
| None -> Fail x
Expand Down
230 changes: 100 additions & 130 deletions src/build.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -69,170 +69,140 @@ val path_set : Path.Set.t -> ('a, 'a) t
dependencies of the action produced by the build arrow. *)
val paths_matching : loc:Loc.t -> File_selector.t -> ('a, Path.Set.t) t

(** [env_var v] records [v] as an environment variable that is read by the
action produced by the build arrow. *)
(** [paths_existing paths] will require as dependencies the files that
actually exist, and return true if the all the paths do actually exist. *)
val paths_existing : Path.t list -> ('a, bool) t

(** [env_var v] records [v] as an environment variable that is read by
the action produced by the build arrow. *)
val env_var : string -> ('a, 'a) t

val alias : Alias.t -> ('a, 'a) t

(** Compute the set of source of all files present in the sub-tree
starting at [dir] and record them as dependencies. *)
val source_tree
: dir:Path.t
-> file_tree:File_tree.t
-> ('a, Path.Set.t) t
starting at [dir] and record them as dependencies. *) val
source_tree : dir:Path.t -> file_tree:File_tree.t -> ('a,
Path.Set.t) t

(** Record dynamic dependencies *)
val dyn_paths : ('a, Path.t list) t -> ('a, 'a) t
val dyn_path_set : ('a, Path.Set.t) t -> ('a, 'a) t
(** Record dynamic dependencies *) val dyn_paths : ('a, Path.t list) t
-> ('a, 'a) t val dyn_path_set : ('a, Path.Set.t) t -> ('a, 'a) t

val vpath : 'a Vspec.t -> (unit, 'a) t
val vpath : 'a Vspec.t -> (unit, 'a) t

(** [catch t ~on_error] evaluates to [on_error exn] if exception [exn] is
raised during the evaluation of [t]. *)
val catch : ('a, 'b) t -> on_error:(exn -> 'b) -> ('a, 'b) t
(** [catch t ~on_error] evaluates to [on_error exn] if exception [exn]
is raised during the evaluation of [t]. *) val catch : ('a, 'b) t
-> on_error:(exn -> 'b) -> ('a, 'b) t

(** [contents path] returns an arrow that when run will return the contents of
the file at [path]. *)
val contents : Path.t -> ('a, string) t
(** [contents path] returns an arrow that when run will return the
contents of the file at [path]. *) val contents : Path.t -> ('a,
string) t

(** [lines_of path] returns an arrow that when run will return the contents of
the file at [path] as a list of lines. *)
val lines_of : Path.t -> ('a, string list) t
(** [lines_of path] returns an arrow that when run will return the
contents of the file at [path] as a list of lines. *) val lines_of
: Path.t -> ('a, string list) t

(** [strings path] is like [lines_of path] except each line is unescaped using
the OCaml conventions. *)
val strings : Path.t -> ('a, string list) t
(** [strings path] is like [lines_of path] except each line is
unescaped using the OCaml conventions. *) val strings : Path.t ->
('a, string list) t

(** Load an S-expression from a file *)
val read_sexp : Path.t -> Dune_lang.syntax -> (unit, Dune_lang.Ast.t) t
(** Load an S-expression from a file *) val read_sexp : Path.t ->
Dune_lang.syntax -> (unit, Dune_lang.Ast.t) t

(** Evaluates to [true] if the file is present on the file system or is the target of a
rule. *)
val file_exists : Path.t -> ('a, bool) t
(** Evaluates to [true] if the file is present on the file system or
is the target of a rule. *) val file_exists : Path.t -> ('a, bool)
t

(** [if_file_exists p ~then ~else] is an arrow that behaves like [then_] if [file_exists
p] evaluates to [true], and [else_] otherwise. *)
val if_file_exists : Path.t -> then_:('a, 'b) t -> else_:('a, 'b) t -> ('a, 'b) t
(** [if_file_exists p ~then ~else] is an arrow that behaves like
[then_] if [file_exists p] evaluates to [true], and [else_]
otherwise. *) val if_file_exists : Path.t -> then_:('a, 'b) t ->
else_:('a, 'b) t -> ('a, 'b) t

(** [file_exists_opt p t] is:
{[
if_file_exists p ~then_:(t >>^ fun x -> Some x) ~else_:(arr (fun _ -> None))
]}
*)
val file_exists_opt : Path.t -> ('a, 'b) t -> ('a, 'b option) t
{[ if_file_exists p ~then_:(t >>^ fun x -> Some x) ~else_:(arr
(fun _ -> None)) ]} *) val file_exists_opt : Path.t -> ('a, 'b) t
-> ('a, 'b option) t

(** Always fail when executed. We pass a function rather than an
exception to get a proper backtrace *)
val fail : ?targets:Path.t list -> fail -> (_, _) t
exception to get a proper backtrace *) val fail : ?targets:Path.t
list -> fail -> (_, _) t

val of_result
: ?targets:Path.t list
-> ('a, 'b) t Or_exn.t
-> ('a, 'b) t
val of_result : ?targets:Path.t list -> ('a, 'b) t Or_exn.t -> ('a,
'b) t

val of_result_map
: ?targets:Path.t list
-> 'a Or_exn.t
-> f:('a -> ('b, 'c) t)
-> ('b, 'c) t
val of_result_map : ?targets:Path.t list -> 'a Or_exn.t -> f:('a ->
('b, 'c) t) -> ('b, 'c) t

(** [memoize name t] is an arrow that behaves like [t] except that its
result is computed only once. *)
val memoize : string -> (unit, 'a) t -> (unit, 'a) t

val run
: dir:Path.t
-> ?stdout_to:Path.t
-> Action.Prog.t
-> ('a, Arg_spec.dynamic) Arg_spec.t list
-> ('a, Action.t) t

val action
: ?dir:Path.t
-> targets:Path.t list
-> Action.t
-> (_, Action.t) t

val action_dyn
: ?dir:Path.t
-> targets:Path.t list
-> unit
-> (Action.t, Action.t) t

(** Create a file with the given contents. *)
val write_file : Path.t -> string -> (unit, Action.t) t
val write_file_dyn : Path.t -> (string, Action.t) t

val copy : src:Path.t -> dst:Path.t -> (unit, Action.t) t
val copy_and_add_line_directive : src:Path.t -> dst:Path.t -> (unit, Action.t) t
result is computed only once. *) val memoize : string -> (unit, 'a)
t -> (unit, 'a) t

val run : dir:Path.t -> ?stdout_to:Path.t -> Action.Prog.t -> ('a,
Arg_spec.dynamic) Arg_spec.t list -> ('a, Action.t) t

val action : ?dir:Path.t -> targets:Path.t list -> Action.t -> (_,
Action.t) t

val action_dyn : ?dir:Path.t -> targets:Path.t list -> unit ->
(Action.t, Action.t) t

(** Create a file with the given contents. *) val write_file : Path.t
-> string -> (unit, Action.t) t val write_file_dyn : Path.t ->
(string, Action.t) t

val copy : src:Path.t -> dst:Path.t -> (unit, Action.t) t val
copy_and_add_line_directive : src:Path.t -> dst:Path.t -> (unit,
Action.t) t

val symlink : src:Path.t -> dst:Path.t -> (unit, Action.t) t

val create_file : Path.t -> (_, Action.t) t
val remove_tree : Path.t -> (_, Action.t) t
val mkdir : Path.t -> (_, Action.t) t
val create_file : Path.t -> (_, Action.t) t val remove_tree : Path.t
-> (_, Action.t) t val mkdir : Path.t -> (_, Action.t) t

(** Merge a list of actions *)
val progn : ('a, Action.t) t list -> ('a, Action.t) t
(** Merge a list of actions *) val progn : ('a, Action.t) t list ->
('a, Action.t) t

val record_lib_deps : Lib_deps_info.t -> ('a, 'a) t

(**/**)


module Repr : sig
type ('a, 'b) t =
| Arr : ('a -> 'b) -> ('a, 'b) t
| Targets : Path.t list -> ('a, 'a) t
| Store_vfile : 'a Vspec.t -> ('a, Action.t) t
| Compose : ('a, 'b) t * ('b, 'c) t -> ('a, 'c) t
| First : ('a, 'b) t -> ('a * 'c, 'b * 'c) t
| Second : ('a, 'b) t -> ('c * 'a, 'c * 'b) t
| Split : ('a, 'b) t * ('c, 'd) t -> ('a * 'c, 'b * 'd) t
| Fanout : ('a, 'b) t * ('a, 'c) t -> ('a, 'b * 'c) t
| Paths_for_rule : Path.Set.t -> ('a, 'a) t
| Paths_glob : File_selector.t -> ('a, Path.Set.t) t
| If_file_exists : Path.t * ('a, 'b) if_file_exists_state ref -> ('a, 'b) t
| Contents : Path.t -> ('a, string) t
| Lines_of : Path.t -> ('a, string list) t
| Vpath : 'a Vspec.t -> (unit, 'a) t
| Dyn_paths : ('a, Path.Set.t) t -> ('a, 'a) t
| Dyn_deps : ('a, Dep.Set.t) t -> ('a, 'a) t
| Record_lib_deps : Lib_deps_info.t -> ('a, 'a) t
| Fail : fail -> (_, _) t
| Memo : 'a memo -> (unit, 'a) t
| Catch : ('a, 'b) t * (exn -> 'b) -> ('a, 'b) t
| Lazy_no_targets : ('a, 'b) t Lazy.t -> ('a, 'b) t
| Deps : Dep.Set.t -> ('a, 'a) t

and 'a memo =
{ name : string
; t : (unit, 'a) t
; mutable state : 'a memo_state
}

and 'a memo_state =
| Unevaluated
| Evaluating
| Evaluated of 'a * Dep.Set.t (* dynamic dependencies *)

and ('a, 'b) if_file_exists_state =
| Undecided of ('a, 'b) t * ('a, 'b) t
| Decided of bool * ('a, 'b) t

and glob_state =
| G_unevaluated of Loc.t * Path.t * Path.t Predicate.t
| G_evaluated of Path.Set.t

val get_if_file_exists_exn : ('a, 'b) if_file_exists_state ref -> ('a, 'b) t
val get_glob_result_exn : glob_state ref -> Path.Set.t
end
module Repr : sig type ('a, 'b) t = | Arr : ('a -> 'b) -> ('a, 'b) t |
Targets : Path.t list -> ('a, 'a) t | Store_vfile : 'a Vspec.t ->
('a, Action.t) t | Compose : ('a, 'b) t * ('b, 'c) t -> ('a, 'c) t
| First : ('a, 'b) t -> ('a * 'c, 'b * 'c) t | Second : ('a, 'b) t
-> ('c * 'a, 'c * 'b) t | Split : ('a, 'b) t * ('c, 'd) t -> ('a *
'c, 'b * 'd) t | Fanout : ('a, 'b) t * ('a, 'c) t -> ('a, 'b * 'c)
t | Paths_for_rule : Path.Set.t -> ('a, 'a) t | Paths_glob :
File_selector.t -> ('a, Path.Set.t) t | If_file_exists : Path.t *
('a, 'b) if_file_exists_state ref -> ('a, 'b) t | Contents : Path.t
-> ('a, string) t | Lines_of : Path.t -> ('a, string list) t |
Vpath : 'a Vspec.t -> (unit, 'a) t | Dyn_paths : ('a, Path.Set.t) t
-> ('a, 'a) t | Dyn_deps : ('a, Dep.Set.t) t -> ('a, 'a) t |
Record_lib_deps : Lib_deps_info.t -> ('a, 'a) t | Fail : fail ->
(_, _) t | Memo : 'a memo -> (unit, 'a) t | Catch : ('a, 'b) t *
(exn -> 'b) -> ('a, 'b) t | Lazy_no_targets : ('a, 'b) t Lazy.t ->
('a, 'b) t | Deps : Dep.Set.t -> ('a, 'a) t

and 'a memo = { name : string ; t : (unit, 'a) t ; mutable state :
'a memo_state }

and 'a memo_state = | Unevaluated | Evaluating | Evaluated of 'a *
Dep.Set.t (* dynamic dependencies *)

and ('a, 'b) if_file_exists_state = | Undecided of ('a, 'b) t * ('a,
'b) t | Decided of bool * ('a, 'b) t

and glob_state = | G_unevaluated of Loc.t * Path.t * Path.t
Predicate.t | G_evaluated of Path.Set.t

val get_if_file_exists_exn : ('a, 'b) if_file_exists_state ref ->
('a, 'b) t val get_glob_result_exn : glob_state ref -> Path.Set.t
end

val repr : ('a, 'b) t -> ('a, 'b) Repr.t

(**/**)
val paths_for_rule : Path.Set.t -> ('a, 'a) t
(**/**) val paths_for_rule : Path.Set.t -> ('a, 'a) t

val merge_files_dyn : target:Path.t -> (Path.t list * string list, Action.t) t
val merge_files_dyn : target:Path.t -> (Path.t list * string list,
Action.t) t
Loading

0 comments on commit 4651e7c

Please sign in to comment.