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

ejgallego · 2019-03-22T02:56:40Z

Dear Dune devs, this is a reworked partial version of #1555 , which only includes the very basic handling of Coq modules and rules.

We piggyback on the local support for dir traversal when (include_subdirs qualified) is enabled to build qualified Coq modules.

I have tested this on a few developments that use recursive modules and so far it works well :)

Below is the commit message:

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:

(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 e+git@x80.org

ejgallego · 2019-03-22T16:14:01Z

Something I don't understand is why vo files are not built on @all, if I target them explicitly, or when adding the install rules, things work well.

src/coq_rules.mli

rgrinberg · 2019-03-25T09:27:17Z

src/coq_rules.ml

+    SC.resolve_program ~dir sctx prg ~loc:None ~hint:"try: opam install coq" in
+  { coqdep = rr "coqdep"
+  ; coqc   = rr "coqc"
+  ; coqpp  = rr "coqpp"


Is there a plan to use coqpp in the future? I don't see it being used anywhere now?

Yes, I'd like to use it to do .mlg -> .ml conversion; I still didn't implement it as I am testing with Coq 8.8 and coqpp was introduced in coq 8.9 so I need to figure out what the best way to conditionally detect it is.

src/coq_module.ml

doc/coq.rst

emillon · 2019-03-25T09:22:57Z

src/coq_module.ml

@@ -0,0 +1,50 @@
+(* This file is licensed under The MIT License *)


I'm not sure this header is necessary given DCO. Someone from Jane Street should comment on this :)

(same for all similar headers)

I thought it would be safer to explicitly state the license :) No problem doing whatever is needed in this area.

emillon · 2019-03-25T09:24:11Z

src/coq_rules.ml

+
+let coq_debug = false
+
+(* TODO:                                       *)


I'd suggest doing this, opening an issue, or removing this comment 🙂

Comment removed; I will indeed open an issue (in the Coq repos) to discuss what library model should Dune + Coq support. There are a few design decisions to make.

emillon · 2019-03-25T09:28:43Z

src/coq_rules.ml

+  ]
+
+let create_ccoq sctx ~dir =
+  let rr prg =


how about renaming this resolve?

Btw, this record might not be entirely useful. First of all, resolve_program is actually cached os there's no need to save its result. Second of all, when we change our rules to take advantage of memoization it's best to just ask for values that you actually use. This will help track dependencies more accurately and re-run less stuff. I will leave it up to you if you want to make the change however, there's no immediate need.

Sounds, good; I have scheduled a removal of the record. I find it useful for now as to quickly see what we do require in the toolchain.

src/coq_rules.ml

emillon · 2019-03-25T09:29:56Z

src/dir_contents.ml

@@ -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 ? *)


don't forget this part :)

I was planning to tackle this a part of #1555 where we add support for depending on Coq plugins, however this may be the wrong place to do it as this should affect the regular library stanza, will remove it for now I think.

src/dune_file.ml

src/stdune/option.mli

rgrinberg · 2019-03-25T09:34:04Z

@ejgallego could you add a test for the @all bug that you're observing. I realize that this might be a bit painful as you will need a fake coqpp/coqc, but we'll need those for tests regardless so we might as well.

Is the issue only caused in (include_subdirs qualified) mode btw?

ejgallego · 2019-03-25T10:11:32Z

Thanks a lot folks, I've done a pass.

@ejgallego could you add a test for the @all bug that you're observing. I realize that this might be a bit painful as you will need a fake coqpp/coqc, but we'll need those for tests regardless so we might as well.

There is a test already using the coq domain, should I lift it to the general case?

Is the issue only caused in (include_subdirs qualified) mode btw?

