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

Standardize handling of Automatic Introduction. #8820

Merged
merged 1 commit into from Nov 9, 2018

Conversation

Projects
None yet
5 participants
@jashug
Copy link
Contributor

commented Oct 25, 2018

This fixes #8791.
We explicitly specify for intro the names of binders which are given by the user. This still can suffer from spurious collisions, see #8819. The implementation is factored out of Lemmas.start_proof_with_initialization.

Kind: bug fix

  • Added / updated test-suite

@jashug jashug requested review from mattam82 and ppedrot as code owners Oct 25, 2018

@jashug jashug force-pushed the jashug:instance-paramter-names-refresh branch from c5cbb5b to 9364efa Oct 25, 2018

@coqbot coqbot removed the needs: rebase label Oct 25, 2018

@Zimmi48 Zimmi48 added the kind: fix label Oct 25, 2018

@jashug jashug force-pushed the jashug:instance-paramter-names-refresh branch from 9364efa to fde28e0 Oct 25, 2018

@jashug jashug requested a review from ejgallego Oct 25, 2018

jashug added a commit to jashug/color that referenced this pull request Oct 26, 2018

Remove duplicate abstraction.
`A` is abstracted over as a section parameter; there is no need to
duplicate that.
Adds compatibility with coq/coq#8820.
@jashug

This comment has been minimized.

Copy link
Contributor Author

commented Oct 26, 2018

A number of developments are now failing, mostly collisions with section variables as far as I can tell. I'll take a shot at writing overlays.

jashug added a commit to jashug/fiat-crypto that referenced this pull request Oct 26, 2018

Remove duplicate abstraction
`base_type` and `base_interp` are already abstracted by the section.
For compatibility with coq/coq#8820.

jashug added a commit to jashug/HoTT that referenced this pull request Oct 26, 2018

Adapt to coq/coq#8820
`EquivalenceInduction.v` had two premises named `HP`.
The changes in `InitialTerminalCategory/` are to avoid coq/coq#8819.

@jashug jashug referenced this pull request Oct 26, 2018

Merged

Adapt to coq/coq#8820 #966

@jashug jashug force-pushed the jashug:instance-paramter-names-refresh branch from fde28e0 to 8722db2 Oct 26, 2018

jashug added a commit to jashug/QuickChick that referenced this pull request Oct 26, 2018

Deduplicate premise name
Change from premises `H1, H2, H2, H3` to `H1, H2, H3, H4`.
Adds compatibility with coq/coq#8820.
@ppedrot
Copy link
Member

left a comment

It's going to be hard to be backward compatible, but the new behaviour looks definitely better.

@ppedrot ppedrot self-assigned this Oct 26, 2018

@ppedrot ppedrot added this to the 8.10+beta1 milestone Oct 26, 2018

fblanqui added a commit to fblanqui/color that referenced this pull request Oct 26, 2018

Remove duplicate abstraction.
`A` is abstracted over as a section parameter; there is no need to
duplicate that.
Adds compatibility with coq/coq#8820.

jashug added a commit to jashug/corn that referenced this pull request Oct 26, 2018

Name premises to avoid collision
This commit adds compatibility with coq/coq#8820.
One `Instance` declaration in `ode/metric.v` appears to fall prey
to coq/coq#8819, naming the premises avoids the problem.

@jashug jashug force-pushed the jashug:instance-paramter-names-refresh branch from 8722db2 to 7283c29 Oct 26, 2018

@jashug jashug force-pushed the jashug:instance-paramter-names-refresh branch from 7283c29 to cb21a12 Oct 26, 2018

@coqbot coqbot removed the needs: rebase label Oct 26, 2018

@jashug

This comment has been minimized.

Copy link
Contributor Author

commented Oct 26, 2018

4 overlays remaining (EDIT: 3, since quickchick was just merged). elpi and math-comp appear to be spurious (and I saw elpi work earlier, though math-comp could be hiding an incompatibility). The Iris part of iris-lambda-rust should go though once lambda-rust bumps their pin. Most of the changes are of one of two types:

Instance type1 (H1 : T) (H1 : T) : R.

Section sec.
Variable X : T.
Instance type2 (X : T) : R.

Where the first one is fixed by deduplicating the premise name (always an unintentional overlap, as far as I could tell) and the second one can be fixed by not abstracting over X : T on the Instance, but leaving the generalization until after the section closes. (This is not always possible, but none of the examples I've looked at were making use of the extra generality within the section)

Issue #8819 also cropped up twice.

For backwards compatibility, there should always be some alpha-renaming that is backwards compatible, though I'd struggle to define sufficient conditions.

jashug added a commit to jashug/HoTT that referenced this pull request Oct 29, 2018

Adapt to coq/coq#8820
`EquivalenceInduction.v` had two premises named `HP`.
The changes in `InitialTerminalCategory/` are to avoid coq/coq#8819.

JasonGross added a commit to mit-plv/fiat-crypto that referenced this pull request Oct 29, 2018

Remove duplicate abstraction
`base_type` and `base_interp` are already abstracted by the section.
For compatibility with coq/coq#8820.

spitters added a commit to HoTT/HoTT that referenced this pull request Nov 3, 2018

@jashug jashug force-pushed the jashug:instance-paramter-names-refresh branch from cb21a12 to 93338cc Nov 4, 2018

@jashug

This comment has been minimized.

Copy link
Contributor Author

commented Nov 4, 2018

All the overlays have been merged. The builds failing on GitLab are the same as failed on the last run of master. In particular, iris-lambda-rust passed. I believe all the failures are spurious and this PR is ready to be merged.

@jashug jashug removed the needs: overlay label Nov 4, 2018

@Zimmi48

This comment has been minimized.

Copy link
Member

commented Nov 5, 2018

There's now a conflict in CHANGES (although this is the one exception when it is OK to solve the merge conflict when merging).

@ppedrot

This comment has been minimized.

Copy link
Member

commented Nov 6, 2018

@jashug can you rebase to get a clean CI run? I'll merge after that.

@jashug jashug force-pushed the jashug:instance-paramter-names-refresh branch from 93338cc to 88a3f90 Nov 6, 2018

@ppedrot

This comment has been minimized.

Copy link
Member

commented Nov 7, 2018

Fiat-crypto died of an out of memory error, I don't know if this is related. I think it used to compile with this PR, right?

@jashug

This comment has been minimized.

Copy link
Contributor Author

commented Nov 7, 2018

If I remember correctly, fiat-crypto was broken on master last time master was run. So I do not believe I have seen this PR compile with fiat-crypto. Unfortunately.

Standardize handling of Automatic Introduction.
This fixes #8791.
We explicitly specify for intro the names of binders which are
given by the user. This still can suffer from spurious collisions,
see #8819.

@jashug jashug force-pushed the jashug:instance-paramter-names-refresh branch from 88a3f90 to 46f6b27 Nov 9, 2018

@ppedrot ppedrot merged commit 46f6b27 into coq:master Nov 9, 2018

4 checks passed

ci/gitlab/pr-8820 Pipeline passed on GitLab
Details
continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details
doc:refman Link to refman build artifact.
Details

ppedrot added a commit that referenced this pull request Nov 9, 2018

@jashug jashug deleted the jashug:instance-paramter-names-refresh branch Dec 4, 2018

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.