Introduce a [coq.extraction] stanza #3299

rgrinberg · 2020-03-27T04:51:12Z

We can list the prelude module and the list of OCaml modules produced.
Dune will then know that compiling this coq file produces a set of ml
sources.

@ejgallego I've opted for something extremely simple so that the current
coq+dune users at least have something usable for now.

TODO

Add documentation
Factor common field handling between theory and extract

ejgallego · 2020-03-27T05:07:31Z

Great, thanks! I'll have a look ASAP , note this may close #2178

ejgallego · 2020-03-27T05:08:45Z

I'm going to validate this CompCert and MetaCoq; IMO if we can cover these use cases [or at least be sure the current approach will work] we can be happy.

src/dune/coq_rules.ml

src/dune/dune_file.ml

rgrinberg · 2020-03-27T06:14:33Z

Are these four last field common with coq.theory ? As mentioned above, another possibility would be to attach the extraction fields to coq.theory ; I guess this way is a bit more flexible tho.

That’s how I went about things originally. But then I realized I needed some sort of map syntax to associate coq modules to the list of source they extracted. After that, I thought about the public/private distinction for extracted code and couldn’t decide if the extracted code of public libraries should be installed or not. In the end I just gave up and went with this simpler approach. The solutions aren’t mutually exclusive or we could always change our mind since we have proper versioning. The code duplication between the fields is something I intend to fix in the next few commits. We have a Buildable.t value for sharing common fields between executables and libraries. I think we should have something similar here.

…

On Mar 26, 2020, 10:49 PM -0700, Emilio Jesús Gallego Arias ***@***.***>, wrote: @ejgallego commented on this pull request. In src/dune/dune_file.ml: > @@ -1976,6 +1976,43 @@ module Coqpp = struct type Stanza.t += T of t end +let coq_syntax = + Dune_lang.Syntax.create ~name:"coq" ~desc:"the coq extension (experimental)" + [ ((0, 1), `Since (1, 9)); ((0, 2), `Since (2, 5)) ] + +module Coq_extract = struct + type t = + { extracted_modules : Module_name.t list + ; prelude : Loc.t * Coq_module.Name.t + ; flags : Ordered_set_lang.Unexpanded.t + ; libraries : (Loc.t * Lib_name.t) list + ; theories : (Loc.t * Coq_lib_name.t) list + ; loc : Loc.t + } Are these four last field common with coq.theory ? As mentioned above, another possibility would be to attach the extraction fields to coq.theory ; I guess this way is a bit more flexible tho. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or unsubscribe.

cpitclaudel · 2020-03-27T13:08:03Z

Very exciting! Can you clarify how this works? If I have a file xyz.v that extracts a single ml file xyz.ml, do I just say (extract_module xyz)?

rgrinberg · 2020-03-27T16:40:11Z

Very exciting! Can you clarify how this works? If I have a file xyz.v that extracts a single ml file xyz.ml, do I just say (extract_module xyz)?

Something like this:

(coq.extract
 (prelude xyz)
 (extracted_modules xyz))

cpitclaudel · 2020-03-27T16:55:44Z

Super. And then the ocaml side can depend on that xyz?

rgrinberg · 2020-03-27T17:08:47Z

Super. And then the ocaml side can depend on that xyz?

Yeah. It's treated as a normal source to be used in libraries & executables.

ejgallego · 2020-03-27T18:53:39Z

@rgrinberg , DCO is missing; from a quick review this looks pretty good; I'll do some testing this weekend. Let me know when you remove the WIP tag.

rgrinberg · 2020-03-28T01:03:28Z

@ejgallego I re-orged things a little bit.

There's now a Coq_rules.Context.t that is shared among the various rule generation functions. It's analogous to the Compilation_context.t we use for compiling OCaml code.
All coq related stanzas now live in Coq_stanza. I think it pays off to leave our code separately from the rest of the dune stuff as much as possible.

src/dune/coq_stanza.ml

ejgallego · 2020-03-28T05:31:54Z

@ejgallego I re-orged things a little bit.

Awesome, thanks @rgrinberg ! I'll have a look ASAP and perform some testing.

rgrinberg · 2020-03-28T06:28:51Z

That’s the default casing coq chooses for extracted sources that don’t correspond to .v files. See Datatypes.ml in the tests for example.

…

