namespace conflict advice

Stream: new members

[Vasily Ilin]

I want to use mul_one https://leanprover-community.github.io/mathlib_docs/algebra/group/defs.html#mul_one in a proof, where I have open algebra.tensor_product. I am getting a namespace-conflict because of it. How do I tell Lean to use the one I want?

[Yaël Dillies]

The correct answer is to mark docs#algebra.tensor_product.mul_one as protected. The bandaid solution is to call _root_.mul_one.

[Vasily Ilin]

Is there anything wrong with _root_.mul_one? What is _root_?

[Yaël Dillies]

The problem with that solution is that it doesn't fix the source of the problem, but that's not something you have to worry about (I will worry about it for you). root is the root namespace, the default namespace that's always open.

[Kyle Miller]

You can think about _root_ as being the root namespace, but technically it's not a namespace and instead a prefix that the parser/elaborator specifically looks for when resolving names. When a name starts with _root_, Lean looks for a declaration whose name is exactly what comes after _root_, ignoring aliases (names due to open or export).

When you're defining something, if the name doesn't start with _root_, it uses the current namespace as a prefix to get the name being defined, and if it does start with _root_ it just removes _root_ to get the name.

[Luis Castillo]

Hi, all! I am using a file to run my lean game and it appears the error "invalid namespace IncidencePlane". Could anyone check if I have to change sth in this file (https://github.com/mmasdeu/hilbertgame/blob/main/src/tutorial_world/incidenceplane.lean)? Thank you!!

[Eric Wieser]

Can you link /paste your full error log? I'm pretty sure you get "import not found" earlier in the error messages, which results in the namespace not existing yet

[Luis Castillo]

Hi, Eric!! The error appears at the bottom right corner of this screen: https://luisscastillo.github.io/lean-game/?world=1&level=5

[Luis Castillo]

I can't perceive the error on GitHub Actions...

[Luis Castillo]

If I open the error, this window appears: You are running Lean in a directory without a leanpkg.toml file, this is NOT supported. Please open the directory containing the leanpkg.toml file instead (using "File / Open Folder..."). More details here: https://leanprover-community.github.io/install/project.html

[Luis Castillo]

Watch this:

• The error disappears when I run lean --path and the answer is:

$ lean --path
{
"is_user_leanpkg_path": false,
"leanpkg_path_file": "C:\\Users\\mypc\\euclidgame\\euclidgame\\leanpkg.path",
"path": [
"C:\\Users\\mypc\\.elan\\toolchains\\leanprover-community--lean---3.46.0\\bin\\..\\library",
"C:\\Users\\mypc\\.elan\\toolchains\\leanprover-community--lean---3.46.0\\bin\\..\\lib\\lean\\library",
"C:\\Users\\mypc\\euclidgame\\euclidgame\\_target/deps/mathlib/src",
"C:\\Users\\mypc\\euclidgame\\euclidgame\\src"
]
}

[Luis Castillo]

However,

• It does not work when I run lean --path and the answer is:

$ lean --path
{
"is_user_leanpkg_path": true,
"leanpkg_path_file": "C:\\Users\\mypc\\.lean\\leanpkg.path",
"path": [
"C:\\Users\\mypc\\.elan\\toolchains\\stable\\bin\\..\\library",
"C:\\Users\\mypc\\.elan\\toolchains\\stable\\bin\\..\\lib\\lean\\library"
]
}

[Luis Castillo]

The problem is that I am using the second path and I do not know how to change it into the first one...

[Luis Castillo]

I've been watching if the error comes from "Install elan" here (https://github.com/luisscastillo/lean-game/blob/main/.github/workflows/euclidegame.yml#L55), but it doesn't...

[Luis Castillo]

If we manage to solve this, then we are done :pray: :heart: