Porting weierstrass_curve as an exercise in learning Lean 4

Stream: new members

[Lars Ericson]

As an exercise in learning Lean 4 I am trying to port the weierstrass_curve file by @Kevin Buzzard referred to in this paper. I made it up to line 154 of the file. If this is already ported please let me know the URL of the GitHub so I can see the Lean 4 solution. Otherwise I would greatly appreciate help. There are a couple of instances with new syntax I don't know how to translate:

"invalid binder annotation"

instance [inhabited R] : inhabited $ weierstrass_curve R :=
⟨⟨default, default, default, default, default⟩⟩

"expected '}'

lemma c_relation : 1728 * W.Δ = W.c₄ ^ 3 - W.c₆ ^ 2 :=
by { simp only [b₂, b₄, b₆, b₈, c₄, c₆, Δ], ring1 }

Other than that here is the first segment:

/-
Lean 4 translation of lines 1-154 of

https://github.com/alreadydone/mathlib/blob/associativity/src/algebraic_geometry/elliptic_curve/weierstrass.lean

as referred to in

https://arxiv.org/pdf/2302.10640.pdf

Code sections in comments starting with DK for Don't Know are ones I don't know how to translate.

-/

import Mathlib.Data.PNat.Prime
import Mathlib.Algebra.CubicDiscriminant
import Mathlib.Analysis.NormedSpace.Basic
import Mathlib.Tactic.LinearCombination
open Mathlib.Tactic.LinearCombination

#check Cubic.disc
#check NormedRing
#check linearCombination
#check CommRing

/-DK

private meta def map_simp : tactic unit :=
`[simp only [map_one, map_bit0, map_bit1, map_neg, map_add, map_sub, map_mul, map_pow]]

private meta def eval_simp : tactic unit :=
`[simp only [eval_C, eval_X, eval_add, eval_sub, eval_mul, eval_pow]]

