mathport failure

Stream: general

[Kevin Buzzard]

In attempting to port the Lean 3 project https://github.com/YaelDillies/LeanTuran to Lean 4, everything went smoothly up until the final ./.lake/build/bin/mathport --make config-project.json Project::all , which fails with

Failed to port { package := "Project", mod3 := `book.FormalBook_Ch11_LinesInThePlane_SylvesterGallai }

The full output (10K lines) contains the lines

[mathport] START book.FormalBook_Ch11_LinesInThePlane_SylvesterGallai

uncaught exception: failed to port Project:Book.FormalBookCh11LinesInThePlaneSylvesterGallai with imports [Leanbin.Init.Default, Mathbin.Tactic.Default, Mathbin.Analysis.InnerProductSpace.Basic, Mathbin.Analysis.InnerProductSpace.Projection]:
import Mathbin.LinearAlgebra.AffineSpace.Independent failed, environment already contains 'Affine.Simplex.independent' from Mathlib.LinearAlgebra.AffineSpace.Independent
 := "Leanbin", mod3 := `init.default }

Anyone have a clue what could be going on?

[Eric Wieser]

docs#Affine.Simplex.independent was renamed very recently (from Affine.Simplex.Independent), which might be relevant

[Kevin Buzzard]

Oh yeah I'm just looking at other errors and it's all the same problem:

uncaught exception: failed to port Project:Rootsystem.F4 with imports [Leanbin.Init.Default, Mathbin.Analysis.InnerProductSpace.Dual, Mathbin.Analysis.NormedSpace.Pointwise, Mathbin.Analysis.Quaternion, Project.Rootsystem.Basic]:
import Mathbin.LinearAlgebra.AffineSpace.Independent failed, environment already contains 'Affine.Simplex.independent' from Mathlib.LinearAlgebra.AffineSpace.Independent

So is there a cheap hack or do I need expert help?

[Kevin Buzzard]

The lean 3 project compiles with mathlib3 commit 65a1391a0106c9204fe45bc73a039f056558cb83 which is current mathlib3 master, and mathport also seems to be on that commit.

[Eric Wieser]

Are you using a more recent copy of mathlib4 than mathport is?

[Eric Wieser]

Or vice versa?

[Kevin Buzzard]

I'm not using any copy of mathlib4 as far as I know? I'm just using LeanTuran and mathport?

[Eric Wieser]

Last time this happened, @Mario Carneiro said:

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)

[Kevin Buzzard]

I suspect I updated mathport with git pull but failed to go through some of the other steps again.

[Kevin Buzzard]

OK I don't know what I'm doing wrong. I deleted mathport and LeanTuran and started by re-cloning everything and going through all the steps on the mathport readme. I get the following errors when running the very final step:

[mathport] START mathlib.combinatorics.additive.salem_spencer

uncaught exception: failed to port Project:Mathlib.Combinatorics.Additive.SalemSpencer with imports [Leanbin.Init.Default, Mathbin.Combinatorics.Additive.SalemSpencer, Mathbin.Data.Zmod.Basic, Project.Mathlib.Algebra.CharP.Basic]:
import Mathbin.LinearAlgebra.AffineSpace.Independent failed, environment already contains 'Affine.Simplex.independent' from Mathlib.LinearAlgebra.AffineSpace.Independent

[mathport] START book.FormalBook_Ch11_LinesInThePlane_SylvesterGallai

uncaught exception: failed to port Project:Book.FormalBookCh11LinesInThePlaneSylvesterGallai with imports [Leanbin.Init.Default, Mathbin.Tactic.Default, Mathbin.Analysis.InnerProductSpace.Basic, Mathbin.Analysis.InnerProductSpace.Projection]:
import Mathbin.LinearAlgebra.AffineSpace.Independent failed, environment already contains 'Affine.Simplex.independent' from Mathlib.LinearAlgebra.AffineSpace.Independent

[mathport] START rootsystem.f4

uncaught exception: failed to port Project:Rootsystem.F4 with imports [Leanbin.Init.Default, Mathbin.Analysis.InnerProductSpace.Dual, Mathbin.Analysis.NormedSpace.Pointwise, Mathbin.Analysis.Quaternion, Project.Rootsystem.Basic]:
import Mathbin.LinearAlgebra.AffineSpace.Independent failed, environment already contains 'Affine.Simplex.independent' from Mathlib.LinearAlgebra.AffineSpace.Independent

[mathport] START mathlib.measure_theory.function.intersectivity

uncaught exception: failed to port Project:Mathlib.MeasureTheory.Function.Intersectivity with imports [Leanbin.Init.Default, Mathbin.MeasureTheory.Function.LpSpace, Mathbin.MeasureTheory.Integral.Average, Mathbin.Order.UpperLower.LocallyFinite, Project.Mathlib.Data.Set.Image]:
import Mathbin.LinearAlgebra.AffineSpace.Independent failed, environment already contains 'Affine.Simplex.independent' from Mathlib.LinearAlgebra.AffineSpace.Independent

[mathport] START mathlib.analysis.convex.continuous

uncaught exception: failed to port Project:Mathlib.Analysis.Convex.Continuous with imports [Leanbin.Init.Default, Mathbin.Analysis.Convex.Intrinsic, Mathbin.Analysis.Convex.Topology, Mathbin.Analysis.InnerProductSpace.PiL2]:
import Mathbin.LinearAlgebra.AffineSpace.Independent failed, environment already contains 'Affine.Simplex.independent' from Mathlib.LinearAlgebra.AffineSpace.Independent

[mathport] START mathlib.measure_theory.measure.lebesgue.eq_haar

uncaught exception: failed to port Project:Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar with imports [Leanbin.Init.Default, Mathbin.MeasureTheory.Measure.Lebesgue.EqHaar, Project.Mathlib.MeasureTheory.Measure.MeasureSpace, Project.Mathlib.MeasureTheory.Measure.OpenPos]:
import Mathbin.LinearAlgebra.AffineSpace.Independent failed, environment already contains 'Affine.Simplex.independent' from Mathlib.LinearAlgebra.AffineSpace.Independent
Failed to port { package := "Project", mod3 := `mathlib.measure_theory.function.intersectivity }

[Mario Carneiro]

Note that mathport master is currently broken, it has not yet recovered from the rc2 bump

[Kevin Buzzard]

If I just want to port a project which depends on mathlib3 master, can I work around this by e.g. using an older version of mathport?

[Mario Carneiro]

yes

[Mario Carneiro]

nothing has really changed syntax-wise in mathport recently, so the only downside will be that the names from the #aligns will be slightly out of date (assuming there have been renames in mathlib)