search

mit-plv / bedrock2

A work-in-progress language and compiler for verified low-level programming
http://adam.chlipala.net/papers/LightbulbPLDI21/
MIT License
297 stars 45 forks source link

[CI] Move update-tested into coq.yml #418

Closed JasonGross closed 6 months ago

JasonGross commented 6 months ago

This version will only work if there's only one .yml file of checks we want to run, but it updates tested more quickly when there are pushes, and doesn't require keeping the list of Coq versions up to date in multiple places.

On top of #417

andres-erbsen commented 6 months ago

Does tested still have a use now that coq ci uses the fiat-crypto version of bedrock2?

samuelgruetter commented 6 months ago

I'm not so familiar with Coq's CI but if it indeed does not reference the tested branch any more, we can just delete update-tested.yml without moving its contents to coq.yml -- the fewer moving parts, the better!

JasonGross commented 6 months ago

Sure, it can just be deleted instead