help wanted: strategic binport experimentation

Stream: mathlib4

[Daniel Selsam]

I think the binport oleans have become usable enough that power users could help a lot by starting to (strategically) experiment with them. The goal right now is to discover, isolate, and categorize issues efficiently. Here are some concrete questions:

• What simp calls break in Lean4 due to the discrimination tree indexing? Are there a few simple rules we could add to Binport to insert no_index annotations that would address the problems?
• Same question for typeclass synthesis.
• Are there simp or typeclass synthesis calls that are failing unexpectedly for reasons besides indexing?
• Post-facto reducible toggling is ignored, and all irreducible annotations are currently ignored as well. Are either of these causing serious issues behind the scenes?
• For things that do already work in Lean4, are there any significant performance regressions compared to Lean3?
• Are there any other issues that are not even on our radar yet?

Notable differences between Binport and Mathlib3:

• Binport automatically translates names to Lean4 style, adding 's as necessary on non-def-eq clashes. The command #lookup3 <ident> prints the new Lean4 name. It is usually (but not always) what you would expect.
• Binport expands all coercions, just as Lean4 does but even more aggressively. It also replaces old coercion instances (e.g. has_coe_to_fun) with new ones (e.g. CoeFun).
• All numerals (i.e. zero/one/bit0/bit1 terms) are wrapped with OfNat but otherwise unchanged.
• As mentioned above, post-facto reducible toggling is ignored, and all irreducible annotations are currently ignored as well.
• As of now, nat.le is not aligned to Lean4's Nat.le, which causes subtle headaches when working with natural numbers.
• foldl notations are not yet auto-ported
• Many small changes in unification and other core algorithms may cause various things to fail or slow down for subtle reasons.

Logistics:

• I regularly upload a tar.gz file to https://github.com/dselsam/mathport/releases/tag/v0.0.0.0 that, when extracted, produces the folder Lib4.
• import Mathlib or import Mathlib.Data.Real.Pi will work if you set LEAN_PATH=<path-to-lean4-lib>:<path-to-Lib4>.
• In general, the binport .oleans should work with either master or nightly. Most commits to lean4 do not break compatibility.
• Obviously, it would be great to have CI for this and a leanpkg-friendly way of using them.

Tips:

• For every Binported olean file Foo.olean, @Mario Carneiro's Synport produces FooSyn.lean with the best-effort syntactic port, which is name-translation-aware and already (syntactically) translates most declarations well. If you are experimenting with theorem foo in file Foo.olean, you may find it a useful starting point to copy-paste the decl from FooSyn.lean into a new file that imports Foo.
• Another approach is to just call #check on the imported theorem and copy-paste the result, factoring out arguments into variables as desired. Note: the Lean4 default pretty-printer is pretty good at concise roundtripping.

[Floris van Doorn]

Stupid question: How do I set LEAN_PATH (1) in VSCode and (2) from the command line? I tried

 LEAN_PATH=/c/Users/Floris/.elan/toolchains/nightly/bin/lean.exe:/d/projects/portMathlib/Lib4 lean Personal/test.lean

and some variations, but it didn't seem to work (WIndows + MINGW64). Also, do I have to add my own leanpkg.toml file?

[Daniel Selsam]

@Floris van Doorn I apologize for not having a cleaner setup yet. LEAN_PATH needs to point to the Lean libraries, not the executable. For me, this is <lean4-repo>/build/release/stage1/lib/lean, so I just open a terminal and write:

LEAN_PATH=/home/dselsam/projects/lean4/build/release/stage1/lib/lean:/home/dselsam/projects/mathport/Lib4 code &

[Daniel Selsam]

If you use elan or some other way of getting the lean4 library, you might need to find the stage1 directory. This might help: find ~ -name "lean.mk".

[Sebastian Ullrich]

lib/lean should already be in the LEAN_PATH implicitly (when running lean)

[Mario Carneiro]

please teach me how to not have to specify lib/lean, this is a huge pain

[Mario Carneiro]

is there a function to call to get the input to give to initSearchPath?

[Daniel Selsam]

@Sebastian Ullrich For people who are willing to download oleans, is there an easy way to add a leanpkg.toml to the binport oleans such that for a new project, leanpkg.toml can depend on binport with a relative path?

[Sebastian Ullrich]

I don't think so, leanpkg assumes it can build everything itself

[Sebastian Ullrich]

@Mario Carneiro You are talking about calling this from a different executable from lean, right? Then we can't know where the libraries could be located in relation to that executable. But if you assume that lean is in the PATH, you could call lean --print-libdir

[Leonardo de Moura]

@Mario Carneiro Here is a hack I used in a test.

