ambiguous import

Stream: general

[Unpronounxfv'cable]

Hi.
I'm using lean3 from OpenBSD ports.
It comes without the mathlib.
So i git-cloned the mathlib, built it with leanpkg and put the result in $HOME/src/mathlib.
If I call
env LEAN_PATH=/usr/local/lib/lean/library/init:/usr/local/lib/lean/library/:$HOME/src/mathlib/src lean src/try.lean
(try.lean imports data.nat, opens nat, and uses nat.gcd),
the following error is blurted:
$HOME/src/lean/try.lean:1:0: error: ambiguous import, it can be '/usr/local/lib/lean/library/init/data/nat/gcd.lean' or '$HOME/src/mathlib/src/data/nat/gcd.lean'
(I substituted $HOME for the actual path)
It seems as if the standard data.nat-module and mathlib's data.nat module export the same symbols.
A second error message is:
invalid import: data.nat.prime could not resolve import: data.nat.prime
which is strange, because prime.lean is under src/mathlib/src/data/nat,
the same directory which contains the gcd.lean, the existence of which just caused the "ambigious import" error.
Is there a way to tell lean3 to just use the first definition found?

[Reid Barton]

/usr/local/lib/lean/library/init should not be on LEAN_PATH.
More generally you're not really supposed to set LEAN_PATH yourself, but maybe the supporting infrastructure doesn't exist yet on OpenBSD, not sure.

[Anne Baanen]

I suspect part of the error is also an incompatible lean version for the mathlib version (some core Lean definitions got moved to mathlib, which can cause this duplication error). Could you add #eval lean.version to your file and report what it says?

[Reid Barton]

The file /usr/local/lib/lean/library/init/data/nat/gcd.lean is init.data.nat relative to /usr/local/lib/lean/library, not data.nat.

[Unpronounxfv'cable]

Anne Baanen said:

I suspect part of the error is also an incompatible lean version for the mathlib version (some core Lean definitions got moved to mathlib, which can cause this duplication error). Could you add #eval lean.version to your file and report what it says?

It says:
(3, (32, 1))

[Unpronounxfv'cable]

It says:
(3, (32, 1))

[Anne Baanen]

Hmm, that is indeed the latest version, so my suspicion was unfounded.

[Unpronounxfv'cable]

Strangerer and strangerer:
lean --path says:
"is_user_leanpkg_path": true,
"leanpkg_path_file": "/home/bauerm/.lean/leanpkg.path",
"path": [
"$HOME/.lean/./.",
"/usr/local/bin/../library",
"/usr/local/bin/../lib/lean/library"
]
When called on the try.lean, it refuses with:
file 'data/nat' not found in the search path
But data.nat should be there even in lean without mathlib, right?

[Reid Barton]

I don't think either the Lean core library or mathlib has a data.nat.