mathport error

Stream: lean4

[Kayla Thomas]

pthomas@PC:~/Desktop/github/mathport$ ./build/bin/mathport --make config-project.json Project::all
uncaught exception: Error decoding JSON: Mathport.Config.dubiousMsg: Bool expected

[Kayla Thomas]

This is after following the instructions for https://github.com/leanprover-community/mathport#running-on-a-project-other-than-mathlib

[Kayla Thomas]

The previous steps worked, except I had to sudo apt install libgmp3-dev instead of gmp gmp-devel.

[Eric Wieser]

This is a new configuration option that was added after those instructions were written

[Eric Wieser]

I guess lean4#2225 is probably to blame for it not being optional

[Scott Morrison]

@Kayla Thomas, thanks for the error report. I've updated the instructions at https://github.com/leanprover-community/mathport/pull/239.

[Scott Morrison]

If you don't want to wait for that PR, you just need to copy across the three new configuration options from config.json to config-project.json.

[Kayla Thomas]

Thank you!

[Kayla Thomas]

I am getting a build error for mathport after pulling the most recent version:

[1885/1940] Building Mathport.Syntax.Translate.Tactic.Mathlib.Apply
error: > LEAN_PATH=./build/lib:./lake-packages/mathlib/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/std/build/lib LD_LIBRARY_PATH=./build/lib:./build/lib /home/pthomas/.elan/toolchains/leanprover--lean4---nightly-2023-05-31/bin/lean ./././Mathport/Syntax/Translate/Command.lean -R ././. -o ./build/lib/Mathport/Syntax/Translate/Command.olean -i ./build/lib/Mathport/Syntax/Translate/Command.ilean -c ./build/ir/Mathport/Syntax/Translate/Command.c --load-dynlib=./build/lib/libleanffi.so
error: stdout:
./././Mathport/Syntax/Translate/Command.lean:533:60: error: unknown parser notation3Item ./././Mathport/Syntax/Translate/Command.lean:537:29: error: expected '[', 'binder_predicate', 'elab', 'elab_rules', 'infix', 'infixl', 'infixr', 'instance', 'macro', 'macro_rules', 'notation', 'notation3', 'postfix', 'prefix', 'syntax' or 'unif_hint' ./././Mathport/Syntax/Translate/Command.lean:549:68: error: expected ':' ./././Mathport/Syntax/Translate/Command.lean:570:80: error: expected '(', identifier or string literal ./././Mathport/Syntax/Translate/Command.lean:572:4: error: IR check failed at 'Mathport.Translate.trNotationCmd._lambda_8', error: unknown declaration '_private.Mathport.Syntax.Translate.Command.0.Mathport.Translate.trNotation3' ./././Mathport/Syntax/Translate/Command.lean:650:4: error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Mathport.Translate.trNotationCmd', and it does not have executable code error: external command /home/pthomas/.elan/toolchains/leanprover--lean4---nightly-2023-05-31/bin/lean` exited with code 1

[Kayla Thomas]

After running elan update:
pthomas@PC:~/Desktop/github/mathport$ lake exe cache get
No files to download
Decompressing 2887 file(s)
pthomas@PC:~/Desktop/github/mathport$ make build
lake build
[1854/1940] Building Mathport.Syntax.Translate.Command
error: > LEAN_PATH=./build/lib:./lake-packages/mathlib/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/std/build/lib LD_LIBRARY_PATH=./build/lib:./build/lib /home/pthomas/.elan/toolchains/leanprover--lean4---nightly-2023-05-31/bin/lean ./././Mathport/Syntax/Translate/Command.lean -R ././. -o ./build/lib/Mathport/Syntax/Translate/Command.olean -i ./build/lib/Mathport/Syntax/Translate/Command.ilean -c ./build/ir/Mathport/Syntax/Translate/Command.c --load-dynlib=./build/lib/libleanffi.so
error: stdout:
./././Mathport/Syntax/Translate/Command.lean:533:60: error: unknown parser notation3Item ./././Mathport/Syntax/Translate/Command.lean:537:29: error: expected '[', 'binder_predicate', 'elab', 'elab_rules', 'infix', 'infixl', 'infixr', 'instance', 'macro', 'macro_rules', 'notation', 'notation3', 'postfix', 'prefix', 'syntax' or 'unif_hint' ./././Mathport/Syntax/Translate/Command.lean:549:68: error: expected ':' ./././Mathport/Syntax/Translate/Command.lean:570:80: error: expected '(', identifier or string literal ./././Mathport/Syntax/Translate/Command.lean:572:4: error: IR check failed at 'Mathport.Translate.trNotationCmd._lambda_8', error: unknown declaration '_private.Mathport.Syntax.Translate.Command.0.Mathport.Translate.trNotation3' ./././Mathport/Syntax/Translate/Command.lean:650:4: error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Mathport.Translate.trNotationCmd', and it does not have executable code error: external command /home/pthomas/.elan/toolchains/leanprover--lean4---nightly-2023-05-31/bin/lean` exited with code 1
make: *** [Makefile build] Error 1
pthomas@PC:~/Desktop/github/mathport$