def declareLeanPath : MetaM Unit := do
  addAndCompile <| Declaration.defnDecl {
    name  := `leanPath
    type  := mkConst ``String
    value := toExpr <| System.SearchPath.separator.toString.intercalate ((← Lean.getBuiltinSearchPath).map toString)
    levelParams := []
    hints := ReducibilityHints.abbrev
    safety := DefinitionSafety.safe
  }

#eval declareLeanPath

unsafe def main : IO Unit := do
  initSearchPath s!"{leanPath}{System.SearchPath.separator}build"
  withImportModules [{ module := `UserAttr.Tst : Import }] {} 0 fun env => ()

[Leonardo de Moura]

We can make it less ugly in the future.

[Mario Carneiro]

ah, clever

[Mario Carneiro]

I guess you could also make leanPath a macro there to get a similar effect

[Sebastian Ullrich]

#eval IO.Process.run { cmd := "lean", args := #["--print-libdir"] }

This one will work even after moving the executable to other machines :)

[Sebastian Ullrich]

@Daniel Selsam However, leanpkg will happily call any Makefile, if it exists, instead of building .oleans on its own. That could be used for downloading the .oleans. But a more robust solution should probably use Lake.

[Floris van Doorn]

Ok, I managed to get Binport working from the command line using the following steps (part of my problem was that I tried to use nightly, which refers to Lean 3 nightly). Sebastian was right that I didn't have to specify the Lean libraries in LEAN_PATH.

• Download and extract the mathport-<hash>.tar.gz file here: https://github.com/dselsam/mathport/releases/tag/v0.0.0.0
• Run (path/to/Lib4 is the path to the folder you just extacted)

cd path/to/Lib4
elan install leanprover/lean4:nightly # (if this fails, close VSCode and try again)
elan override set leanprover/lean4:nightly

• Make a test file, for example Personal/test.lean with the contents

import Mathlib.Data.Real.Basic

open Real

#check Real

• Run

LEAN_PATH=path/to/Lib4 lean Personal/test.lean

[Floris van Doorn]

Is there also a way to configure LEAN_PATH for the Lean server in VSCode?

[Daniel Selsam]

Great, I am glad you got it to work.

[Floris van Doorn]

My question might be easy to miss in the previous message.

Is there also a way to configure LEAN_PATH for the Lean server in VSCode?

[Daniel Selsam]

Sorry, I think I misunderstood your question. Does this not work for you?

LEAN_PATH=path/to/Lib4 code Personal/test.lean &

[Floris van Doorn]

Ah, I didn't understand that was the way to open VSCode.
If I run

 LEAN_PATH=~/.elan/toolchains/leanprover--lean4---nightly/lib/lean:/d/projects/portMathlib/Lib4 code Personal/test.lean &

I get a bunch of errors, like this

test.lean:1:0
file 'C:\Users\Floris\.elan\toolchains\leanprover--lean4---nightly\lib\lean\init.lean' not found in the LEAN_PATH
test.lean:1:0
file 'D:\projects\portMathlib\Lib4\Mathlib\Data\Real\Basic.lean' not found in the LEAN_PATH
test.lean:1:0
file 'C:\Users\Floris\.elan\toolchains\leanprover--lean4---nightly\lib\lean\Lean\Data\Name.lean' not found in the LEAN_PATH
test.lean:2:0
invalid import: init
could not resolve import: init
test.lean:2:0
invalid import: Mathlib.Data.Real.Basic
could not resolve import: Mathlib.Data.Real.Basic
test.lean:2:0
invalid import: Lean.Data.Name
could not resolve import: Lean.Data.Name

[Floris van Doorn]

Is this the correct lib/lean (it's not in a folder stage1, but it is the output of lean --print-libdir

[Daniel Selsam]

I think you are calling lean3 :) init.lean is capitalized in Lean4. Maybe you are using the lean3 VSCode extension?

[Floris van Doorn]

Oh, that might be true. Until now I believe my VSCode used the leanpkg.toml to figure out whether to use lean 3 or lean 4. (or maybe I disabled/enabled some extensions in different folders, not actually sure)

[Daniel Selsam]

Another worrying sign: it is looking for .lean files (which don't exist) as opposed to .olean files (which do).

[Daniel Selsam]

My VSCode is happy with .oleans only, so this issue will probably go away once you are using the Lean4 extension.

[Floris van Doorn]

I'm now disabling the lean extension, and I have the lean4 extension installed.

If I do LEAN_PATH=... code Personal/test.lean & [edited] the extension does not seem to activate at all (no highlighting, no yellow bars)
If I do LEAN_PATH=... code . & I get the error

`leanpkg print-paths` failed:

stderr:
configuring Mathlib 0.1
d:\projects\portMathlib\Lib4 must contain a unique '.lean' file as the package root

[Daniel Selsam]

Did you mean code Personal/test.lean?

[Floris van Doorn]

If I move away Liquid.lean I get

`leanpkg print-paths` failed:

stderr:
configuring Mathlib 0.1
no such file or directory (error code: 2)
  file: .\Mathlib\Data\Real\Basic.lean

[Floris van Doorn]

ah yes

[Floris van Doorn]

that's what I did (and isn't working)

