Build fails on 8.11

[JasonGross]

COQC /home/runner/work/coqutil/coqutil/src/coqutil/Datatypes/ListSet.v
Error: Tactic failure: Proof search failed.

Please fix, or revert 4986e2638c376283c2e015795b57434fc9e42f6d. This breaks fiat-crypto's opam package CI

[JasonGross]

(Should we protect the master branch of coqutil and demand that future changes be made via PR?)

[JasonGross]

cc @samuelgruetter

[samuelgruetter]

(Should we protect the master branch of coqutil and demand that future changes be made via PR?)

I don't want to have to worry about legacy Coq versions each time I edit a file. But I understand that you're annoyed if your CI breaks :wink: We had a similar issue with bedrock2 running on Coq's CI and breaking it too often, and we solved it by adding a branch called tested and an auto-fast-forward script that fast-forwards tested to master only if the build on master succeeded, do you think a similar solution could work here too?

[JasonGross]

do you think a similar solution could work here too?

Yeah, that sounds good. Would you be willing to set that up? (I could also try my hand at it)

[samuelgruetter]

(I could also try my hand at it)

Yeah I'd appreciate if you could take care of this :+1:

[JasonGross]

and an auto-fast-forward script that fast-forwards tested to master only if the build on master succeeded, do you think a similar solution could work here too?

Hm, would the coqutil opam package then also track the tested branch?

[JasonGross]

I've made https://github.com/mit-plv/coqutil/blob/master/.github/workflows/update-tested.yml, hopefully it works

[JasonGross]

It fails with "Error: no check runs found" https://github.com/mit-plv/coqutil/runs/4830983483?check_suite_focus=true

Any ideas?

[samuelgruetter]

My guess is that the "name" of these runs doesn't match, and I don't understand whether the ... at the end of these names are just inserted by my browser when viewing the runs, or also on the server side. When I zoom out in my browser, no matter how far I zoom out, the name always gets displayed as build (8.14.0, coq-8.14.0 libcoq-8.14.0-ocaml-dev, 1, ppa:jgross-h/many-coq-versions-ocaml-4-11, ..., whereas in update-tested.yml, you didn't abbreviate this one: build (8.14.0, coq-8.14.0 libcoq-8.14.0-ocaml-dev, 1, ppa:jgross-h/many-coq-versions-ocaml-4-11). So I guess one way would be to fiddle with these ..., but a better way would be to define better names for these runs in .github/workflows/coq.yml, do you know if that's possible?

[JasonGross]

you didn't abbreviate this one: build (8.14.0, coq-8.14.0 libcoq-8.14.0-ocaml-dev, 1, ppa:jgross-h/many-coq-versions-ocaml-4-11).

I copied https://github.com/samuelgruetter/check-ci-success/blob/a9c8f2f5a8052876a9367b5e3bcd44cd5e9a8daf/check_ci_success.py#L71 and looked at https://api.github.com/repos/mit-plv/coqutil/commits/master/check-runs, via curl https://api.github.com/repos/mit-plv/coqutil/commits/master/check-runs | jq '[.check_runs | [.[] | .name] ]', which gives

[
  [
    "Update tested",
    "Update tested",
    "Update tested",
    "Update tested",
    "Update tested",
    "build (Ubuntu LTS, coq libcoq-ocaml-dev, 1, ubuntu-20.04)",
    "build (v8.14, coq libcoq-ocaml-dev, 1, ppa:jgross-h/coq-8.14-daily, ubuntu-latest)",
    "build (master, coq libcoq-ocaml-dev, 1, ppa:jgross-h/coq-master-daily, --warnings, ubuntu-latest)",
    "build (8.11.2, coq-8.11.2 libcoq-8.11.2-ocaml-dev, 1, ppa:jgross-h/many-coq-versions-ocaml-4-05, ...",
    "build (8.12.2, coq-8.12.2 libcoq-8.12.2-ocaml-dev, 1, ppa:jgross-h/many-coq-versions-ocaml-4-05, ...",
    "build (8.13.1, coq-8.13.1 libcoq-8.13.1-ocaml-dev, 1, ppa:jgross-h/many-coq-versions-ocaml-4-05, ...",
    "build (8.14.0, coq-8.14.0 libcoq-8.14.0-ocaml-dev, 1, ppa:jgross-h/many-coq-versions-ocaml-4-11, ..."
  ]
]

I guess I mis-typed.