Keyword global for cloning theories
#764
Conversation
|
Thanks! Running CI now. I am not sure about the addition of a keyword. Could this be done without? As a broader thing to consider (not for this PR), I think we don't need locality or globality information until typing, so perhaps they could be passed in using the option mechanism instead of blocking a keyword? This may then make it simpler to also extend locality to the case of nested sections (a longstanding grumble), for example as @strub what do we think? Follow-up issue? @loutr , please do run locally on the examples as well. (Make check should take care of those once stdlib is done.) It is not your responsibility to fix proofs in the external CI, only to liaise with their maintainer. (I think I'll add "write contributor guidelines" up as an issue, and add a maintainer field to the external CI config.) |
|
Sorry for the weekend delay.. It would be best indeed to incorporate this new "global" semantics within the existing syntax, but it is so user-directed that I don't see how to do it in a consistent way. I don't know about this option mechanism but I'd be glad to adapt this PR to it. Otherwise, this little work started from a discussion with @bgregoir, which we shared later on with @strub. As for the examples, I forgot to mention it but I also did run them successfully (apart from the |
|
I agree with you Francois we can/should certainly use something like #[global] but for uniformity we should also replace local with #[local] and what about "declare". And do we want to do this in the same PR ? |
|
Not in the same PR for sure. Given that this does not break external CI (I was worried about introducing |
|
For the |
strub
left a comment
strub
left a comment
There was a problem hiding this comment.
We have a single commit policy. Please, squash your PR.
strub
left a comment
strub
left a comment
There was a problem hiding this comment.
Could you add a simple unit test in tests/?
|
I added a few comments. Otherwise, we are good to go. |
Provides a new `global` keyword that can be used with theory cloning (as opposed to local), that typically allows to reexport (sub)theories of an otherwise local theory. feat: added global keyword and control flow modification fix: fix local overriding behaviour fix: use correct (relocalised) item for checking feat(printing): display theory locality feat: apply correct locality to cloned _theories_ style(add_item hook): reduce passing around of the `override_locality` parameter fix: still change locality when within local scope feat(cloning): notify change on visibility style(section): more readable `generalize_ctheorem` function feat(parser): make the `global` keyword non-reserved test: unit test for the `global` keyword cloning functionality
loutr
force-pushed
the
global-clone-keyword
branch
from
5c08a51 to
bfdf4da
Compare
Sorry, I thought it would be done automatically upon rebase, it's done.
Done, I deem it satisfactory but feel free to also make comments about it. |
4 participants
This pull request adds a
globalkeyword that ensures thatgives public visibility to newly-cloned items from theory
A. This might be useful in patterns likein order to reexport only specific parts of interest from a given theory
A. It does not change the standard behaviourthat
clone A as Bpreserves the visibility ofAfor items ofB. Commit df336f8 provides an information message when this happens when cloning a local theory (withcloneand notlocal clone), and also informs on the existence of theglobalkeyword.This also addresses issue #747, because it gives the right visibility to the new theory itself, and not only its items; which properly clears the theory and escapes the assertion failure.
This has been tested on the standard library successfully but was not otherwise submitted to more tests; I will of course try to fix errors if they arise.