Skip to content

Conversation

@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 4, 2023
@SkySkimmer SkySkimmer requested review from a team as code owners July 4, 2023 16:21
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 4, 2023
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 4, 2023
@SkySkimmer SkySkimmer requested a review from a team as a code owner July 4, 2023 16:24
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 4, 2023
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jul 4, 2023

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

@SkySkimmer SkySkimmer added this to the 8.19+rc1 milestone Jul 4, 2023
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jul 4, 2023

🔴 CI failures at commit 5ef97ca without any failure in the test-suite

✔️ Corresponding jobs for the base commit bf260b4 succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-atbr, ci-bbv, ci-bedrock2, ci-bignums, ci-category_theory, ci-compcert, ci-coq_dpdgraph, ci-coquelicot, ci-cross_crypto, ci-equations_test, ci-fiat_crypto_legacy, ci-fiat_parsers, ci-itree, ci-metacoq, ci-quickchick, ci-relation_algebra, ci-smtcoq, ci-verdi_raft, ci-vst
  • You can also pass me a specific list of targets to minimize as arguments.
  • If you tag me saying @coqbot ci minimize all, I will additionally minimize the following target (which I do not suggest minimizing): ci-geocoq (because base job at bf260b4 failed)

@SkySkimmer
Copy link
Contributor Author

I did some overlays but I'm stopping here for a while

@SkySkimmer SkySkimmer added the needs: overlay This is breaking external developments we track in CI. label Jul 5, 2023
@SkySkimmer SkySkimmer closed this Jul 6, 2023
@SkySkimmer SkySkimmer deleted the intuit-auto branch July 6, 2023 11:25
@coqbot-app coqbot-app bot removed this from the 8.19+rc1 milestone Jul 6, 2023
@SkySkimmer
Copy link
Contributor Author

I don't have time to do all this overlay stuff for this.

@palmskog
Copy link
Contributor

I have now fixed all these intuition deprecations in all "my" projects in Coq's CI, such as Verdi Raft. I hope the PR can be revived at some point. The work in #18164 shows that it should be possible, and maintainers can do their part to pitch in. In the meantime, it seems like Itauto is good to recommend as a replacement for intuition in new projects.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

needs: overlay This is breaking external developments we track in CI.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants