Generating globally unique identifiers

Stream: metaprogramming / tactics

[Eric Wieser]

docs#assert_not_exists is failing in #17904 because the unique name being generated appears to only be unique within the environment at that point in time. It seems that there's a uniqueness diamond where two files containing supposedly unique names can't be imported simultaneously because of a name clash.

Is there some way to get the current filename and line number to reduce the chance of such a clash?

[Eric Wieser]

The offending lines are here: https://github.com/leanprover-community/mathlib/blob/fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e/src/tactic/assert_exists.lean#L64-L65

[Eric Wieser]

(cc @Xavier Roblot, just to let you know I understand why your PR is failing)

[Eric Wieser]

#17916 is my workaround to at least reduce the probability of this happening.