This is a hack-ish (? perhaps it's normal, I don't know) way of selecting which branch of a proof repository should be used when running external CI checks. The external CI configuration is used as a default branch to check. However, when running in EasyCrypt branch X (or in a PR related to EasyCrypt branch X), the external CI check will run in the proof repository's branch merge-X if it exists, only checking the default branch if merge-X does not exist.
This, combined with some light scripting on the proof repository side of things, then supports the following workflow, meant to engage when we make breaking changes to EasyCrypt:
We open a PR from branch X introducing a breaking change;
External CI checks predictably fail, and we notify maintainers and guide proof fixes;
Proof fixes in the external proof repo are commited to branch merge-X, which gets them checked using branch X (local validation);
We re-run the PR CI on EasyCrypt, which then runs the checks on branch merge-X of the external proof repository;
Once all indicators are green, we know that all external proofs are ready to merge a fix (or that we should take other action), and we can synchronise merges.
This is not meant as a way to allow external proofs to block merging of important changes to EC, but as a way of synchronising our tool engineering with others' proof engineering with limited CI config fiddling.
This is meant to support the ultimate merging of #605, which is the first breaking change we make where proofs fixed to work after the merge are not valid proofs in the pre-merge version of EC—requiring synchronisation instead of just waiting for fixes to be pushed.
The quality of the script can likely be improved, but I am not trained as an engineer, so this is the best I can do.
This is a hack-ish (? perhaps it's normal, I don't know) way of selecting which branch of a proof repository should be used when running external CI checks. The external CI configuration is used as a default branch to check. However, when running in EasyCrypt branch
X(or in a PR related to EasyCrypt branchX), the external CI check will run in the proof repository's branchmerge-Xif it exists, only checking the default branch ifmerge-Xdoes not exist.This, combined with some light scripting on the proof repository side of things, then supports the following workflow, meant to engage when we make breaking changes to EasyCrypt:
Xintroducing a breaking change;merge-X, which gets them checked using branchX(local validation);merge-Xof the external proof repository;This is not meant as a way to allow external proofs to block merging of important changes to EC, but as a way of synchronising our tool engineering with others' proof engineering with limited CI config fiddling.
This is meant to support the ultimate merging of #605, which is the first breaking change we make where proofs fixed to work after the merge are not valid proofs in the pre-merge version of EC—requiring synchronisation instead of just waiting for fixes to be pushed.
The quality of the script can likely be improved, but I am not trained as an engineer, so this is the best I can do.