Skip to content

Commit 135bc01

Browse files
committed
feat: add cache support for nightly-testing-YYYY-MM-DD tags (leanprover-community#28029)
I often find myself wanting a cache for a nightly-testing-YYYY-MM-DD tag (e.g. when nightly-testing itself is broken, but I need a recent working Mathlib to test something against). The current remote detection code doesn't work, but this seems to fix it. Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
1 parent 7348e5b commit 135bc01

File tree

1 file changed

+31
-1
lines changed

1 file changed

+31
-1
lines changed

Cache/Requests.lean

Lines changed: 31 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -117,6 +117,28 @@ def extractPRNumber (ref : String) : Option Nat := do
117117
else
118118
none
119119

120+
/-- Check if we're in a detached HEAD state at a nightly-testing tag -/
121+
def isDetachedAtNightlyTesting (mathlibDepPath : FilePath) : IO Bool := do
122+
-- Get the current commit hash and check if it's a nightly-testing tag
123+
let currentCommit ← IO.Process.output
124+
{cmd := "git", args := #["rev-parse", "HEAD"], cwd := mathlibDepPath}
125+
if currentCommit.exitCode == 0 then
126+
let commitHash := currentCommit.stdout.trim
127+
let tagInfo ← IO.Process.output
128+
{cmd := "git", args := #["name-rev", "--tags", commitHash], cwd := mathlibDepPath}
129+
if tagInfo.exitCode == 0 then
130+
let parts := tagInfo.stdout.trim.splitOn " "
131+
-- git name-rev returns "commit_hash tags/tag_name" or just "commit_hash undefined" if no tag
132+
if parts.length >= 2 && parts[1]!.startsWith "tags/" then
133+
let tagName := parts[1]!.drop 5 -- Remove "tags/" prefix
134+
return tagName.startsWith "nightly-testing-"
135+
else
136+
return false
137+
else
138+
return false
139+
else
140+
return false
141+
120142
/--
121143
Attempts to determine the GitHub repository of a version of Mathlib from its Git remote.
122144
If the current commit coincides with a PR ref, it will determine the source fork
@@ -134,11 +156,19 @@ def getRemoteRepo (mathlibDepPath : FilePath) : IO RepoInfo := do
134156
if currentBranch.exitCode == 0 then
135157
let branchName := currentBranch.stdout.trim.stripPrefix "heads/"
136158
IO.println s!"Current branch: {branchName}"
159+
160+
-- Check if we're in a detached HEAD state at a nightly-testing tag
161+
let isDetachedAtNightlyTesting ← if branchName == "HEAD" then
162+
isDetachedAtNightlyTesting mathlibDepPath
163+
else
164+
pure false
165+
137166
-- Check if we're on a branch that should use nightly-testing remote
138167
let shouldUseNightlyTesting := branchName == "nightly-testing" ||
139168
branchName.startsWith "lean-pr-testing-" ||
140169
branchName.startsWith "batteries-pr-testing-" ||
141-
branchName.startsWith "bump/"
170+
branchName.startsWith "bump/" ||
171+
isDetachedAtNightlyTesting
142172

143173
if shouldUseNightlyTesting then
144174
-- Try to use nightly-testing remote

0 commit comments

Comments
 (0)