[Merged by Bors] - feat(ci): run lint and tests in parallel

[robertylewis]

Actions doesn't let us run steps in parallel, but we can run jobs in parallel. The lint and test jobs are part of the same workflow. Understanding Actions terminology is half the battle.

[gebner]

• We need to tell bors about the new CI jobs.
• Can we maybe retire the "upload precompiled mathlib zip file" step now if the first job generates an artifact anyhow?

[gebner]

• Installing the python dependencies should be moved to the documentation generation job.

[gebner]

Apparently the zip file doesn't preserve the permissions. We probably need to switch to "precompiled tar.gz".

[bryangingechen]

Apparently the zip file doesn't preserve the permissions. We probably need to switch to "precompiled tar.gz".

Yeah, that looks like it's tracked here: actions/upload-artifact#38

[bryangingechen]

• We need to tell bors about the new CI jobs.

Done.

• Can we maybe retire the "upload precompiled mathlib zip file" step now if the first job generates an artifact anyhow?

I don't understand. Isn't that the step that generates and uploads the artifact?

Apparently the zip file doesn't preserve the permissions. We probably need to switch to "precompiled tar.gz".

I just added a bunch more chmod +x's for now. I'll look into taring before generating the artifact after dinner.

Done.

[bryangingechen]

bors try

[bors]

try

Build succeeded:

• Run tests and docs
• Lint mathlib
• Build mathlib

[bryangingechen]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests and docs

[gebner]

• Can we maybe retire the "upload precompiled mathlib zip file" step now if the first job generates an artifact anyhow?

I don't understand. Isn't that the step that generates and uploads the artifact?

Sorry, I missed that at first. I thought github actions has some built-in support to save the current directory.