private meta def C_simp : tactic unit := `[simp only [C_0, C_1, C_neg, C_add, C_sub, C_mul, C_pow]]

-/

universe u v

variable {R : Type u}

@[ext] structure weierstrass_curve (R : Type u) := (a₁ a₂ a₃ a₄ a₆ : R)

/-DK: "invalid binder annotation"

instance [inhabited R] : inhabited $ weierstrass_curve R :=
⟨⟨default, default, default, default, default⟩⟩

-/

namespace weierstrass_curve

variable [CommRing R] (W : weierstrass_curve R)

section quantity

/-- The `b₂` coefficient of a Weierstrass curve. -/
@[simp] def b₂ : R := W.a₁ ^ 2 + 4 * W.a₂

/-- The `b₄` coefficient of a Weierstrass curve. -/
@[simp] def b₄ : R := 2 * W.a₄ + W.a₁ * W.a₃

/-- The `b₆` coefficient of a Weierstrass curve. -/
@[simp] def b₆ : R := W.a₃ ^ 2 + 4 * W.a₆

/-- The `b₈` coefficient of a Weierstrass curve. -/
@[simp] def b₈ : R :=
W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2

/-DK: "expected '}'"
lemma b_relation : 4 * W.b₈ = W.b₂ * W.b₆ - W.b₄ ^ 2 := by { simp only [b₂, b₄, b₆, b₈], ring1 }
-/

/-- The `c₄` coefficient of a Weierstrass curve. -/
@[simp] def c₄ : R := W.b₂ ^ 2 - 24 * W.b₄

/-- The `c₆` coefficient of a Weierstrass curve. -/
@[simp] def c₆ : R := -W.b₂ ^ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆

/-- The discriminant `Δ` of a Weierstrass curve. If `R` is a field, then this polynomial vanishes
if and only if the cubic curve cut out by this equation is singular. Sometimes only defined up to
sign in the literature; we choose the sign used by the LMFDB. For more discussion, see
[the LMFDB page on discriminants](https://www.lmfdb.org/knowledge/show/ec.discriminant). -/
@[simp] def Δ : R := -W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆

/-DK: "expected '}'"

lemma c_relation : 1728 * W.Δ = W.c₄ ^ 3 - W.c₆ ^ 2 :=
by { simp only [b₂, b₄, b₆, b₈, c₄, c₆, Δ], ring1 }

-/

end quantity

section variable_change

/-! ### Variable changes -/

variable (u : Rˣ) (r s t : R)

/-- The Weierstrass curve over `R` induced by an admissible linear change of variables
$(X, Y) \mapsto (u^2X + r, u^3Y + u^2sX + t)$ for some $u \in R^\times$ and some $r, s, t \in R$. -/
@[simps] def variable_change : weierstrass_curve R :=
{ a₁ := ↑u⁻¹ * (W.a₁ + 2 * s),
  a₂ := ↑u⁻¹ ^ 2 * (W.a₂ - s * W.a₁ + 3 * r - s ^ 2),
  a₃ := ↑u⁻¹ ^ 3 * (W.a₃ + r * W.a₁ + 2 * t),
  a₄ := ↑u⁻¹ ^ 4 * (W.a₄ - s * W.a₃ + 2 * r * W.a₂ - (t + r * s) * W.a₁ + 3 * r ^ 2 - 2 * s * t),
  a₆ := ↑u⁻¹ ^ 6 * (W.a₆ + r * W.a₄ + r ^ 2 * W.a₂ + r ^ 3 - t * W.a₃ - t ^ 2 - r * t * W.a₁) }

end variable_change

end weierstrass_curve

[Eric Wieser]

It's not really recommended to port lean3 code by hand; we have mathport which does 90% of the work for you,

[Eric Wieser]

port-status#algebraic_geometry/elliptic_curve/weierstrass will tell you if it's been ported already

[Eric Wieser]

... it has not, because there are 40 files it needs that have also not been ported

[Ruben Van de Velde]

And all the dependencies whose port is in progress, are blocked, unfortunately, so it's been at 40 for a week or two

[Lars Ericson]

OK I'll learn how to run mathport, thanks. I did the Lean 3 tutorials but I guess there is not a rewrite of these for Lean 4, so I am trying to learn Lean 4 by example (I can look at Mathlib4 for examples) and by translating Lean 3 code that I have an interest in (particularly elliptic curves and anything having to do with the definition of modular forms). I don't think this is an unusual way to learn Lean, for example this note on modular forms starts with "So I've been slowly learning some lean by looking at the modular forms code".

[Eric Wieser]

You will have a very bad time trying to learn lean4 by porting a file that needs other lean4 code that doesn't exist

[Eric Wieser]

port-status#algebraic_geometry/elliptic_curve/weierstrass#graph shows there are a very large number of pre-requisites missing

[Lars Ericson]

@Eric Wieser so, for example, ring_theory.matrix_algebra is available to port. The machine-ported version is here. If I want I can copy that to my local Lean mathlib directory, open it, replace Mathbin. with Mathlib, and I've almost got a ported file. And then it gets complicated.

info: [498/1017] Building Mathlib.Order.Heyting.Basic
info: [509/1017] Building Mathlib.Algebra.Order.Sub.Canonical
info: [512/1017] Building Mathlib.Algebra.Order.Monoid.WithTop
error: > LEAN_PATH=./build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/std/build/lib LD_LIBRARY_PATH=/usr/local/cuda/lib64:./build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/std/build/lib:./build/lib /home/catskills/.elan/toolchains/leanprover--lean4---nightly-2023-05-16/bin/lean -DwarningAsError=true -Dpp.unicode.fun=true ./././Mathlib/Algebra/Group/Opposite.lean -R ././. -o ./build/lib/Mathlib/Algebra/Group/Opposite.olean -i ./build/lib/Mathlib/Algebra/Group/Opposite.ilean -c ./build/ir/Mathlib/Algebra/Group/Opposite.c
error: stderr:
failed to write './build/lib/Mathlib/Algebra/Group/Opposite.olean': 2 No such file or directory
error: external command `/home/catskills/.elan/toolchains/leanprover--lean4---nightly-2023-05-16/bin/lean` exited with code 1

[Johan Commelin]

On the other hand, you could also use scripts/start_port.sh to do that "copy to local mathlib, replace mathbin" dance...

[Eric Wieser]

It's not just that you _can_ run the script Johan mentions, but it's very strongly preferred that you do, else it creates more work for reviewers

[Lars Ericson]

@Johan Commelin thank you, I will try https://github.com/leanprover-community/mathlib4/blob/master/scripts/start_port.sh
I have some basic gaps in my understanding of how the process works:

• I don't know the architecture of VS Code, so I don't know how it connects with a Lean 3 or a Lean 4.
• If I download Mathlib 4 and then cd into it and do "code .", and I click on a line of code in that repo, then the Lean Infoview will come up. If I just name a file "foo.lean" and open it in VS code, it starts looking for Lean Server forever, and Lean Infoview doesn't work.
• Lean 4 uses prefix MathLib, but the partial ports in the mathlib3port repo use MathBin as a prefix. When I try to load one of those files, it wants to write an OLean file.
• I don't know what OLean is.
• I don't know if I need to distinguish Lean 4 files from Lean 3 by using a .lean4 extension.
• I don't know what "lake" and "elan" are.

I want to get into a situation where I have done a Git Update to the latest update of the 3 to 4 port, be able to see a porting leaf node file in VS Code with a Lean InfoView, and be able to try to get it to typecheck, and then submit a pull request for that. I just want to focus on the individual file editing part, for leaf node files that are 99% complete. For Ubuntu, is there a guide to fill in my knowledge gaps above?

[Yakov Pechersky]

• The lean extensions just "know" based on the directory structure.
• For lean4, you can't just have a naked .lean file and have VSCode "work" on it, it requires support from other configuration files in the directory context. lake (Lean-make) handles creation of new projects.
• The start_port.sh scrip handles getting the most recent "mathbin" in the background, it does not require you to maintain your own clone of "mathbin". The script will also handle all the proper string replacement of "Mathbin" to "Mathlib".
• .olean is the compiled content of a .lean, which relies on the presence of other compatible .oleans. Having .olean means that your VSCode (lean server) won't have to recompile everything every time. During a port, you can run lake exe cache get to retrieve .olean files from a cache that is automatically maintained for Mathlib.
• Like I said above, what differentiates a .lean file in lean3 from lean4 is the context of other files in the directory. (Similar to how .py is the same extension for python2 and python3).
• lake is Lean-make. elan is the lean version/release manager. It is invoked almost entirely automatically by lake, and you shouldn't have to interact with elan on the cli to be able to start a port, edit files in VSCode, make git commits, or push.

[Lars Ericson]

For https://leanprover-community.github.io/mathlib-port-status/file/algebra/direct_limit, what does please-adopt mean in the message

• This file is currently being ported at #4052. please-adopt mathlib-port

I can't tell if it is already being ported and leave it be, or if an automated translation has been touched up by a human who has issued a pull request and it is waiting for review, or what.

[Lars Ericson]

It is listed as an unfinished dependency for https://leanprover-community.github.io/mathlib-port-status/file/algebraic_geometry%2Felliptic_curve%2Fweierstrass#graph

This one: https://leanprover-community.github.io/mathlib-port-status/file/linear_algebra/matrix/special_linear_group

has tags

• This file is currently being ported at #3710. help-wanted WIP mathlib-port

It says help-wanted but it looks like somebody did some work but they are not authorized users and merging is blocked.

[Lars Ericson]

There are 6 files that algebra.elliptic_curve.weierstrass depends on and they all seem to be in a kind of blocked/ready for review status.

[Lars Ericson]

Also for something completely unported like https://leanprover-community.github.io/mathlib-port-status/file/ring_theory/power_series/basic, there is no Mathlib4 folder for power_series present, but scripts/start_port.sh is looking for an existing file. I assume that step 0 is that mathport is run on ring_theory/power_series/basic and the files and directories are renamed from mathlib3 style (underscores) to mathlib4 style (capitalization). How would I port a file when step 0 hasn't been done yet?

[Ruben Van de Velde]

Lars Ericson said:

Also for something completely unported like https://leanprover-community.github.io/mathlib-port-status/file/ring_theory/power_series/basic, there is no Mathlib4 folder for power_series present, but scripts/start_port.sh is looking for an existing file. I assume that step 0 is that mathport is run on ring_theory/power_series/basic and the files and directories are renamed from mathlib3 style (underscores) to mathlib4 style (capitalization). How would I port a file when step 0 hasn't been done yet?

The mathport output exists and start_port will download it if you run it with argument Mathlib/RingTheory/PowerSeries/Basic.lean

[Ruben Van de Velde]

https://github.com/leanprover-community/mathlib3port/blob/master/Mathbin/RingTheory/PowerSeries/Basic.lean

[Lars Ericson]

In this page I don't see PowerSeries/Basic.lean depending on LinArith/Default.lean, but that's what it is telling me:

error: no such file or directory (error code: 2)
  file: ./././Mathlib/Tactic/Linarith/Default.lean

If I search for "linarith" in mathlib porting status, I don't get anything.

Screenshot-from-2023-05-20-08-20-55.png

So I will restart with scripts/start_port.sh Mathlib/Tactic/Linarith/Default.lean. That seems to create a separate branch on my PC? I hope that these branches are just local and that I'm not creating branches in the main repository just by running start_port.sh. Also does that mean I have separate branches for the PowerSeries start_port versus the LinArith start_port?

[Lars Ericson]

Note that if I just delete my mathlib4 and start from scratch, it looks good but doesn't create a Default.lean file in the Linarith directory:

Screenshot-from-2023-05-20-08-27-34.png

[Eric Wieser]

Just remove the import, we are not porting things in the tactic directory

[Ruben Van de Velde]

Why does anything even import that file in mathlib 3?

[Eric Wieser]

Why wouldn't it?

[Eric Wieser]

To answer a previous question; yes, start_port.sh creates local branches, and it creates a new one every time you run it

[Lars Ericson]

@Eric Wieser suppose I git clone mathlib4, do a start_port.sh and then decide I want to work on a more upstream file. If I completely remove the directory and start over, then I am only removing a local branch, and it doesn't impact anything on GitHub, is that correct? I assume so, just double checking.

[Eric Wieser]

You don't need to (and shouldn't) delete the folder; git is very happy for you to have multiple local branches.

[Eric Wieser]

And no, local branches don't impact things on GitHub.

[Lars Ericson]

After deleting the LinArith import, it breaks around line 129 on

def monomial (n : σ →₀ ℕ) : R →ₗ[R] MvPowerSeries σ R :=
  LinearMap.stdBasis R _ n
#align mv_power_series.monomial MvPowerSeries.monomial

in particular on

LinearMap.stdBasis R _ n

which has type

  ?m.8198 n →ₗ[R] (i : σ →₀ ℕ) → ?m.8198 i : Type (max ?u.7443 ?u.7440 ?u.7443)

but Lean4 expects type

R →ₗ[R] MvPowerSeries σ R : Type (max ?u.7443 ?u.7443 ?u.7440)

where

variable (R) [Semiring R]

and MvPowerSeries is declared on line 86 as

def MvPowerSeries (σ : Type _) (R : Type _) :=
  (σ →₀ ℕ) → R

so it is unable to unify

• ?m.8198 n with Rand
• ?m.8198 i with R

I need a hint.

[Eric Wieser]

These sorts of problems are annoying to solve and not great for first time porters

[Eric Wieser]

The first thing I would try is filling in the underscore

[Eric Wieser]

I already expect this file to be a pain, for the same reason that the MonoidAlgebra files were; Lean4 is much less happy with us saying things like "Type A is type B, with the same addition but different multiplication"

[Lars Ericson]

@Eric Wieser that's a good hint but I wonder if it is something more subtle. The system is giving me this problem explanation:

Screenshot-from-2023-05-21-11-06-46.png

It is saying it has max ?u.7443 ?u.7440 ?u.7443) but it wants max ?u.7443 ?u.7443 ?u.7440 or more simply it sees pattern ABA and it wants pattern AAB. I'm not sure that filling in the underscore with a concrete type will resolve that.

[Lars Ericson]

Note that

σ: Type ?u.7440
R: Type ?u.7443

so it is saying it expects to have a max R R σ and it is getting a max R σ R, so that's a clue.

It's telling me that earlier in the conversion process some arguments got switched around in terms of what this definition depends on.

[Eric Wieser]

The problem is that it can't work out ?m.8198. Filling out the underscore should fix that.

[Eric Wieser]

Note that someone else is now working on this file at !4#4167

[Lars Ericson]

I just figured it out , replace _ with

(fun _ => R)

through the magic of programming by example

Screenshot-from-2023-05-21-11-41-43.png

That said I will look for another file to work on given !4#4167.

[Lars Ericson]

I don't understand how that turns a max R σ R into a max R R σ but it works.

[Lars Ericson]

@Eric Wieser when there is a please-adopt tag for example for DirectLimit, does that mean it is open for volunteers? For some like the above where there is a pending PR, clearly not. Not as clear for DirectLimit, which has recent activity by @Scott Morrison .

[Eric Wieser]

Lars Ericson said:

I don't understand how that turns a max R σ R into a max R R σ but it works.

Those things (or at least, the ?-versions) are equal by definition in the first place

[Lars Ericson]

For special linear group it has tags help-wanted and was recently worked on by Parcly-Taxel who added the tag help-wanted, does that mean they just want hints but are still working on it?

[Lars Ericson]

In summary for weierstrass curve, there are now 4 dependencies and all 4 are In Progress, so no work available there.

[Lars Ericson]

However the dependency graph shows 4 open items, but the list below of Unported Dependencies lists every node in the graph. Are these all open to work on, or does the dependency graph only highlight the nodes that are already being worked on?

[Ruben Van de Velde]

There is no point in starting to port a module before its dependencies have been ported

[Ruben Van de Velde]

Once some of those four in-progress ports have been merged, more work may become available

[Lars Ericson]

@Ruben Van de Velde how about linear_algebra.matrix.charpoly.coeff . This is shown as

linear_algebra.matrix.charpoly.coeff ⟷ ?

There is no corresponding mathport file. How does one proceed in this case?

[Lars Ericson]

That one is at the root of the dependency graph. However the 4 files I mentioned are much further down in the dependency graph and have PRs. So it seems that people are porting modules before their dependencies have been ported, is that correct?

Screenshot-from-2023-05-21-12-07-09.png

[Ruben Van de Velde]

Oh, my information was out of date. That one does seem ready for porting, but you're saying the file doesn't exist in the mathlib3port repository? Was it added to mathlib 3 very recently?

[Lars Ericson]

That is how I read the ? in this display:

Screenshot-from-2023-05-21-12-08-09.png

[Lars Ericson]

There is a coeff.lean in mathlib3. It doesn't appear in the mathport. There is only a Charpoly/Basic.lean. How to proceed in this case?

[Lars Ericson]

Do I do a start_port.sh LinearAlgebra/Matrix/Charpoly/Coeff.lean and then manually create the file from the mathlib3 source? This will be obviously harder than taking the automatic translation given by mathport if it existed.

[Ruben Van de Velde]

The ? in the port status means that the file doesn't exist in mathlib4 yet; it needs to be imported from mathlib3port

[Ruben Van de Velde]

This is what start_port.sh does

[Ruben Van de Velde]

You can see the autogenerated lean4 code that mathport generated here: https://github.com/leanprover-community/mathlib3port/blob/master/Mathbin/LinearAlgebra/Matrix/Charpoly/Coeff.lean

[Ruben Van de Velde]

Our job in porting is copying that output into the mathlib4 repository and fixing anything mathport got wrong

[Ruben Van de Velde]

So you can go ahead and run start_port.sh LinearAlgebra/Matrix/Charpoly/Coeff.lean, and that will create a branch in your local repository where that file exists, and you can then check if it compiles or needs any adjustments

[Ruben Van de Velde]

Does that help?

[Damiano Testa]

I just found this conversation and have opened just now a PR...

[Damiano Testa]

There is one proof that still need fixing, though...

[Damiano Testa]

!4#4169

[Ruben Van de Velde]

Okay, then I revert to my previous message: the four five dependencies of algebraic_geometry.elliptic_curve.weierstrass that are available for porting, are already in progress :)

[Damiano Testa]

For the record, I was following a path towards quadratic reciprocity, not Weierstrass models...

[Ruben Van de Velde]

This is at the top of the list of available modules by dependents, so that's not surprising

[Ruben Van de Velde]

@Damiano Testa I pushed enough to make it build, but need to run now. Can you look at my changes and see if you can tidy it up? Otherwise I'll take another look later tonigh

[Damiano Testa]

Ah, sure! Thanks!

[Damiano Testa]

@Ruben Van de Velde, thank you for the fixes!

I cleaned up the file: assuming that now the unused variable linter is satisfied, the file is ready for review!

[Scott Morrison]

Yes, help-wanted typically means that contributions are welcome, and please-adopt means that not only is help wanted, but the original author doesn't anticipate making further progress (whether do to availability or problems they don't understand).

[Lars Ericson]

It seems like ring_theory.integral_closure is free to work on. It is now the critical path for weierstrass_curve.

Screenshot-from-2023-05-21-18-40-32.png

[Lars Ericson]

Integral closures of ideals and rings

[Johan Commelin]

Why are you linking to that PDF?

[Johan Commelin]

Porting a file shouldn't involve scavenger hunts through the mathematical literature

[Lars Ericson]

@Johan Commelin I feel like I will be better at porting a file about integral closures if I know what an integral closure is. When I find texts that seem particularly helpful on the topic of integral closures, I like to share them, in case they might be helpful for other people.

[Lars Ericson]

That said, there is a problem with this file: It includes

import Mathlib.RingTheory.Adjoin.Fg

but this is not included in the dependency graph. Why isn't it included?

[Lars Ericson]

Actually Fg.lean is in the porting directory, but it is not in the dependency graph.

[Lars Ericson]

I will open a start_port for Fg.lean but, given that it is not in the dependency graph, I'm not sure whether it's non-inclusion is a problem with respect to porting.

[Lars Ericson]

Oh wait my bad, it is in mathlib4, but as FG.lean, not Fg.lean, and Lean 4 is case sensitive, where I guess Lean 3 was not, or is it an artifact of the porting script?

[Lars Ericson]

So it needs an added

import Mathlib.RingTheory.Polynomial.Basic

and within that file it requires degree_le which is now degreeLE and mem_degree_le now mem_degreeLE. It is also breaking on the occurence of by_contradiction. What is the Lean 4 of by_contradiction`?

