error: unknown declaration _private

Stream: general

[Floris van Doorn]

I got an error in the CI that I've never seen before, during the export as low-level text file step:

Run lean --recursive --export=mathlib.txt src/
  lean --recursive --export=mathlib.txt src/
  shell: /usr/bin/bash -e {0}
<unknown>:1:1: error: unknown declaration '_private.1263093571.lt'
Error: Process completed with exit code 1.

https://github.com/leanprover-community/mathlib/runs/3932628186

Anyone knows what's up here? I already tried re-running all jobs, it's a reproducible error.

[Floris van Doorn]

Oh, this has been mentioned here
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/bors.20failing
Was there any solution to this? Is this just an unlucky hash collision or something?

[Floris van Doorn]

@Bryan Gin-ge Chen

[Bryan Gin-ge Chen]

The error didn't come back after bors split the batch in the failure I linked to, so it being some kind of hash collision makes sense to me.

[Floris van Doorn]

Ok, thanks! I tried merging into master. Hopefully that "fixes" it.

[Kevin Buzzard]

I don't know anything about CI but I'm interested in learning what a hash collision is. I thought that a hash was something like a 64 character string of garbage and the chances of two different collections of files having the same hash was something we'd never see before the sun burnt out

[Ruben Van de Velde]

It depends on how many characters you use

[Floris van Doorn]

This is probably not an actual hash collision (because in that case I would expect an error of the form declaration ... already exists).
As Ruben says, it depends on the number of characters you use. In the name of the private definition you see that it uses 10 digits, which is still a huge amount, but already a lot less (if we made 300k private definitions, we'd get some hash collisions).
Secondly, it depends on how you generate these hashes. For private definitions, no random number generator is used, so that the name will be the same if you compile the (same) library twice. So it computes it based on some data about the library. In Lean 2 we got a hash collision this way (leanprover/lean#648), since for two private declarations this data was exactly the same.

[Floris van Doorn]

I just got another curious error message in the export as low-level text file step:

/home/ghrunner/actions-runner/_work/_temp/0b458b3b-45ef-4c14-a948-d0340aaa6393.sh: line 1: 1393818 Killed                  lean --recursive --export=mathlib.txt src/

https://github.com/leanprover-community/mathlib/runs/3963242676