I̶ ̶d̶o̶n̶'̶t̶ ̶t̶h̶i̶n̶k̶ ̶s̶o̶,̶ ̶i̶f̶ ̶y̶o̶u̶ ̶l̶o̶o̶k̶ ̶a̶t̶ ̶t̶h̶e̶ ̶o̶u̶t̶p̶u̶t̶ ̶o̶f̶ ̶t̶h̶e̶ ̶t̶e̶s̶t̶s̶ ̶[̶a̶n̶d̶ ̶t̶h̶e̶ ̶d̶i̶f̶f̶ ̶w̶i̶t̶h̶ ̶h̶t̶t̶p̶s̶:̶/̶/̶g̶i̶t̶h̶u̶b̶.̶c̶o̶m̶/̶e̶j̶g̶a̶l̶l̶e̶g̶o̶/̶d̶u̶n̶e̶/̶t̶r̶e̶e̶/̶c̶o̶q̶+̶r̶e̶c̶u̶r̶s̶i̶v̶e̶+̶i̶n̶s̶t̶a̶l̶l̶ ̶w̶h̶e̶r̶e̶ ̶t̶h̶e̶ ̶i̶n̶s̶t̶a̶l̶l̶ ̶r̶u̶l̶e̶s̶ ̶w̶o̶r̶k̶a̶r̶o̶u̶n̶d̶ ̶t̶h̶e̶ ̶b̶u̶g̶]̶ ̶i̶t̶ ̶s̶e̶e̶m̶s̶ ̶t̶o̶ ̶h̶a̶p̶p̶e̶n̶ ̶i̶n̶ ̶b̶o̶t̶h̶ ̶m̶o̶d̶e̶s̶.̶

Note that I am using (include_subdirs unqualified) as an alias for coq-qualified.

ejgallego · 2019-03-25T11:44:27Z

Is the issue only caused in (include_subdirs qualified) mode btw?

Update @rgrinberg , indeed the issue is only present in that case, sorry for the wrong diagnosis; it seems that the @all alias doesn't see the targets in the subdirs.

Zimmi48 · 2019-03-25T12:21:58Z

doc/coq.rst

+******
+
+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


Actually, a Coq project could contain OCaml files without being a plugin. There is a specific (and standard case) which is an OCaml project where some OCaml files are automatically extracted from Coq files, and some others are hand-written. At some point, it would be good to have good Dune support for this.

A Coq plugin is a Coq project containing OCaml files that link to the Coq API.

I will refine this a bit; but indeed I will not talk about extraction until we get support for it.

Zimmi48 · 2019-03-25T12:23:59Z

doc/coq.rst

+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``


I am not sure I understand the choice of -R over -Q which was IIMN the recommended choice these days.

I think virtually no library will compile with -Q, note that once installed -Q is implicit as of today given that coqtop includes the top level user-contribs.

We need to discuss the library model indeed, but I'll open an issue for that as there are many complications. For now this PR and 1555 will just reach the point single libraries can be handled properly as in coq makefile.

I suggest you leave this for now and just create an issue. We'll address this in a subsequent PR.

Understood, thanks!

Many libraries actually rely on -Q as of today and it would be good that there is no regression for these libraries (as coq_makefile supports the two options). That being said, I can understand that this is still experimental support and could be seen as a later refinement.

rgrinberg · 2019-03-25T12:39:37Z

Update @rgrinberg , indeed the issue is only present in that case, sorry for the wrong diagnosis; it seems that the @ALL alias doesn't see the targets in the subdirs.

Yeah, this issue actually affects OCaml as well. The only reason why the situation wasn't observed is that the archive targets would be included in @all and those would pick up the sub-targets.

I suggest you leave this for now and just create an issue. We'll address this in a subsequent PR.

src/dir_contents.ml

ejgallego · 2019-03-25T17:49:14Z

@rgrinberg @ejgallego I'd recommend adding a separate Travis job using one of the Docker images there: https://github.com/coq-community/docker-coq. This would avoid the need for recompiling Coq.

Thanks @Zimmi48 , that's indeed another option; we could even test that in a separate repos [and do more comprehensive testing]

At least the problem here is that we have many options to choose from :) in this case it is a good problem to have :)

I added the real thing, which admittedly is very heavy, just to be sure we were testing the real beast :)

p.s: @rgrinberg most of the time complexity of installing Coq does indeed stem from the fact the Coq has no modular build; so opam will build a large package including the standard library which is quite heavy; the core of Coq is much lighter [dune compiles it in my laptop in less than 2 mins]

Indeed, we are not very far from the moment we can split the stdlib from the coq package, even coqdep could be packaged independently, which in this case would add just a few seconds to the compilation.

Zimmi48 · 2019-03-26T09:26:33Z

That's a good point @ejgallego given that the Dune support is precisely what is going to make this splitting possible.