[Lars Ericson]

Never mind that's now byContradiction.

[Lars Ericson]

There are quite a few name to be remapped for example aeval_map_algebra_map, nat_degree, mod_by_monic_add_div. I can find those.

[Lars Ericson]

This one I don't understand, the code is:

theorem fG_adjoin_of_finite {s : Set A} (hfs : s.Finite) (his : ∀ x ∈ s, IsIntegral R x) :
    (Algebra.adjoin R s).toSubmodule.FG :=

and the error message is

(kernel) declaration has metavariables 'fG_adjoin_of_finite'

How to handle declaration has metavariables ?

[Damiano Testa]

@Lars Ericson, I made an attempt at porting IntegralClosure and fixed some of the issues. If you want to either push your own attempts or try your hand at what I cannot do, feel free to do so!

!4#4196

[Ruben Van de Velde]

Lars Ericson said:

Oh wait my bad, it is in mathlib4, but as FG.lean, not Fg.lean, and Lean 4 is case sensitive, where I guess Lean 3 was not, or is it an artifact of the porting script?

Everything in mathlib 3 is lower case, so mathport has to guess a capitalization, which we don't always agree with.

[Mario Carneiro]

mathport isn't great at telling the difference between words and acronyms

[Lars Ericson]

All of the root nodes of weierstrass are In Progress now.