On Mar 27, 2020, 11:18 PM -0700, Emilio Jesús Gallego Arias ***@***.***>, wrote: @ejgallego commented on this pull request. In src/dune/coq_stanza.ml: > List.concat_map t.extracted_modules ~f:(fun m -> let m = Module_name.to_string m in + let m = + if String.Caseless.equal prelude m then I mean Extraction vs Separate Extraction etc... actually, how did you manage to generate Foo.ml in your first message? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or unsubscribe.

ejgallego · 2020-03-28T06:41:24Z

That’s the default casing coq chooses for extracted sources that don’t correspond to .v files. See Datatypes.ml in the tests for example.

Actually that's because the Coq module is Datatypes.v, see in Prelude:

Require Export Datatypes.

so in a sense it is respecting the case; should it not?

test/blackbox-tests/test-cases/coq/extract/run.t

src/dune/coq_stanza.ml

rgrinberg · 2020-03-28T17:10:39Z

Yeah I suppose this is the simplest way about things.

…

On Mar 28, 2020, 8:40 AM -0700, Emilio Jesús Gallego Arias ***@***.***>, wrote: @ejgallego commented on this pull request. In test/blackbox-tests/test-cases/coq/extract/run.t: > @@ -16,7 +16,7 @@ $ cat >dune <<EOF > (coq.extract > (prelude extract) - > (extracted_modules Datatypes Extract)) + > (extracted_modules datatypes extract)) So indeed Coq's convention is respect the capitalization of the original module, AFAICT OCaml doesn't care about this, so why not use here Datatypes extract ? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or unsubscribe.

ejgallego · 2020-03-28T17:36:52Z

doc/dune-files.rst

+
+- ``<optional-fields>`` are ``flags``, ``theories``, and ``libraries``. All of
+  these fields have the same meaning as in the ``coq.theory`` stanza.
+


IMHO it would be worth nothing that the extracted modules will become usable from a regular (library ,...) stanza; quite a few users of this feature will be new to Dune and this will not be obvious to them.

Makes sense. By the way, what do you think of introducing coq.rst for all coq related documentation? That page would include a tutorial style introduction and a reference of all the coq related stanzas.

👍
It used to exist but was removed in the recent refactoring of the refman. But it would be great if it was reintroduced.

Indeed it used to be its own, self-contained section; but was removed in favor of merging into the general stanza file. Personally I think it makes more sense the old way, so I'm all for it.

Old chapter can be seen here https://github.com/ocaml/dune/blob/1.11.4/doc/coq.rst

I see. Was there a discussion regarding this change? I’d like to see the arguments for keeping everything in one place.

doc/dune-files.rst

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

simplifies passing usual arguments Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

Preserve the orginal case written by users Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

* Stop passing it along with super_context * In coq, use Context.run to guarantee that we never forget this dir Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

So that we can re-use for extraction Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

* For extraction, we use the current dir * For compilation, we use the build_dir Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

rgrinberg · 2020-03-30T19:07:48Z

I see. I made the change you've suggested.

Let's keep things simple for now and just evolve it based on user's needs and the changes in coq itself.

@vzaliva is another user that asked for extraction support. See if this PR works for you.

ejgallego · 2020-03-30T22:13:05Z

I see. I made the change you've suggested.

Thanks, things seem fine in my testing; please merge when you want.

Let's keep things simple for now and just evolve it based on user's needs and the changes in coq itself.

Indeed; as far as I can see all the issues I've seen are really Coq problems upstream so I'd rather fix Coq than to add more workarounds in Dune.

[coq] Introduce a coq.extraction stanza We can list the prelude module and the list of OCaml modules produced. Dune will then know that compiling this coq file produces a set of ml sources.

@diml