This is a cherry-pick of the directory traversal parts from the Dune PR (ocaml#1968). I was uncomfortable with the misnaming done there, so this PR enables the `(include_subdirs qualified)` syntax and provides a `local` part to the traversal so clients [such as the Coq mode] can use it. Note that this does introduce a bit of overhead in the tree traversal, especially in deep trees, it should be possible to optimize if we deem it necessary.

This is a cherry-pick of the directory traversal parts from the Dune PR (ocaml#1968). I was uncomfortable with the misnaming done there, so this PR enables the `(include_subdirs qualified)` syntax and provides a `local` part to the traversal so clients [such as the Coq mode] can use it. Note that this does introduce a bit of overhead in the tree traversal, especially in deep trees, it should be possible to optimize if we deem it necessary. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

ejgallego · 2019-03-26T16:32:09Z

This PR now depends on #1980 , IMHO once that one is in, we could merge this without too much problem.

This is a cherry-pick of the directory traversal parts from the Dune PR (ocaml#1968). I was uncomfortable with the misnaming done there, so this PR enables the `(include_subdirs qualified)` syntax and provides a `local` part to the traversal so clients [such as the Coq mode] can use it. Note that this does introduce a bit of overhead in the tree traversal, especially in deep trees, it should be possible to optimize if we deem it necessary. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

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 <e+git@x80.org>

Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

rgrinberg · 2019-03-29T05:16:20Z

However, this doesn't seem straightforward. In particular, we may have
to re-implement Lib.DB which is not trivial.

To keep things simple, let's follow Jeremie's advice (he's usually right about this stuff) and start with just copying lib.ml into coqlib.ml and ripping out all the stuff that's irrelevant to coq (selects, variants, virtual libraries). We can always find common abstractions later.

Something that might be of interest to you is the discussion regarding resolved names: #1900 (comment)

I believe this idea could be quite useful as well and perhaps all languages supported by dune can be handled the same way at this name resolution level.

ejgallego · 2019-03-29T07:45:01Z

To keep things simple, let's follow Jeremie's advice (he's usually right about this stuff) and start with just copying lib.ml into coqlib.ml and ripping out all the stuff that's irrelevant to coq (selects, variants, virtual libraries). We can always find common abstractions later.

Something that might be of interest to you is the discussion regarding resolved names: #1900 (comment)

I believe this idea could be quite useful as well and perhaps all languages supported by dune can be handled the same way at this name resolution level.

Thanks @rgrinberg , indeed it'd be great to share the same resolution level; I will open an specific issue for the Coq library model [in the coq repos] tho; there are some minor nits to be addressed, in particular w.r.t. how things work with "legacy" libs.

A very annoying thing for example is that Coq installs OCaml and Coq modules all together, so having a transition plan needs some thinking.

rgrinberg · 2019-03-29T08:29:36Z

A very annoying thing for example is that Coq installs OCaml and Coq modules all together, so having a transition plan needs some thinking.

You're talking about the stdlib, right? Or the installation using the coq generate makefile?

ejgallego · 2019-03-29T08:30:32Z

You're talking about the stdlib, right? Or the installation using the coq generate makefile?

Both, but coq_makefile is the main problem here.

ejgallego added the coq label Mar 22, 2019

ejgallego requested a review from a user March 22, 2019 02:56

ejgallego requested review from emillon and rgrinberg as code owners March 22, 2019 02:56

ejgallego force-pushed the coq+recursive branch 6 times, most recently from 41cb9d1 to 721472a Compare March 22, 2019 04:30

rgrinberg reviewed Mar 25, 2019

View reviewed changes

src/coq_rules.mli Outdated Show resolved Hide resolved

rgrinberg reviewed Mar 25, 2019

View reviewed changes

src/coq_module.ml Outdated Show resolved Hide resolved

emillon reviewed Mar 25, 2019

View reviewed changes

ejgallego force-pushed the coq+recursive branch from 721472a to a23b9d4 Compare March 25, 2019 10:08

ejgallego force-pushed the coq+recursive branch 2 times, most recently from 04750a2 to 596d8fa Compare March 25, 2019 10:17

Zimmi48 mentioned this pull request Mar 25, 2019

[coq] Allow Coq libraries to depend on OCaml ones. #1555

Merged

ejgallego force-pushed the coq+recursive branch from 596d8fa to 125b030 Compare March 25, 2019 11:42

ejgallego force-pushed the coq+recursive branch 2 times, most recently from aaba6c5 to 695d746 Compare March 25, 2019 12:07

ejgallego changed the title ~~[lang] Preliminary Coq support, core part with recursive modules.~~ [lang] Preliminary Coq support, core part with recursively qualified modules. Mar 25, 2019

ejgallego force-pushed the coq+recursive branch from 695d746 to ca79eaa Compare March 25, 2019 12:12

Zimmi48 reviewed Mar 25, 2019

View reviewed changes

rgrinberg reviewed Mar 25, 2019

View reviewed changes

src/dir_contents.ml Outdated Show resolved Hide resolved

rgrinberg approved these changes Mar 25, 2019

View reviewed changes

aalekseyev mentioned this pull request Mar 26, 2019

Memoize dir contents #1979

Merged

ejgallego mentioned this pull request Mar 26, 2019

[dir_contents] Allow qualified traversal of directories. #1980

Merged

ejgallego force-pushed the coq+recursive branch from 22903c6 to 07e243c Compare March 26, 2019 16:31

ejgallego force-pushed the coq+recursive branch from 07e243c to 3585fd5 Compare March 26, 2019 16:31

ejgallego force-pushed the coq+recursive branch from 3585fd5 to 28c7739 Compare March 26, 2019 16:35

ejgallego force-pushed the coq+recursive branch from 28c7739 to d971316 Compare March 27, 2019 15:42

ejgallego force-pushed the coq+recursive branch from d971316 to 0815f1e Compare March 27, 2019 16:46

ejgallego force-pushed the coq+recursive branch from 0815f1e to db2ed20 Compare March 28, 2019 13:39

ejgallego force-pushed the coq+recursive branch from db2ed20 to 95bbd20 Compare March 28, 2019 15:24

ejgallego added 2 commits March 29, 2019 00:36

[travis] Enable Coq tests [using OPAM]

0181fbc

Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

ejgallego force-pushed the coq+recursive branch from 95bbd20 to 0181fbc Compare March 28, 2019 23:36

ejgallego merged commit e82c70f into ocaml:master Mar 29, 2019

ejgallego deleted the coq+recursive branch March 29, 2019 02:11

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

ejgallego commented Mar 22, 2019 •

edited

Loading

ejgallego commented Mar 22, 2019

rgrinberg Mar 25, 2019

ejgallego Mar 25, 2019

emillon Mar 25, 2019

emillon Mar 25, 2019

ejgallego Mar 25, 2019

emillon Mar 25, 2019

ejgallego Mar 25, 2019

emillon Mar 25, 2019

rgrinberg Mar 25, 2019

ejgallego Mar 25, 2019

emillon Mar 25, 2019

ejgallego Mar 25, 2019 •

edited

Loading

rgrinberg commented Mar 25, 2019

ejgallego commented Mar 25, 2019 •

edited

Loading

ejgallego commented Mar 25, 2019

Zimmi48 Mar 25, 2019

ejgallego Mar 25, 2019

Zimmi48 Mar 25, 2019

ejgallego Mar 25, 2019

ejgallego Mar 25, 2019

Zimmi48 Mar 25, 2019

rgrinberg commented Mar 25, 2019

ejgallego commented Mar 25, 2019

Zimmi48 commented Mar 26, 2019

ejgallego commented Mar 26, 2019

rgrinberg commented Mar 29, 2019

ejgallego commented Mar 29, 2019

rgrinberg commented Mar 29, 2019

ejgallego commented Mar 29, 2019

		@@ -0,0 +1,50 @@
		(* This file is licensed under The MIT License *)

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

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

Conversation

ejgallego commented Mar 22, 2019 • edited Loading

ejgallego commented Mar 22, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ejgallego Mar 25, 2019 • edited Loading

Choose a reason for hiding this comment

rgrinberg commented Mar 25, 2019

ejgallego commented Mar 25, 2019 • edited Loading

ejgallego commented Mar 25, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

rgrinberg commented Mar 25, 2019

ejgallego commented Mar 25, 2019

Zimmi48 commented Mar 26, 2019

ejgallego commented Mar 26, 2019

rgrinberg commented Mar 29, 2019

ejgallego commented Mar 29, 2019

rgrinberg commented Mar 29, 2019

ejgallego commented Mar 29, 2019

ejgallego commented Mar 22, 2019 •

edited

Loading

ejgallego Mar 25, 2019 •

edited

Loading

ejgallego commented Mar 25, 2019 •

edited

Loading