Commit graph

495 commits

Author SHA1 Message Date
Sebastian Ullrich
116b708269
chore: CI: ensure cache reuse in update-stage0 (#10359) 2025-09-12 14:56:32 +00:00
dependabot[bot]
757426b099
chore: CI: bump actions/checkout from 4 to 5 (#10219)
Bumps [actions/checkout](https://github.com/actions/checkout) from 4 to
5.
<details>
<summary>Release notes</summary>
<p><em>Sourced from <a
href="https://github.com/actions/checkout/releases">actions/checkout's
releases</a>.</em></p>
<blockquote>
<h2>v5.0.0</h2>
<h2>What's Changed</h2>
<ul>
<li>Update actions checkout to use node 24 by <a
href="https://github.com/salmanmkc"><code>@​salmanmkc</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/2226">actions/checkout#2226</a></li>
<li>Prepare v5.0.0 release by <a
href="https://github.com/salmanmkc"><code>@​salmanmkc</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/2238">actions/checkout#2238</a></li>
</ul>
<h2>⚠️ Minimum Compatible Runner Version</h2>
<p><strong>v2.327.1</strong><br />
<a
href="https://github.com/actions/runner/releases/tag/v2.327.1">Release
Notes</a></p>
<p>Make sure your runner is updated to this version or newer to use this
release.</p>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/actions/checkout/compare/v4...v5.0.0">https://github.com/actions/checkout/compare/v4...v5.0.0</a></p>
<h2>v4.3.0</h2>
<h2>What's Changed</h2>
<ul>
<li>docs: update README.md by <a
href="https://github.com/motss"><code>@​motss</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/1971">actions/checkout#1971</a></li>
<li>Add internal repos for checking out multiple repositories by <a
href="https://github.com/mouismail"><code>@​mouismail</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/1977">actions/checkout#1977</a></li>
<li>Documentation update - add recommended permissions to Readme by <a
href="https://github.com/benwells"><code>@​benwells</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/2043">actions/checkout#2043</a></li>
<li>Adjust positioning of user email note and permissions heading by <a
href="https://github.com/joshmgross"><code>@​joshmgross</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/2044">actions/checkout#2044</a></li>
<li>Update README.md by <a
href="https://github.com/nebuk89"><code>@​nebuk89</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/2194">actions/checkout#2194</a></li>
<li>Update CODEOWNERS for actions by <a
href="https://github.com/TingluoHuang"><code>@​TingluoHuang</code></a>
in <a
href="https://redirect.github.com/actions/checkout/pull/2224">actions/checkout#2224</a></li>
<li>Update package dependencies by <a
href="https://github.com/salmanmkc"><code>@​salmanmkc</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/2236">actions/checkout#2236</a></li>
<li>Prepare release v4.3.0 by <a
href="https://github.com/salmanmkc"><code>@​salmanmkc</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/2237">actions/checkout#2237</a></li>
</ul>
<h2>New Contributors</h2>
<ul>
<li><a href="https://github.com/motss"><code>@​motss</code></a> made
their first contribution in <a
href="https://redirect.github.com/actions/checkout/pull/1971">actions/checkout#1971</a></li>
<li><a href="https://github.com/mouismail"><code>@​mouismail</code></a>
made their first contribution in <a
href="https://redirect.github.com/actions/checkout/pull/1977">actions/checkout#1977</a></li>
<li><a href="https://github.com/benwells"><code>@​benwells</code></a>
made their first contribution in <a
href="https://redirect.github.com/actions/checkout/pull/2043">actions/checkout#2043</a></li>
<li><a href="https://github.com/nebuk89"><code>@​nebuk89</code></a> made
their first contribution in <a
href="https://redirect.github.com/actions/checkout/pull/2194">actions/checkout#2194</a></li>
<li><a href="https://github.com/salmanmkc"><code>@​salmanmkc</code></a>
made their first contribution in <a
href="https://redirect.github.com/actions/checkout/pull/2236">actions/checkout#2236</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/actions/checkout/compare/v4...v4.3.0">https://github.com/actions/checkout/compare/v4...v4.3.0</a></p>
<h2>v4.2.2</h2>
<h2>What's Changed</h2>
<ul>
<li><code>url-helper.ts</code> now leverages well-known environment
variables by <a href="https://github.com/jww3"><code>@​jww3</code></a>
in <a
href="https://redirect.github.com/actions/checkout/pull/1941">actions/checkout#1941</a></li>
<li>Expand unit test coverage for <code>isGhes</code> by <a
href="https://github.com/jww3"><code>@​jww3</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/1946">actions/checkout#1946</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/actions/checkout/compare/v4.2.1...v4.2.2">https://github.com/actions/checkout/compare/v4.2.1...v4.2.2</a></p>
<h2>v4.2.1</h2>
<h2>What's Changed</h2>
<ul>
<li>Check out other refs/* by commit if provided, fall back to ref by <a
href="https://github.com/orhantoy"><code>@​orhantoy</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/1924">actions/checkout#1924</a></li>
</ul>
<h2>New Contributors</h2>
<ul>
<li><a href="https://github.com/Jcambass"><code>@​Jcambass</code></a>
made their first contribution in <a
href="https://redirect.github.com/actions/checkout/pull/1919">actions/checkout#1919</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/actions/checkout/compare/v4.2.0...v4.2.1">https://github.com/actions/checkout/compare/v4.2.0...v4.2.1</a></p>
<!-- raw HTML omitted -->
</blockquote>
<p>... (truncated)</p>
</details>
<details>
<summary>Changelog</summary>
<p><em>Sourced from <a
href="https://github.com/actions/checkout/blob/main/CHANGELOG.md">actions/checkout's
changelog</a>.</em></p>
<blockquote>
<h1>Changelog</h1>
<h2>V5.0.0</h2>
<ul>
<li>Update actions checkout to use node 24 by <a
href="https://github.com/salmanmkc"><code>@​salmanmkc</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/2226">actions/checkout#2226</a></li>
</ul>
<h2>V4.3.0</h2>
<ul>
<li>docs: update README.md by <a
href="https://github.com/motss"><code>@​motss</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/1971">actions/checkout#1971</a></li>
<li>Add internal repos for checking out multiple repositories by <a
href="https://github.com/mouismail"><code>@​mouismail</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/1977">actions/checkout#1977</a></li>
<li>Documentation update - add recommended permissions to Readme by <a
href="https://github.com/benwells"><code>@​benwells</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/2043">actions/checkout#2043</a></li>
<li>Adjust positioning of user email note and permissions heading by <a
href="https://github.com/joshmgross"><code>@​joshmgross</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/2044">actions/checkout#2044</a></li>
<li>Update README.md by <a
href="https://github.com/nebuk89"><code>@​nebuk89</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/2194">actions/checkout#2194</a></li>
<li>Update CODEOWNERS for actions by <a
href="https://github.com/TingluoHuang"><code>@​TingluoHuang</code></a>
in <a
href="https://redirect.github.com/actions/checkout/pull/2224">actions/checkout#2224</a></li>
<li>Update package dependencies by <a
href="https://github.com/salmanmkc"><code>@​salmanmkc</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/2236">actions/checkout#2236</a></li>
</ul>
<h2>v4.2.2</h2>
<ul>
<li><code>url-helper.ts</code> now leverages well-known environment
variables by <a href="https://github.com/jww3"><code>@​jww3</code></a>
in <a
href="https://redirect.github.com/actions/checkout/pull/1941">actions/checkout#1941</a></li>
<li>Expand unit test coverage for <code>isGhes</code> by <a
href="https://github.com/jww3"><code>@​jww3</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/1946">actions/checkout#1946</a></li>
</ul>
<h2>v4.2.1</h2>
<ul>
<li>Check out other refs/* by commit if provided, fall back to ref by <a
href="https://github.com/orhantoy"><code>@​orhantoy</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/1924">actions/checkout#1924</a></li>
</ul>
<h2>v4.2.0</h2>
<ul>
<li>Add Ref and Commit outputs by <a
href="https://github.com/lucacome"><code>@​lucacome</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/1180">actions/checkout#1180</a></li>
<li>Dependency updates by <a
href="https://github.com/dependabot"><code>@​dependabot</code></a>- <a
href="https://redirect.github.com/actions/checkout/pull/1777">actions/checkout#1777</a>,
<a
href="https://redirect.github.com/actions/checkout/pull/1872">actions/checkout#1872</a></li>
</ul>
<h2>v4.1.7</h2>
<ul>
<li>Bump the minor-npm-dependencies group across 1 directory with 4
updates by <a
href="https://github.com/dependabot"><code>@​dependabot</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/1739">actions/checkout#1739</a></li>
<li>Bump actions/checkout from 3 to 4 by <a
href="https://github.com/dependabot"><code>@​dependabot</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/1697">actions/checkout#1697</a></li>
<li>Check out other refs/* by commit by <a
href="https://github.com/orhantoy"><code>@​orhantoy</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/1774">actions/checkout#1774</a></li>
<li>Pin actions/checkout's own workflows to a known, good, stable
version. by <a href="https://github.com/jww3"><code>@​jww3</code></a> in
<a
href="https://redirect.github.com/actions/checkout/pull/1776">actions/checkout#1776</a></li>
</ul>
<h2>v4.1.6</h2>
<ul>
<li>Check platform to set archive extension appropriately by <a
href="https://github.com/cory-miller"><code>@​cory-miller</code></a> in
<a
href="https://redirect.github.com/actions/checkout/pull/1732">actions/checkout#1732</a></li>
</ul>
<h2>v4.1.5</h2>
<ul>
<li>Update NPM dependencies by <a
href="https://github.com/cory-miller"><code>@​cory-miller</code></a> in
<a
href="https://redirect.github.com/actions/checkout/pull/1703">actions/checkout#1703</a></li>
<li>Bump github/codeql-action from 2 to 3 by <a
href="https://github.com/dependabot"><code>@​dependabot</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/1694">actions/checkout#1694</a></li>
<li>Bump actions/setup-node from 1 to 4 by <a
href="https://github.com/dependabot"><code>@​dependabot</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/1696">actions/checkout#1696</a></li>
<li>Bump actions/upload-artifact from 2 to 4 by <a
href="https://github.com/dependabot"><code>@​dependabot</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/1695">actions/checkout#1695</a></li>
<li>README: Suggest <code>user.email</code> to be
<code>41898282+github-actions[bot]@users.noreply.github.com</code> by <a
href="https://github.com/cory-miller"><code>@​cory-miller</code></a> in
<a
href="https://redirect.github.com/actions/checkout/pull/1707">actions/checkout#1707</a></li>
</ul>
<h2>v4.1.4</h2>
<ul>
<li>Disable <code>extensions.worktreeConfig</code> when disabling
<code>sparse-checkout</code> by <a
href="https://github.com/jww3"><code>@​jww3</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/1692">actions/checkout#1692</a></li>
<li>Add dependabot config by <a
href="https://github.com/cory-miller"><code>@​cory-miller</code></a> in
<a
href="https://redirect.github.com/actions/checkout/pull/1688">actions/checkout#1688</a></li>
<li>Bump the minor-actions-dependencies group with 2 updates by <a
href="https://github.com/dependabot"><code>@​dependabot</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/1693">actions/checkout#1693</a></li>
<li>Bump word-wrap from 1.2.3 to 1.2.5 by <a
href="https://github.com/dependabot"><code>@​dependabot</code></a> in <a
href="https://redirect.github.com/actions/checkout/pull/1643">actions/checkout#1643</a></li>
</ul>
<h2>v4.1.3</h2>
<!-- raw HTML omitted -->
</blockquote>
<p>... (truncated)</p>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="08c6903cd8"><code>08c6903</code></a>
Prepare v5.0.0 release (<a
href="https://redirect.github.com/actions/checkout/issues/2238">#2238</a>)</li>
<li><a
href="9f265659d3"><code>9f26565</code></a>
Update actions checkout to use node 24 (<a
href="https://redirect.github.com/actions/checkout/issues/2226">#2226</a>)</li>
<li>See full diff in <a
href="https://github.com/actions/checkout/compare/v4...v5">compare
view</a></li>
</ul>
</details>
<br />


[![Dependabot compatibility
score](https://dependabot-badges.githubapp.com/badges/compatibility_score?dependency-name=actions/checkout&package-manager=github_actions&previous-version=4&new-version=5)](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>
2025-09-09 11:53:35 +00:00
dependabot[bot]
b81ea5ee9c
chore: CI: bump actions/download-artifact from 4 to 5 (#10220)
Bumps
[actions/download-artifact](https://github.com/actions/download-artifact)
from 4 to 5.
<details>
<summary>Release notes</summary>
<p><em>Sourced from <a
href="https://github.com/actions/download-artifact/releases">actions/download-artifact's
releases</a>.</em></p>
<blockquote>
<h2>v5.0.0</h2>
<h2>What's Changed</h2>
<ul>
<li>Update README.md by <a
href="https://github.com/nebuk89"><code>@​nebuk89</code></a> in <a
href="https://redirect.github.com/actions/download-artifact/pull/407">actions/download-artifact#407</a></li>
<li>BREAKING fix: inconsistent path behavior for single artifact
downloads by ID by <a
href="https://github.com/GrantBirki"><code>@​GrantBirki</code></a> in <a
href="https://redirect.github.com/actions/download-artifact/pull/416">actions/download-artifact#416</a></li>
</ul>
<h2>v5.0.0</h2>
<h3>🚨 Breaking Change</h3>
<p>This release fixes an inconsistency in path behavior for single
artifact downloads by ID. <strong>If you're downloading single artifacts
by ID, the output path may change.</strong></p>
<h4>What Changed</h4>
<p>Previously, <strong>single artifact downloads</strong> behaved
differently depending on how you specified the artifact:</p>
<ul>
<li><strong>By name</strong>: <code>name: my-artifact</code> → extracted
to <code>path/</code> (direct)</li>
<li><strong>By ID</strong>: <code>artifact-ids: 12345</code> → extracted
to <code>path/my-artifact/</code> (nested)</li>
</ul>
<p>Now both methods are consistent:</p>
<ul>
<li><strong>By name</strong>: <code>name: my-artifact</code> → extracted
to <code>path/</code> (unchanged)</li>
<li><strong>By ID</strong>: <code>artifact-ids: 12345</code> → extracted
to <code>path/</code> (fixed - now direct)</li>
</ul>
<h4>Migration Guide</h4>
<h5> No Action Needed If:</h5>
<ul>
<li>You download artifacts by <strong>name</strong></li>
<li>You download <strong>multiple</strong> artifacts by ID</li>
<li>You already use <code>merge-multiple: true</code> as a
workaround</li>
</ul>
<h5>⚠️ Action Required If:</h5>
<p>You download <strong>single artifacts by ID</strong> and your
workflows expect the nested directory structure.</p>
<p><strong>Before v5 (nested structure):</strong></p>
<pre lang="yaml"><code>- uses: actions/download-artifact@v4
  with:
    artifact-ids: 12345
    path: dist
# Files were in: dist/my-artifact/
</code></pre>
<blockquote>
<p>Where <code>my-artifact</code> is the name of the artifact you
previously uploaded</p>
</blockquote>
<p><strong>To maintain old behavior (if needed):</strong></p>
<pre lang="yaml"><code>&lt;/tr&gt;&lt;/table&gt; 
</code></pre>
</blockquote>
<p>... (truncated)</p>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="634f93cb29"><code>634f93c</code></a>
Merge pull request <a
href="https://redirect.github.com/actions/download-artifact/issues/416">#416</a>
from actions/single-artifact-id-download-path</li>
<li><a
href="b19ff43027"><code>b19ff43</code></a>
refactor: resolve download path correctly in artifact download tests
(mainly ...</li>
<li><a
href="e262cbee4a"><code>e262cbe</code></a>
bundle dist</li>
<li><a
href="bff23f9308"><code>bff23f9</code></a>
update docs</li>
<li><a
href="fff8c148a8"><code>fff8c14</code></a>
fix download path logic when downloading a single artifact by id</li>
<li><a
href="448e3f862a"><code>448e3f8</code></a>
Merge pull request <a
href="https://redirect.github.com/actions/download-artifact/issues/407">#407</a>
from actions/nebuk89-patch-1</li>
<li><a
href="47225c44b3"><code>47225c4</code></a>
Update README.md</li>
<li>See full diff in <a
href="https://github.com/actions/download-artifact/compare/v4...v5">compare
view</a></li>
</ul>
</details>
<br />


[![Dependabot compatibility
score](https://dependabot-badges.githubapp.com/badges/compatibility_score?dependency-name=actions/download-artifact&package-manager=github_actions&previous-version=4&new-version=5)](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>
2025-09-09 11:53:09 +00:00
Sebastian Ullrich
96c42b95fa
chore: CI: reintroduce lost CTEST_OPTIONS (#10211) 2025-09-02 09:26:29 +00:00
Sebastian Ullrich
43dc9f45d1
chore: CI: disable broken test on macOS x64 2025-08-27 13:14:32 +02:00
Sebastian Ullrich
d06fff0f13
chore: CI: use restored ccache cache in update-stage0 2025-08-27 11:44:46 +02:00
Sebastian Ullrich
6810d31602
chore: CI: cache again on failure (#10137) 2025-08-26 14:47:05 +00:00
Sebastian Ullrich
6a3fc281ad
chore: CI: use Namespace.so checkout action for Linux Lake (#10103) 2025-08-26 09:19:58 +00:00
Joachim Breitner
13e8cb5a3a
perf: reorder DiscrTree.Key constructors (#10110)
this PR reorders the `DiscrTree.Key` constructors to match the order
given in the manually written `DiscrTree.Key.ctorIdx`. This allows us to
use the auto-generated one, and moreover lets this code benefit from
special compiler support for `.ctorIdx`, once that lands.
2025-08-25 16:13:43 +00:00
Sebastian Ullrich
5ccea92a09
chore: revert "chore: CI: use Namespace.so checkout action for Linux Lake" (#10102)
Reverts leanprover/lean4#10100 pending a fix for running it on master
2025-08-24 15:58:25 +00:00
Sebastian Ullrich
3fc3f5d240
chore: CI: use Namespace.so checkout action for Linux Lake (#10100)
~1min ~> ~10s
2025-08-24 15:24:50 +00:00
Sebastian Ullrich
17f76f3bd7
chore: CI: recover dropped install suffixes (#10076) 2025-08-23 15:15:26 +00:00
Sebastian Ullrich
9b4911f8f6
chore: CI: fix Linux Lake on PR half-merge (#10029) 2025-08-21 13:25:53 +00:00
Sebastian Ullrich
f678b40660
chore: make USE_LAKE the default (#10016) 2025-08-21 11:43:25 +00:00
Sebastian Ullrich
679df58329
chore: revert "chore: make USE_LAKE the default" (#10011)
Reverts leanprover/lean4#10003, which broke the merge queue's breakage
check
2025-08-20 19:52:57 +00:00
Sebastian Ullrich
44891fe0c0
chore: make USE_LAKE the default (#10003) 2025-08-20 19:24:10 +00:00
Sebastian Ullrich
8d34dfe914
chore: CI: make cached Lake primary job (#9401) 2025-08-19 20:43:00 +00:00
Sebastian Ullrich
c9a6446041
chore: CI: include tests in rebootstrap check (#9788) 2025-08-07 15:37:36 +00:00
Mac Malone
dbfeb9e2da
chore: upload build directory as artifact in cache CI (#9600)
This PR adds a step to the cached Linux Lake CI to upload the build
directory. This will help us debug any cache failures.
2025-07-28 20:29:51 +00:00
Sebastian Ullrich
ff1d3138bf
refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Sebastian Ullrich
04be1c6b5c
chore: CI: cached Lake as secondary job (#9486) 2025-07-23 13:26:35 +00:00
Sebastian Ullrich
e28569f2a1
perf: minimize exported codegen data (#9356)
To be documented
2025-07-22 09:05:49 +00:00
Sebastian Ullrich
9fc31abb1f
chore: benchmark using USE_LAKE (#9361) 2025-07-17 18:44:29 +00:00
Markus Himmel
3878d6da85
chore: Grove: bump version (#9419) 2025-07-17 15:02:17 +00:00
Markus Himmel
ca9b804163
chore: ci: specify which Linux toolchain Grove should download (#9405)
Since the old version of the workflow will run on PRs, we'll have to
"test" this on master.
2025-07-16 13:15:13 +00:00
Sebastian Ullrich
97698bfc38
chore: CI: use faster Windows runners for releases (#9357) 2025-07-14 16:26:22 +00:00
Sebastian Ullrich
7f1869016a
chore: CI: do not use large runners for secondary jobs (#9352)
macOS in particular is expensive to use large machines for more than
necessary
2025-07-14 15:00:58 +00:00
Markus Himmel
a7789d863c
chore: Grove: update and enable on master (#9353) 2025-07-14 09:21:51 +00:00
Sebastian Ullrich
357b5f9ed8
chore: CI: restore cache in update-stage0 (#9179)
Avoid rebuilding stage 0 all the time
2025-07-03 20:55:14 +00:00
Joachim Breitner
47b795a302
chore: CI: run stage0 update on faster runner (#9178)
To avoid it losing races against the merge queue.
2025-07-03 16:14:46 +00:00
dependabot[bot]
8e5dfb0fd1
chore: CI: bump softprops/action-gh-release from 2.2.2 to 2.3.2 (#9139)
Bumps
[softprops/action-gh-release](https://github.com/softprops/action-gh-release)
from 2.2.2 to 2.3.2.
<details>
<summary>Release notes</summary>
<p><em>Sourced from <a
href="https://github.com/softprops/action-gh-release/releases">softprops/action-gh-release's
releases</a>.</em></p>
<blockquote>
<h2>v2.3.2</h2>
<ul>
<li>fix: revert fs <code>readableWebStream</code> change</li>
</ul>
<h2>v2.3.1</h2>
<!-- raw HTML omitted -->
<h2>What's Changed</h2>
<h3>Bug fixes 🐛</h3>
<ul>
<li>fix: fix file closing issue by <a
href="https://github.com/WailGree"><code>@​WailGree</code></a> in <a
href="https://redirect.github.com/softprops/action-gh-release/pull/629">softprops/action-gh-release#629</a></li>
</ul>
<h2>New Contributors</h2>
<ul>
<li><a href="https://github.com/WailGree"><code>@​WailGree</code></a>
made their first contribution in <a
href="https://redirect.github.com/softprops/action-gh-release/pull/629">softprops/action-gh-release#629</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/softprops/action-gh-release/compare/v2.3.0...v2.3.1">https://github.com/softprops/action-gh-release/compare/v2.3.0...v2.3.1</a></p>
<h2>v2.3.0</h2>
<!-- raw HTML omitted -->
<ul>
<li>Migrate from jest to vitest</li>
<li>Replace <code>mime</code> with <code>mime-types</code></li>
<li>Bump to use node 24</li>
<li>Dependency updates</li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/softprops/action-gh-release/compare/v2.2.2...v2.3.0">https://github.com/softprops/action-gh-release/compare/v2.2.2...v2.3.0</a></p>
</blockquote>
</details>
<details>
<summary>Changelog</summary>
<p><em>Sourced from <a
href="https://github.com/softprops/action-gh-release/blob/master/CHANGELOG.md">softprops/action-gh-release's
changelog</a>.</em></p>
<blockquote>
<h2>2.3.2</h2>
<ul>
<li>fix: revert fs <code>readableWebStream</code> change</li>
</ul>
<h2>2.3.1</h2>
<h3>Bug fixes 🐛</h3>
<ul>
<li>fix: fix file closing issue by <a
href="https://github.com/WailGree"><code>@​WailGree</code></a> in <a
href="https://redirect.github.com/softprops/action-gh-release/pull/629">softprops/action-gh-release#629</a></li>
</ul>
<h2>2.3.0</h2>
<ul>
<li>Migrate from jest to vitest</li>
<li>Replace <code>mime</code> with <code>mime-types</code></li>
<li>Bump to use node 24</li>
<li>Dependency updates</li>
</ul>
<h2>2.2.2</h2>
<h2>What's Changed</h2>
<h3>Bug fixes 🐛</h3>
<ul>
<li>fix: updating release draft status from true to false by <a
href="https://github.com/galargh"><code>@​galargh</code></a> in <a
href="https://redirect.github.com/softprops/action-gh-release/pull/316">softprops/action-gh-release#316</a></li>
</ul>
<h3>Other Changes 🔄</h3>
<ul>
<li>chore: simplify ref_type test by <a
href="https://github.com/steinybot"><code>@​steinybot</code></a> in <a
href="https://redirect.github.com/softprops/action-gh-release/pull/598">softprops/action-gh-release#598</a></li>
<li>fix(docs): clarify the default for tag_name by <a
href="https://github.com/muzimuzhi"><code>@​muzimuzhi</code></a> in <a
href="https://redirect.github.com/softprops/action-gh-release/pull/599">softprops/action-gh-release#599</a></li>
<li>test(release): add unit tests when searching for a release by <a
href="https://github.com/rwaskiewicz"><code>@​rwaskiewicz</code></a> in
<a
href="https://redirect.github.com/softprops/action-gh-release/pull/603">softprops/action-gh-release#603</a></li>
<li>dependency updates</li>
</ul>
<h2>2.2.1</h2>
<h2>What's Changed</h2>
<h3>Bug fixes 🐛</h3>
<ul>
<li>fix: big file uploads by <a
href="https://github.com/xen0n"><code>@​xen0n</code></a> in <a
href="https://redirect.github.com/softprops/action-gh-release/pull/562">softprops/action-gh-release#562</a></li>
</ul>
<h3>Other Changes 🔄</h3>
<ul>
<li>chore(deps): bump <code>@​types/node</code> from 22.10.1 to 22.10.2
by <a href="https://github.com/dependabot"><code>@​dependabot</code></a>
in <a
href="https://redirect.github.com/softprops/action-gh-release/pull/559">softprops/action-gh-release#559</a></li>
<li>chore(deps): bump <code>@​types/node</code> from 22.10.2 to 22.10.5
by <a href="https://github.com/dependabot"><code>@​dependabot</code></a>
in <a
href="https://redirect.github.com/softprops/action-gh-release/pull/569">softprops/action-gh-release#569</a></li>
<li>chore: update error and warning messages for not matching files in
files field by <a
href="https://github.com/ytimocin"><code>@​ytimocin</code></a> in <a
href="https://redirect.github.com/softprops/action-gh-release/pull/568">softprops/action-gh-release#568</a></li>
</ul>
<h2>2.2.0</h2>
<h2>What's Changed</h2>
<h3>Exciting New Features 🎉</h3>
<!-- raw HTML omitted -->
</blockquote>
<p>... (truncated)</p>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="72f2c25fcb"><code>72f2c25</code></a>
release 2.3.2</li>
<li><a
href="552dc5524b"><code>552dc55</code></a>
fix: revert <code>fs:readableWebStream</code> change (<a
href="https://redirect.github.com/softprops/action-gh-release/issues/632">#632</a>)</li>
<li><a
href="f3cad8bcbf"><code>f3cad8b</code></a>
release 2.3.1</li>
<li><a
href="07a2257003"><code>07a2257</code></a>
fix: fix file closing issue (<a
href="https://redirect.github.com/softprops/action-gh-release/issues/629">#629</a>)</li>
<li><a
href="d5382d3e6f"><code>d5382d3</code></a>
release 2.3.0</li>
<li><a
href="a0e2122208"><code>a0e2122</code></a>
feat: migrate from jest to vitest (<a
href="https://redirect.github.com/softprops/action-gh-release/issues/626">#626</a>)</li>
<li><a
href="8836085300"><code>8836085</code></a>
chore: replace <code>mime</code> with <code>mime-types</code> (<a
href="https://redirect.github.com/softprops/action-gh-release/issues/624">#624</a>)</li>
<li><a
href="86463358d8"><code>8646335</code></a>
chore: bump node to 20.19.2</li>
<li><a
href="46b284799f"><code>46b2847</code></a>
chore(deps): bump the npm group across 1 directory with 5 updates (<a
href="https://redirect.github.com/softprops/action-gh-release/issues/623">#623</a>)</li>
<li><a
href="37fd9d0351"><code>37fd9d0</code></a>
chore(deps): bump undici from 5.28.5 to 5.29.0 (<a
href="https://redirect.github.com/softprops/action-gh-release/issues/621">#621</a>)</li>
<li>Additional commits viewable in <a
href="da05d55257...72f2c25fcb">compare
view</a></li>
</ul>
</details>
<br />


[![Dependabot compatibility
score](https://dependabot-badges.githubapp.com/badges/compatibility_score?dependency-name=softprops/action-gh-release&package-manager=github_actions&previous-version=2.2.2&new-version=2.3.2)](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>
2025-07-01 21:22:15 +00:00
dependabot[bot]
5c86fd271f
chore: CI: bump dawidd6/action-download-artifact from 10 to 11 (#9137)
Bumps
[dawidd6/action-download-artifact](https://github.com/dawidd6/action-download-artifact)
from 10 to 11.
<details>
<summary>Release notes</summary>
<p><em>Sourced from <a
href="https://github.com/dawidd6/action-download-artifact/releases">dawidd6/action-download-artifact's
releases</a>.</em></p>
<blockquote>
<h2>v11</h2>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/dawidd6/action-download-artifact/compare/v10...v11">https://github.com/dawidd6/action-download-artifact/compare/v10...v11</a></p>
</blockquote>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="ac66b43f0e"><code>ac66b43</code></a>
node_modules: upgrade</li>
<li><a
href="9b54a0a70c"><code>9b54a0a</code></a>
Update README.md</li>
<li>See full diff in <a
href="https://github.com/dawidd6/action-download-artifact/compare/v10...v11">compare
view</a></li>
</ul>
</details>
<br />


[![Dependabot compatibility
score](https://dependabot-badges.githubapp.com/badges/compatibility_score?dependency-name=dawidd6/action-download-artifact&package-manager=github_actions&previous-version=10&new-version=11)](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>
2025-07-01 21:21:43 +00:00
dependabot[bot]
402cba6f09
chore: CI: bump dcarbone/install-jq-action from 3.1.1 to 3.2.0 (#9138)
Bumps
[dcarbone/install-jq-action](https://github.com/dcarbone/install-jq-action)
from 3.1.1 to 3.2.0.
<details>
<summary>Release notes</summary>
<p><em>Sourced from <a
href="https://github.com/dcarbone/install-jq-action/releases">dcarbone/install-jq-action's
releases</a>.</em></p>
<blockquote>
<h2>v3.2.0</h2>
<h2>What's Changed</h2>
<ul>
<li>case sensitive is off by <a
href="https://github.com/Rupreht"><code>@​Rupreht</code></a> in <a
href="https://redirect.github.com/dcarbone/install-jq-action/pull/19">dcarbone/install-jq-action#19</a></li>
<li>Adding 1.8.0 stuff by <a
href="https://github.com/dcarbone"><code>@​dcarbone</code></a> in <a
href="https://redirect.github.com/dcarbone/install-jq-action/pull/20">dcarbone/install-jq-action#20</a></li>
</ul>
<h2>New Contributors</h2>
<ul>
<li><a href="https://github.com/Rupreht"><code>@​Rupreht</code></a> made
their first contribution in <a
href="https://redirect.github.com/dcarbone/install-jq-action/pull/19">dcarbone/install-jq-action#19</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/dcarbone/install-jq-action/compare/v3.1.1...v3.2.0">https://github.com/dcarbone/install-jq-action/compare/v3.1.1...v3.2.0</a></p>
</blockquote>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="b7ef57d46e"><code>b7ef57d</code></a>
Adding 1.8.0 stuff (<a
href="https://redirect.github.com/dcarbone/install-jq-action/issues/20">#20</a>)</li>
<li><a
href="2eac2baa38"><code>2eac2ba</code></a>
case sensitive is off (<a
href="https://redirect.github.com/dcarbone/install-jq-action/issues/19">#19</a>)</li>
<li>See full diff in <a
href="https://github.com/dcarbone/install-jq-action/compare/v3.1.1...v3.2.0">compare
view</a></li>
</ul>
</details>
<br />


[![Dependabot compatibility
score](https://dependabot-badges.githubapp.com/badges/compatibility_score?dependency-name=dcarbone/install-jq-action&package-manager=github_actions&previous-version=3.1.1&new-version=3.2.0)](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>
2025-07-01 21:21:20 +00:00
Sebastian Ullrich
aadc74bee2 perf: do not import non-meta IR 2025-06-27 08:13:31 -07:00
David Thrane Christiansen
2bb27af0d4
chore: automatically create reference manual PR branches (#9033)
This PR adds a Mathlib-like testing and feedback system for the
reference manual. Lean PRs will receive comments that reflect the status
of the language reference with respect to the PR.
2025-06-27 13:23:41 +00:00
Markus Himmel
65ea45b17b
chore: ci: fixes to Grove workflow (#9014) 2025-06-26 12:15:51 +00:00
Markus Himmel
790ae27f2b
chore: ci: fixes to Grove workflow (#9013) 2025-06-26 11:13:19 +00:00
Markus Himmel
40d2c99463
chore: ci: fixes to Grove workflow (#9012) 2025-06-26 09:55:06 +00:00
Markus Himmel
4f1d828541
chore: ci: build Linux toolchain for master commits (but not merge queue runs) (#9010) 2025-06-26 08:20:04 +00:00
Markus Himmel
d3dda9f6d4
chore: initial Grove setup (#8997) 2025-06-26 05:03:02 +00:00
Kim Morrison
8fe068ef68
feat: move lean-pr-testing-NNNN branches to a fork (#8933)
This PR changes the CI setup to generate `lean-pr-testing-NNNN` branches
for Mathlib on the `leanprover-community/mathlib4-nightly-testing` fork,
rather than on the main repo.
2025-06-24 03:30:43 +00:00
Sebastian Ullrich
e129e75e66
chore: CI: temporarily disable .olean cache 2025-06-18 11:12:56 +09:00
Sebastian Ullrich
3b2990b381
chore: CI: work around test-speedcenter breaking on ubuntu-latest 2025-06-17 18:14:12 +09:00
Joachim Breitner
47c294b3a9
chore: make Linux Release CI job secondary (#8818)
Follow-up to #8817.
2025-06-16 21:29:07 +00:00
Joachim Breitner
5568e06160
chore: Run “Linux release” for PRs as secondary job (#8817)
This PR reifnes #8739 to make sure we get a linux release in the PR
release.
2025-06-16 20:45:10 +00:00
Sebastian Ullrich
242429a262
chore: CI: provide more than 8GB RAM (#8812)
We started running into OOMs in the test suite. This is the faster
alternative to lowering test parallelism.
2025-06-16 11:58:06 +00:00
Sebastian Ullrich
3feb63231e
chore: merge-checkout test fixed and removed from exclusions on master 2025-06-13 15:30:58 +02:00
Sebastian Ullrich
121ce56506
chore: CI: make "Linux Lake" primary PR CI job (#8739)
Comes with .olean caching and module system-powered short-circuiting
2025-06-13 11:27:49 +00:00
Johan Commelin
c53ab2835c
fix: pin version of softprops/action-gh-release (#8710)
This PR pins the precise hash of softprops/action-gh-release to

    softprops/action-gh-release@da05d55257

because the latest version is broken.
See https://github.com/softprops/action-gh-release/issues/628 for more
details.
2025-06-11 00:08:18 +00:00
Kim Morrison
e904314742
feat: add SHA-suffixed PR release tags (#8702)
This PR enhances the PR release workflow to create both short format and
SHA-suffixed release tags. Creates both pr-release-{PR_NUMBER} and
pr-release-{PR_NUMBER}-{SHORT_SHA} tags, generates separate releases for
both formats, adds separate GitHub status checks, and updates
Batteries/Mathlib testing branches to use SHA-suffixed tags for exact
commit traceability.

This removes the need for downstream repositories to deal with the
toolchain changing without the toolchain name changing.
2025-06-10 07:09:08 +00:00