Skip to content

add jasmin installation to external CI jobs #793

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 3 commits into
base: main
Choose a base branch
from
Draft

Conversation

fdupress
Copy link
Member

@fdupress fdupress commented Aug 5, 2025

Draft PR to check effect on CI times for now. This is to eventually, ultimately, and finally enable #725.

This forces the use of the EasyCrypt+Jasmin docker image
to measure CI performance impact. It should be reverted if
and when we decide to include Jasmin in the main docker image.
@fdupress
Copy link
Member Author

fdupress commented Aug 6, 2025

Time impact is about 10 seconds per external CI job. Not sure about the bandwidth impact on the image. (Didn't measure before losing access to a convenient machine; we could usefully layer it to keep both images.)

@strub does this deserve more engineering to make sure we only install Jasmin for external CI jobs that request it, or are we happy to pay the small performance price for a simpler CI job?

@fdupress
Copy link
Member Author

fdupress commented Aug 8, 2025

Outcomes:

  • time cost is acceptable;
  • layering on docker image is desirable—add jasmin dependencies as a layer on top of the base image.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant