As preparation for the module system, and in hopes it will be faster
than and replace the Nix CI. Secondary build jobs do not block merging.
Also makes macOS aarch64 a secondary build job on the PR level, where it
is the current bottleneck.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
This PR enables the language server to present multiple disjoint line
ranges as being worked on. Even before parallelism lands, we make use of
this feature to show post-elaboration tasks such as kernel checking on
the first line of a declaration to distinguish them from the final
tactic step.
Bumps
[mymindstorm/setup-emsdk](https://github.com/mymindstorm/setup-emsdk)
from 12 to 14.
<details>
<summary>Release notes</summary>
<p><em>Sourced from <a
href="https://github.com/mymindstorm/setup-emsdk/releases">mymindstorm/setup-emsdk's
releases</a>.</em></p>
<blockquote>
<h2>Version 14</h2>
<h1>Breaking Changes</h1>
<p>The default cache key naming scheme was changed from
<code>{Emscripten version}-{OS type}-${CPU architecture}-master</code>
to <code>{Github workflow name}-{Emscripten version}-{OS type}-${CPU
architecture}</code>. If <code>actions-cache-folder</code> is defined,
ensure that there are no conflicts with other caches to prevent
issues.</p>
<h1>Changelog</h1>
<ul>
<li>Add option to override cache key naming scheme (<a
href="https://redirect.github.com/mymindstorm/setup-emsdk/issues/20">#20</a>)</li>
<li>Add workflow name to cache key naming scheme (<a
href="https://redirect.github.com/mymindstorm/setup-emsdk/issues/20">#20</a>)</li>
<li>Updated dependencies to latest versions</li>
</ul>
<h2>Version 13</h2>
<ul>
<li>Updated to Node 20</li>
</ul>
</blockquote>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="6ab9eb1bda"><code>6ab9eb1</code></a>
v13 -> v14</li>
<li><a
href="bb630c3bf4"><code>bb630c3</code></a>
Update all dependencies to latest versions</li>
<li><a
href="74881103d0"><code>7488110</code></a>
Add workflow ID to cache key and cache key override option (<a
href="https://redirect.github.com/mymindstorm/setup-emsdk/issues/40">#40</a>)</li>
<li><a
href="d233ac12b0"><code>d233ac1</code></a>
v13</li>
<li><a
href="1749b22b40"><code>1749b22</code></a>
npm audit fix + update runtime to node20</li>
<li>See full diff in <a
href="https://github.com/mymindstorm/setup-emsdk/compare/v12...v14">compare
view</a></li>
</ul>
</details>
<br />
[](https://docs.github.com/en/github/managing-security-vulnerabilities/about-dependabot-security-updates#about-compatibility-scores)
Dependabot will resolve any conflicts with this PR as long as you don't
alter it yourself. You can also trigger a rebase manually by commenting
`@dependabot rebase`.
[//]: # (dependabot-automerge-start)
[//]: # (dependabot-automerge-end)
---
<details>
<summary>Dependabot commands and options</summary>
<br />
You can trigger Dependabot actions by commenting on this PR:
- `@dependabot rebase` will rebase this PR
- `@dependabot recreate` will recreate this PR, overwriting any edits
that have been made to it
- `@dependabot merge` will merge this PR after your CI passes on it
- `@dependabot squash and merge` will squash and merge this PR after
your CI passes on it
- `@dependabot cancel merge` will cancel a previously requested merge
and block automerging
- `@dependabot reopen` will reopen this PR if it is closed
- `@dependabot close` will close this PR and stop Dependabot recreating
it. You can achieve the same result by closing it manually
- `@dependabot show <dependency name> ignore conditions` will show all
of the ignore conditions of the specified dependency
- `@dependabot ignore this major version` will close this PR and stop
Dependabot creating any more for this major version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this minor version` will close this PR and stop
Dependabot creating any more for this minor version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this dependency` will close this PR and stop
Dependabot creating any more for this dependency (unless you reopen the
PR or upgrade to it yourself)
</details>
Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Fixes a workflow bug where the `check-level` was not always set
correctly. Arguments to a `gh` call used to determine the `check_level`
were accidentally outside of the relevant command substitution (`$(gh
...)`).
-----
This can be observed in [these
logs](https://github.com/leanprover/lean4/actions/runs/10859763037/job/30139540920),
where the check level (shown first under "configure build matrix") is
`2`, but the PR does not have the `release-ci` tag. As a "test", run the
script for "set check level" printed in those logs (with some lines
omitted):
```
check_level=0
labels="$(gh api repos/leanprover/lean4/pulls/5343) --jq '.labels'"
if echo "$labels" | grep -q "release-ci"; then
check_level=2
elif echo "$labels" | grep -q "merge-ci"; then
check_level=1
fi
echo "check_level=$check_level"
```
Note that this prints `check_level=2`, but changing `labels` to
`labels="$(gh api repos/leanprover/lean4/pulls/5343 --jq '.labels')"`
prints `check_level=0`.
Previously, the CI would run upon every label addition, including things
like `builds-mathlib`
or `will-merge-soon`, possibly triggering a new PR release, new mathlib
builds etc. Very wasteful!
Unfortunately (but not surprisingly) Github does not offer a nice way of
saying
“this workflow depends on that label, please re-run if changed”. Not
enough
functional programmer or nix enthusiasts there, I guess…
So here is the next iteration trying to work with what we have from
Github:
A new workflow watches for (only) `full-ci` label addition or deletion,
and then re-runs
the CI job for the current PR.
Sounds simple? But remember, this is github!
* `github.event.pull_request.labels.*.name` is *not* updated when a job
is re-run.
(This is actually a reasonable step towards determinism, but doesn't
help us
constructing this work-around.)
Ok, so let’s use the API to fetch the current state of the label.
* There is no good way to say “find the latest run of workflow `"CI"` on
PR `$n`”.
The best approximation seems to search by branch and triggering event.
This can
probably go wrong if there are multiple PRs from different repos with
the same
head ref name (`patch-1` anyone?). Let’s hope that it doesn’t happen too
often.
* You cannot just rerun a workflow. You can only rerun a finished
workflow. So cancel
it first. And `sleep` a bit…
So let’s see how well this will work. It’s plausibly an improvement.
macos-latest changed to arm64. It should not be hard to switch our setup
to cross-compiling x64 instead of arm64 but let's get master green again
first.
