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 broken bench job flocq3 #16853

Merged
merged 1 commit into from Nov 21, 2022
Merged

Conversation

SkySkimmer
Copy link
Contributor

They've been broken for a long time

@SkySkimmer SkySkimmer requested a review from a team as a code owner November 18, 2022 21:38
@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 Nov 18, 2022
@JasonGross
Copy link
Member

What's wrong with rewriter-perf-SuperFast? (It's not supposed to be broken)

@SkySkimmer
Copy link
Contributor Author

- File "./src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap/_10_SuperFast.v", line 3, characters 11-27:
- Error: Illegal application: 
- The term "NatUtil.Thunked.nat_rect" of type "forall P : Type, (unit -> P) -> (nat -> P -> P) -> nat -> P"
- cannot be applied to the terms
-  "list Z" : "Set"
-  "fun H : Z => repeat H (Z.to_nat 1)" : "Z -> list Z"
- The 2nd term has type "Z -> list Z" which should be coercible to "unit -> list Z".

any bench in the last ? months

@JasonGross
Copy link
Member

- File "./src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap/_10_SuperFast.v", line 3, characters 11-27:
- Error: Illegal application: 
- The term "NatUtil.Thunked.nat_rect" of type "forall P : Type, (unit -> P) -> (nat -> P -> P) -> nat -> P"
- cannot be applied to the terms
-  "list Z" : "Set"
-  "fun H : Z => repeat H (Z.to_nat 1)" : "Z -> list Z"
- The 2nd term has type "Z -> list Z" which should be coercible to "unit -> list Z".

any bench in the last ? months

Sorry, I'll fix this shortly, and make sure it doesn't break again (apparently this was missing from the CI of rewriter). Please don't remove from the bench though. (Feel free to move it to the end of the list or whatever though)

JasonGross added a commit to JasonGross/rewriter that referenced this pull request Nov 19, 2022
@JasonGross
Copy link
Member

The rewriter issue should be fixed by mit-plv/rewriter#88 once I finish and merge it

@SkySkimmer SkySkimmer changed the title Remove broken bench jobs (flocq3, rewriter-perf-SuperFast) Remove broken bench job flocq3 Nov 19, 2022
JasonGross added a commit to JasonGross/rewriter that referenced this pull request Nov 20, 2022
@ppedrot ppedrot self-assigned this Nov 21, 2022
@ppedrot ppedrot added kind: infrastructure CI, build tools, development tools. and removed needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Nov 21, 2022
@ppedrot ppedrot added this to the 8.17+rc1 milestone Nov 21, 2022
@ppedrot
Copy link
Member

ppedrot commented Nov 21, 2022

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 67db136 into coq:master Nov 21, 2022
@SkySkimmer SkySkimmer deleted the bench-broken branch November 21, 2022 21:52
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: infrastructure CI, build tools, development tools.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants