CI issues

Stream: general

[Ruben Van de Velde]

It seems like scripts/detect_errors.py is failing with a syntax error, like in https://github.com/leanprover-community/mathlib/pull/9526/checks?check_run_id=3789550714 and https://github.com/leanprover-community/mathlib/pull/9443/checks?check_run_id=3789549047

[Eric Wieser]

The azure2 runner has the wrong python version installed

[Eric Wieser]

@Bryan Gin-ge Chen, do you remember why we turned off the CI feature that installs the correct version of python as part of the build?

[Gabriel Ebner]

That doesn't work for self-hosted runners I believe.

[Gabriel Ebner]

#9531

[Johan Commelin]

Are there any systems where python == python 3.x, but where there is no python3 executable by default?

[Gabriel Ebner]

Not that I know of.

[Anne Baanen]

PEP 394 recommends always providing a python3 (or python2) executable and linking python to either one of them.

[Anne Baanen]

So in general, no, that shouldn't happen.

[Johan Commelin]

Ok, so this is a no-brainer. Let's merge it.

[Eric Wieser]

Gabriel Ebner said:

Not that I know of.

Do venvs create both versions?

[Gabriel Ebner]

At least my venv does: python, python3, and python3.9

[Ruben Van de Velde]

I wonder why bors decided to run #9469 rather than #9531

[Bryan Gin-ge Chen]

We didn't put a special priority on #9531, so when we re-added it after it failed, I guess it went to the end of the line. It seems to be running now though.

[Jireh Loreaux]

On the lint mathlib CI step I am getting the following error during "retrieve build". I reran but it gave the same error. Can someone explain / help?

Starting download for precompiled-mathlib-3.42.0-7b6fa2b8
Directory structure has been setup for the artifact
Total number of files that will be downloaded: 1
Total file count: 1 ---- Processed file #0 (0.0%)
Error: An error occurred while attempting to decompress the response stream
A 200 response code has been received while attempting to download an artifact
Exponential backoff for retry #1. Waiting for 4959 milliseconds before continuing the download
Total file count: 1 ---- Processed file #0 (0.0%)
Total file count: 1 ---- Processed file #0 (0.0%)
Total file count: 1 ---- Processed file #0 (0.0%)
Total file count: 1 ---- Processed file #0 (0.0%)
Total file count: 1 ---- Processed file #0 (0.0%)
Finished backoff for retry #1, continuing with download

See here: https://github.com/leanprover-community/mathlib/runs/5836892681?check_suite_focus=true

[Jireh Loreaux]

The error is longer, but it's basically more of the same. It seems like it just can't find the build? But I don't know why that would be.

[Arthur Paulino]

Seems like it took ~2 minutes to fail. Do you have enough RAM to try and reproduce it locally?

[Jireh Loreaux]

I can try, but I think not. Is 5GB free enough? And what is the procedure exactly? mk_all and then what?

[Bryan Gin-ge Chen]

From the logs it looks to me like a temporary hiccup on GitHub's side (though I don't see any issues posted at https://www.githubstatus.com yet?). I just tried re-running the failed jobs again but it looks like they're failing with the same error.

[Arthur Paulino]

Seems like GitHub actions is struggling to download artifacts from Azure:

{"$id":"1","innerException":null,"message":"The user 'System:PublicAccess;aaaaaaaa-aaaa-aaaa-aaaa-aaaaaaaaaaaa' is not authorized to access this resource.","typeName":"Microsoft.TeamFoundation.Framework.Server.UnauthorizedRequestException, Microsoft.TeamFoundation.Framework.Server","typeKey":"UnauthorizedRequestException","errorCode":0,"eventId":3000}

[Bryan Gin-ge Chen]

I've just tried re-running all jobs, in case that refreshes the artifact and fixes things somehow. :shrug:

[Jireh Loreaux]

Okay, thanks.

[Bryan Gin-ge Chen]

Looks like it's working this time!