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

[Merged by Bors] - chore: do not set release-ci label upon failed PR test #15775

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - chore: do not set release-ci label upon failed PR test #15775

wants to merge 2 commits into from

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Aug 13, 2024

with leanprover/lean4#5022 the need for this
should have disappeared

@nomeata nomeata added the CI Modifies the continuous integration / deployment setup label Aug 13, 2024
@github-actions GitHub Actions
Copy link

github-actions bot commented Aug 13, 2024 •
edited
Loading

PR summary cc02f583b3

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

@nomeata nomeata added the easy < 20s of review time. See the lifecycle page for guidelines. label Aug 13, 2024
@nomeata nomeata requested a review from kim-em August 14, 2024 14:40
@kim-em
Copy link
Contributor

kim-em commented Aug 15, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Aug 15, 2024
mathlib-bors bot pushed a commit that referenced this pull request Aug 15, 2024
@nomeata
chore: do not set release-ci label upon failed PR test (#15775)
e024d5c 
with leanprover/lean4#5022 the need for this
should have disappeared
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Aug 15, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: do not set release-ci label upon failed PR test [Merged by Bors] - chore: do not set release-ci label upon failed PR test Aug 15, 2024
@mathlib-bors mathlib-bors bot closed this Aug 15, 2024
@mathlib-bors mathlib-bors bot deleted the joachim/no-release-ci branch August 15, 2024 10:59
nomeata added a commit that referenced this pull request Aug 15, 2024
@nomeata
chore: do not set release-ci label upon failed PR test (#15775)
40bc4fe 
with leanprover/lean4#5022 the need for this
should have disappeared
nomeata added a commit that referenced this pull request Aug 23, 2024
@nomeata
Squashed commit of lean-pr-testing-4154
37add2f 
commit 6d957dc
Author: Joachim Breitner <[email protected]>
Date:   Thu Aug 22 15:10:57 2024 +0200

    Fix proof

commit 5b95381
Merge: 48bea5e bc78dd4
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Thu Aug 22 11:24:01 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit 48bea5e
Author: Joachim Breitner <[email protected]>
Date:   Wed Aug 21 18:35:50 2024 +0200

    Switch to Mathlib.Init

commit 4d38bbd
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Wed Aug 21 18:25:08 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit f84b84d
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Wed Aug 21 09:58:00 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit f958309
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Wed Aug 21 09:39:13 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit 4b976ec
Author: Joachim Breitner <[email protected]>
Date:   Wed Aug 21 10:54:32 2024 +0200

    Try to remove some nolints

commit 0cbb129
Author: Joachim Breitner <[email protected]>
Date:   Wed Aug 21 10:53:14 2024 +0200

    Reduce diff

commit a485ac8
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Tue Aug 20 08:02:41 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit b5cb54a
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Mon Aug 19 13:09:14 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit 8b1ce21
Author: Joachim Breitner <[email protected]>
Date:   Mon Aug 19 12:56:07 2024 +0200

    Like this?

commit e6ce4b5
Author: Joachim Breitner <[email protected]>
Date:   Mon Aug 19 11:38:06 2024 +0200

    nolint attributes

commit e24f1c6
Author: Joachim Breitner <[email protected]>
Date:   Mon Aug 19 11:15:52 2024 +0200

    Another simp only gone

commit a9d54a8
Author: Joachim Breitner <[email protected]>
Date:   Mon Aug 19 11:11:30 2024 +0200

    aesop_cat broke :-(

commit b4edcec
Author: Joachim Breitner <[email protected]>
Date:   Mon Aug 19 11:03:43 2024 +0200

    Use dsimp only

commit 8e66ddd
Author: Joachim Breitner <[email protected]>
Date:   Mon Aug 19 10:28:04 2024 +0200

    Fixes in ComposableArrows

commit 471b000
Author: Joachim Breitner <[email protected]>
Date:   Mon Aug 19 10:18:56 2024 +0200

    Use cond_false

commit 8120390
Author: Joachim Breitner <[email protected]>
Date:   Mon Aug 19 10:14:41 2024 +0200

    No rfl after simp needed anymore

commit 0544693
Author: Joachim Breitner <[email protected]>
Date:   Mon Aug 19 10:13:00 2024 +0200

    Less dsimp only

commit 5cffe6e
Author: Joachim Breitner <[email protected]>
Date:   Mon Aug 19 10:10:21 2024 +0200

    More autoParam

commit 8e019f8
Author: Joachim Breitner <[email protected]>
Date:   Fri Aug 16 17:16:43 2024 +0200

    More fixes

commit 7b6f094
Author: Joachim Breitner <[email protected]>
Date:   Fri Aug 16 17:13:46 2024 +0200

    More fixes

commit 3151f57
Author: Joachim Breitner <[email protected]>
Date:   Fri Aug 16 17:10:35 2024 +0200

    More [autoParam]

commit 54a6616
Author: Joachim Breitner <[email protected]>
Date:   Fri Aug 16 17:07:19 2024 +0200

    Some fixes

commit 9c41f64
Author: Joachim Breitner <[email protected]>
Date:   Fri Aug 16 12:15:03 2024 +0200

    Check for cold cache

commit 66ff376
Author: Joachim Breitner <[email protected]>
Date:   Fri Aug 16 14:54:25 2024 +0200

    No longer needed dsimps?

commit 2298410
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Fri Aug 16 12:24:02 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit 8bca337
Author: Joachim Breitner <[email protected]>
Date:   Fri Aug 16 12:17:43 2024 +0200

    Some reasonable fixes

commit 14247a2
Author: Joachim Breitner <[email protected]>
Date:   Fri Aug 16 12:16:08 2024 +0200

    Revert "work-around dsimp Function.eval"

    This reverts commit 8c36154.

commit 0c86721
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Fri Aug 16 10:35:28 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit 4b2124e
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Fri Aug 16 09:45:57 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit 125f713
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Fri Aug 16 08:51:57 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit af7ab6c
Author: Joachim Breitner <[email protected]>
Date:   Fri Aug 16 08:16:31 2024 +0200

    Style exception

commit f11401e
Author: Joachim Breitner <[email protected]>
Date:   Fri Aug 16 08:08:49 2024 +0200

    toAdditive: transport MatcherInfo

commit 8c36154
Author: Joachim Breitner <[email protected]>
Date:   Thu Aug 15 18:27:00 2024 +0200

    work-around dsimp Function.eval

commit 5fcef86
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Thu Aug 15 14:24:51 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit d4e2758
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Thu Aug 15 13:59:06 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit af1456c
Author: Joachim Breitner <[email protected]>
Date:   Thu Aug 15 15:49:23 2024 +0200

    Fix call to getEqnsFor?

commit c62ab2f
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Thu Aug 15 12:30:12 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit d9bc3e9
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Thu Aug 15 11:47:22 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit 40bc4fe
Author: Joachim Breitner <[email protected]>
Date:   Thu Aug 15 10:50:26 2024 +0000

    chore: do not set release-ci label upon failed PR test (#15775)

    with leanprover/lean4#5022 the need for this
    should have disappeared

commit 2ff3b31
Merge: 33a583e b8ad879
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Thu Aug 15 10:32:05 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit 33a583e
Merge: 1c951db 85647f2
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Mon Jun 3 15:24:02 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit 1c951db
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Mon May 13 18:13:38 2024 +0000

    Trigger CI for leanprover/lean4#4154

commit f05d463
Author: leanprover-community-mathlib4-bot <[email protected]>
Date:   Mon May 13 17:26:47 2024 +0000

    Update lean-toolchain for testing leanprover/lean4#4154
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@nomeata @bjoernkjoshanssen
chore: do not set release-ci label upon failed PR test (#15775)
2546135 
with leanprover/lean4#5022 the need for this
should have disappeared
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@nomeata @bjoernkjoshanssen
chore: do not set release-ci label upon failed PR test (#15775)
1f23434 
with leanprover/lean4#5022 the need for this
should have disappeared
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024
@nomeata @bjoernkjoshanssen
chore: do not set release-ci label upon failed PR test (#15775)
971c664 
with leanprover/lean4#5022 the need for this
should have disappeared
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em Awaiting requested review from kim-em

Assignees
No one assigned
Labels
CI Modifies the continuous integration / deployment setup easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@nomeata @kim-em