Zulip Chat Archive

I've noticed that mathport generates incorrect #align when a theorem uses the _root_ namespace. For example, it tries to do is_unit._root_.is_unit_map_of_left_inverse when it should be is_unit_map_of_left_inverse. What would be the right place to submit an issue for this?

Yakov Pechersky (Nov 27 2022 at 01:45):

https://github.com/leanprover-community/mathport/

Yakov Pechersky (Nov 27 2022 at 01:47):

https://github.com/leanprover-community/mathport/blob/f071992a732b95d49b75111dfbdd9cdd9cd371dc/Mathport/Syntax/Translate/Command.lean#L240

Reid Barton (Jan 23 2023 at 18:48):

I also notice this.

Reid Barton (Jan 23 2023 at 18:48):

Does mathport understand _root_ at all?

Reid Barton (Jan 23 2023 at 19:03):

I see more and more lemmas that used lemma _root_.foo in mathlib 3, that got translated into lemma foo in mathlib 4

Reid Barton (Jan 23 2023 at 19:03):

It's probably not a huge deal but it would be more correct to preserve it

Mario Carneiro (Jan 23 2023 at 19:05):

we could calculate whether _root_ is needed and use it only then, but I worry that this will cause a huge disruption if it happens to get a namespace declaration wrong

Mario Carneiro (Jan 23 2023 at 19:06):

Then again, you can already see the result of mathport's perspective of what the namespace is in the generated #align statements, and I don't think those need bulk modification that often

Reid Barton (Jan 23 2023 at 19:40):

hmm, is the idea that mathport doesn't know what name the user actually wrote in a def in mathlib 3, and it has to reverse engineer it from the new constant?

Mario Carneiro (Jan 23 2023 at 20:00):

No, mathport also knows what the user wrote and so an alternative would be to preserve the _root_ness of the original definition instead of resolving and unresolving the name

Mario Carneiro (Jan 23 2023 at 20:01):

If we can do it correctly, I think it would be better to just use it when necessary. We don't preserve lean 3 parentheses either

Reid Barton (Jan 23 2023 at 20:02):

I'm sort of guessing at what is happening because I saw some names that were (inadvertently?) moved into whatever namespace was open at the time, but I didn't look into how that happened. Certainly, there are many other names that do use _root_

Mario Carneiro (Jan 23 2023 at 20:03):

an example where it would make a difference is if the lean 3 file had

def foo := 1
def _root_.bar := 2
namespace A
def a := 1
def _root_.b := 2
def _root_.A.c := 3
end A

then the translated version would be

def foo := 1
def bar := 2
namespace A
def a := 1
def _root_.b := 2
def c := 3
end A

if we reconstruct _root_ness

Mario Carneiro (Jan 23 2023 at 20:05):

Right now mathport just never uses _root_, which is definitely wrong

Mario Carneiro (Jan 23 2023 at 20:06):

it has a heuristic for aligning short names that involves removing the same number of namespaces on both fully qualified names, which can have weird behavior if the lean 3 name is in an unrelated namespace because of use of _root_