ambiguous import on OpenBSD

Stream: new members

[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.gcd relative to /usr/local/lib/lean/library, not data.nat.gcd.

[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.

[Reid Barton]

Don't be confused by init/data/nat/default.lean. It is module init.data.nat, and imported automatically by default.

[Notification Bot]

This topic was moved here from #general > ambiguous import by Eric Wieser

[Unpronounxfv'cable]

I will first try to run tests on the packaged lean before i post more confusing stuff here. Thanks, all

[Bryan Gin-ge Chen]

Anne Baanen said:

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

The latest released version (and the version that mathlib master uses) is actually 3.33.0, but I don't know if that's the issue here.

[Reid Barton]

Don't worry about posting confusing stuff! If you're new to Lean and trying to run it on a not-really-supported system, things are bound to be confusing.