Conversation
|
This PR includes a second CEP that you proposed a week or two ago. Is that what you intended? |
herbelin
force-pushed
the
discharge-on-the-fly
branch
from
664d8c1 to
90f3ba4
Compare
|
Not intended :(.Sorry, removed. |
| - extending a section content enriches simultaneously and hereditarily all section levels (i.e. `Definition f := t` adds `Top.f` to all section levels, `Top.S.f` to all section levels from level `Top.S`, `Top.S.T.f` to all section levels from level `Top.S.T`, etc.); there are however three kinds of declarations (see below) | ||
| - closing a section drops the active copy of the environment/state and makes active the environment/state of the outer section (which itself growed since the fork) | ||
|
|
||
| ## Definitionally connecting the different copies |
There was a problem hiding this comment.
Definitional equality is not enough in practice, the various copies must also be identified in the following contexts:
- in the syntactic phase of rewrite pattern matching
- in patterns of
Hint - as canonical keys
- in
Searchresults
(and I'm not sure how exhaustive is this list)
There are at least the two following ways to address this problem:
- Use a notation instead of a definition for aliases in each sections
- Call
Declare Equivalent Keysall the time and make sure it is taken into account by every relevant part of the system (and document it properly cf [Declare Equivalent Keys] should be documented rocq#4551).
Ideally, intermediate definitions should be discarded when exiting the section.
(Optionally, also, in the future, it would be nice if re-entering a named section could provide the same context and the same aliases....)
There was a problem hiding this comment.
as canonical keys
In my experiences to provide simultaneously the non-discharged and discharged versions of a canonical key, I had several incompatibilities. Studying the reason of these incompatibilities might help to understand if there is a way to make it working, but that does not seem to be straightforward to support (see for instance the failure on mathcomp I got when the discharged versions of a canonical projection are also allowed to be used).
the various copies must also be identified
By identified, I guess you mean eq_constr-equal (alpha-convertible) vs conv-equal. Is it that you think that it would help compatibility? In any case, I struggled in not breaking too much compatibility in rocq-prover/rocq#17888. I'm a bit pessimistic about the room for manœuver that we have.
(Optionally, also, in the future, it would be nice if re-entering a named section could provide the same context and the same aliases....)
I agree. And it is not impossible to do if we accept to keep the inside of sections in vo files. And, at worst, even if keeping the inner of sections in vo files happens to be too costly in size, we may also recompute dynamically the instances.
[In any case, thanks for your support!]
|
Regarding the drop of |
3 participants
Rendered here.