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="72f2c25fcb552dc5524bhttps://redirect.github.com/softprops/action-gh-release/issues/632 ">#632</a>)</li>
<li><a
href="f3cad8bcbf07a2257003https://redirect.github.com/softprops/action-gh-release/issues/629 ">#629</a>)</li>
<li><a
href="d5382d3e6fa0e2122208https://redirect.github.com/softprops/action-gh-release/issues/626 ">#626</a>)</li>
<li><a
href="8836085300https://redirect.github.com/softprops/action-gh-release/issues/624 ">#624</a>)</li>
<li><a
href="86463358d846b284799fhttps://redirect.github.com/softprops/action-gh-release/issues/623 ">#623</a>)</li>
<li><a
href="37fd9d0351https://redirect.github.com/softprops/action-gh-release/issues/621 ">#621</a>)</li>
<li>Additional commits viewable in <a
href="da05d55257...72f2c25fcbhttps://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="ac66b43f0e9b54a0a70chttps://github.com/dawidd6/action-download-artifact/compare/v10...v11 ">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>
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="b7ef57d46ehttps://redirect.github.com/dcarbone/install-jq-action/issues/20 ">#20</a>)</li>
<li><a
href="2eac2baa38https://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 />
[](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
Sebastian Ullrich
5023b40576
chore: CI: fix cache ( #8579 )
...
* include .olean variants
* include SHA in key on push as well
2025-06-02 08:00:42 +00:00
dependabot[bot]
e7b24479ed
chore: CI: bump dawidd6/action-download-artifact from 9 to 10 ( #8578 )
...
Bumps
[dawidd6/action-download-artifact](https://github.com/dawidd6/action-download-artifact )
from 9 to 10.
<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>v10</h2>
<h2>What's Changed</h2>
<ul>
<li>Fix the download-commit test to actually look for a commit by <a
href="https://github.com/mstorsjo "><code>@mstorsjo</code></a> in <a
href="https://redirect.github.com/dawidd6/action-download-artifact/pull/330 ">dawidd6/action-download-artifact#330</a></li>
<li>Add the option "ref", specifying either a commit or a
branch by <a
href="https://github.com/mstorsjo "><code>@mstorsjo</code></a> in <a
href="https://redirect.github.com/dawidd6/action-download-artifact/pull/329 ">dawidd6/action-download-artifact#329</a></li>
</ul>
<h2>New Contributors</h2>
<ul>
<li><a href="https://github.com/mstorsjo "><code>@mstorsjo</code></a>
made their first contribution in <a
href="https://redirect.github.com/dawidd6/action-download-artifact/pull/330 ">dawidd6/action-download-artifact#330</a></li>
</ul>
<p><strong>Full Changelog</strong>: <a
href="https://github.com/dawidd6/action-download-artifact/compare/v9...v10 ">https://github.com/dawidd6/action-download-artifact/compare/v9...v10 </a></p>
</blockquote>
</details>
<details>
<summary>Commits</summary>
<ul>
<li><a
href="4c1e823582https://redirect.github.com/dawidd6/action-download-artifact/issues/329 ">#329</a>)</li>
<li><a
href="a708c3c648https://redirect.github.com/dawidd6/action-download-artifact/issues/330 ">#330</a>)</li>
<li><a
href="19f6be5f04https://github.com/dawidd6/action-download-artifact/compare/v9...v10 ">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>
2025-06-01 21:37:06 +00:00
Tobias Grosser
ed6c78048e
chore: skip OS X aarch64 CI only in merge groups ( #8334 )
...
This PR enables the build of all artifacts for custom releases, e.g.,
releases outside the main lean4 repository.
This resolves https://github.com/leanprover/lean4/issues/8333 .
2025-05-27 11:51:59 +00:00
Kim Morrison
c1866a7b7e
chore: fix awaiting-mathlib.yml ( #8480 )
...
This PR hopefully fixes a problem from #8471 , which even the most
cursory testing (by me!) should have detected.
2025-05-26 02:13:00 +00:00
Kim Morrison
bdbb659765
chore: while awaiting-mathlib, show yellow status not red ( #8471 )
...
This PR changes the CI check when the `awaiting-mathlib` label is
present. If `breaks-mathlib` is present, it shows a red cross, but if
neither `breaks-mathlib` nor `builds-mathlib` is present it shows a
yellow circle.
2025-05-25 12:38:56 +00:00
Joachim Breitner
fc3c82b1c7
chore: denixify stage0-updater workflow ( #8452 )
...
This PR lets the stage0 autoupdater build lean using the `cmake`
infrastructure, not the deprecated nix infrastructure.
2025-05-23 13:12:50 +00:00
Sebastian Ullrich
e635eeacd3
chore: CI: replace Nix CI with Linux release ( #8335 )
...
Nix cannot handle the awesomeness of our stdlib anymore.
2025-05-14 15:31:40 +00:00
David Thrane Christiansen
12ff2d8c49
chore: remove old documentation site ( #7974 )
...
This PR removes the old documentation overview site, as its content has
moved to the main Lean website infrastructure.
This should be merged when the new website section is deployed, after
installing appropriate redirects.
Developer documentation is remaining in Markdown form, but it will no
longer be part of the documentation hosted on the Lean website. Example
code stays here for CI, but it is now rendered via a Verso plugin.
2025-05-14 14:31:33 +00:00
Sebastian Ullrich
29fc6a46a8
chore: CI: exclude test not compatible with Lake CI
2025-05-01 12:58:44 +02:00
Sebastian Ullrich
20a9db6357
chore: CI: run Linux Lake in all configurations
...
Otherwise master never has a cache for it
2025-04-26 13:25:29 +02:00
Sebastian Ullrich
96cda3f498
chore: CI: revert accidentally disabling Lake cache
2025-04-24 15:01:09 +02:00
Sebastian Ullrich
d5494a306c
chore: CI: extend list of virtual merge checkout files
2025-04-24 08:43:42 +02:00
Sebastian Ullrich
5c7a7d6406
chore: CI: reset reldebug check level
2025-04-23 14:31:59 +02:00
Sebastian Ullrich
fbbf42e82f
chore: fix reldebug preset ( #8051 )
...
Build with assertions, but without debug info
2025-04-23 10:05:11 +00:00
Sebastian Ullrich
791bba0091
feat: LLVM 15 -> 19 ( #6063 )
...
This PR updates the version of LLVM and clang used by and shipped with
Lean to 19.1.2
Fixes #5649
2025-04-21 17:18:18 +00:00
Sebastian Ullrich
d6c30a8a0a
chore: disable build of old manual
2025-04-21 18:40:11 +02:00
Sebastian Ullrich
a52e0c5ba5
chore: CI: bring back Lake build job ( #8020 )
...
Thanks to recent fixes
2025-04-18 13:42:27 +00:00
Sebastian Ullrich
8ea6465e6d
chore: CI: disable Linux 32bit ( #7924 )
...
A 2GB heap is just not that much even before fragmentation
2025-04-12 09:29:13 +00:00
Sebastian Ullrich
0669a04704
chore: CI: limit CCACHE_SIZE to 400MB ( #7922 )
2025-04-11 17:09:16 +00:00
