Uniformize semantics of :> in class after deprecation phase of #16230 #18590
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
coqbot-app
bot
added
the
needs: full CI
proux01
force-pushed
the
cleanup_16230
branch
from
1f06c14
to
9b95a02
Compare
proux01
added
the
request: full CI
proux01
force-pushed
the
cleanup_16230
branch
from
9b95a02
to
27e0859
Compare
coqbot-app
bot
removed
request: full CI
|
The job library:ci-fiat_crypto_legacy has failed in allow failure mode |
proux01
added a commit
to math-comp/analysis
that referenced
this pull request
Jan 31, 2024
proux01
added a commit
to proux01/InteractionTrees
that referenced
this pull request
Jan 31, 2024
proux01
added a commit
to coq-community/coq-ext-lib
that referenced
this pull request
Jan 31, 2024
proux01
added a commit
to math-comp/analysis
that referenced
this pull request
Jan 31, 2024
proux01
added a commit
to coq-community/math-classes
that referenced
this pull request
Jan 31, 2024
proux01
added a commit
to coq-community/math-classes
that referenced
this pull request
Jan 31, 2024
proux01
added a commit
to coq-community/atbr
that referenced
this pull request
Jan 31, 2024
palmskog
added a commit
to coq-community/atbr
that referenced
this pull request
Jan 31, 2024
proux01
added a commit
to proux01/QuickChick
that referenced
this pull request
Jan 31, 2024
proux01
added a commit
to proux01/relation-algebra
that referenced
this pull request
Jan 31, 2024
proux01
added
kind: cleanup
liyishuai
pushed a commit
to QuickChick/QuickChick
that referenced
this pull request
Feb 1, 2024
liyishuai
pushed a commit
to coq-community/coq-ext-lib
that referenced
this pull request
Feb 1, 2024
proux01
added a commit
to coq-community/corn
that referenced
this pull request
Feb 1, 2024
proux01
added
the
request: full CI
proux01
force-pushed
the
cleanup_16230
branch
from
27e0859
to
32444fb
Compare
coqbot-app
bot
removed
the
request: full CI
|
CI green, as far as I'm concerned, this is ready |
|
Still waiting for fcl |
I don't know why f-c-l is still allow failure. It was originally put there due to the intricacy of the tactic scripts, but it has not had an issue that required patching the tactics in a long time, it no longer tries to maintain backwards compatibily, and it has caught bugs that no other CI development has caught. I think it should be moved out of allowed failure. I'll try to create an overlay within the next couple days to a week. The fix is just to replace |
JasonGross
added a commit
to JasonGross/fiat-crypto
that referenced
this pull request
Mar 12, 2024
For coq/coq#18590 Change made with ```bash python -c "$(printf 'import re\nfs = {f:open(f, "r").read() for f in (%s)}\nfs2 = {f:[m for m in re.findall(r"%s", c, flags=re.MULTILINE|re.DOTALL) if not m.startswith("Existing") and ":>" in m and re.search(r"%s", m, flags=re.MULTILINE|re.DOTALL)] for f, c in fs.items()}\nfs3 = {f:m for f, m in fs2.items() if m}\nfs4 = {}\nfor f, m in fs3.items():\n orig = rep = fs[f]\n for val in m:\n rep = rep.replace(val, val.replace(":>", "::"))\n fs4[f] = rep\nfor f, c in fs4.items():\n open(f, "w").write(c)' "$(printf '"%s", ' $(git grep --name-only 'Class '))" '(?:Existing\s+)?Class\s.*?\.\s' ':=\s*{')" ```
JasonGross
reviewed
Mar 12, 2024
doc/changelog/02-specification-language/18590-cleanup_16230.rst
Outdated
Show resolved
Hide resolved
JasonGross
added a commit
to mit-plv/fiat-crypto
that referenced
this pull request
Mar 12, 2024
For coq/coq#18590 Change made with ```bash python -c "$(printf 'import re\nfs = {f:open(f, "r").read() for f in (%s)}\nfs2 = {f:[m for m in re.findall(r"%s", c, flags=re.MULTILINE|re.DOTALL) if not m.startswith("Existing") and ":>" in m and re.search(r"%s", m, flags=re.MULTILINE|re.DOTALL)] for f, c in fs.items()}\nfs3 = {f:m for f, m in fs2.items() if m}\nfs4 = {}\nfor f, m in fs3.items():\n orig = rep = fs[f]\n for val in m:\n rep = rep.replace(val, val.replace(":>", "::"))\n fs4[f] = rep\nfor f, c in fs4.items():\n open(f, "w").write(c)' "$(printf '"%s", ' $(git grep --name-only 'Class '))" '(?:Existing\s+)?Class\s.*?\.\s' ':=\s*{')" ```
proux01
added
the
request: full CI
This way, in next version, we can finally have :> declare a coercion in any record declaration, including typeclasses. Whereas :: consistently declares typeclass instances since Coq 8.18.
coqbot-app
bot
removed
the
request: full CI
|
The job library:ci-fiat_crypto_legacy has failed in allow failure mode |
|
@JasonGross fiat_crypto_legacy is still failing, apparently your script did not handle definitional typeclasses |
JasonGross
added a commit
to JasonGross/fiat-crypto
that referenced
this pull request
Mar 14, 2024
I fixed my script and made mit-plv/fiat-crypto#1830, which will auto-merge once CI finishes running there |
JasonGross
added a commit
to mit-plv/fiat-crypto
that referenced
this pull request
Mar 14, 2024
|
Thanks that seems to work |
SkySkimmer
removed
the
needs: overlay
|
@coqbot merge now |
|
Thanks! |
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 ends the deprecation phases of #16230 and #15802 that introduced :: instead of :> for subclasses in Class declarations. Now :> produces an error in
Classbefore we can make it mean coercion in all record declarations (including typeclasses) in next version.Updated documented syntax by runningmake doc_gram_rsts.Overlays (to be merged before the current PR):
To prepare overlays, just ensure that the code compiles with any Coq >= 8.18 and options
-w +future-coercion-class-constructorand-w +future-coercion-class-field