…lugin, dune-private-libs and dune-glob (2.5.0) CHANGES: - Add a `--release` option meaning the same as `-p` but without the package filtering. This is useful for custom `dune` invocation in opam files where we don't want `-p` (ocaml/dune#3260, @diml) - Fix a bug introduced in 2.4.0 causing `.bc` programs to be built with `-custom` by default (ocaml/dune#3269, fixes ocaml/dune#3262, @diml) - Allow contexts to be defined with local switches in workspace files (ocaml/dune#3265, fix ocaml/dune#3264, @rgrinberg) - Delay expansion errors until the rule is used to build something (ocaml/dune#3261, fix ocaml/dune#3252, @rgrinberg, @diml) - [coq] Support for theory dependencies and compositional builds using new field `(theories ...)` (ocaml/dune#2053, @ejgallego, @rgrinberg) - From now on, each version of a syntax extension must be explicitely tied to a minimum version of the dune language. Inconsistent versions in a `dune-project` will trigger a warning for version <=2.4 and an error for versions >2.4 of the dune language. (ocaml/dune#3270, fixes ocaml/dune#2957, @voodoos) - [coq] Bump coq lang version to 0.2. New coq features presented this release require this version of the coq lang. (ocaml/dune#3283, @ejgallego) - Prevent installation of public executables disabled using the `enabled_if` field. Installation will now simply skip such executables instead of raising an error. (ocaml/dune#3195, @voodoos) - `dune upgrade` will now try to upgrade projects using versions <2.0 to version 2.0 of the dune language. (ocaml/dune#3174, @voodoos) - Add a `top` command to integrate dune with any toplevel, not just utop. It is meant to be used with the new `#use_output` directive of OCaml 4.11 (ocaml/dune#2952, @mbernat, @diml) - Allow per-package `version` in generated `opam` files (ocaml/dune#3287, @toots) - [coq] Introduce the `coq.extraction` stanza. It can be used to extract OCaml sources (ocaml/dune#3299, fixes ocaml/dune#2178, @rgrinberg) - Load ppx rewriters in dune utop and add pps field to toplevel stanza. Ppx extensions will now be usable in the toplevel (ocaml/dune#3266, fixes ocaml/dune#346, @stephanieyou) - Add a `(subdir ..)` stanza to allow evaluating stanzas in sub directories. (ocaml/dune#3268, @rgrinberg) - Fix a bug preventing one from running inline tests in multiple modes (ocaml/dune#3352, @diml) - Allow the use of the `%{profile}` variable in the `enabled_if` field of the library stanza. (ocaml/dune#3344, @mrmr1993) - Allow the use of `%{ocaml_version}` variable in `enabled_if` field of the library stanza. (ocaml/dune#3339, @voodoos) - Fix dune build freezing on MacOS when cache is enabled. (ocaml/dune#3249, fixes #ocaml/dune#2973, @artempyanykh)

rgrinberg requested a review from a user March 27, 2020 04:51

rgrinberg requested a review from ejgallego as a code owner March 27, 2020 04:51

ejgallego mentioned this pull request Mar 27, 2020

Feature request: support for extracted OCaml files in Coq builds #2178

Closed

rgrinberg commented Mar 27, 2020

View reviewed changes

src/dune/coq_rules.ml Outdated Show resolved Hide resolved

ejgallego reviewed Mar 27, 2020

View reviewed changes

src/dune/dune_file.ml Outdated Show resolved Hide resolved

rgrinberg force-pushed the extraction branch from 849b1ae to 36f2e8e Compare March 27, 2020 19:04

rgrinberg requested review from emillon and nojb as code owners March 27, 2020 21:50

rgrinberg force-pushed the extraction branch from a1e793d to 02de68b Compare March 28, 2020 01:00

rgrinberg changed the title ~~[WIP] Introduce a [coq.extract] stanza~~ Introduce a [coq.extract] stanza Mar 28, 2020

rgrinberg commented Mar 28, 2020

View reviewed changes

src/dune/coq_stanza.ml Outdated Show resolved Hide resolved

ejgallego reviewed Mar 28, 2020

View reviewed changes

test/blackbox-tests/test-cases/coq/extract/run.t Outdated Show resolved Hide resolved

ejgallego reviewed Mar 28, 2020

View reviewed changes

src/dune/coq_stanza.ml Show resolved Hide resolved

rgrinberg force-pushed the extraction branch from ecd8a56 to b19ec1c Compare March 28, 2020 17:31

ejgallego reviewed Mar 28, 2020

View reviewed changes

Zimmi48 reviewed Mar 28, 2020

View reviewed changes

doc/dune-files.rst Outdated Show resolved Hide resolved

rgrinberg force-pushed the extraction branch from 30efed2 to 3ccc65a Compare March 28, 2020 19:08

rgrinberg added 21 commits March 30, 2020 11:54

[coq] Use DuneExtraction as the dummy wrapper name

e0a5aed

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

Factor out flag handling

0f14b16

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

[coq] move bootstrap to own module

6b4847f

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

[coq] move stanzas to [Coq_stanza]

9c388ec

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

[coq] document coq.extract

