search

mit-plv / fiat-crypto

Cryptographic Primitive Code Generation by Fiat
http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf
Other
717 stars 147 forks source link

Unify Coq CI into a single .yml file #1798

Open JasonGross opened 11 months ago

JasonGross commented 11 months ago

This shares structure a lot more, and will also enable us to (eventually) just check if the generated OCaml code is identical across Coq versions and platforms.

Note that we no longer check generated files on most platforms, and we only validate on Coq master.

JasonGross commented 11 months ago

Hm, probably it would be better to use reusable workflows rather than blocking future steps across platforms

andres-erbsen commented 11 months ago

I think branching on the platform inside a larger script isn't great. Reusable workflows might work, but I am not familiar with them.

If we didn't have CI-specific workarounds, I think I would like to have a deps script for each platform and then source the right one. Unfortunately it seems that most of the files in this diff are full of stuff that is really specific to oddities of the proprietary CI infrastructure and I am not sure what to make of it.