why does leanbin have mathport as a dependency?

Stream: lean4

[Scott Morrison]

@Daniel Selsam, I am confused about why in the mathport repository, in Lib4/leanbin/lakefile.lean, we have mathport itself as a dependency. Could you explain this to me?

[Mario Carneiro]

That's probably a workaround until we get Mathport.Prelude upstreamed to mathlib4

[Mac]

I second this, it confused me as well

[Mario Carneiro]

PS: I haven't compiled mathport in a while, I was waiting for the lake stuff to settle down

[Mario Carneiro]

We need Mathport.Prelude to be available to compile both mathport and the files produced by mathport

[Scott Morrison]

I don't understand though how Mathport.Prelude even gets pulled in while compiling .lean files in leanbin or mathbin. I can't find it being imported anywhere.

[Daniel Selsam]

Scott Morrison said:

Daniel Selsam, I am confused about why in the mathport repository, in Lib4/leanbin/lakefile.lean, we have mathport itself as a dependency. Could you explain this to me?

@Mario Carneiro is right, it is a temporary workaround since Mathport.Prelude is a dependency, and it has not been upstreamed to Mathlib4 yet.

[Mario Carneiro]

The leanbin generated files depend on Mathport.Prelude, i.e. they reference it in the "import lines"

[Scott Morrison]

Ah, you mean the oleans there generated in leanbin.

[Daniel Selsam]

Scott Morrison said:

I don't understand though how Mathport.Prelude even gets pulled in while compiling .lean files in leanbin or mathbin. I can't find it being imported anywhere.

When generating the environment for binport/synport-ing a file with no imports, we start by importing Mathport and Mathlib4: https://github.com/leanprover/mathport/blob/master/Mathport.lean#L27 Once/if Mathport.Prelude is moved to Mathlib4, then we would only need to import Mathlib4 here.

[Scott Morrison]

(Silly me was looking for import Mathport.* in the files generated by synport.)

[Mario Carneiro]

by leanbin you mean the olean files generated from the lean 3 core library, right?

[Mario Carneiro]

The olean files generated by mathport differ subtly from the lean files, since the oleans are made by binport and the leans by synport

[Scott Morrison]

Yes, I think I get it now.

[Mario Carneiro]

in particular, the binport oleans always import Mathport.Prelude but synport files don't

[Mario Carneiro]

which explains your confusion in the other thread

[Mario Carneiro]

synport files do actually need Mathport.Prelude or something roughly equivalent to it to be transitively imported, but we're relying on the user to work that out

[Mario Carneiro]

we would rather have whatever that is be a piece of mathlib4, because mathlib4 isn't supposed to depend directly on mathport

[Scott Morrison]

So --- would it be a useful thing for me to do to start moving Mathport/Prelude/ into mathlib4?

[Mario Carneiro]

@Daniel Selsam What is the status of building mathport depending on mathlib4?

[Mario Carneiro]

I think that is a prerequisite for this move

[Mario Carneiro]

although I suppose you can do a copy now

[Scott Morrison]

mathport currently builds off a recent-but-not-quite-master commit from mathlib4
Ah, I'm still confused. :-)

[Mac]

@Mario Carneiro looking at what is in Mathport.Prelude it seems like the #align command is most used to build the initial state of the renameExt -- shouldn't that just be an internal part of the Environment mathport builds?

[Mario Carneiro]

The #align command is intended to proliferate in mathlib4 for the duration of the port

[Mac]

oh, that surprises me

[Mario Carneiro]

it is there to improve the quality of binport/synport translations when porting files high up in the dependency tree

[Mario Carneiro]

once mathlib is completely ported we won't need #align anymore, but that will be a while

[Mario Carneiro]

actually even after the port is done we might want to keep #align around until we completely drop support for lean 3 migration

[Scott Morrison]

Actually, I think I was right above, that mathport is being built with a dependency on mathlib4. The lakefile.lean just says:

import Lake

open Lake DSL System

package mathport {
  dependencies := #[{
    name := "mathlib",
    -- We point to a particular commit in mathlib4,
    -- as changes to tactics in mathlib4 often cause breakages here,
    -- particularly in `Mathport/Syntax/Translate/Tactic/Mathlib.lean`.
    -- We'll need to keep updating that file, and bumping the commit here.
    src := Source.git "https://github.com/leanprover-community/mathlib4.git" "b28a3d51e722d8b43367035e0eb5790b4cb6da53",
    dir := FilePath.mk "."
  }],
  binRoot := `MathportApp
  moreLinkArgs :=
    if Platform.isWindows then
      #["-Wl,--export-all"]
    else
      #["-rdynamic"]
}

[Scott Morrison]

so we're not quite depending on mathlib4 master, but it's a commit or two behind.

[Mario Carneiro]

since third party projects can also benefit from it

[Mac]

yeah, from what I see mathport is based off mathlib4 so you should just be able to merge Mathport.Prelude into mathlib4 proper, right?

[Mario Carneiro]

@Scott Morrison Does that lakefile actually work though? I'm still eagerly awaiting your "how to build mathport" description

[Mac]

yes it does

[Scott Morrison]

Yes! That lakefile actually works, and has been merged into the master branch of mathport.

[Scott Morrison]

You can build mathport, and run it, from the Makefile.

[Scott Morrison]

It even works inside a Docker container (I wanted to be sure there were no stray dependencies on anything outside the mathport folder!)

[Scott Morrison]

The "how to build mathport" description is in the comments at the top of the Makefile, and is hopefully pretty thorough. The README just refers you to the Makefile for now.

[Mario Carneiro]

In that case, I guess a move should work, provided you change import Mathport.Prelude in the sources to import Mathlib.Init and ensure that Mathlib.Init contains everything we need

[Mac]

What I would argue should be done though (at least eventually) is that leanbin, etc. should depend on mathport and its build step should be either poritng Lean 3 or downloading the prebuilt artifacts (if they are available)

[Mario Carneiro]

Actually maybe Mathlib.Init is too low level - Mathport.Prelude (purports to) include all lean 3 and mathlib tactics

[Mario Carneiro]

Maybe Mathlib.MathportPrelude is better for the near term

[Scott Morrison]

Returning to the original topic of this thread, I am now very confused!

I just rebuilt mathport, having, as an experiment, deleted the dependency on mathport in Leanbin/lakefile.lean.

.... contrary to the explanations above it seems everything works just as well....?

[Mario Carneiro]

Local dependencies will be resolved the normal way by lake

[Mario Carneiro]

Did you try using the built program though? mathport needs those files at runtime too

[Scott Morrison]

I mean, I did a full run of mathport on lean3 and mathlib3, and can open the synported files, etc., and see exactly the same error messages as before.

[Scott Morrison]

(I've spun off a docker build with that dependency removed, to check in a clean environment. I think the point may just be that we're setting LEAN_PATH when we actually run mathport, and so it is finding those files even without Leanbin/lakefile.lean recording a dependency on mathport.)

[Scott Morrison]

I finished checking that we can remove the dependency specified in the Lib4/leanbin/lakefile.lean to mathport: https://github.com/leanprover/mathport/pull/35. This does build from scratch successfully, for what it's worth.