Skip to content

[Merged by Bors] - ci: Revert cache get default behavior for skip-proofwidgets #35542

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

Closed
marcelolynch wants to merge 1 commit into from
Closed

[Merged by Bors] - ci: Revert cache get default behavior for skip-proofwidgets #35542

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 9 additions & 9 deletions .github/workflows/build_template.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -323,7 +323,7 @@ jobs:

# Fail quickly if the cache is completely cold, by checking for Mathlib.Init
echo "Attempting to fetch olean for Mathlib/Init.lean from cache..."
../tools-branch/.lake/build/bin/cache get Mathlib/Init.lean
../tools-branch/.lake/build/bin/cache --skip-proofwidgets get Mathlib/Init.lean

- name: get cache (2/3 - test Mathlib.Init cache)
id: get_cache_part2_test
Expand All @@ -343,10 +343,10 @@ jobs:
if [[ "${{ steps.get_cache_part2_test.outcome }}" == "success" ]]; then
echo "Fetching all remaining cache..."

../tools-branch/.lake/build/bin/cache get
../tools-branch/.lake/build/bin/cache --skip-proofwidgets get

# Run again with --repo, to ensure we actually get the oleans.
../tools-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get
../tools-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} --skip-proofwidgets get
else
echo "WARNING: 'lake build --no-build -v Mathlib.Init' failed."
echo "No cache for 'Mathlib.Init' available or it could not be prepared."
Expand Down Expand Up @@ -413,8 +413,8 @@ jobs:
shell: bash
run: |
cd pr-branch
../tools-branch/.lake/build/bin/cache get Archive.lean
../tools-branch/.lake/build/bin/cache get Counterexamples.lean
../tools-branch/.lake/build/bin/cache --skip-proofwidgets get Archive.lean
../tools-branch/.lake/build/bin/cache --skip-proofwidgets get Counterexamples.lean

- name: build archive
id: archive
Expand Down Expand Up @@ -708,16 +708,16 @@ jobs:
- name: get cache for Mathlib
run: |
# Run once without --repo, so we can diagnose what `lake exe cache get` wants to do by itself.
lake exe cache --include-proofwidgets get
lake exe cache get
# Run again with --repo, so ensure we actually get the oleans.
lake exe cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} --include-proofwidgets get
lake exe cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get

- name: get cache for Archive and Counterexamples
run: |
# Run once without --repo, so we can diagnose what `lake exe cache get` wants to do by itself.
lake exe cache --include-proofwidgets get Archive Counterexamples
lake exe cache get Archive Counterexamples
# Run again with --repo, so ensure we actually get the oleans.
lake exe cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} --include-proofwidgets get Archive Counterexamples
lake exe cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get Archive Counterexamples

- name: verify that everything was available in the cache
run: |
Expand Down
6 changes: 2 additions & 4 deletions Cache/Main.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ Commands:
Options:
--repo=OWNER/REPO Override the repository to fetch/push cache from
--staging-dir=<output-directory> Required for 'stage', 'stage!', 'unstage' and 'put-staged': staging directory.
--include-proofwidgets Include fetching/building ProofWidgets release assets during 'get'
--skip-proofwidgets Skip fetching/building ProofWidgets release assets during 'get'

* Linked files refer to local cache files with corresponding Lean sources
* Commands ending with '!' should be used manually, when hot-fixes are needed
Expand Down Expand Up @@ -101,9 +101,7 @@ def main (args : List String) : IO Unit := do
-- parse relevant options, ignore the rest
let repo? ← parseNamedOpt "repo" options
let stagingDir? ← parseNamedOpt "staging-dir" options
let includeProofWidgets := parseFlagOpt "include-proofwidgets" options
let inGitHubActions := (← IO.getEnv "GITHUB_ACTIONS") == some "true"
let skipProofWidgets := inGitHubActions && !includeProofWidgets
let skipProofWidgets := parseFlagOpt "skip-proofwidgets" options

let mut roots : Std.HashMap Lean.Name FilePath ← parseArgs args
if roots.isEmpty then do
Expand Down
Loading