Screenshot-from-2023-05-22-22-24-12.png

[Lars Ericson]

@Damiano Testa I will look for the sorrys in IntegralClosure.lean. I am trying to load it now from scratch, it takes about 30+ minutes to build on my PC.

[Lars Ericson]

Actually I can't even get to the error messages because it is stuck on the 1010'th construct out of 1129:

Screenshot-from-2023-05-23-00-53-28.png

Is it possible that this is one of those billion year waits? I.e. a concrete example of intractibility creeping into the definition stack of Lean 4?

[Lars Ericson]

On the other hand it's not using any CPU so I don't know what to make of it. I will try restarting and see if that helps.

[Lars Ericson]

And now it's fine. Confusing.

[Lars Ericson]

I also don't see any sorry's so I'll assume this file was completed converted.

[Eric Wieser]

You shouldn't have to build everything, lake exe cache get will load a build of n-1 of the files you need

[Eric Wieser]

Make sure that lean is not running when you run it

[Ruben Van de Velde]

And yes, integral closure has been finished already

[Damiano Testa]

The port moves fast, especially with files that are straightforward!

Once !4#4238 gets merged, I'll give a go to ring_theory.adjoin_root.

[Lars Ericson]

@Damiano Testa that one and field_theory.separable are root nodes now.

Screenshot-from-2023-05-23-07-41-14.png