[Daniel Selsam]

I assume it uses the file suffix to guess the extension.

[Floris van Doorn]

No, I typed test.lean, just copied it wrong.

[Floris van Doorn]

Yes, VSCode tends to use the file extension to decide which extension to activate.

[Daniel Selsam]

What if you click on the language mode icon on the bottom right, and navigate to Lean4?

[Floris van Doorn]

Ok, then I get syntax highlighting, but no compilation. Trying to refresh file dependencies gives
image.png

[Floris van Doorn]

It seems that the extension is happier (but still not happy) if I open the project folder...

[Daniel Selsam]

Floris van Doorn said:

Ok, then I get syntax highlighting, but no compilation.

This is what happens to me when LEAN_PATH is set wrong. Can you try creating a new folder with just Test.lean, moving to that folder, and then (with LEAN_PATH set) opening code Test.lean &?

[Daniel Selsam]

Or maybe you are in restricted mode and need to click "Trust workspace"?

[Floris van Doorn]

That doesn't seem to work, still the same behavior... I think I'm also not in restricted mode
image.png

[Floris van Doorn]

This is what I did

Floris@MSI MINGW64 /d/projects/portMathlib/Lib4
$ cd Personal/

Floris@MSI MINGW64 /d/projects/portMathlib/Lib4/Personal
$ LEAN_PATH=~/.elan/toolchains/leanprover--lean4---nightly/lib/lean:/d/projects/portMathlib/Lib4 code Test.lean &
[1] 1184

Floris@MSI MINGW64 /d/projects/portMathlib/Lib4/Personal
$ lean --print-libdir
c:\Users\Floris\.elan\toolchains\leanprover--lean4---nightly\lib\lean

[Daniel Selsam]

I am sorry, this is a mess. I have very little experience with VSCode. It works fine on my end but I don't know how many ambient factors might be in play. If you still have energy, I might be able to help you better on Zoom with screen-sharing.

[Floris van Doorn]

Thanks Daniel, for helping me through this. The solution was to maken leanprover/lean4:nightly the default version for elan.

[Floris van Doorn]

I updated my earlier post (https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/help.20wanted.3A.20strategic.20binport.20experimentation/near/250061877) with hopefully robust instructions for how to get this working, even if you haven't used/installed Lean 4 before.

[Eric Rodriguez]

A thing I do to make this sort of lean3/lean4 switching easier is just use Code Insiders for Lean4, and VSCode retail for lean3. Then neither of them can get confused :)

[Patrick Massot]

VSCodium

[Kevin Buzzard]

Am I right in thinking that this could become some sort of training ground for Lean 4? the game is to take an arbitrary file in some training branch of mathlib3, leave the imports as they are and then try and translate the rest manually into lean 4? It could be interesting for people who want to try learning Lean 4 by formalising mathematics which they find interesting -- they will not be limited by mathlib4's sketchy support for most things.

[Daniel Selsam]

Unfortunately the liquid (ea56bbc38c8b50c3569a7bf9560b4d0fc73eb978) and mathlib (5dc8bc169bd8773735520e6b9680ce3b65b80bd7) packages can no longer be imported together due to name clashes in normed_group_hom_completion.lean.

[Daniel Selsam]

Kevin Buzzard said:

Am I right in thinking that this could become some sort of training ground for Lean 4? the game is to take an arbitrary file in some training branch of mathlib3, leave the imports as they are and then try and translate the rest manually into lean 4? It could be interesting for people who want to try learning Lean 4 by formalising mathematics which they find interesting -- they will not be limited by mathlib4's sketchy support for most things.

Please note that I tried to phrase my request carefully ("power users ... strategically experiment with ... categorize issues efficiently"). The binport oleans are not ready for regular use. Right now, I think it only makes sense for experts who are invested in the port to experiment with them. I'll defer to them when it passes the threshold where casual users will have fun with them. Also, the better game might be starting from the synported files with an added #exit on top , and gradually pushing down the #exit as more declarations/proofs are "revived".

[Patrick Massot]

Daniel Selsam said:

Unfortunately the liquid (ea56bbc38c8b50c3569a7bf9560b4d0fc73eb978) and mathlib (5dc8bc169bd8773735520e6b9680ce3b65b80bd7) packages can no longer be imported together due to name clashes in normed_group_hom_completion.lean.

Lean 3 seems to use them together just fine according to CI. What's happening in Lean 4?

[Scott Morrison]

Floris van Doorn said:

I updated my earlier post (https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/help.20wanted.3A.20strategic.20binport.20experimentation/near/250061877) with hopefully robust instructions for how to get this working, even if you haven't used/installed Lean 4 before.

Thanks very much for this, @Floris van Doorn, your instructions worked flawlessly.

[Scott Morrison]

I'm still missing something fundamental here.

If I go and implement a missing tactic, and push that to the mathlib4 repository, how will that ever be seen by mathport? None of the files in the mathport bundle import anything from mathlib4, so I'm not seeing how a synported file can take advantage of new implementations of tactics.

[Scott Morrison]

In a different direction, I've also quickly got stuck playing with mathport. Following Floris' instructions, I opened Mathlib/SetTheory/PgameSyn.lean.

The first error is invalid field 'nth_le', the environment does not contain 'List.nth_le' which is easily fixable by changing nth_le to nthLe. That then produces:

application type mismatch
  List.nthLe L i.val (_ : i.1 < List.length L)
argument
  Fin'.is_lt _
has type
  i.1 < List.length L : Prop
but is expected to have type
  i.val < List.length' L : Prop

which I'm mystified by. I can't find any trace of List.length' in Lean3, Lean4, mathlib3, or mathlib4.

Is binport renaming Lean3's list.length to List.length' because it doesn't look the same as Lean4's List.length?

[Daniel Selsam]

Scott Morrison said:

Is binport renaming Lean3's list.length to List.length' because it doesn't look the same as Lean4's List.length?

I tried to warn about this in my original post:

Binport automatically translates names to Lean4 style, adding 's as necessary on non-def-eq clashes. The command #lookup3 <ident> prints the new Lean4 name. It is usually (but not always) what you would expect.

[Daniel Selsam]

Scott Morrison said:

Is binport renaming Lean3's list.length to List.length' because it doesn't look the same as Lean4's List.length?

Yes, exactly. Binport first generates the candidate name List.length using the capitalization conventions, and then checks the environment to see if a declaration already exists with that name.

• If no such declaration exists, the candidate name is used
• If a declaration exists and is definitionally-equal to the lean3 one (or the natural extension of definitional equality for inductive types), it throws out the lean3 declaration and translates all future uses of it to the lean4 one. We refer to this as aligning the lean3 declaration to the lean4 one.
• If a declaration with the name already exists and it is not def-eq-compatible with the lean3 one, binport adds a ' to the name and iteratively checks the environment again, etc.

[Daniel Selsam]

Scott Morrison said:

I'm still missing something fundamental here.

If I go and implement a missing tactic, and push that to the mathlib4 repository, how will that ever be seen by mathport? None of the files in the mathport bundle import anything from mathlib4, so I'm not seeing how a synported file can take advantage of new implementations of tactics.

@Mario Carneiro and I are in the process of refactoring so that Mathport and the binport oleans it produces both depend on Mathlib4. Currently, they are disconnected, but soon the syntax synport generates will refer to the actual Mathlib4 tactics.

[Daniel Selsam]

Scott Morrison said:

I opened Mathlib/SetTheory/PgameSyn.lean.

There are many unfortunate capitalizations like this. I will add some support for an extensible word-split list (e.g. pgame -> ["p", "game"])

[Scott Morrison]

Just for my understanding regarding the List.length issue, how are we going to deal with this? Mario earlier suggested that we could replace Lean4's List.length with the naive one, and add an @[implementedBy] attribute pointing to the tail recursive version.

[Daniel Selsam]

Not my department but here is a guess: it stays List.length' for now, and eventually once the compiler supports custom simp rules, List.length could become the slow version and we would write @[csimp] theorem List.length_eq_lengthTR ... to instruct the compiler to replace List.length with the tail recursive List.lengthTR.

[Leonardo de Moura]

I am going to add basic csimp support. The basic version will only support "constant replacement" theorems of the form @f = @g. This is good enough for solving issues like List.length'. Unfortunately, full support for simp rules has been postponed, and we don't know when we will have cycles to work on it.

[Leonardo de Moura]

Do you have a list of all problematic definitions?

[Daniel Selsam]

I can instrument binport to produce a list of all clashes. I thought I was already emitting these in the logs but I don't seem to be in an easily-greppable way.

[Leonardo de Moura]

I added the [csimp] attribute. I have redefined List.length and List.append as we did in Lean 3. We can now align them.