From 721472a9a9ec686524c28216cf3975c1edafea9d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 19 Nov 2018 20:14:21 +0100 Subject: [PATCH] [lang] Preliminary Coq support. This commit adds experimental Coq support to Dune. See Dune issue 1446 for more details. The patch adds a new stanza `(coqlib ...)` enabled by adding `(using coq 0.1)` to `dune-project`. The stanza looks like: ```lisp (coqlib (name Ltac2) ; Determines the `-R` flag (synopsis "Ltac 2 Plugin") ; (modules core Lib.mod) (flags -warn -no-cbv)) ; Flags for `coqc` ``` The functionality of the mode is basic, but it should suffice to replace and extend most uses of `coq_makefile`. The main remaining issue is the definition of on Coq libraries. Local support for Coq libraries should suffice in the short-term. That is to say, `(coqlib ....)` will only see libraries in the same scope, and rely on Coq's default rules for the rest. However, this doesn't seem straightforward. In particular, we may have to re-implement `Lib.DB` which is not trivial. Upcoming commits will add: - support for depending on ML libraries; - generation of `(install ...)` rules; Signed-off-by: Emilio Jesus Gallego Arias --- CHANGES.md | 2 + Makefile | 5 +- doc/coq.rst | 62 ++++++++++ doc/index.rst | 1 + src/coq_module.ml | 50 ++++++++ src/coq_module.mli | 29 +++++ src/coq_rules.ml | 111 ++++++++++++++++++ src/coq_rules.mli | 15 +++ src/dir_contents.ml | 70 +++++++++-- src/dir_contents.mli | 3 + src/dune_file.ml | 54 +++++++++ src/dune_file.mli | 17 +++ src/gen_rules.ml | 5 + src/stdune/option.ml | 5 + src/stdune/option.mli | 2 + test/blackbox-tests/dune.inc | 12 +- test/blackbox-tests/gen_tests.ml | 14 ++- test/blackbox-tests/test-cases/coq/base/bar.v | 3 + test/blackbox-tests/test-cases/coq/base/dune | 5 + .../test-cases/coq/base/dune-project | 3 + test/blackbox-tests/test-cases/coq/base/foo.v | 1 + .../test-cases/coq/rec_module/a/bar.v | 5 + .../test-cases/coq/rec_module/b/foo.v | 1 + .../test-cases/coq/rec_module/c/d/bar.v | 1 + .../test-cases/coq/rec_module/c/ooo.v | 1 + .../test-cases/coq/rec_module/dune | 7 ++ .../test-cases/coq/rec_module/dune-project | 3 + test/blackbox-tests/test-cases/coq/run.t | 5 + 28 files changed, 474 insertions(+), 18 deletions(-) create mode 100644 doc/coq.rst create mode 100644 src/coq_module.ml create mode 100644 src/coq_module.mli create mode 100644 src/coq_rules.ml create mode 100644 src/coq_rules.mli create mode 100644 test/blackbox-tests/test-cases/coq/base/bar.v create mode 100644 test/blackbox-tests/test-cases/coq/base/dune create mode 100644 test/blackbox-tests/test-cases/coq/base/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/base/foo.v create mode 100644 test/blackbox-tests/test-cases/coq/rec_module/a/bar.v create mode 100644 test/blackbox-tests/test-cases/coq/rec_module/b/foo.v create mode 100644 test/blackbox-tests/test-cases/coq/rec_module/c/d/bar.v create mode 100644 test/blackbox-tests/test-cases/coq/rec_module/c/ooo.v create mode 100644 test/blackbox-tests/test-cases/coq/rec_module/dune create mode 100644 test/blackbox-tests/test-cases/coq/rec_module/dune-project create mode 100644 test/blackbox-tests/test-cases/coq/run.t diff --git a/CHANGES.md b/CHANGES.md index 9f135b6158d3..b59da2272864 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -11,6 +11,8 @@ unreleased - Fix glob dependencies on installed directories (#1965, @rgrinberg) +- Experimental Coq support (1466, @ejgallego) + 1.8.2 (10/03/2019) ------------------ diff --git a/Makefile b/Makefile index 1bafa1802a84..78acd78de07f 100644 --- a/Makefile +++ b/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 diff --git a/doc/coq.rst b/doc/coq.rst new file mode 100644 index 000000000000..a198fe437021 --- /dev/null +++ b/doc/coq.rst @@ -0,0 +1,62 @@ +.. _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 (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 ) + (synopsis ) + (modules ) + (flags )) + +Library Composition and Handling +=================== + +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`` +- the ``modules`` field does allow to constraint the set of modules + included in the library, similarly to its OCaml counterpart +- ```` will be passed to ``coqc``. + +The ``coqlib`` stanza does not yet support composition of Coq +libraries. In the current version, 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 unqualified) + +to the ``dune`` will make Dune to consider all the modules in the +current directory and sub-directories, qualified in the current Coq +style. diff --git a/doc/index.rst b/doc/index.rst index bd04eeecfda3..8cb0e32880db 100644 --- a/doc/index.rst +++ b/doc/index.rst @@ -24,6 +24,7 @@ Welcome to dune's documentation! jsoo variants formatting + coq faq known-issues migration diff --git a/src/coq_module.ml b/src/coq_module.ml new file mode 100644 index 000000000000..2d48ddec256a --- /dev/null +++ b/src/coq_module.ml @@ -0,0 +1,50 @@ +(* This file is licensed under The MIT License *) +(* (c) MINES ParisTech 2018-2019 *) +(* Written by: Emilio Jesús Gallego Arias *) + +open! Stdune + +(* 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.die "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) diff --git a/src/coq_module.mli b/src/coq_module.mli new file mode 100644 index 000000000000..4605a9b5b56c --- /dev/null +++ b/src/coq_module.mli @@ -0,0 +1,29 @@ +(* This file is licensed under The MIT License *) +(* (c) MINES ParisTech 2018-2019 *) +(* Written by: Emilio Jesús Gallego Arias *) + +open! Stdune + +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:string + (** 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 diff --git a/src/coq_rules.ml b/src/coq_rules.ml new file mode 100644 index 000000000000..175862db3d80 --- /dev/null +++ b/src/coq_rules.ml @@ -0,0 +1,111 @@ +(* 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 + +(* TODO: *) +(* - save library information *) + +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, _ext = 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 + + (* *) + 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) + ] + +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 ~scope (s : Dune_file.Coq.t) = + + if coq_debug then + Format.eprintf "[gen_rules] @[dir: %a@\nscope: %a@]@\n%!" + Path.pp dir Path.pp Scope.(root scope) + ; + + 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 diff --git a/src/coq_rules.mli b/src/coq_rules.mli new file mode 100644 index 000000000000..6ed39c367586 --- /dev/null +++ b/src/coq_rules.mli @@ -0,0 +1,15 @@ +(* 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 + -> scope:Scope.t + -> Dune_file.Coq.t + -> (unit, Action.t) Build.t list diff --git a/src/dir_contents.ml b/src/dir_contents.ml index 723f1dc474a8..3a18a9b0cefe 100644 --- a/src/dir_contents.ml +++ b/src/dir_contents.ml @@ -180,6 +180,7 @@ type t = ; modules : Modules.t Lazy.t ; c_sources : C_sources.t Lazy.t ; mlds : (Dune_file.Documentation.t * Path.t list) list Lazy.t + ; coq_modules : Coq_module.t list String.Map.t Lazy.t } and kind = @@ -239,6 +240,16 @@ let mlds t (doc : Documentation.t) = (List.map map ~f:(fun (d, _) -> d.Documentation.loc)) ] +let coq_modules_of_library t ~name = + let map = Lazy.force t.coq_modules in + match String.Map.find map name with + | Some x -> x + | None -> + Exn.code_error "Dir_contents.coq_modules_of_library" + [ "name", Sexp.Encoder.string name + ; "available", Sexp.Encoder.(list string) (String.Map.keys map) + ] + (* As a side-effect, setup user rules and copy_files rules. *) let load_text_files sctx ft_dir { Dir_with_dune. @@ -255,6 +266,10 @@ 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 ? *) + [] | Menhir.T menhir -> Menhir_rules.targets menhir | Rule rule -> @@ -338,6 +353,28 @@ let build_mlds_map (d : _ Dir_with_dune.t) ~files = Some (doc, List.map (String.Map.values mlds) ~f:(Path.relative dir)) | _ -> None) +let coq_modules_of_files ~subdirs = + let filter_v_files (dir, local, files) = + (dir, local, String.Set.filter files ~f:(fun f -> Filename.check_suffix f ".v")) in + let subdirs = List.map subdirs ~f:filter_v_files in + let build_mod_dir (dir, prefix, files) = + String.Set.to_list files |> List.map ~f:(fun file -> + let name, _ = Filename.split_extension file in + Coq_module.make ~source:Path.(relative dir file) ~prefix ~name) in + let modules = List.concat_map ~f:build_mod_dir subdirs in + modules + +(* TODO: Build reverse map and check duplicates, however, are duplicates harmful? + * In Coq all libs are "wrapped" so including a module twice is not so bad. + *) +let build_coq_modules_map (d : _ Dir_with_dune.t) ~dir ~modules = + List.fold_left d.data ~init:String.Map.empty ~f:(fun map -> function + | Coq.T coq -> + let modules = Coq_module.Eval.eval coq.modules + ~parse:Coq_module.(parse ~dir) ~standard:modules in + String.Map.add map (snd coq.name) modules + | _ -> map) + let cache = Hashtbl.create 32 let clear_cache () = @@ -367,6 +404,9 @@ let rec get sctx ~dir = C_sources.make d ~c_sources:(C_sources.load_sources ~dune_version ~dir:d.ctx_dir ~files)) + ; coq_modules = + lazy (build_coq_modules_map d ~dir:d.ctx_dir + ~modules:(coq_modules_of_files ~subdirs:[dir,[],files])) } | Some (_, None) | None -> @@ -376,6 +416,7 @@ let rec get sctx ~dir = ; modules = lazy Modules.empty ; mlds = lazy [] ; c_sources = lazy C_sources.empty + ; coq_modules = lazy String.Map.empty } in Hashtbl.add cache dir t; @@ -389,7 +430,7 @@ let rec get sctx ~dir = Hashtbl.find_exn cache dir end | Group_root (ft_dir, d) -> - let rec walk ft_dir ~dir acc = + let rec walk ft_dir ~dir ~local acc = match Dir_status.DB.get dir_status_db ~dir with @@ -399,20 +440,21 @@ let rec get sctx ~dir = | None -> File_tree.Dir.files ft_dir | Some d -> load_text_files sctx ft_dir d in - walk_children ft_dir ~dir ((dir, files) :: acc) + walk_children ft_dir ~dir ~local ((dir, local, files) :: acc) | _ -> acc - and walk_children ft_dir ~dir acc = + and walk_children ft_dir ~dir ~local acc = String.Map.foldi (File_tree.Dir.sub_dirs ft_dir) ~init:acc ~f:(fun name ft_dir acc -> let dir = Path.relative dir name in - walk ft_dir ~dir acc) + let local = local @ [name] in + walk ft_dir ~dir ~local acc) in let files = load_text_files sctx ft_dir d in - let subdirs = walk_children ft_dir ~dir [] in + let subdirs = walk_children ft_dir ~dir ~local:[] [] in let modules = lazy ( let modules = - List.fold_left ((dir, files) :: subdirs) ~init:Module.Name.Map.empty - ~f:(fun acc (dir, files) -> + List.fold_left ((dir, [], files) :: subdirs) ~init:Module.Name.Map.empty + ~f:(fun acc (dir, _, files) -> let modules = modules_of_files ~dir ~files in Module.Name.Map.union acc modules ~f:(fun name x y -> Errors.fail (Loc.in_file @@ -434,8 +476,8 @@ let rec get sctx ~dir = let dune_version = d.dune_version in let init = C.Kind.Dict.make String.Map.empty in let c_sources = - List.fold_left ((dir, files) :: subdirs) ~init - ~f:(fun acc (dir, files) -> + List.fold_left ((dir, [], files) :: subdirs) ~init + ~f:(fun acc (dir, _, files) -> let sources = C_sources.load_sources ~dir ~dune_version ~files in let f acc sources = String.Map.union acc sources ~f:(fun name x y -> @@ -458,18 +500,23 @@ let rec get sctx ~dir = in C_sources.make d ~c_sources ) in + let coq_modules = lazy ( + build_coq_modules_map d ~dir:d.ctx_dir + ~modules:(coq_modules_of_files ~subdirs:((dir,[],files)::subdirs)) + ) in let t = { kind = Group_root - (lazy (List.map subdirs ~f:(fun (dir, _) -> get sctx ~dir))) + (lazy (List.map subdirs ~f:(fun (dir, _, _) -> get sctx ~dir))) ; dir ; text_files = files ; modules ; c_sources ; mlds = lazy (build_mlds_map d ~files) + ; coq_modules } in Hashtbl.add cache dir t; - List.iter subdirs ~f:(fun (dir, files) -> + List.iter subdirs ~f:(fun (dir, _local, files) -> Hashtbl.add cache dir { kind = Group_part t ; dir @@ -477,5 +524,6 @@ let rec get sctx ~dir = ; modules ; c_sources ; mlds = lazy (build_mlds_map d ~files) + ; coq_modules }); t diff --git a/src/dir_contents.mli b/src/dir_contents.mli index 7c466c7abea2..cabb1782f220 100644 --- a/src/dir_contents.mli +++ b/src/dir_contents.mli @@ -34,6 +34,9 @@ val lookup_module : t -> Module.Name.t -> Dune_file.Buildable.t option (** All mld files attached to this documentation stanza *) val mlds : t -> Dune_file.Documentation.t -> Path.t list +(** Coq modules of library [name] is the Coq library name. *) +val coq_modules_of_library : t -> name:string -> Coq_module.t list + val get : Super_context.t -> dir:Path.t -> t type kind = private diff --git a/src/dune_file.ml b/src/dune_file.ml index d4b261d55ce8..5979cd57c64c 100644 --- a/src/dune_file.ml +++ b/src/dune_file.ml @@ -1788,6 +1788,60 @@ module Menhir = struct }) end +module Coq = struct + + type t = + (* ; public : Public_lib.t option *\) *) + { name : Loc.t * string + (* TODO: validate name *) + ; synopsis : string option + ; modules : Ordered_set_lang.t + ; flags : Ordered_set_lang.Unexpanded.t + ; libraries : Lib_dep.t list + (** ocaml libraries *) + ; loc : Loc.t + ; enabled_if : Blang.t + } + + let syntax = + Syntax.create + ~name:"coq" + ~desc:"the coq extension (experimental)" + [ 0, 1 ] + + let decode = + record + (* let_map name = field_o "name" Lib_name.Local.decode_loc + * and public = Public_lib.public_name_field *) + (let+ name = field "name" (located string) + and+ loc = loc + and+ synopsis = field_o "synopsis" string + and+ flags = field_oslu "flags" + and+ modules = modules_field "modules" + and+ libraries = field "libraries" Lib_deps.decode ~default:[] + and+ enabled_if = enabled_if + in + (* { name + * ; public *) + { name + ; synopsis + ; modules + ; flags + ; libraries + ; loc + ; enabled_if + }) + + type Stanza.t += T of t + + let () = + Dune_project.Extension.register_simple + syntax + (return [ "coqlib", decode >>| fun x -> [T x] ]) + +end + + module Alias_conf = struct type t = { name : string diff --git a/src/dune_file.mli b/src/dune_file.mli index 0f2b4ed3c1c5..f90a0fb13124 100644 --- a/src/dune_file.mli +++ b/src/dune_file.mli @@ -353,6 +353,23 @@ module Menhir : sig type Stanza.t += T of t end +module Coq : sig + + type t = + (* ; public : Public_lib.t option *\) *) + { name : Loc.t * string + ; synopsis : string option + ; modules : Ordered_set_lang.t + ; flags : Ordered_set_lang.Unexpanded.t + ; libraries : Lib_dep.t list + (** ocaml libraries *) + ; loc : Loc.t + ; enabled_if : Blang.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 155846ef3607..e6264a48d34d 100644 --- a/src/gen_rules.ml +++ b/src/gen_rules.ml @@ -185,6 +185,11 @@ module Gen(P : sig val sctx : Super_context.t end) = struct | Some cctx -> Menhir_rules.gen_rules cctx m ~dir:ctx_dir end + | Coq.T m when Expander.eval_blang expander m.enabled_if -> + (* Format.eprintf "[coq] gen_rules called @\n%!"; *) + let dir = ctx_dir in + let coq_rules = Coq_rules.setup_rules ~sctx ~dir ~scope ~dir_contents m in + SC.add_rules ~dir:ctx_dir sctx coq_rules | _ -> ()); let dyn_deps = let pred = diff --git a/src/stdune/option.ml b/src/stdune/option.ml index 16a05bff6be6..f076ef01dfaf 100644 --- a/src/stdune/option.ml +++ b/src/stdune/option.ml @@ -39,6 +39,11 @@ let value_exn = function | Some x -> x | None -> Exn.code_error "Option.value_exn" [] +let value_map t ~f ~default = + match t with + | Some x -> f x + | None -> default + let some x = Some x let some_if cond x = diff --git a/src/stdune/option.mli b/src/stdune/option.mli index d32a34792758..6a304e5c3e87 100644 --- a/src/stdune/option.mli +++ b/src/stdune/option.mli @@ -22,6 +22,8 @@ val forall: 'a t -> f:('a -> bool) -> bool val value : 'a t -> default:'a -> 'a val value_exn : 'a t -> 'a +val value_map : 'a t -> f:('a -> 'b) -> default:'b -> 'b + val some : 'a -> 'a t val some_if : bool -> 'a -> 'a t diff --git a/test/blackbox-tests/dune.inc b/test/blackbox-tests/dune.inc index 993efd5e108b..40a531075d52 100644 --- a/test/blackbox-tests/dune.inc +++ b/test/blackbox-tests/dune.inc @@ -95,6 +95,14 @@ test-cases/copy_files (progn (run %{exe:cram.exe} -test run.t) (diff? run.t run.t.corrected))))) +(alias + (name coq) + (deps (package dune) (source_tree test-cases/coq)) + (action + (chdir + test-cases/coq + (progn (run %{exe:cram.exe} -test run.t) (diff? run.t run.t.corrected))))) + (alias (name cross-compilation) (deps (package dune) (source_tree test-cases/cross-compilation)) @@ -1625,4 +1633,6 @@ (alias (name runtest-disabled) (deps (alias envs-and-contexts))) -(alias (name runtest-js) (deps (alias js_of_ocaml))) \ No newline at end of file +(alias (name runtest-js) (deps (alias js_of_ocaml))) + +(alias (name runtest-coq) (deps (alias coq))) \ No newline at end of file diff --git a/test/blackbox-tests/gen_tests.ml b/test/blackbox-tests/gen_tests.ml index d8aca4fab120..d753339260b4 100644 --- a/test/blackbox-tests/gen_tests.ml +++ b/test/blackbox-tests/gen_tests.ml @@ -61,10 +61,11 @@ module Test = struct ; skip_platforms : Platform.t list ; enabled : bool ; js : bool + ; coq : bool ; external_deps : bool } - let make ?env ?skip_ocaml ?(skip_platforms=[]) ?(enabled=true) ?(js=false) + let make ?env ?skip_ocaml ?(skip_platforms=[]) ?(enabled=true) ?(js=false) ?(coq=false) ?(external_deps=false) name = { name ; env @@ -73,6 +74,7 @@ module Test = struct ; external_deps ; enabled ; js + ; coq } let pp_sexp fmt t = @@ -123,6 +125,7 @@ let exclusions = let odoc = make ~external_deps:true ~skip_ocaml:"4.02.3" in [ make "js_of_ocaml" ~external_deps:true ~js:true ~env:("NODE", Sexp.parse "%{bin:node}") + ; make "coq" ~external_deps:true ~coq:true ; make "github25" ~env:("OCAMLPATH", Dune_lang.atom "./findlib-packages") ; odoc "odoc" ; odoc "odoc-unique-mlds" @@ -179,13 +182,14 @@ let pp_group fmt (name, tests) = let () = let tests = Lazy.force all_tests in - (* The runtest target has a "specoial" definition. It includes all tests - except for js and disabled tests *) + (* The runtest target has a "special" definition. It includes all + tests except for js, coq, and disabled tests *) tests |> List.iter ~f:(fun t -> Format.printf "%a@.@." Test.pp_sexp t); - [ "runtest", (fun (t : Test.t) -> not t.js && t.enabled) + [ "runtest", (fun (t : Test.t) -> not t.js && not t.coq && t.enabled) ; "runtest-no-deps", (fun (t : Test.t) -> not t.external_deps && t.enabled) ; "runtest-disabled", (fun (t : Test.t) -> not t.enabled) - ; "runtest-js", (fun (t : Test.t) -> t.js && t.enabled) ] + ; "runtest-js", (fun (t : Test.t) -> t.js && t.enabled) + ; "runtest-coq", (fun (t : Test.t) -> t.coq && t.enabled) ] |> List.map ~f:(fun (name, predicate) -> (name, List.filter tests ~f:predicate)) |> Format.pp_print_list diff --git a/test/blackbox-tests/test-cases/coq/base/bar.v b/test/blackbox-tests/test-cases/coq/base/bar.v new file mode 100644 index 000000000000..4627b76131c1 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/base/bar.v @@ -0,0 +1,3 @@ +From basic Require Import foo. + +Definition mynum (i : mynat) := 3. diff --git a/test/blackbox-tests/test-cases/coq/base/dune b/test/blackbox-tests/test-cases/coq/base/dune new file mode 100644 index 000000000000..be9cdd1880b8 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/base/dune @@ -0,0 +1,5 @@ +(coqlib + (name basic) + ; (public_name dune.test.basic) + (modules) + (synopsis "Test Coq library")) diff --git a/test/blackbox-tests/test-cases/coq/base/dune-project b/test/blackbox-tests/test-cases/coq/base/dune-project new file mode 100644 index 000000000000..0f1c4e5f17f9 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/base/dune-project @@ -0,0 +1,3 @@ +(lang dune 1.4) + +(using coq 0.1) diff --git a/test/blackbox-tests/test-cases/coq/base/foo.v b/test/blackbox-tests/test-cases/coq/base/foo.v new file mode 100644 index 000000000000..53e0ce1b1526 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/base/foo.v @@ -0,0 +1 @@ +Definition mynat := nat. diff --git a/test/blackbox-tests/test-cases/coq/rec_module/a/bar.v b/test/blackbox-tests/test-cases/coq/rec_module/a/bar.v new file mode 100644 index 000000000000..b1e4f474ced9 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/rec_module/a/bar.v @@ -0,0 +1,5 @@ +From rec_module Require Import b.foo. +From rec_module Require Import c.ooo. +From rec_module Require c.d.bar. + +Definition mynum (i : mynat) := 3 + ooo_nat + c.d.bar.bar_nat. diff --git a/test/blackbox-tests/test-cases/coq/rec_module/b/foo.v b/test/blackbox-tests/test-cases/coq/rec_module/b/foo.v new file mode 100644 index 000000000000..53e0ce1b1526 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/rec_module/b/foo.v @@ -0,0 +1 @@ +Definition mynat := nat. diff --git a/test/blackbox-tests/test-cases/coq/rec_module/c/d/bar.v b/test/blackbox-tests/test-cases/coq/rec_module/c/d/bar.v new file mode 100644 index 000000000000..b68bd7244fba --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/rec_module/c/d/bar.v @@ -0,0 +1 @@ +Definition bar_nat : nat := 4. diff --git a/test/blackbox-tests/test-cases/coq/rec_module/c/ooo.v b/test/blackbox-tests/test-cases/coq/rec_module/c/ooo.v new file mode 100644 index 000000000000..07d40e567986 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/rec_module/c/ooo.v @@ -0,0 +1 @@ +Definition ooo_nat : nat := 10. diff --git a/test/blackbox-tests/test-cases/coq/rec_module/dune b/test/blackbox-tests/test-cases/coq/rec_module/dune new file mode 100644 index 000000000000..8c8b5efe8661 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/rec_module/dune @@ -0,0 +1,7 @@ +(coqlib + (name rec_module) + ; (public_name dune.test.basic) + (modules :standard) + (synopsis "Test Coq library")) + +(include_subdirs unqualified) diff --git a/test/blackbox-tests/test-cases/coq/rec_module/dune-project b/test/blackbox-tests/test-cases/coq/rec_module/dune-project new file mode 100644 index 000000000000..0f1c4e5f17f9 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/rec_module/dune-project @@ -0,0 +1,3 @@ +(lang dune 1.4) + +(using coq 0.1) diff --git a/test/blackbox-tests/test-cases/coq/run.t b/test/blackbox-tests/test-cases/coq/run.t new file mode 100644 index 000000000000..de134a1dcf70 --- /dev/null +++ b/test/blackbox-tests/test-cases/coq/run.t @@ -0,0 +1,5 @@ + $ dune build --root base --display short --debug-dependency-path @all + Entering directory 'base' + + $ dune build --root rec_module --display short --debug-dependency-path @all + Entering directory 'rec_module'