## Stream: new members

### Topic: Porting weierstrass_curve as an exercise in learning Lean 4

#### Lars Ericson (May 14 2023 at 15:09):

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 (May 14 2023 at 17:16):

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

#### Eric Wieser (May 14 2023 at 17:17):

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

#### Eric Wieser (May 14 2023 at 17:17):

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

#### Ruben Van de Velde (May 14 2023 at 17:56):

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 (May 15 2023 at 11:51):

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 (May 15 2023 at 12:17):

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 (May 15 2023 at 12:18):

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

#### Lars Ericson (May 18 2023 at 01:57):

@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 (May 18 2023 at 05:48):

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

#### Eric Wieser (May 18 2023 at 06:23):

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 (May 19 2023 at 00:26):

@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 (May 19 2023 at 01:04):

• 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 (May 19 2023 at 23:59):

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 (May 20 2023 at 00:03):

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

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 (May 20 2023 at 00:05):

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 (May 20 2023 at 00:11):

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 (May 20 2023 at 06:03):

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 (May 20 2023 at 06:05):

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

#### Lars Ericson (May 20 2023 at 12:23):

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 (May 20 2023 at 12:27):

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 (May 20 2023 at 18:53):

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

#### Ruben Van de Velde (May 20 2023 at 18:55):

Why does anything even import that file in mathlib 3?

Why wouldn't it?

#### Eric Wieser (May 20 2023 at 19:48):

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 (May 20 2023 at 22:21):

@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 (May 20 2023 at 22:43):

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

#### Eric Wieser (May 20 2023 at 22:43):

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

#### Lars Ericson (May 20 2023 at 23:14):

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 (May 20 2023 at 23:23):

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

#### Eric Wieser (May 20 2023 at 23:25):

The first thing I would try is filling in the underscore

#### Eric Wieser (May 20 2023 at 23:27):

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 (May 21 2023 at 15:09):

@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 (May 21 2023 at 15:19):

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 (May 21 2023 at 15:27):

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

#### Eric Wieser (May 21 2023 at 15:28):

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

#### Lars Ericson (May 21 2023 at 15:42):

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 (May 21 2023 at 15:45):

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

#### Lars Ericson (May 21 2023 at 15:51):

@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 (May 21 2023 at 15:52):

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 (May 21 2023 at 15:55):

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 (May 21 2023 at 15:57):

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

#### Lars Ericson (May 21 2023 at 16:00):

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 (May 21 2023 at 16:02):

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

#### Ruben Van de Velde (May 21 2023 at 16:04):

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

#### Lars Ericson (May 21 2023 at 16:05):

@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 (May 21 2023 at 16:07):

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 (May 21 2023 at 16:07):

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 (May 21 2023 at 16:08):

That is how I read the ? in this display:

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

#### Lars Ericson (May 21 2023 at 16:12):

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 (May 21 2023 at 16:13):

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 (May 21 2023 at 16:17):

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 (May 21 2023 at 16:17):

This is what start_port.sh does

#### Ruben Van de Velde (May 21 2023 at 16:18):

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 (May 21 2023 at 16:19):

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

#### Ruben Van de Velde (May 21 2023 at 16:20):

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

Does that help?

#### Damiano Testa (May 21 2023 at 16:21):

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

#### Damiano Testa (May 21 2023 at 16:22):

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

!4#4169

#### Ruben Van de Velde (May 21 2023 at 16:24):

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 (May 21 2023 at 16:26):

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

#### Ruben Van de Velde (May 21 2023 at 16:30):

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

#### Ruben Van de Velde (May 21 2023 at 16:38):

@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 (May 21 2023 at 16:40):

Ah, sure! Thanks!

#### Damiano Testa (May 21 2023 at 16:54):

@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 (May 21 2023 at 21:31):

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 (May 21 2023 at 22:41):

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 (May 21 2023 at 22:47):

Integral closures of ideals and rings

#### Johan Commelin (May 21 2023 at 22:57):

Why are you linking to that PDF?

#### Johan Commelin (May 21 2023 at 22:58):

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

#### Lars Ericson (May 21 2023 at 23:11):

@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 (May 21 2023 at 23:13):

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 (May 21 2023 at 23:14):

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

#### Lars Ericson (May 21 2023 at 23:15):

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 (May 21 2023 at 23:17):

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 (May 21 2023 at 23:48):

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 (May 21 2023 at 23:51):

Never mind that's now byContradiction.

#### Lars Ericson (May 22 2023 at 00:02):

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 (May 22 2023 at 00:04):

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) :


and the error message is

(kernel) declaration has metavariables 'fG_adjoin_of_finite'


How to handle declaration has metavariables ?

#### Damiano Testa (May 22 2023 at 05:02):

@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 (May 22 2023 at 05:16):

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 (May 22 2023 at 05:17):

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

#### Lars Ericson (May 23 2023 at 02:24):

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

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

#### Lars Ericson (May 23 2023 at 02:27):

@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 (May 23 2023 at 04:55):

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 (May 23 2023 at 04:56):

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 (May 23 2023 at 04:57):

And now it's fine. Confusing.

#### Lars Ericson (May 23 2023 at 04:58):

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

#### Eric Wieser (May 23 2023 at 05:01):

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 (May 23 2023 at 05:01):

Make sure that lean is not running when you run it

#### Ruben Van de Velde (May 23 2023 at 05:05):

And yes, integral closure has been finished already

#### Damiano Testa (May 23 2023 at 08:01):

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 (May 23 2023 at 11:41):

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

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

#### Lars Ericson (May 23 2023 at 11:53):

@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 (May 23 2023 at 12:07):

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 (May 23 2023 at 12:34):

You're missing the get on lake exe cache get

#### Lars Ericson (May 23 2023 at 21:29):

I am looking at Algebra.BigOperators.NormNum line 52

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

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 (May 23 2023 at 21:33):

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 (May 23 2023 at 21:34):

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 (May 23 2023 at 21:34):

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

#### Lars Ericson (May 24 2023 at 00:39):

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 (May 24 2023 at 02:20):

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 (May 24 2023 at 02:34):

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 (May 24 2023 at 02:42):

First fix for this one is replace Emetric with EMetric.

Last updated: Dec 20 2023 at 11:08 UTC