Skip to content

Conversation

@Villetaneuse
Copy link
Contributor

Give to Logic/Adjointification.v and Reals/Rtrigo_facts.v the same permissions as the other files in the stdlib (rw-r--r--).

This is a glorious PR, achieving +0/-0 modifications.

@Villetaneuse Villetaneuse requested review from a team as code owners December 6, 2023 19:03
@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
@ppedrot ppedrot self-assigned this Dec 7, 2023
@ppedrot
Copy link
Member

ppedrot commented Dec 8, 2023

@coqbot run full ci

@coqbot-app coqbot-app bot 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 8, 2023
@Villetaneuse
Copy link
Contributor Author

Certainly nothing could really be broken by the fact that two .v files had x permissions and now do not.
Here are the failures:
jasmin:

File "./lang/varmap.v", line 1013, characters 4-7:
Error:
In environment
wsw : WithSubWord
vm1 : ?B → ?A
vm2 : ?B → ?A
vm1' : Vm.t
vm2' : Vm.t
d : Sv.t
The term "vm1" has type "?B → ?A" while it is expected to have type "Vm.t".

unimath : timeout
metacoq:

File "./theories/Syntax/PCUICOnFreeVars.v", line 57, characters 7-34:
Error: The LHS of (shiftnP_add 1)
    (shiftnP 1 (shiftnP _ _) _)
does not match any subterm of the goal
Command exited with non-zero status 1

test-suite:base:dev: timeout

Give to Logic/Adjointification.v and Reals/Rtrigo_facts.v the same
permissions as the other files in the stdlib (rw-r--r--).
@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 9, 2023
@Villetaneuse
Copy link
Contributor Author

@coqbot run full ci

@coqbot-app coqbot-app bot 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 9, 2023
@ppedrot
Copy link
Member

ppedrot commented Dec 9, 2023

@Villetaneuse one is never cautious enough. The failures do look unrelated but that means that the CI on master is quite broken. We already knew about jasmin, but now metacoq is also broken.

@SkySkimmer
Copy link
Contributor

We know about metacoq too, cf MetaRocq/metarocq#1028

@coqbot-app
Copy link
Contributor

coqbot-app bot commented Dec 9, 2023

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

@ppedrot ppedrot added the kind: internal API, ML documentation... label Dec 10, 2023
@ppedrot ppedrot added this to the 8.20+rc1 milestone Dec 10, 2023
@ppedrot
Copy link
Member

ppedrot commented Dec 10, 2023

@coqbot merge now

@coqbot-app coqbot-app bot merged commit a38dada into rocq-prover:master Dec 10, 2023
@Villetaneuse Villetaneuse deleted the consistent_perms branch December 10, 2023 17:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

kind: internal API, ML documentation...

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants