Kim Morrison
14f80172bc
chore: typo in fix-pr-release.yml ( #5601 )
2024-10-02 23:04:39 +00:00
Joachim Breitner
56b78a0ed1
chore: pr-release.yml: fix bot’s username to look for ( #5495 )
...
This didn’t make it in with #5490 , but seems to be needed, just as in
https://github.com/leanprover-community/mathlib4/pull/17182/files (the
code is duplicated in both repos, and should be the same).
2024-09-27 15:29:53 +00:00
Kim Morrison
3817b16c35
chore: use separate secrets for commenting and branching in pr-release.yml ( #5490 )
...
Hopefully this will resolve the problem of duplicated comments when the
bots post about Mathlib CI status.
2024-09-27 07:27:55 +00:00
Kim Morrison
9eef726204
chore: commit lake-manifest.json when updating lean-pr-testing branches ( #5489 )
2024-09-27 06:52:24 +00:00
Kim Morrison
5017b2bfbf
chore: Mathlib's lean-pr-testing-NNNN branches should use Batteries' lean-pr-testing-NNNN branches ( #5444 )
...
The problem here was that in Mathlib's `lean-pr-testing-NNNN` branches,
we were setting Batteries to a `nightly-testing-YYYY-MM-DD` branch. This
means that when we merge or rebase a new `nightly-with-mathlib` into a
Lean PR, the corresponding Mathlib testing branch would keep using an
old version of Batteries.
We also make sure to bump Batteries if Mathlib's `lean-pr-testing-NNNN`
branch already exists.
2024-09-24 01:33:38 +00:00
euprunin
cda6733f97
chore: fix spelling mistakes in non-Lean files ( #5430 )
...
Co-authored-by: euprunin <euprunin@users.noreply.github.com>
2024-09-23 21:11:20 +00:00
thorimur
5eea8355ba
fix: set check level correctly during workflow ( #5344 )
...
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`.
2024-09-14 08:14:08 +00:00
thorimur
60bb451d45
feat: allow addition of release-ci label via comment ( #5343 )
...
Updates the PR labeling workflow to allow an external contributor to add
the `release-ci` label to their own PR via comment. This is allows users
on Windows and Intel-based macs to generate toolchains for local
testing. The pull request template is also updated to reflect this.
-----
See Zulip discussion
[here](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/No.20binary.20for.20lean.20PR.20testing.20locally ).
2024-09-14 08:13:48 +00:00
Henrik Böving
da9c68a37a
feat: import LeanSAT's tactic frontends
...
Co-authored-by: Markus Himmel <markus@lean-fro.org>
2024-08-28 18:14:39 +02:00
Joachim Breitner
15c6ac2076
chore: restart-on-label: Also filter by commit SHA ( #5099 )
2024-08-20 07:45:43 +00:00
Sebastian Ullrich
a43356591c
chore: CI: fix 32bit stage 0 builds ( #5052 )
...
Let's link stage 0 against libuv in both cases, even if for Emscripten
we won't for stage 1
2024-08-15 12:35:25 +00:00
Joachim Breitner
7283e2c14e
chore: pr-release: pass --retry to curl ( #5025 )
...
Since https://github.com/curl/curl/pull/4465 curl adheres to the
`Retry-After` header, so maybe this fixes the issues with
```
jq: error (at <stdin>:5): Cannot index string with string "body"
```
that sometimes make this workflow fail.
2024-08-13 16:19:43 +00:00
Joachim Breitner
f500af99e8
chore: ci.yaml: build MacOS Aarch64 release for PRs by default ( #5022 )
...
should make https://github.com/leanprover-community/mathlib4/pull/13301
unnecessary, which has a fair number of bad side-effects
2024-08-13 15:34:44 +00:00
Joachim Breitner
11be29e68c
chore: pr-release: adjust lakefile editing sed to new git syntax ( #5014 )
2024-08-13 12:03:51 +00:00
Henrik Böving
74f9dea701
feat: use save-always in cache action ( #5010 )
...
Follows up on
https://github.com/leanprover/lean4/pull/5003#issuecomment-2284813940
2024-08-13 09:27:15 +00:00
Henrik Böving
ecb35795eb
chore: upgrade cache action to silence warnings ( #5003 )
...
According to the release notes of cache this should not break anything
as they merely upgraded the node version.
2024-08-12 15:46:53 +00:00
Markus Himmel
c237c1f9fb
feat: link LibUV ( #4963 )
2024-08-12 12:33:24 +00:00
Sebastian Ullrich
adc799584c
fix: split libleanshared on Windows to avoid symbol limit
2024-08-12 14:14:42 +02:00
Sebastian Ullrich
7ef2d2fea2
chore: CI: remove rebase command
...
We'll try using the buttons provided by GitHub for now
2024-08-08 11:17:52 +02:00
Sebastian Ullrich
a29bca7f00
chore: CI: placate linter
2024-08-07 16:52:18 +02:00
Sebastian Ullrich
12a714a6f9
chore: CI: fix rebase command
2024-08-07 14:27:53 +02:00
Sebastian Ullrich
cdc7ed0224
chore: CI: fix rebase command
2024-08-07 14:21:43 +02:00
Sebastian Ullrich
217abdf97a
chore: CI: fix rebase command
2024-08-07 14:15:18 +02:00
Sebastian Ullrich
490a2b4bf9
chore: CI: fix rebase command
2024-08-07 14:05:00 +02:00
Sebastian Ullrich
84d45deb10
chore: CI: fix rebase
2024-08-07 14:02:57 +02:00
Sebastian Ullrich
f46d216e18
chore: CI: !rebase PR comment command
2024-08-07 13:53:17 +02:00
Sebastian Ullrich
efc99b982e
chore: deprecate Nix-based build, remove interactive components ( #4895 )
...
Users who prefer the flake build should maintain it externally
2024-08-02 09:57:34 +00:00
Sebastian Ullrich
abf4206e9c
chore: CI: fix msys2
2024-07-29 10:25:59 +02:00
Joachim Breitner
a5b8d5b486
chore: upon nightly release, trigger nightly_bump_toolchain on mathlib4 ( #4838 )
...
as discussed at
https://leanprover.zulipchat.com/#narrow/stream/428973-nightly-testing/topic/Bumping.20more.20often/near/453976634
2024-07-26 06:51:19 +00:00
Joachim Breitner
d4f2db9559
chore: report github actions failure on zulip ( #4830 )
...
only the master branch
2024-07-25 11:15:33 +00:00
Sebastian Ullrich
0768ad4eb9
chore: CI: Jira sync
2024-07-24 19:52:55 +02:00
Sebastian Ullrich
6d971827e2
chore: CI: add back dropped check-stage3
2024-07-24 09:03:11 +02:00
Sebastian Ullrich
582d6e7f71
chore: CI: update download-artifact actions
2024-07-09 10:17:19 +02:00
Joachim Breitner
955135b3f9
chore: bump actions/checkout and actions/upload-artifacts ( #4664 )
...
to reduce warnings on CI. Based on the changelogs/migrations guides I
found they should work as before.
2024-07-07 20:26:59 +00:00
Joachim Breitner
04fefdd728
chore: restart-on-label: wait for 30s ( #4663 )
...
this doesn't work reliable when it cancels jobs. Maybe sleeping helps.
2024-07-05 19:50:14 +00:00
Joachim Breitner
cc5c95f377
chore: CI: restart-on-label: view run more often ( #4640 )
...
this job sometimes fails, maybe a race condition with the `gh run
cancel` not happenign quickly enough. Maybe more verbose output will
help understand this better.
2024-07-03 12:35:50 +00:00
Sebastian Ullrich
62c5bc5d0d
chore: manual nightly trigger ( #4638 )
...
Now that nightly releases may fail more often because of more checks,
let's make it possible to retry them on a later commit
2024-07-03 08:19:07 +00:00
Joachim Breitner
d39c4d6a1c
chore: pr-release: use right tag name ( #4632 )
...
this improves upon #4598
2024-07-02 21:06:55 +00:00
Joachim Breitner
be54ccd246
chore: pr-release: adjust to new lakefile.lean syntax ( #4598 )
...
as per
f5c3f06aa7
2024-07-01 08:48:33 +00:00
Joachim Breitner
0629eebc09
chore: release triggers update of release.lean-lang.org ( #4531 )
2024-06-30 10:39:32 +00:00
Kim Morrison
0f416c6a83
chore: mark releases as prerelease ( #4544 )
2024-06-24 01:04:04 +00:00
Sebastian Ullrich
16cad2b45c
chore: CI: do not fetch complete history
2024-06-13 14:50:49 +02:00
Sebastian Ullrich
6d265b42b1
chore: CI: fix github.event.pull_request.merge_commit_sha sometimes not being available
2024-06-13 14:47:42 +02:00
Sebastian Ullrich
c5120c1d0d
chore: CI: fix Wasm release-ci ( #4442 )
2024-06-13 11:58:49 +00:00
Sebastian Ullrich
37f8b0390d
chore: CI: fix workflow change breaking unrebased PRs ( #4441 )
2024-06-13 09:56:31 +00:00
Sebastian Ullrich
bd3b466f2f
chore: CI: fix speedcenter tests ( #4440 )
2024-06-13 10:53:47 +02:00
Sebastian Ullrich
a8de4b3b06
chore: CI: use Namespace runners ( #4427 )
2024-06-12 16:06:41 +00:00
Joachim Breitner
42f12967a6
chore: CI: pr-release: install elan ( #4361 )
...
PR #4333 added a call to `lake`, but that needs elan installed
2024-06-05 08:20:57 +00:00
Kim Morrison
05ea3ac19f
chore: update batteries in manifest when creating lean-pr-testing-NNNN at Mathlib ( #4333 )
2024-06-04 01:45:37 +00:00
Sebastian Ullrich
f05a82799a
chore: CI: restore macOS aarch64 install sufix
2024-05-26 14:29:56 +02:00