[Mario Carneiro]

should be fixed

[Kayla Thomas]

Yep. Thank you!

[Rishi Mehta]

Hello, I'm trying to port a lean 3 project to lean 4 following the instructions on the mathport README. I got to the point of running ./build/bin/mathport --make config-project.json Project::all, but this gives me the error:

uncaught exception: failed to port Project:MyProject.SolveGoals with imports [Leanbin.Init.Default, Mathbin.Tactic.Default, Mathbin.Data.List.Defs]:
import Mathbin.Order.Lattice failed, environment already contains 'MonotoneOn.map_sup' from Mathlib.Order.Lattice

Any idea what this is?

[María Inés de Frutos Fernández]

I think it is caused by the missing aligns, but maybe someone can confirm this. I opened #7529.

[Eric Wieser]

@Yaël Dillies, is this an incomplete forward-port?

[Yaël Dillies]

Yes exactly. You were the one asking for a pre-forward port PR.

[Eric Wieser]

I think this is more a reminder that #out-of-sync is an obstacle to mathport

[Eric Wieser]

(at least, if you don't use the port-complete tag and just hope that master of both will be fine)

[María Inés de Frutos Fernández]

I am getting this mathport error:

uncaught exception: uncaught exception: failed to port Project:Galois with
imports [Leanbin.Init.Default, Mathbin.FieldTheory.KrullTopology,
Mathbin.FieldTheory.IsAlgClosed.AlgebraicClosure, Mathbin.GroupTheory.Abelianization]:

import Mathbin.Algebra.Order.Ring.Canonical failed, environment already contains
'CanonicallyOrderedCommSemiring.toCanonicallyOrderedAddMonoid'
from Mathlib.Algebra.Order.Ring.Canonical

I think this may have been caused by the name change in #7503; is the solution to add this align?

#align canonically_ordered_comm_semiring.to_canonically_ordered_add_monoid CanonicallyOrderedCommSemiring.toCanonicallyOrderedAddCommMonoid

[Eric Wieser]

I think that line is a bad idea, because docs3#canonically_ordered_comm_semiring.to_canonically_ordered_add_monoid doesn't exist

[Eric Wieser]

Sorry, got my PRs crossed. Yes, that align is good, but I think we should wait for @Mario Carneiro's opinion on why things break without it

[Mario Carneiro]

As I mentioned in another thread, this error is generally an indication that you have two incompatible versions of mathlib4 in use, and the usual way to fix it is to make sure everything is at the latest version (rerun the make commands)

[Mario Carneiro]

The presence or non-presence of aligns does not cause this error. The only way you can legitimately get this error is if you have two definitions with the same name in different files that don't import each other, but this would fail anyway in mathlib CI because Mathlib.lean would not be able to build

[María Inés de Frutos Fernández]

Do I need to download mathport again? I have repeated all the steps here, starting from the lake exe cache get, and I am still getting the same error.

[Mario Carneiro]

you should also git pull if it's not a new clone of mathport

[María Inés de Frutos Fernández]

Ah ok, thanks!

[Bhavik Mehta]

I'm presuming this thread is for miscellaneous errors in mathport - are naming errors when using mathport expected, or should I try to make an issue / isolate what's happening?

[Mario Carneiro]

What are the circumstances?

[Mario Carneiro]

Unfortunately yes, there are some cases in which mathport will not perform renames it knows about when the identifier is used in certain positions (most notably after dot notation and in some tactics)

[Bhavik Mehta]

That was one of my cases - simple_graph.adj.ne used in dot notation changed .ne to .Ne for some reason. I also had some rewrites not get renamed, and a different thing where mathport chose the name but then didn't use the new name later on

[Mario Carneiro]

yeah those are basically both known issues

[Mario Carneiro]

(the reason it renamed .ne to .Ne was because it doesn't have the type information to know what declaration is being referred to there so it makes its best guess based on other declarations and dot notation things it has seen)