Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove Printing Primitive Projection Compatibility #9306

Merged
merged 1 commit into from Feb 18, 2019

Conversation

@SkySkimmer
Copy link
Contributor

commented Jan 4, 2019

The code to generate the legacy bodies is moved to its only user in
extraction.

It almost seems like we could remove it (ie no special extraction code
for primitive projection constants) but then we run into issues with
automatic unboxing eg Record foo := { a : nat; b : a <= 5 }. gets
extracted to type foo = nat and (if we remove the special code) let a = a.

@ppedrot

ppedrot approved these changes Jan 4, 2019

Copy link
Member

left a comment

I am supportive of this change. I regularly stumble on this piece of code, wish to remove it and realize the printing option is still there.

@maximedenes maximedenes self-assigned this Jan 4, 2019

@herbelin

This comment has been minimized.

Copy link
Member

commented Jan 4, 2019

I'm ok with this PR, but native projections seem to still be under-exploited. A roadmap would probably be useful. For instance, it seems that it would be a good objective to move the most standard projections (e.g. fst, snd, proj1_sig, proj2_sig,projT1_sig, projT2_sig, ...) to a compact representation with minimal compatibility break. If we can do it, users will be able to do it for their own records with minimal efforts. Is it a kind of objective that we could target for 2019?

@maximedenes

This comment has been minimized.

Copy link
Member

commented Jan 10, 2019

This needs a CHANGES entry. Also, was the option undocumented?

@SkySkimmer SkySkimmer force-pushed the SkySkimmer:remove-projection-legacy-match branch from 43d607a to bf6fba1 Jan 10, 2019

@SkySkimmer SkySkimmer requested a review from coq/doc-maintainers as a code owner Jan 10, 2019

@SkySkimmer

This comment has been minimized.

Copy link
Contributor Author

commented Jan 10, 2019

was the option undocumented

It was incorrectly documented as on by default.

Remove Printing Primitive Projection Compatibility
The code to generate the legacy bodies is moved to its only user in
extraction.

It almost seems like we could remove it (ie no special extraction code
for primitive projection constants) but then we run into issues with
automatic unboxing eg `Record foo := { a : nat; b : a <= 5 }.` gets
extracted to `type foo = nat` and (if we remove the special code) `let
a = a`.

@SkySkimmer SkySkimmer force-pushed the SkySkimmer:remove-projection-legacy-match branch from bf6fba1 to 723f443 Jan 10, 2019

user-level, and one must use the :flag:`Printing Primitive Projection Compatibility`
to display unfolded primitive projections as matches and distinguish them from folded ones.
user-level, and there is no way to display unfolded projections differently
from folded ones.

This comment has been minimized.

Copy link
@SkySkimmer

SkySkimmer Jan 10, 2019

Author Contributor

I just noticed this change as sphinx was failing due to missing ref. This is pretty bad IMO, maybe we should delay the PR.

This comment has been minimized.

Copy link
@Zimmi48

Zimmi48 Jan 16, 2019

Member

Impressive what the user documentation (with fatal warnings) can do to help the developers 😃

@Zimmi48
Copy link
Member

left a comment

Change looks OK beyond the issue noted by Gaëtan. In particular, since it is a printing option, and thus has no semantics impact, it feels acceptable to remove it without deprecating it first.

user-level, and one must use the :flag:`Printing Primitive Projection Compatibility`
to display unfolded primitive projections as matches and distinguish them from folded ones.
user-level, and there is no way to display unfolded projections differently
from folded ones.

This comment has been minimized.

Copy link
@Zimmi48

Zimmi48 Jan 16, 2019

Member

Impressive what the user documentation (with fatal warnings) can do to help the developers 😃

@SkySkimmer

This comment has been minimized.

Copy link
Contributor Author

commented Feb 18, 2019

If nobody decides to merge this within a week I'll take it as a decision to keep the option for now, and so I'll close the PR.

@ppedrot

This comment has been minimized.

Copy link
Member

commented Feb 18, 2019

@maximedenes it seems that there is no opposition, isn't there? If you don't have time to merge this in @SkySkimmer's window I'll do it.

@maximedenes

This comment has been minimized.

Copy link
Member

commented Feb 18, 2019

it seems that there is no opposition, isn't there

Indeed, so let's merge. Sorry, I missed this PR because of the "needs: discussion" label. But IIRC, it was discussed during the last WG. Or at least the general plan around primitive projections was.

@maximedenes maximedenes merged commit 723f443 into coq:master Feb 18, 2019

7 of 9 checks passed

GitLab CI pipeline Pipeline completed with errors on GitLab CI
Details
library:ci-fiat-crypto job_execution_timeout on GitLab CI
Details
Pull request checks Passed.
Details
continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details
coq.coq Build #20190110.18 succeeded
Details
doc:ml-api:odoc: ml-api artifact Link to ml-api build artifact.
Details
doc:refman: refman artifact Link to refman build artifact.
Details
doc:refman: stdlib artifact Link to stdlib build artifact.
Details

maximedenes added a commit that referenced this pull request Feb 18, 2019

Merge PR #9306: Remove Printing Primitive Projection Compatibility
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: ppedrot

@SkySkimmer SkySkimmer deleted the SkySkimmer:remove-projection-legacy-match branch Feb 19, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.