CI error in the "run tests" phase

Stream: general

[Rémy Degenne]

I have a CI error I don't understand at #10713 . At theexport 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]

Might be a cache bug - merging master might be enough to invalidate whatever bad cache it's using

[Rémy Degenne]

Thanks I'll try that