[coq] Allow dependencies and composition with local Coq libraries. #2053

ejgallego · 2019-04-11T22:05:44Z

We support simple composition of Coq libraries using the
(theories ...) field. The main changes are:

Coq libraries now have a Coq_lib.t type
Stanza scanning does now initialize a Coq_lib.DB, per
scope. Supporting inter-scope public libraries is left for a future
PR.
We properly compose when the stdlib is in scope, this allows to have
a compositional build with Coq itself; note that as of today, in a
composed build the stdlib prefix Coq is introduced qualified; this
reflects upstream roadmap of deprecating implicit libs. See comment
in Scope.public_libs

We have added tests for:

simple composition
composition with plugin
cyclic composition
boot composition [disabled until Coq 8.12 is released]
inter-scope composition [fails for now]

We leave for future work:

Allow to depend on theories in a different scope
Allow to depend on theories installed globally, likely this will
require the 2.0 version of the Coq language
Validation of Coq library names should be improved [clarify upstream
rules]

Includes changes by Rudi Grinberg [many suggestions] and Théo
Zimmerman [documentation review]

src/coq_lib.ml

src/coq_lib.mli

src/coq_rules.ml

src/dune_file.ml

ejgallego · 2019-04-12T15:34:53Z

Ok, so I am reasonably happy with this; testing seems to be doing fine and the code is not too horrible.

A big todo is indeed to define the notion of coq libraries names, this is a slightly complex issue so I'll think about it a couple of days [as the library names are really wrappers and there can be overlapping].

IMHO I think it does make sense to add both closure and the possibility to depend on globally-installed libs on this PR; no point on having the users go thru incomplete steps.

src/coq_rules.ml

Zimmi48 · 2020-03-07T11:32:32Z

Even if (boot) is mostly for internal use, it would seem better if it were documented, no?

ejgallego · 2020-03-07T18:28:51Z

Even if (boot) is mostly for internal use, it would seem better if it were documented, no?

I'm reluctant to have it documented yet, it is too unstable. Note that it was not introduced in this PR.

ejgallego · 2020-03-09T22:52:47Z

Rebased, @rgrinberg I'll wait to merge until your change request is lifted.

ejgallego · 2020-03-13T21:28:33Z

Added a couple of cleanups + check on private vs public libs.

src/dune/coq_lib.ml

src/dune/coq_lib_name.ml

src/dune/coq_rules.ml

rgrinberg · 2020-03-18T09:48:17Z

I had a first pass. Everything looks mostly fine. I think this is good to go for 2.5

We support simple composition of Coq libraries using the `(theories ...)` field. The main changes are: - Coq libraries now have a `Coq_lib.t` type - Stanza scanning does now initialize a `Coq_lib.DB`, per scope. Supporting inter-scope public libraries is left for a future PR. - We properly compose when the stdlib is in scope, this allows to have a compositional build with Coq itself; note that as of today, in a composed build the stdlib prefix `Coq` is introduced qualified; this reflects upstream roadmap of deprecating implicit libs. See comment in `Scope.public_libs` We have added tests for: - simple composition - composition with plugin - cyclic composition - boot composition [disabled until Coq 8.12 is released] - inter-scope composition [fails for now] We leave for future work: - Allow to depend on theories in a different scope - Allow to depend on theories installed globally, likely this will require the 2.0 version of the Coq language - Validation of Coq library names should be improved [clarify upstream rules] Includes changes by Rudi Grinberg [many suggestions] and Théo Zimmerman [documentation review] Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

We place them into a module; error handling in this part could indeed use more work but this is a first step. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

For now we follow very simple rules, public theories cannot depend on any way on private ones. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

ejgallego · 2020-03-18T20:08:34Z

I had a first pass. Everything looks mostly fine. I think this is good to go for 2.5

Thanks @rgrinberg , comments addressed, except for the one on Result_monad which I'm not sure what should be done.

I'm gonna submit the second part of this, supporting inter-scope composition, that should hopefully make the construction of the Coq_lib.DB less intrusive and a bit more modular.

Make it more like the way we handle applicative Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

rgrinberg · 2020-03-18T22:47:51Z

Looks good so far. I'd like to see a lot of the DB handling stuff to be consistent between coq & ocaml, but I suppose there's no rush.

ejgallego · 2020-03-18T22:56:24Z

Thanks @rgrinberg !

I'd like to see a lot of the DB handling stuff to be consistent between coq & ocaml, but I suppose there's no rush.

For now I'm going to separate the handling a bit more so the code is aware of different DBs , we will see how it looks. I think in the coq-lang 1.0 version we will be a bit limited on what we can do; hopefully once we revise the model and stop supporting coq_makefile we should be able to improve things.

This PR is a RFC, as it is not clear what we'd like to do here. There are two choices to support libraries : - extend native Dune scope [current approach, introduced by ocaml#2053] - make Super_context aware of the existence of different scope DB Both approaches have strengths and weaknesses; the first one for example forces to extend some `Lib` internals and indeed a few checks there don't really make sense for Coq; the second approach introduces some code duplication. It seems to me that the approach this PR proposes could make more sense; code duplication could be solved by using some programming abstractions.

