From 48bea5e7edd4b5131080e15806784b532ac82e6c Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 21 Aug 2024 18:35:50 +0200 Subject: [PATCH] Switch to Mathlib.Init --- .github/workflows/bors.yml | 6 +++--- .github/workflows/build.yml | 6 +++--- .github/workflows/build.yml.in | 6 +++--- .github/workflows/build_fork.yml | 6 +++--- 4 files changed, 12 insertions(+), 12 deletions(-) diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml index 820d0031f98a7..fc23f92e9c063 100644 --- a/.github/workflows/bors.yml +++ b/.github/workflows/bors.yml @@ -152,9 +152,9 @@ jobs: id: get run: | lake exe cache clean - # Fail quickly if the cache is completely cold, by checking for Batteries.WF - lake exe cache get Batteries.WF - ! test -e ./.lake/packages/batteries/.lake/build/lib/Batteries/WF.olean || lake exe cache get + # Fail quickly if the cache is completely cold, by checking for Mathlib.Init + lake exe cache get Mathlib.Init + ! test -e .lake/build/lib/Mathlib/Init.olean || lake exe cache get - name: build mathlib id: build diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index a9f63936182ce..6c2b580ae9c1a 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -159,9 +159,9 @@ jobs: id: get run: | lake exe cache clean - # Fail quickly if the cache is completely cold, by checking for Batteries.WF - lake exe cache get Batteries.WF - ! test -e ./.lake/packages/batteries/.lake/build/lib/Batteries/WF.olean || lake exe cache get + # Fail quickly if the cache is completely cold, by checking for Mathlib.Init + lake exe cache get Mathlib.Init + ! test -e .lake/build/lib/Mathlib/Init.olean || lake exe cache get - name: build mathlib id: build diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in index 9a0d55d477b5b..5a26b10a2a937 100644 --- a/.github/workflows/build.yml.in +++ b/.github/workflows/build.yml.in @@ -138,9 +138,9 @@ jobs: id: get run: | lake exe cache clean - # Fail quickly if the cache is completely cold, by checking for Batteries.WF - lake exe cache get Batteries.WF - ! test -e ./.lake/packages/batteries/.lake/build/lib/Batteries/WF.olean || lake exe cache get + # Fail quickly if the cache is completely cold, by checking for Mathlib.Init + lake exe cache get Mathlib.Init + ! test -e .lake/build/lib/Mathlib/Init.olean || lake exe cache get - name: build mathlib id: build diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml index 7869e6552d78b..e849add6d9669 100644 --- a/.github/workflows/build_fork.yml +++ b/.github/workflows/build_fork.yml @@ -156,9 +156,9 @@ jobs: id: get run: | lake exe cache clean - # Fail quickly if the cache is completely cold, by checking for Batteries.WF - lake exe cache get Batteries.WF - ! test -e ./.lake/packages/batteries/.lake/build/lib/Batteries/WF.olean || lake exe cache get + # Fail quickly if the cache is completely cold, by checking for Mathlib.Init + lake exe cache get Mathlib.Init + ! test -e .lake/build/lib/Mathlib/Init.olean || lake exe cache get - name: build mathlib id: build