Skip to content
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

Deactivate macOS CI runners? #119

Closed
ahelwer opened this issue Feb 8, 2024 · 3 comments
Closed

Deactivate macOS CI runners? #119

ahelwer opened this issue Feb 8, 2024 · 3 comments

Comments

@ahelwer
Copy link
Collaborator

ahelwer commented Feb 8, 2024

Currently the macOS CI takes over twice as long to run as the linux and windows CI runs: https://github.com/tlaplus/Examples/actions/runs/7835386801

This got substantially worse after the work to add models to most of the specs, because macOS CI runners see a strange amount of overhead for each model (for example a model taking 1 second to run on the other runners takes 8 seconds to run on the macOS runner). Looking online it seems slow macOS CI runners is a common problem experienced by developers across github.

Ideally the CI would run for ten minutes at most, and I don't think the macOS runner is providing enough value (given the similarity to linux) to justify keeping it around. Perhaps we could add a scheduled CI run to test on macOS once per week.

@lemmy
Copy link
Member

lemmy commented Feb 8, 2024

AFAIK there are also much faster m1-based Github runners now.

@ahelwer
Copy link
Collaborator Author

ahelwer commented Feb 8, 2024

Ah, you have to specify macos-14 instead of macos-latest to get those. Running the CI with that it does seem as though it's faster. Great, problem solved!

Edit: actually problem is not solved. It still takes twice as long. I think deactivating macOS is the move.

@lemmy
Copy link
Member

lemmy commented Jul 16, 2024

I recommend reactivating macOS for the same reason it was kept for tlaplus/tlaplus. macOS is the most popular platform and shares similarities with Linux, though it is not identical. Additionally, the rate of changes in this repository is very low, so allowing 30 minutes instead of 15 minutes for tasks is acceptable.

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

No branches or pull requests

2 participants