Topic: Guinea pigs wanted
Gabriel Ebner (Jul 04 2021 at 17:26):
Johan's department at the Universität Freiburg has recently sponsored four additional VMs to speed up our CI. At the moment, they are still sitting idly, waiting for you!
Do you want your PRs to build 4x as fast as before? All you have to do is to merge master into your PR and they will be built on the German runners. (You might run into errors and bugs. We haven't really tested this yet. That's what we need you for!)
Damiano Testa (Jul 05 2021 at 11:30):
Gabriel, I thought of trying this out, but when I merged master, my version was already up to date and I am not sure that this got registered. Now I am seeing
continuous integration / Lint mathlib (push) In progress — This check has started... continuous integration (mathlib forks) / Lint mathlib (fork) (push) Skipped continuous integration / Run tests (push) In progress — This check has started... continuous integration (mathlib forks) / Run tests (fork) (push) Skipped
and I imagine that the faster machines are the Skipped (forked) ones. Am I doing something wrong? Are Johan's machines working?
Of course, this is very low priority!
Gabriel Ebner (Jul 05 2021 at 11:31):
(mathlib forks) is the (slower) github runners. They are skipped when you push something to the main mathlib repository. When you push it to your own fork (which doesn't have access to the Uni Freiburg machines), then the complement is skipped.
Damiano Testa (Jul 05 2021 at 11:32):
Ah, great! Now I do feel like a Guinea pig!
Yaël Dillies (Jul 05 2021 at 18:40):
Is it how a workflow looks like? https://github.com/leanprover-community/mathlib/runs/2992673323
Yaël Dillies (Jul 05 2021 at 18:42):
Oh wait too late! It compiled :grinning_face_with_smiling_eyes:
Yaël Dillies (Jul 05 2021 at 18:43):
This is indeed faaaaast
Last updated: Aug 03 2023 at 10:10 UTC