Guinea pigs wanted

Stream: general

[Gabriel Ebner]

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]

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]

Don't worry, (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]

Ah, great! Now I do feel like a Guinea pig!

[Yaël Dillies]

Is it how a workflow looks like? https://github.com/leanprover-community/mathlib/runs/2992673323

[Yaël Dillies]

Oh wait too late! It compiled :grinning_face_with_smiling_eyes:

[Yaël Dillies]

This is indeed faaaaast