Skip to content

Commit c6b3276

Browse files
committed
chore: allow uploading oleans for LeanHammer (leanprover-community#31327)
This is a preparatory PR that modifies Cache.lean to allow uploading oleans for LeanHammer, paving the way for future PRs to experiment with adding LeanHammer to mathlib. Requested from [#general > lean hammer install failing for 4.24 @ 💬](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/lean.20hammer.20install.20failing.20for.204.2E24/near/554002277)
1 parent 6f5d80b commit c6b3276

File tree

1 file changed

+6
-1
lines changed

1 file changed

+6
-1
lines changed

Cache/IO.lean

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,12 @@ def isPartOfMathlibCache (mod : Name) : Bool := #[
4343
`OpenAIClient,
4444
`Reap,
4545
-- Allow PRs to upload oleans for Canonical for testing.
46-
`Canonical,].contains mod.getRoot
46+
`Canonical,
47+
-- Allow PRs to upload oleans for LeanHammer for testing.
48+
`Duper,
49+
`Auto,
50+
`PremiseSelection,
51+
`Hammer].contains mod.getRoot
4752

4853
/-- Target directory for caching -/
4954
initialize CACHEDIR : FilePath ← do

0 commit comments

Comments
 (0)