[coq] Introduce Coq_scope #3280
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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>
ejgallego
added a commit
to ejgallego/dune
that referenced
this pull request
Mar 19, 2020
We make the handling of Coq theories to be independent of `Lib`, which deals with OCaml libs. This is in preparation for the introduction of composition with inter-scope public Coq theories. This is softer alternative to ocaml#3280, at the cost of introducing some uglier code in `Scope`.
ejgallego
added a commit
to ejgallego/dune
that referenced
this pull request
Mar 19, 2020
We make the handling of Coq theories to be independent of `Lib`, which deals with OCaml libs. This is in preparation for the introduction of composition with inter-scope public Coq theories. This is softer alternative to ocaml#3280, at the cost of introducing some uglier code in `Scope`. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
|
What semantics for coq scopes do you have in mind? If they are the same as OCaml, I think it makes sense to keep a single scope for all libraries. Yes, you must deal with some spurious cases, but the end result is consistent semantics and the same interface for OCaml, Coq, (and C) libraries. I think that's quite valuable. |
|
Indeed it seems to me that we can keep the same scope semantics; closing this experiment as it doesn't make a lot of sense. |
ejgallego
added a commit
to ejgallego/dune
that referenced
this pull request
Mar 19, 2020
We make the handling of Coq theories to be independent of `Lib`, which deals with OCaml libs. This is in preparation for the introduction of composition with inter-scope public Coq theories. This is softer alternative to ocaml#3280, at the cost of introducing some uglier code in `Scope`. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
stephanieyou
pushed a commit
to stephanieyou/dune
that referenced
this pull request
Apr 7, 2020
We make the handling of Coq theories to be independent of `Lib`, which deals with OCaml libs. This is in preparation for the introduction of composition with inter-scope public Coq theories. This is softer alternative to ocaml#3280, at the cost of introducing some uglier code in `Scope`. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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 #2053 ─
modified
ScopeandLibadding 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
Scopea bit more so we don't have to mess withLib.library_related_stanzaThat's one option but still seems a bit invasive and messy for
scope.ml, implemented in [coq] Rework Coq_lib.DB handling as not to interfere withLib#3281 .split all Coq-related scope code to
Coq_scopeand handle thingsthere. 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.
What you think folks (cc: @rgrinberg ) I lean towards taking #3281
Signed-off-by: Emilio Jesus Gallego Arias e+git@x80.org