[Lars Ericson]

@Eric Wieser thank you, so the drill to start work on porting a file looks like

git clone https://github.com/leanprover-community/mathlib4.git
cd mathlib4
lake exe cache get
scripts/start_port.sh Mathlib/FieldTheory/Separable.lean
code .

[Lars Ericson]

Note I am still getting a build sequence for Separable.lean but it is running much faster with the lake exe cache:

info: [819/1138] Building Mathlib.Algebra.Module.Hom

[Eric Wieser]

You're missing the get on lake exe cache get

[Lars Ericson]

I am looking at Algebra.BigOperators.NormNum line 52

unsafe def decide_eq (l r : expr) : tactic (Bool × expr) := do

the original mathlib 3 text is

meta def decide_eq (l r : expr) : tactic (bool × expr) := do

The Lean 4 error message is

function expected at
  tactic
term has type
  ?m.11

on subexpression

tactic (Bool × expr)

where #check tactic gives unknown identifier 'tactic'.

Any hint greatly appreciated. I guess Lean 4 tactics are completely different than Lean 3 especially the metaprogramming thereof and this looks like a metaprogramming section.

[Anne Baanen]

This is indeed because the file defines a tactic and tactics are very different in Lean 4. I've started a port in the norm_num-bigop branch.

[Eric Wieser]

