Currently, we work around some odd namespacing behavior for private opaque definitions from the Lean frontend by simply un-privating them in our fixture files. The issue is described in this discussion, essentially Lean will namespace private definitions differently depending on what file they are referenced from. If we reference them from an outside file, the frontend decides to additionally qualify the namespaces of these definitions with the file path, but does not do so within the file itself. This is problematic because our caching of constants in the store depends on these names, and we can end up with two different versions of the same constant. An example from that discussion:
It turns out that the private definition Lean.Macro.MethodsRefPointed is referred to by _private.0.Lean.Macro.MethodsRefPointed within Prelude.lean itself, but by _private.Fixtures.Termination.Init.Prelude.0.Lean.Macro.MethodsRefPointed outside of it. So it's compiled separately in Prelude.lean and SizeOf.lean to produce two different constants. If we compile Prelude.lean first, then we're stuck with that version of Lean.Macro.Context.rec that uses _private.0.Lean.Macro.MethodsRefPointed in its type, but the definition above uses _private.Fixtures.Termination.Init.Prelude.0.Lean.Macro.MethodsRefPointed in the lambda for the minor premise. This results in a constant mismatch between these two versions of the private def.
Because we can't further reduce opaque definitions, the typechecker is left with the applied opaque constant that can potentially have different names depending on where it is used, which can result in spurious typechecker constant mismatch errors. Lean clearly doesn't suffer from this problem in its own typechecking, so my first guess is that it's able to reduce them to some more fundamental and unique representation. Pending an investigation where we try to replicate Lean's handling of this issue, perhaps a quick hacky fix would be to manually insert the file path qualifiers ourselves whenever we encounter such a def (in its original file) to prevent this duplication.
Currently, we work around some odd namespacing behavior for private opaque definitions from the Lean frontend by simply un-privating them in our fixture files. The issue is described in this discussion, essentially Lean will namespace private definitions differently depending on what file they are referenced from. If we reference them from an outside file, the frontend decides to additionally qualify the namespaces of these definitions with the file path, but does not do so within the file itself. This is problematic because our caching of constants in the store depends on these names, and we can end up with two different versions of the same constant. An example from that discussion:
Because we can't further reduce
opaquedefinitions, the typechecker is left with the applied opaque constant that can potentially have different names depending on where it is used, which can result in spurious typechecker constant mismatch errors. Lean clearly doesn't suffer from this problem in its own typechecking, so my first guess is that it's able to reduce them to some more fundamental and unique representation. Pending an investigation where we try to replicate Lean's handling of this issue, perhaps a quick hacky fix would be to manually insert the file path qualifiers ourselves whenever we encounter such a def (in its original file) to prevent this duplication.