search

formosa-crypto / formosa-x-wing

3 stars 0 forks source link

CI + external CI #1

Open fdupress opened 18 hours ago

fdupress commented 18 hours ago

Hi folks, (that's @mbbarbosa and @JoaoDiogoDuarte)

I'm thinking I should use my newfound free time productively, and figured I'd offer free effort to set you guys up with continuous proof-checking and the external CI. (This will help me understand how costly doing so "as a service" is.)

There are a couple of things to figure out before I embark on a long-dreaded dive into github actions' insanity. For my own proofs, I typically enjoy having the proof's main check with EasyCrypt's latest stable, and have all other branches check with EasyCrypt's main. (And we have a way of making exceptions for branches that should check with a specific EasyCrypt commit.)

Would that mode of checking work for youse?

JoaoDiogoDuarte commented 18 hours ago

Hi François,

That sounds like a great idea! I tested this proof with the latest Easycrypt stable release and it worked. As I also don't expect there to be any wild and crazy branches, testing with main seems fine.

What do you think @mbbarbosa?

Thanks for the effort!

fdupress commented 14 hours ago

The proof does not go through with EasyCrypt main. Some problems with the cloning that are harder than my brain right now.

We will need at least one branch that checks with EasyCrypt main to set up the external CI. This could be this proof's main, of course, but then it needs fixed up.