Porting tactic files is an exercise in understanding how the tactic worked in lean 3 and then rewriting it largely from scratch, right?

[Anne Baanen]

Also I came up with a few improvements to the tactic so I'm planning to basically redo it entirely.

[Lars Ericson]

I am looking at algebra.category.Algebra.basic. It lists no dependencies, but line 14 of the ported file

import Mathbin.Algebra.Category.Module.Basic

refers to a dependency Module/Basic.lean. This does not seem to be ported, but it is not listed as a dependency.

Why is the dependency graph blank/dependency not shown here?

[Lars Ericson]

Regarding Algebra.Category.Module.Basic, it is marked as already in process:

WARNING: The file is already in the process of being ported in mathlib4#3260.

However as I mentioned it is not shown as a dependency (nothing is in the dependency graph of) Algebra.Category.Algebra.basic. Maybe the problem is the lowercase "b" in basic?

I'm looking at the first page of Unported files and it looks like some are actually in process, have dependencies that are not listed, or are otherwise not in the status of being leaf nodes that are not being worked on in some way. That is, the files in the list are ones that are actually snarled up in some way that is not being shown in the dependency graph display.

Screenshot-from-2023-05-23-22-19-25.png

[Lars Ericson]

OK I found one which is unported but all of the imports are ported, MeasureTheory.Function.AeEqFun.lean. It is listed by the dependency checker as depending on unported analysis.normed.mul_action. However, this module is not imported into AeEqFun, so I don't know why it's listed.

[Lars Ericson]

First fix for this one is replace Emetric with EMetric.