This PR is a RFC, as I'm not convinced at all this should be the way to go before we introduce handling of public Coq theories as to allow their inter-scope composition. The current approach to handling Coq theories ─ introduced in ocaml#2053 ─ modified `Scope` and `Lib` adding a new library-like stanza type, `Coq_theory`. However, handling of libraries and theories is quite different so the above approach led to a few spurious code cases. There are two choices to improve this situation before we introduce `coq_public_libs`: - refactor `Scope` a bit more so we don't have to mess with `Lib.library_related_stanza` That's one option but still seems a bit invasive and messy for `scope.ml`. - split all Coq-related scope code to `Coq_scope` and handle things there. This is what this PR does. This approach does introduce some code duplication, so it is not clear if it is indeed a gain w.r.t. current status-quo. Code duplication could be solved by using some programming abstractions. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

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

ejgallego added the coq label Apr 11, 2019

ejgallego requested review from emillon and rgrinberg as code owners April 11, 2019 22:05

ejgallego force-pushed the coq+compose_local branch 12 times, most recently from c5caafd to 14e8916 Compare April 12, 2019 01:57

ejgallego requested a review from a user April 12, 2019 01:57

rgrinberg requested changes Apr 12, 2019

View reviewed changes

src/coq_lib.ml Outdated Show resolved Hide resolved

src/coq_lib.mli Outdated Show resolved Hide resolved

src/coq_rules.ml Outdated Show resolved Hide resolved

src/coq_rules.ml Outdated Show resolved Hide resolved

src/dune_file.ml Outdated Show resolved Hide resolved

ejgallego force-pushed the coq+compose_local branch 7 times, most recently from a902897 to bf5fff2 Compare April 12, 2019 15:19

ejgallego mentioned this pull request Apr 12, 2019

[coq] 1.0 version coq language version meta-issue #1998

Open

8 tasks

rgrinberg reviewed Apr 12, 2019

View reviewed changes

src/coq_rules.ml Outdated Show resolved Hide resolved

ejgallego force-pushed the coq+compose_local branch 3 times, most recently from bd9d7c4 to 0f1eb64 Compare April 12, 2019 19:24

ejgallego force-pushed the coq+compose_local branch from e6acc17 to ad17af8 Compare March 9, 2020 22:52

ejgallego force-pushed the coq+compose_local branch 2 times, most recently from aa96f7a to 326c1ee Compare March 13, 2020 21:28

ejgallego requested a review from rgrinberg March 16, 2020 11:30

ejgallego force-pushed the coq+compose_local branch 2 times, most recently from 758d8ac to 9722700 Compare March 18, 2020 08:26

rgrinberg requested changes Mar 18, 2020

View reviewed changes

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

rgrinberg reviewed Mar 18, 2020

View reviewed changes

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

rgrinberg reviewed Mar 18, 2020

View reviewed changes

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

rgrinberg reviewed Mar 18, 2020

View reviewed changes

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

ejgallego added 3 commits March 18, 2020 16:05

[coq] Refactor Coq_lib errors messages

5e59623

We place them into a module; error handling in this part could indeed use more work but this is a first step. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

[coq] Don't allow public theories to depend on private ones.

c912149

For now we follow very simple rules, public theories cannot depend on any way on private ones. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

ejgallego force-pushed the coq+compose_local branch from 9722700 to c912149 Compare March 18, 2020 20:05

Clean up monad handling

e72ee32

Make it more like the way we handle applicative Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

rgrinberg merged commit 71ac33f into ocaml:master Mar 18, 2020

ejgallego deleted the coq+compose_local branch March 18, 2020 22:54

ejgallego mentioned this pull request Mar 19, 2020

[coq] Introduce Coq_scope #3280

Closed

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

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[coq] Allow dependencies and composition with local Coq libraries. #2053

[coq] Allow dependencies and composition with local Coq libraries. #2053

ejgallego commented Apr 11, 2019 •

edited

Loading

ejgallego commented Apr 12, 2019

Zimmi48 commented Mar 7, 2020

ejgallego commented Mar 7, 2020

ejgallego commented Mar 9, 2020

ejgallego commented Mar 13, 2020

rgrinberg commented Mar 18, 2020 •

edited

Loading

ejgallego commented Mar 18, 2020

rgrinberg commented Mar 18, 2020

ejgallego commented Mar 18, 2020

[coq] Allow dependencies and composition with local Coq libraries. #2053

[coq] Allow dependencies and composition with local Coq libraries. #2053

Conversation

ejgallego commented Apr 11, 2019 • edited Loading

ejgallego commented Apr 12, 2019

Zimmi48 commented Mar 7, 2020

ejgallego commented Mar 7, 2020

ejgallego commented Mar 9, 2020

ejgallego commented Mar 13, 2020

rgrinberg commented Mar 18, 2020 • edited Loading

ejgallego commented Mar 18, 2020

rgrinberg commented Mar 18, 2020

ejgallego commented Mar 18, 2020

ejgallego commented Apr 11, 2019 •

edited

Loading

rgrinberg commented Mar 18, 2020 •

edited

Loading