Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

chore: update batteries in manifest when creating lean-pr-testing-NNNN at Mathlib #4333

Merged
merged 1 commit into from
Jun 4, 2024
Merged

chore: update batteries in manifest when creating lean-pr-testing-NNNN at Mathlib #4333

merged 1 commit into from
Jun 4, 2024

Conversation

semorrison
Copy link
Collaborator

No description provided.

@semorrison semorrison requested a review from Kha as a code owner June 3, 2024 23:33
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc June 3, 2024 23:36 Inactive
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jun 3, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f65e3ae9859a4288b94b4a9fda93f406244d8dbc --onto 81f5b07215b077f9b5be677f8689617512d3322c. (2024-06-03 23:53:13)

@semorrison semorrison added this pull request to the merge queue Jun 4, 2024
Merged via the queue into master with commit 05ea3ac Jun 4, 2024
13 checks passed
@semorrison semorrison deleted the pr-release-update-batteries branch June 4, 2024 02:14
Komyyy pushed a commit to Komyyy/lean4 that referenced this pull request Jun 4, 2024
@semorrison @Komyyy
chore: update batteries in manifest when creating lean-pr-testing-NNN…
f1969f1 
…N at Mathlib (leanprover#4333)
@nomeata
Copy link
Contributor

nomeata commented Jun 5, 2024

This didn't quite work, it seems:

Run git config user.name "leanprover-community-mathlib4-bot"
Using base tag: nightly-testing-2024-06-04
Branch exists: 0
Branch does not exist, creating it.
Switched to a new branch 'lean-pr-testing-4360'
/home/runner/work/_temp/b852685f-f684-4b04-8e4a-256967af7905.sh: line 21: lake: command not found
Error: Process completed with exit code 127.

https://github.com/leanprover/lean4/actions/runs/9380284107/job/25826966898

Trying a quick fix in #4361

@nomeata nomeata mentioned this pull request Jun 5, 2024
Merged
github-merge-queue bot pushed a commit that referenced this pull request Jun 5, 2024
@nomeata
chore: CI: pr-release: install elan (#4361)
42f1296 
PR #4333 added a call to `lake`, but that needs elan installed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Kha Kha Awaiting requested review from Kha Kha is a code owner

Assignees
No one assigned
Labels
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@semorrison @leanprover-community-mathlib4-bot @nomeata