Skip to content

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

Merged
rgrinberg merged 4 commits intoocaml:masterfrom
ejgallego:coq+compose_local
Mar 18, 2020
Merged

[coq] Allow dependencies and composition with local Coq libraries.#2053
rgrinberg merged 4 commits intoocaml:masterfrom
ejgallego:coq+compose_local

Conversation

@ejgallego
Copy link
Copy Markdown
Collaborator

@ejgallego ejgallego commented Apr 11, 2019 •
edited
Loading

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]

@ejgallego ejgallego added the coq label Apr 11, 2019
@ejgallego ejgallego force-pushed the coq+compose_local branch 12 times, most recently from c5caafd to 14e8916 Compare April 12, 2019 01:57
@ejgallego ejgallego requested a review from a user April 12, 2019 01:57
rgrinberg
rgrinberg requested changes Apr 12, 2019
View reviewed changes
@ejgallego ejgallego force-pushed the coq+compose_local branch 7 times, most recently from a902897 to bf5fff2 Compare April 12, 2019 15:19
@ejgallego
Copy link
Copy Markdown
Collaborator Author

ejgallego commented Apr 12, 2019

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.

@ejgallego ejgallego mentioned this pull request Apr 12, 2019
Open
8 tasks
rgrinberg
rgrinberg reviewed Apr 12, 2019
View reviewed changes
@ejgallego ejgallego force-pushed the coq+compose_local branch 3 times, most recently from bd9d7c4 to 0f1eb64 Compare April 12, 2019 19:24
rgrinberg
rgrinberg reviewed Feb 9, 2020
View reviewed changes
rgrinberg
rgrinberg reviewed Feb 9, 2020
View reviewed changes
@ejgallego ejgallego mentioned this pull request Feb 26, 2020
Merged
@ejgallego ejgallego force-pushed the coq+compose_local branch 3 times, most recently from d22f43f to 9cfed05 Compare February 27, 2020 05:09
@ejgallego
Copy link
Copy Markdown
Collaborator Author

ejgallego commented Mar 7, 2020

Hi folks! It took a while but IMO this is finally ready for merging.

I think code in some parts can be cleaned up a bit, I plan to keep working on this to provide inter-scope composition which is the main next feature we want. I've opted not to implement that yet as in-scope composition is enough to (finally!!) bootstrap Coq.

Testing so far seems pretty positive.

@ejgallego
Copy link
Copy Markdown
Collaborator Author

ejgallego commented Mar 7, 2020

More generally, I think we can refactor the scope code to handle libraries on different languages in less of an ad-hoc way, I will try something in the PR for the inter-scope composition.

@ejgallego ejgallego mentioned this pull request Mar 7, 2020
Merged
@ejgallego
Copy link
Copy Markdown
Collaborator Author

ejgallego commented Mar 7, 2020

I see I'm late for 2.4 by very little O_O @rgrinberg should I move the change entry to 2.4.1 or directly to 2.5?

@Zimmi48
Copy link
Copy Markdown
Contributor

Zimmi48 commented Mar 7, 2020

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

@ejgallego
Copy link
Copy Markdown
Collaborator Author

ejgallego commented Mar 7, 2020

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
Copy link
Copy Markdown
Collaborator Author

ejgallego commented Mar 9, 2020

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

@ejgallego
Copy link
Copy Markdown
Collaborator Author

ejgallego commented Mar 13, 2020

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

rgrinberg
rgrinberg requested changes Mar 18, 2020
View reviewed changes
rgrinberg
rgrinberg reviewed Mar 18, 2020
View reviewed changes
rgrinberg
rgrinberg reviewed Mar 18, 2020
View reviewed changes
rgrinberg
rgrinberg reviewed Mar 18, 2020
View reviewed changes
@rgrinberg
Copy link
Copy Markdown
Member

rgrinberg commented Mar 18, 2020 •
edited
Loading

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

@ejgallego
[coq] Allow dependencies and composition with local Coq libraries.
b411ec7 
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>
@ejgallego
[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>
@ejgallego
[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
Copy link
Copy Markdown
Collaborator Author

ejgallego commented Mar 18, 2020

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.

@rgrinberg
Clean up monad handling
e72ee32 
Make it more like the way we handle applicative

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>
@rgrinberg
Copy link
Copy Markdown
Member

rgrinberg commented Mar 18, 2020

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
Copy link
Copy Markdown
Collaborator Author

ejgallego commented Mar 18, 2020

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.

@ejgallego ejgallego mentioned this pull request Mar 19, 2020
Closed
@rgrinberg rgrinberg mentioned this pull request Apr 10, 2020
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@rgrinberg rgrinberg rgrinberg requested changes

@emillon emillon Awaiting requested review from emillon

@nojb nojb Awaiting requested review from nojb

+1 more reviewer

@Zimmi48 Zimmi48 Zimmi48 left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

coq

Projects

Coq + Dune
Archived in project

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@ejgallego @Zimmi48 @cpitclaudel @rgrinberg