8000 [ssr] Backport from MathComp by pi8027 · Pull Request #18374 · rocq-prover/rocq · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

[ssr] Backport from MathComp #18374

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 2 commits into from
Dec 7, 2023
Merged

[ssr] Backport from MathComp #18374

merged 2 commits into from
Dec 7, 2023

Conversation

pi8027
Copy link
Contributor
@pi8027 pi8027 commented Dec 6, 2023 •
edited
Loading

This PR contains the backport of the following PRs:

  • [ ] Added / updated test-suite.
  • Added changelog.
  • Added / updated documentation.
    • [ ] Documented any new / changed user messages.
    • [ ] Updated documented syntax by running make doc_gram_rsts.
  • Opened overlay pull requests.

@pi8027 pi8027 requested a review from a team as a code owner December 6, 2023 14:23
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Dec 6, 2023
@pi8027
Copy link
Contributor Author
pi8027 commented Dec 6, 2023

The implicit status of some lemmas looks weird to me, and I don't know what to do with them. So, I'm postponing the backport of the following PRs:

@pi8027 pi8027 added this to the 8.20+rc1 milestone Dec 6, 2023
pi8027 added a commit to math-comp/math-comp that referenced this pull request Dec 6, 2023
@pi8027
Cleanup backported stuff following rocq-prover/rocq#18374
7ce7c74
proux01
proux01 reviewed Dec 6, 2023
View reviewed changes
@proux01 proux01 changed the title Backport from MathComp [ssr] Backport from MathComp Dec 6, 2023
@proux01 proux01 added kind: cleanup Code removal, deprecation, refactorings, etc. part: ssreflect The SSReflect proof language. labels Dec 6, 2023
pi8027 added a commit to math-comp/math-comp that referenced this pull request Dec 6, 2023
@pi8027
Cleanup backported stuff following rocq-prover/rocq#18374
c777358
@proux01 proux01 removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Dec 7, 2023
@proux01 proux01 self-assigned this Dec 7, 2023
@proux01
Copy link
Contributor
proux01 commented Dec 7, 2023

This has already been tested in mathcomp's CI so @pi8027 if you add a changelog entry telling fun_scope is deprecated in favor of function_scope, I'll merge.

@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Dec 7, 2023
@pi8027
Copy link
Contributor Author
pi8027 commented Dec 7, 2023

Done.

@pi8027 pi8027 force-pushed the backport-mathcomp branch from 6cd8605 to a545405 Compare December 7, 2023 11:05
@proux01 proux01 removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Dec 7, 2023
@proux01
Copy link
Contributor
proux01 commented Dec 7, 2023

@coqbot merge now

@coqbot-app coqbot-app bot merged commit ec5438c into rocq-prover:master Dec 7, 2023
@pi8027 pi8027 deleted the backport-mathcomp branch December 7, 2023 15:51
@pi8027 pi8027 mentioned this pull request Dec 7, 2023
Merged
3 tasks
@SkySkimmer
Copy link
Contributor

This broke CI jasmin https://gitlab.inria.fr/coq/coq/-/jobs/3672075 analysis https://gitlab.inria.fr/coq/coq/-/jobs/3672063

@SkySkimmer SkySkimmer mentioned this pull request Dec 7, 2023
Merged
@proux01
Copy link
Contributor
proux01 commented Dec 7, 2023 •
edited
Loading

Analysis should be fixed. Maybe jasmin too, otherwise we can probably temporarily make jasmin allow_failure, it should soon move to MC 2 anyway jasmin-lang/jasmin#560

@proux01
Copy link
Contributor
proux01 commented Dec 7, 2023

But indeed, I should have remembered that we still have MC1 in the CI here.

@SkySkimmer
Copy link
Contributor
SkySkimmer commented Dec 7, 2023 •
edited
Loading

You should have run full CI regardless

proux01 added a commit to proux01/coq that referenced this pull request Dec 8, 2023
@proux01
[CI] Temporarily turn jasmin allow_failure
3f7e13f 
Currently broken because I forgot to run CI before merging
rocq-prover#18374

I'm currently working on a fix but it may take me a pair of days.
@proux01 proux01 mentioned this pull request Dec 8, 2023
Merged
@SkySkimmer
Copy link
Contributor

Metacoq also broke https://gitlab.inria.fr/coq/coq/-/jobs/3672093

@proux01
Copy link
Contributor
proux01 commented Dec 8, 2023

I'm looking at it.

@herbelin herbelin mentioned this pull request Dec 8, 2023
Merged
1 task
proux01 added a commit to proux01/metacoq that referenced this pull request Dec 8, 2023
@proux01
Fix breakage from rocq-prover/rocq#18374
b4575af
@proux01 proux01 mentioned this pull request Dec 8, 2023
Merged
@proux01
Copy link
Contributor
proux01 commented Dec 8, 2023

Here is a fix for Metacoq: MetaRocq/metarocq#1028

ppedrot added a commit to MetaRocq/metarocq that referenced this pull request Dec 9, 2023
@ppedrot
Merge pull request #1028 from proux01/fix_coq_18374
9b70a13 
Fix breakage from rocq-prover/rocq#18374
proux01 added a commit to proux01/jasmin that referenced this pull request Dec 10, 2023
@proux01
Fix after rocq-prover/rocq#18374
e9d5d81 
Te PR rocq-prover/rocq#18374 moved the "_ =1 _"
notation of ssreflect from function_scope to type_scope.
This requires some disembiguation wit the "_ =1 _" of Jasmin in vm_scope.
@proux01 proux01 mentioned this pull request Dec 10, 2023
Merged
proux01 pushed a commit to math-comp/math-comp that referenced this pull request Dec 11, 2023
@pi8027 @proux01
Cleanup backported stuff following rocq-prover/rocq#18374
5db5e2d
vbgl pushed a commit to jasmin-lang/jasmin that referenced this pull request Dec 11, 2023
@proux01
Fix uses of the “_ =1 _” notation
3b41b22 
The PR rocq-prover/rocq#18374 moved the "_ =1 _"
notation of ssreflect from function_scope to type_scope.
This requires some disembiguation wit the "_ =1 _" of Jasmin in vm_scope.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@proux01 proux01 proux01 left review comments

@gares gares gares approved these changes

Assignees

@proux01 proux01

Labels
kind: cleanup Code removal, deprecation, refactorings, etc. part: ssreflect The SSReflect proof language.
Projects
None yet
Milestone
8.20+rc1
Development

Successfully merging this pull request may close these issues.
4 participants
@pi8027 @proux01 @SkySkimmer @gares
0