Zulip Chat Archive

Stream: new members

Topic: ambiguous import on OpenBSD


Unpronounxfv'cable (Sep 22 2021 at 13:46):

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 (Sep 22 2021 at 13:47):

/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 (Sep 22 2021 at 13:48):

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 (Sep 22 2021 at 13:48):

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 (Sep 22 2021 at 13:49):

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 (Sep 22 2021 at 13:59):

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

Anne Baanen (Sep 22 2021 at 13:59):

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

Unpronounxfv'cable (Sep 22 2021 at 14:05):

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 (Sep 22 2021 at 14:09):

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

Reid Barton (Sep 22 2021 at 14:11):

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

Notification Bot (Sep 22 2021 at 14:12):

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

Unpronounxfv'cable (Sep 22 2021 at 14:16):

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

Bryan Gin-ge Chen (Sep 22 2021 at 14:38):

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 (Sep 22 2021 at 14:43):

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.


Last updated: Dec 20 2023 at 11:08 UTC