Zulip Chat Archive

Stream: general

Topic: CI error in the "run tests" phase

Rémy Degenne (Dec 14 2021 at 08:28):

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 (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: Dec 20 2023 at 11:08 UTC