1cce500

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

[coq] Introduce Coq.Context

2dd4000

simplifies passing usual arguments Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

[coq] Add coq flags to Context

04b9b19

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

[coq] Add more fields to Coq_rules.Context

991ed95

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

[coq] treat extracted list of strings

e32d2fd

Preserve the orginal case written by users Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

[coq] update docs

10557f8

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

[coq] Move boot_type to context

7ca5339

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

[coq] little re-org

4888857

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

[coq] Use correct dir for ml_target_names

3a27436

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

Simplify build_dir handling

9dac391

* Stop passing it along with super_context * In coq, use Context.run to guarantee that we never forget this dir Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

[coq] move source_rule to own function

4222b58

So that we can re-use for extraction Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

[coq] improve coqdep errors

8e0e8b0

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

[coq] run coqdep out of correct dir

ee74014

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

[coq] make coq.extract use coqdep

e50324d

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

[coq] rename extract to extraction

584d082

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

Update CHANGES

9b11e6e

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

[coq] change dir of coqc depending on purpose

2ca3397

* For extraction, we use the current dir * For compilation, we use the build_dir Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

rgrinberg force-pushed the extraction branch from 941ec06 to 2ca3397 Compare March 30, 2020 19:06

rgrinberg merged commit 623706d into ocaml:master Mar 31, 2020

rgrinberg mentioned this pull request Apr 10, 2020

[new release] dune-build-info, dune, dune-configurator, dune-action-plugin, dune-private-libs and dune-glob (2.5.0) ocaml/opam-repository#16170

Merged

ejgallego mentioned this pull request Feb 4, 2021

Allow to have a coq.extraction and coq.theory in the same directory #4158

Open

Alizter added the coq label Jun 6, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Introduce a [coq.extraction] stanza #3299

Introduce a [coq.extraction] stanza #3299

rgrinberg commented Mar 27, 2020 •

edited

Loading

ejgallego commented Mar 27, 2020

ejgallego commented Mar 27, 2020

rgrinberg commented Mar 27, 2020 via email

cpitclaudel commented Mar 27, 2020

rgrinberg commented Mar 27, 2020

cpitclaudel commented Mar 27, 2020

rgrinberg commented Mar 27, 2020

ejgallego commented Mar 27, 2020

rgrinberg commented Mar 28, 2020

ejgallego commented Mar 28, 2020

rgrinberg commented Mar 28, 2020 via email

ejgallego commented Mar 28, 2020 •

edited

Loading

rgrinberg commented Mar 28, 2020 via email

ejgallego Mar 28, 2020

rgrinberg Mar 28, 2020

Zimmi48 Mar 28, 2020

ejgallego Mar 28, 2020

rgrinberg Mar 28, 2020

rgrinberg commented Mar 30, 2020

ejgallego commented Mar 30, 2020


		- ``<optional-fields>`` are ``flags``, ``theories``, and ``libraries``. All of
		these fields have the same meaning as in the ``coq.theory`` stanza.

Introduce a [coq.extraction] stanza #3299

Introduce a [coq.extraction] stanza #3299

Conversation

rgrinberg commented Mar 27, 2020 • edited Loading

TODO

ejgallego commented Mar 27, 2020

ejgallego commented Mar 27, 2020

rgrinberg commented Mar 27, 2020 via email

cpitclaudel commented Mar 27, 2020

rgrinberg commented Mar 27, 2020

cpitclaudel commented Mar 27, 2020

rgrinberg commented Mar 27, 2020

ejgallego commented Mar 27, 2020

rgrinberg commented Mar 28, 2020

ejgallego commented Mar 28, 2020

rgrinberg commented Mar 28, 2020 via email

ejgallego commented Mar 28, 2020 • edited Loading

rgrinberg commented Mar 28, 2020 via email

ejgallego Mar 28, 2020

Choose a reason for hiding this comment

rgrinberg Mar 28, 2020

Choose a reason for hiding this comment

Zimmi48 Mar 28, 2020

Choose a reason for hiding this comment

ejgallego Mar 28, 2020

Choose a reason for hiding this comment

rgrinberg Mar 28, 2020

Choose a reason for hiding this comment

rgrinberg commented Mar 30, 2020

ejgallego commented Mar 30, 2020

rgrinberg commented Mar 27, 2020 •

edited

Loading

ejgallego commented Mar 28, 2020 •

edited

Loading