mathlib is broken

Stream: general

[Kenny Lau]

The new Lean (merged just yesterday) breaks mathlib

[Mario Carneiro]

naturally

[Kenny Lau]

what should we do then?

[Mario Carneiro]

the breakage is mostly just theorems that moved from here to there or vice versa

[Mario Carneiro]

travis seems to disagree

[Kenny Lau]

$ cd /c/lean

Kenny Lau@DESKTOP-F01EMD3 MINGW64 /c/lean
$ git log -1 --pretty=oneline
92826917a252a6092cffaf5fc5f1acb1f8cef379 fix(library/module_mgr): ignore '\r' changes

Kenny Lau@DESKTOP-F01EMD3 MINGW64 /c/lean
$ cd /c/mathlib

Kenny Lau@DESKTOP-F01EMD3 MINGW64 /c/mathlib
$ git pull
Already up-to-date.

Kenny Lau@DESKTOP-F01EMD3 MINGW64 /c/mathlib
$ winpty /c/lean/bin/lean --make
C:\mathlib\tactic\mk_iff_of_inductive_prop.lean:50:9: error: unknown identifier
'drop_pis'
[...]

[Kenny Lau]

I think travis uses the old lean

[Gabriel Ebner]

Travis uses the Lean version specified in leanpkg.toml.

[Kenny Lau]

which is 3.4.1

[Mario Carneiro]

in that case I think we're fine

[Mario Carneiro]

we can just make an update commit at some point

[Kenny Lau]

so I need to refrain from using 3.4.2? I really like the \r fix though...

[Mario Carneiro]

adapting to 3.4.2 isn't totally trivial, at least we have to import the removed things and remove any mathlib patches for the bugs

[Kenny Lau]

https://github.com/leanprover/lean/compare/17fe3de...master

[Kenny Lau]

changes

[Kenny Lau]

I'll just go back to 3.4.1 then

[Mario Carneiro]

I can't find a 3.4.2 on lean repo

[Mario Carneiro]

are you sure it's released?

[Sebastian Ullrich]

It's not. The nightly is.

[Kenny Lau]

I build Lean myself

[Sebastian Ullrich]

I'm ready to release 3.4.2, but maybe someone wants to port mathlib first and make sure everything works out. With the intended branch layout, that would happen on the master branch while regular mathlib stays on the 3.4.1 default branch :) ...

[Kenny Lau]

oh man imagine when Lean 4 comes out

[Kenny Lau]

@Mario Carneiro I think coinductive was removed, and I think tactic/mk_iff_of_inductive_prop.lean depends on it

[Bryan Gin-ge Chen]

The branch 3.4.2 in leanprover-community/mathlib compiles with the latest nightly Lean. I didn't commit any changes to leanpkg.toml so if you want to try it out, you'll have to change 3.4.1 to nightly after you checkout.

For reference, here are the relevant commits to base Lean removing coinductive_predicates and removing relators and transfer.

All I did was copy the old coinductive_predicates to meta, merge the old relator into logic/relator, copy transfer to tactics, and then add the necessary import statements. I think the only thing that was removed that hasn't been added back in this branch is the transfer-related stuff in library/data/dlist since it only seemed to be used in the code in int that was removed.

[Mario Carneiro]

Looks good. @Sebastian Ullrich , I think we are go for launch

[Bryan Gin-ge Chen]

@Mario Carneiro I forgot to mention that the file tests/coinductive currently uses #check, #print and admit, which seems to be against mathlib style.

[Abhimanyu Pallavi Sudhir]

so I need to refrain from using 3.4.2? I really like the \r fix though...

What's the \r fix?

[Bryan Gin-ge Chen]

@Abhimanyu Pallavi Sudhir It's a fix for an issue that windows users were having with unnecessary recompilation: see https://github.com/leanprover/lean/pull/1986

[Bryan Gin-ge Chen]

I've PR'd the 3.4.2 branch: https://github.com/leanprover/mathlib/pull/610

[Bryan Gin-ge Chen]

@Mario Carneiro The recent "feat(data/complex/basic): smul_re,im" commit has broken mathlib (travis). The issue is these lemmas in ring_theory.algebra.

[Rob Lewis]

Fixed, thanks for pointing this out.

[Johan Commelin]

Some lines were removed from https://github.com/leanprover-community/mathlib/blob/c91e6c2eb882b0fea4f4bdbba2b1c498cdf40da1/src/ring_theory/algebra.lean#L348-L355 which I think is good.
However, I don't like the names of https://github.com/leanprover-community/mathlib/commit/72634d2c5ca048582107778aab164ac12aba0d40 because there is now • in sight. Shouldn't these be called coe_mul_re or something like that? Or they might also actually use the scalar multiplication, but maybe that imports too much high-level stuff?

[Mario Carneiro]

I don't think complex should ever use • except in translating facts from modules

[Mario Carneiro]

there should be a simp lemma that rewrites r • x : complex to \u r * x

[Johan Commelin]

Ok, that's fine with me.

[Johan Commelin]

So maybe those removed lemmas should be replaced with those simp lemmas

[Johan Commelin]

But I still think that the current smul_re doesn't follow the naming conventions.

[Mario Carneiro]

given that there aren't going to be any theorems about smul itself like this, I think it's fine, since it's still "morally" smul