!4#2977 Algebra.DirectSum.TensorProduct

Stream: mathlib4

[Eric Wieser]

I've spent more than an hour on a single declaration in !4#2977 (port-status#linear_algebra/direct_sum/tensor_product) and am having a very bad tmie

[Eric Wieser]

The proof takes on the order of minutes before spitting out an error, and about every other change the syntax highlighting breaks and I have to restart the lean server

[Eric Wieser]

Example of broken highlighting:

image.png

[Eric Wieser]

The error message there is nonsensical and refers to unknown constant 'DirectSum.toModulR', which feels as though it's reporting an error about the mangled code that it's highlighting, not the code that is actually in the editor

[Kevin Buzzard]

One hack I found when Lean gets into this state is to go up to the theorem or definition you're working on and just change theorem to theoremq or definition to defq and then change it back. It's quicker than recompiling the entire file and seems to fix the syntax highlighting issue.

[Eric Wieser]

That doesn't work for me here

[Eric Wieser]

The orange bars jump around, but the syntax remains broken

[Kevin Buzzard]

I'm about to get on the tube @Eric Wieser but I don't want to duplicate work. Is it safe for me to play around with this (and possibly get nowhere)?

[Eric Wieser]

I might keep fighting it, but absolutely

[Eric Wieser]

I'd like to know if the bizarre editing experience is something weird with gitpod or something you can reproduce

[Kevin Buzzard]

ain't no gitpod underground. I'll get back to you in an hour.

[Matthew Ballard]

Is this working now?

[Matthew Ballard]

It does take a little bit to check but the proof you pushed for this result seems to work ok

[Eric Wieser]

I was able to get it to work just now

[Eric Wieser]

But I had to add a nasty number of (_)s

[Eric Wieser]

Does adding set_option profiler true slow things down considerably?

[Matthew Ballard]

A bit, yes. Tracing isDefEq also seems to to drag. I’ve had to bump heart beats after adding these

[Eric Wieser]

Ah, my lean server had crashed, but the orange bars stick around so it's hard to tell. The result is compilation of TensorProduct.directSum took 47.7s.

[Matthew Ballard]

Better than a lot of files

[Kevin Buzzard]

So I got it working too. I didn't experience the desyncing error reporting but perhaps that was a problem with the earlier long proof which was working when I pulled. Here's some diffs between my solution and what's on github:

You said

    repeat'
      first
        |rw [compr₂_apply]|rw [comp_apply]|rw [id_apply]|rw [mk_apply]|rw [DirectSum.toModule_lof]
        |rw [map_tmul]|rw [lift.tmul]|rw [flip_apply]|rw [curry_apply]

I said

    simp only [compr₂_apply, comp_apply, id_apply, mk_apply, DirectSum.toModule_lof, map_tmul, lift.tmul, flip_apply, curry_apply]

because it looks less odd. And you said

  erw [directSumLeft_tmul_lof, Dfinsupp.mapRange.linearEquiv_apply]
  exact Dfinsupp.mapRange_single

but I said

  rw [directSumLeft_tmul_lof]
  exact Dfinsupp.mapRange_single (hf := fun _ => rfl)

[Kevin Buzzard]

which makes me wonder if Lean 3 exact was able to solve an implicitfun _ => rfl before.

[Matthew Ballard]

There are other records of weird syntax errors on Zulip. I don’t know if a single culprit has been identified.

Did you try outlining the fields of directSum to speed it up?

[Eric Wieser]

What do you mean by outlining?

[Eric Wieser]

@Kevin Buzzard, the repeat first stuff was from mathport, your proof sounds much beter

[Matthew Ballard]

Construct each field in a separate declaration

[Eric Wieser]

Feel free to push your tidier proofs

[Kevin Buzzard]

I removed the repeat proof because in my experience proofs like that can be super slow and I wondered if this was causing the slowdown

[Kevin Buzzard]

But it was still slow afterwards

[Matthew Ballard]

Eric Wieser said:

Feel free to push your tidier proofs

Just comments from the peanut gallery. Are we happy with the time?