mathport fails

Stream: mathlib4

[Yury G. Kudryashov]

See, e.g., https://github.com/leanprover-community/mathport/actions/runs/5438759147/jobs/9890195349

[Yury G. Kudryashov]

https://github.com/leanprover-community/mathport/actions/workflows/predata.yml

[Yury G. Kudryashov]

It looks like a build machine doesn't have mathlibtools and we don't install them as a part of the CI.

[Yury G. Kudryashov]

@Floris van Doorn You broke it by adding leanproject get-cache in https://github.com/leanprover-community/mathport/pull/244

[Yury G. Kudryashov]

Should we install mathlibtools on the runner or drop this line in the CI?

[Yury G. Kudryashov]

(e.g., by checking for an environment variable)

[Floris van Doorn]

Oh, that is unfortunate. I don't know what the best way to fix it is.

[Alex J. Best]

Installing mathlibtools as a CI step seems quite a reasonable fix, many of our existing actions already do this

[Yury G. Kudryashov]

Do we need this cache in CI?

[Yury G. Kudryashov]

If not, then another fix is to do if [[ -z "$SOME_GITHUB_ENV_VAR" ]]; then leanproject get-cache; fi

[Yury G. Kudryashov]

I mean, if we're going to recompile mathlib anyway, then why bother downloading another 100M?

[Yury G. Kudryashov]

https://github.com/leanprover-community/mathport/pull/245

[Mario Carneiro]

@Floris van Doorn could you clarify the motivation for the leanproject get-cache and git fetch steps added to the makefile? Those makefile targets are not supposed to be getting a full copy of the project, only enough to make mathport work

[Mario Carneiro]

Plus, get-cache can cause conflicts with the oleans downloaded from predata. We also have to ensure that the oleans are not present before running lean --make --ast --tlean because compilation is skipped if they are and then we don't get the ast.json files

[Floris van Doorn]

Mario Carneiro said:

Floris van Doorn could you clarify the motivation for the leanproject get-cache and git fetch steps added to the makefile? Those makefile targets are not supposed to be getting a full copy of the project, only enough to make mathport work

If I didn't do that before running mathport oneshot, all of mathlib3 would be compiled when running mathport oneshot on my machine.

[Floris van Doorn]

For mathport oneshot are we supposed to recompile all of mathlib3 with the --ast flag ourselves?
Or is there a difference with what should happen for the main mathport function and the mathport oneshot function?

[Floris van Doorn]

git fetch was added because I already ran mathport oneshot on an earlier version of Lean/mathlib, and the current script just errored with "unknown commit <sha>" or something.

[Yury G. Kudryashov]

Mario said during the meeting that the "download release" step should give you oleans.

[Mario Carneiro]

In my command history is the following method to update mathport such that make oneshot will run quickly:

git pull && \
lake exe cache get && \
lake build && \
./download-release.sh && \
make clean-oneshot && \
cd sources/mathlib/ && \
leanproject get-cache && \
cd ../..

[Mario Carneiro]

The download-release.sh method does give you oleans, but I have often hit the issue that lean 3 refuses to accept them as up to date and will try to recompile everything

[Mario Carneiro]

How about we take all the commands above except the git pulland put them in a prep-oneshot makefile target? I don't want to be running that as part of the usual makefile targets (which are mainly intended to be run by CI, which does not need this), and I also don't want to run it as part of make oneshot because that will make it take a lot longer and repeatedly re-download things.

[Patrick Massot]

I don't know if this is the same discussion but each time I tried to run mathport on a project depending on mathlib following the instructions on the mathport README, I had to wait a long time for this lean --make --ast --tlean step (that is flagged as "get some coffee" in the README).

[Mario Carneiro]

you should not personally have to run that step at all, except as part make oneshot on your own project

[Mario Carneiro]

it is equivalent to compiling your project in lean 3

[Mario Carneiro]

if it's a big project, yes it could take a while

[Patrick Massot]

I was reading https://github.com/leanprover-community/mathport/#running-on-a-project-other-than-mathlib

[Mario Carneiro]

yeah that's the one that compiles your project

[Patrick Massot]

And I'm talking about line which contains "get coffee". This line clearly compiles mathlib.

[Mario Carneiro]

