Zulip Chat Archive

Stream: general

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):

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 (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: Dec 20 2023 at 11:08 UTC