## Stream: general

### Topic: mathlib is broken

#### Kenny Lau (Jan 12 2019 at 15:28):

The new Lean (merged just yesterday) breaks mathlib

naturally

#### Kenny Lau (Jan 12 2019 at 15:29):

what should we do then?

#### Mario Carneiro (Jan 12 2019 at 15:29):

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

#### Mario Carneiro (Jan 12 2019 at 15:30):

travis seems to disagree

#### Kenny Lau (Jan 12 2019 at 15:31):

$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

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 (Jan 12 2019 at 15:32):

I think travis uses the old lean

#### Gabriel Ebner (Jan 12 2019 at 15:32):

Travis uses the Lean version specified in leanpkg.toml.

which is 3.4.1

#### Mario Carneiro (Jan 12 2019 at 15:33):

in that case I think we're fine

#### Mario Carneiro (Jan 12 2019 at 15:33):

we can just make an update commit at some point

#### Kenny Lau (Jan 12 2019 at 15:33):

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

#### Mario Carneiro (Jan 12 2019 at 15:34):

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 (Jan 12 2019 at 15:35):

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

changes

#### Kenny Lau (Jan 12 2019 at 15:35):

I'll just go back to 3.4.1 then

#### Mario Carneiro (Jan 12 2019 at 15:37):

I can't find a 3.4.2 on lean repo

#### Mario Carneiro (Jan 12 2019 at 15:37):

are you sure it's released?

#### Sebastian Ullrich (Jan 12 2019 at 15:37):

It's not. The nightly is.

#### Kenny Lau (Jan 12 2019 at 15:38):

I build Lean myself

#### Sebastian Ullrich (Jan 12 2019 at 15:39):

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 (Jan 12 2019 at 15:47):

oh man imagine when Lean 4 comes out

#### Kenny Lau (Jan 12 2019 at 18:35):

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

#### Bryan Gin-ge Chen (Jan 13 2019 at 22:28):

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 (Jan 14 2019 at 01:26):

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

#### Bryan Gin-ge Chen (Jan 14 2019 at 14:49):

@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 (Jan 18 2019 at 15:18):

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 (Jan 18 2019 at 15:25):

@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 (Jan 18 2019 at 15:25):

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

#### Bryan Gin-ge Chen (Mar 31 2019 at 17:20):

@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 (Mar 31 2019 at 19:35):

Fixed, thanks for pointing this out.

#### Johan Commelin (Apr 01 2019 at 06:55):

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 (Apr 01 2019 at 06:59):

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

#### Mario Carneiro (Apr 01 2019 at 07:00):

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

#### Johan Commelin (Apr 01 2019 at 07:03):

Ok, that's fine with me.

#### Johan Commelin (Apr 01 2019 at 07:03):

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

#### Johan Commelin (Apr 01 2019 at 07:03):

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

#### Mario Carneiro (Apr 01 2019 at 07:04):

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

Last updated: May 13 2021 at 23:16 UTC