Skip to content

Commit

Permalink
Trigger CI for leanprover/lean4#6744
Browse files Browse the repository at this point in the history
  • Loading branch information
leanprover-community-mathlib4-bot committed Feb 4, 2025
2 parents 4865865 + 9bdd95b commit 4acb642
Show file tree
Hide file tree
Showing 1,159 changed files with 22,137 additions and 17,561 deletions.
5 changes: 5 additions & 0 deletions .github/workflows/daily.yml
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,10 @@ jobs:
./elan-init -y --default-toolchain none
echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
# Checkout repository, so that we can fetch tags to decide which branch we want.
- name: Checkout branch or tag
uses: actions/checkout@v4

- name: Fetch latest tags (if nightly)
if: matrix.branch_type == 'nightly'
run: |
Expand All @@ -52,6 +56,7 @@ jobs:
echo "BRANCH_REF=${{ env.LATEST_TAG }}" >> "$GITHUB_ENV"
fi
# Checkout the branch or tag we want to test.
- name: Checkout branch or tag
uses: actions/checkout@v4
with:
Expand Down
10 changes: 6 additions & 4 deletions .github/workflows/maintainer_bors.yml
Original file line number Diff line number Diff line change
Expand Up @@ -77,13 +77,15 @@ jobs:
( steps.user_permission.outputs.require-result == 'true' ||
steps.merge_or_delegate.outputs.bot == 'true' ) }}
id: remove_labels
name: Remove "awaiting-author"
name: Remove "awaiting-author" and "maintainer-merge"
# we use curl rather than octokit/request-action so that the job won't fail
# (and send an annoying email) if the labels don't exist
run: |
curl --request DELETE \
--url "https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}${{ github.event.pull_request.number }}/labels/awaiting-author" \
--header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
for label in awaiting-author maintainer-merge; do
curl --request DELETE \
--url "https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}${{ github.event.pull_request.number }}/labels/${label}" \
--header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
done
- name: Set up Python
if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
Expand Down
4 changes: 3 additions & 1 deletion .github/workflows/maintainer_merge.yml
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ jobs:
# both set simultaneously: depending on the event that triggers the PR, usually only one is set
env:
AUTHOR: ${{ github.event.comment.user.login }}${{ github.event.review.user.login }}
PR_AUTHOR: ${{ github.event.issue.user.login }}${{ github.event.pull_request.user.login }}
PR_NUMBER: ${{ github.event.issue.number }}${{ github.event.pull_request.number }}
COMMENT_EVENT: ${{ github.event.comment.body }}
COMMENT_REVIEW: ${{ github.event.review.body }}
Expand All @@ -32,6 +33,7 @@ jobs:
- name: Find maintainer merge/delegate
id: merge_or_delegate
run: |
echo "PR author: ${PR_AUTHOR}"
COMMENT="${COMMENT_EVENT}${COMMENT_REVIEW}"
# we strip `\r` since line endings from GitHub contain this character
Expand Down Expand Up @@ -81,7 +83,7 @@ jobs:
echo ""
message="$(
./scripts/maintainer_merge_message.sh "${AUTHOR}" "${{ steps.merge_or_delegate.outputs.mOrD }}" "${EVENT_NAME}" "${PR_NUMBER}" "${PR_URL}" "${PR_TITLE_ISSUE}${PR_TITLE_PR}" "${COMMENT_EVENT}${COMMENT_REVIEW}"
./scripts/maintainer_merge_message.sh "${AUTHOR}" "${{ steps.merge_or_delegate.outputs.mOrD }}" "${EVENT_NAME}" "${PR_NUMBER}" "${PR_URL}" "${PR_TITLE_ISSUE}${PR_TITLE_PR}" "${COMMENT_EVENT}${COMMENT_REVIEW}" "${PR_AUTHOR}"
)"
printf 'title<<EOF\n%s\nEOF' "${message}" | tee "$GITHUB_OUTPUT"
Expand Down
2 changes: 0 additions & 2 deletions Archive/Examples/IfNormalization/Result.lean
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes
-/
import Archive.Examples.IfNormalization.Statement
import Mathlib.Algebra.Order.Monoid.Canonical.Defs
import Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
import Mathlib.Data.List.AList
import Mathlib.Tactic.Recall

Expand Down
4 changes: 1 addition & 3 deletions Archive/Examples/IfNormalization/WithoutAesop.lean
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes, Kim Morrison
-/
import Archive.Examples.IfNormalization.Statement
import Mathlib.Algebra.Order.Monoid.Canonical.Defs
import Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
import Mathlib.Data.List.AList

/-!
Expand All @@ -20,7 +18,7 @@ we put primes on the declarations in the file.)
namespace IfExpr

attribute [local simp] eval normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars
List.disjoint max_add_add_right max_mul_mul_left Nat.lt_add_one_iff le_add_of_le_right
List.disjoint

theorem eval_ite_ite' {a b c d e : IfExpr} {f : ℕ → Bool} :
(ite (ite a b c) d e).eval f = (ite a (ite b d e) (ite c d e)).eval f := by
Expand Down
3 changes: 0 additions & 3 deletions Archive/Wiedijk100Theorems/FriendshipGraphs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,6 @@ Authors: Aaron Anderson, Jalex Stark, Kyle Miller
-/
import Mathlib.Combinatorics.SimpleGraph.AdjMatrix
import Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
import Mathlib.Data.Int.ModEq
import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic.IntervalCases

/-!
# The Friendship Theorem
Expand Down
3 changes: 1 addition & 2 deletions Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,8 @@ Copyright (c) 2021 Damiano Testa. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Damiano Testa
-/
import Mathlib.Data.ZMod.Basic
import Mathlib.Algebra.Order.Monoid.Basic
import Mathlib.Algebra.Ring.Subsemiring.Order
import Mathlib.Data.ZMod.Basic

/-!
Expand Down
5 changes: 0 additions & 5 deletions Counterexamples/CliffordAlgebraNotInjective.lean
Original file line number Diff line number Diff line change
Expand Up @@ -5,12 +5,7 @@ Authors: Eric Wieser
-/
import Mathlib.Algebra.CharP.Pi
import Mathlib.Algebra.CharP.Quotient
import Mathlib.Algebra.CharP.Two
import Mathlib.Algebra.MvPolynomial.CommRing
import Mathlib.Data.ZMod.Basic
import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
import Mathlib.LinearAlgebra.Finsupp.SumProd
import Mathlib.RingTheory.MvPolynomial.Basic
import Mathlib.RingTheory.MvPolynomial.Ideal

Expand Down
3 changes: 1 addition & 2 deletions Counterexamples/HomogeneousPrimeNotPrime.lean
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johan Commelin, Eric Wieser, Jujian Zhang
-/
import Mathlib.Algebra.Divisibility.Prod
import Mathlib.Data.Fintype.Units
import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal
import Mathlib.Data.ZMod.Basic
import Mathlib.Tactic.DeriveFintype

/-!
# A homogeneous ideal that is homogeneously prime but not prime
Expand Down
2 changes: 0 additions & 2 deletions Counterexamples/QuadraticForm.lean
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Wieser
-/
import Mathlib.LinearAlgebra.QuadraticForm.Basic
import Mathlib.Algebra.CharP.Two
import Mathlib.Data.ZMod.Basic

/-!
# `QuadraticForm R M` and `Subtype LinearMap.IsSymm` are distinct notions in characteristic 2
Expand Down
Loading

0 comments on commit 4acb642

Please sign in to comment.