Rémy Degenne (Dec 14 2021 at 08:28):
I have a CI error I don't understand at #10713 . At the
export as low-level text file step of the
Run tests CI, I get the error
Run lean --recursive --export=mathlib.txt src/ <unknown>:1:1: error: unknown declaration '_private.3627408217.add' Error: Process completed with exit code 1.
(You can go to the PR and click on
details on the failing CI for more info)
I ran the tests several times because I thought it might go away on its own, but the error stays. Does anyone know what I should do about it?
Eric Wieser (Dec 14 2021 at 08:45):
Might be a cache bug - merging master might be enough to invalidate whatever bad cache it's using
Rémy Degenne (Dec 14 2021 at 08:48):
Thanks I'll try that
Last updated: Aug 03 2023 at 10:10 UTC