compiling mathlib is not in the job description

[Patrick Massot]

Then something is failing.

[Mario Carneiro]

maybe steps 2 and 3 there should be interchanged

[Patrick Massot]

It's getting late here, but I'll try to experiment more tomorrow or on Wednesday.

[Mario Carneiro]

it is possible that the same get-cache issue that happens in local oneshot also happens in project oneshot

[Mario Carneiro]

in which case the proposed prep-oneshot command should also help there

[Patrick Massot]

I'm not talking about one-shot here, but about whole project port.

[Mario Carneiro]

I know

[Mario Carneiro]

I'm saying that the same fix would affect both

[Riccardo Brasca]

I just used mathport on flt-regular, and everything worked pretty well. In particular I didn't have to compile mathlib.

[Riccardo Brasca]

The only thing that was not perfect is that mathport wrote all the import lines (those related to files of the project) as import Myproject..., but this is very easy to fix.

[Riccardo Brasca]

So thanks to all the people that made this so easy!

[Johan Commelin]

Riccardo Brasca said:

The only thing that was not perfect is that mathport wrote all the import lines (those related to files of the project) as import Myproject..., but this is very easy to fix.

I think even with mathlib we have a script that fixes those kind of things

[Riccardo Brasca]

Maybe if this is expected we can mention it in the Wiki (it says that one has to replace Mathbin)

[Eric Wieser]

I think the expectation is now that you moved your files into a new import namespace?

[Eric Wieser]

Or do you literally mean the string "MyProject" rather than your actual project name?

[Gabriel Ebner]

FYI, mathport once again fails to build with the latest mathlib. Now that the port is done, I'm no longer going to keep it working. (It will still keep pulling changes from mathlib3, but it won't pick up new tactic syntaxes or align statements in mathlib.) Feel free to fix it if you need mathport. I have disabled the cron build in the meanwhile because I am getting an email every time it fails. https://github.com/leanprover-community/mathport/commit/2107e736c89fd69467fe93ecfca8d44552f8cb7a

[Eric Wieser]

Won't this be an issue for downstream projects using the last unported file?

[Kevin Buzzard]

Do any such projects exist?

[Patrick Massot]

Yes, the sphere eversion project happens to use spheres.

[Kevin Buzzard]

Oh lol I had assumed the last one was the finite type morphisms file (and I couldn't think of any project using that). Funny how algebraic geometry and differential geometry finished at pretty much the same time.

[Kevin Buzzard]

Ok I've just caught up on the rss stream. So looks like algebra beat analysis :P

[Scott Morrison]

I attempted to fix mathport in https://github.com/leanprover-community/mathport/pull/247. If that works, then we should remember to turn on the update cron job.

[Mario Carneiro]

Yes, I would rather not drop mathport support until everything in lean 3 is ported (including external projects), which basically means for the indefinite future

[Mario Carneiro]

we can reduce the CI frequency or run it on demand though

[Mario Carneiro]

it would be great if mathport CI emails me instead of gabriel though, @Gabriel Ebner did you do something to set this up?

[Sebastian Ullrich]

I believe GitHub simply messages the person that last touched the CI file

[Eric Wieser]

Don't we want to stop the mathlib4 updates in mathport once we cut the port-complete tag?

[Eric Wieser]

With the intent being that mathport is then a tool to jump between the port-complete tags in mathlib and mathlib4.

[Mario Carneiro]

I don't see why we wouldn't want to jump to the latest mathlib4

[Eric Wieser]

Because there's no guarantee that will align with mathlib3 any more

[Mario Carneiro]

it should, at least tactic-wise

[Eric Wieser]

Not #align-wise though if things start being deleted in refactors

[Mario Carneiro]

if the aligns are different that's not a big deal but if mathport doesn't compile anymore on latest then we need to fix that

[Eric Wieser]

What's the advantage of working on new mathlib4?

[Mario Carneiro]

if you are bumping an old lean 3 project then it's not good enough to go to old mathlib4, and the latter part of the work does not have much automated assistance ATM

[Mario Carneiro]

are we planning on doing something about that?

[Mario Carneiro]

otherwise it's just leaving these folks high and dry

[Mario Carneiro]

mathlib is currently very much a "live at head" ecosystem, so putting people on an old version is not helpful

[Eric Wieser]

That's no different to anyone who has a lean4 project that they've abandoned for a while though

[Mario Carneiro]

no, because this is the approved migration path

[Mario Carneiro]

the migration path should terminate on something that is actually new

[Eric Wieser]

In what way is port-complete mathlib4 not "actually new"?

[Mario Carneiro]

we should have a migration path for old lean 4 as well, although I am willing to accept manual breakage and fixage for early lean 4 work since it's not stable yet

[Eric Wieser]

My thinking is that getting people to Lean4 + old mathlib4 safely is a better choice than half-getting them to new mathlib4 and saying "sorry, we can't match things up any more"

[Mario Carneiro]

Eric Wieser said:

In what way is port-complete mathlib4 not "actually new"?

If there is a solid path from port-complete mathlib4 and head mathlib4, then that's fine. But it doesn't sound like that will be the case going forward

[Mario Carneiro]

Eric Wieser said:

My thinking is that getting people to Lean4 + old mathlib4 safely is a better choice than half-getting them to new mathlib4 and saying "sorry, we can't match things up any more"

I disagree. If they want this they can use port-complete mathport too

[Mario Carneiro]

but latest mathport should use latest everything, at least as long as mathlib4 doesn't have stable releases

[Eric Wieser]

I guess port-complete existing in mathport is sufficient to provide the tool that I want to use

[Mario Carneiro]

I think it is okay if the #aligns gradually rot but aren't actively destroyed in the near term

[Eric Wieser]

It seems to me this approach is encouraging downstream projects to stay in Lean 3 as long as possible

[Eric Wieser]

Because while they remain stale lean3 projects there'll be a tool that tries to convert to latest mathlib4

[Mario Carneiro]

I don't see how? It's keeping the migration path open long enough for it to actually happen

[Eric Wieser]

But if they mathport now, they become a stale lean4 project and are out of options

[Mario Carneiro]

thinking about this stuff the day after mathlib is done is definitely premature for all the big projects out there that couldn't even start porting until mathlib finished

[Mario Carneiro]

just like mathlib itself, they probably won't mathport in one go, although this depends on the complexity of the project

[Mario Carneiro]

Once it's in lean 4 the responsibility shifts to keeping up with mathlib normally; if it is abandoned for some time after porting then this might be difficult and I agree we should do something about this issue

[Mario Carneiro]

I actually wouldn't be surprised if mathport still has a significant amount of additional growth to come when it comes to external projects, because mathlib has a relatively uniform style and external projects might exercise new code paths or rely on things that were skipped for mathlib purposes

[Eric Wieser]

Mario Carneiro said:

just like mathlib itself, they probably won't mathport in one go, although this depends on the complexity of the project

I would speculate that it is probably easiest to have a fixed version of mathlib4 in mind when porting piece-by-piece, rather than having moving target

[Mario Carneiro]

perhaps, that's a decision for the project maintainers

[Mario Carneiro]

one reason in particular to want to bump is because something in the project caused a bug report which was fixed upstream and now you want the results

[Mario Carneiro]

same as with mathlib bumps

[Scott Morrison]

PR re-enabling the update mathlib4 cron job is at https://github.com/leanprover-community/mathport/pull/249

[Mario Carneiro]

We can decrease the rate to nightly, right?

[Notification Bot]

18 messages were moved from this topic to #mathlib4 > #align_import by Eric Wieser.

[Yaël Dillies]

Trying to mathport LeanAPAP, and I get this:

-- PLEASE REPORT THIS TO MATHPORT DEVS, THIS SHOULD NOT HAPPEN.
-- failed to format: unknown constant 'Expectations.Mathlib.Algebra.BigOperators.Expect.«term𝔼_in_with_,_»'
theorem
  expect_congr
  ( f g : α → 𝕜 ) ( p : α → Prop ) [ DecidablePred p ] ( h : ∀ x ∈ s , p x → f x = g x )
    : 𝔼 i in s with p i , f i = 𝔼 i in s with p i , g i
  := by rw [ expect , sum_congr rfl ] · rfl simpa using h

[Yaël Dillies]

Pretty sure this is just my expectation notation being borked by mathport, but since you said to report, here it is:

localized "notation `𝔼` binders ` in ` s ` with ` p:(scoped:49 p, p) `, ` r:(scoped:67 f, finset.expect (s.filter p) f) := r" in expectations
localized "notation `𝔼` binders ` in ` s `, ` r:(scoped:67 f, finset.expect s f) := r" in expectations
localized "notation `𝔼` binders ` with ` p:(scoped:49 p, p) `, ` r:(scoped:67 f, finset.expect (finset.univ.filter p) f) := r" in expectations
localized "notation `𝔼` binders `, ` r:(scoped:67 f, finset.expect finset.univ f) := r" in expectations

[Bhavik Mehta]

Note this notation is surprisingly useful in combinatorics, especially probabilistic combinatorics, so it would be really nice if Lean 4 supports writing something like this as Lean 3 does

[Mario Carneiro]

See whether it helps to put a name on the notation; I recall we had to name all localized notations because of name clashes between re-opened versions of the same notation

[Mario Carneiro]

what does lean think about the notation

scoped[Expectations]
  notation3"𝔼 "(...)" in "s" with "p:49:(scoped p => p)", "r:67:(scoped f =>
    Finset.expect s.filterₓ p f) => r

?

[Mario Carneiro]

does it give an error when processing this command (ignoring any issues in the expressions themselves)?

[Mario Carneiro]

my guess is that notation3 is rejecting this because you used scoped twice

[Mario Carneiro]

synport doesn't run many commands, but it does need to run notation commands so that it can elaborate the syntax

[Mario Carneiro]

a really cheap fix is to replace the notation with

scoped[Expectations]
  notation3"𝔼 "(...)" in "s" with "p", "r:67:(scoped f =>
    Finset.expect s.filterₓ p f) => r

(or the lean 3 equivalent) and see if mathport accepts it despite the lean 3 compilation errors

[Bhavik Mehta]

Mario Carneiro said:

my guess is that notation3 is rejecting this because you used scoped twice

I thought so too, I wasn't aware that using scoped twice was allowed until I tried doing this - I don't think mathlib uses it anywhere, so I'm not at all surprised that mathport doesn't like it

[Mario Carneiro]

actually it is notation3 itself (the mathlib command) that rejects it

[Mario Carneiro]

If I comment out the line that throws the error, it more or less seems to work (although it doesn't generate a delaborator, but this is fine for synport)

[Mario Carneiro]

actually even the delaborator generation works, you just have to write Set.filter s instead of s.filter

[Bhavik Mehta]

Mario Carneiro said:

actually even the delaborator generation works, you just have to write Set.filter s instead of s.filter

Finset.filter rather than Set.filter?

[Mario Carneiro]

The lack of type information here is exactly why the delaborator fails :grinning:

[Bhavik Mehta]

Hmm, I thought the Finset.expect should be enough - the first argument to that should be known to be a Finset - or is that not how it works?

[Mario Carneiro]

Although the code seems to ... do something, it is very confusing to me what the actual semantics of multiple scoped is. I may need to play with lean 3 a bit to see how the expansion for p is used in the expansion for f

[Mario Carneiro]

@Bhavik Mehta It just says s, it doesn't have a type ascription

[Mario Carneiro]

for all we know it's a s : Foo and there exists Foo.filter producing a Finset

[Kyle Miller]

I might have added that hasScoped check, and I think it was only because the delaborator it generates is sketchy. Each scoped clause thinks it's responsible for filling out the list of binders, if I remember correctly

[Mario Carneiro]

that might be fine, since the meaning of double filling a binder is that the two occurrences have to match

[Mario Carneiro]

this is used to interpret non-linear patterns

[Kyle Miller]

It's not checking that the binders match though, rather it's accumulating the binders twice (s.pushBinder in matchScoped is the only thing that updates the binders array)

[Mario Carneiro]

TBH I wouldn't be surprised if lean 3 does that too

[Mario Carneiro]

@Yaël Dillies Have you ever tried to use this notation with more than one binder? I get type errors with something like

variable {α β} (s : Finset α) (p : α → α → Prop) (f : α → α → β)
#check 𝔼 (i : α) (j : α) in s with p i j, f i j

but it might just have always been like that

[Mario Carneiro]

#6793