Zulip Chat Archive

Stream: general

Topic: mathlib is broken


view this post on Zulip Kenny Lau (Jan 12 2019 at 15:28):

The new Lean (merged just yesterday) breaks mathlib

view this post on Zulip Mario Carneiro (Jan 12 2019 at 15:29):

naturally

view this post on Zulip Kenny Lau (Jan 12 2019 at 15:29):

what should we do then?

view this post on Zulip Mario Carneiro (Jan 12 2019 at 15:29):

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

view this post on Zulip Mario Carneiro (Jan 12 2019 at 15:30):

travis seems to disagree

view this post on Zulip 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
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'
[...]

view this post on Zulip Kenny Lau (Jan 12 2019 at 15:32):

I think travis uses the old lean

view this post on Zulip Gabriel Ebner (Jan 12 2019 at 15:32):

Travis uses the Lean version specified in leanpkg.toml.

view this post on Zulip Kenny Lau (Jan 12 2019 at 15:33):

which is 3.4.1

view this post on Zulip Mario Carneiro (Jan 12 2019 at 15:33):

in that case I think we're fine

view this post on Zulip Mario Carneiro (Jan 12 2019 at 15:33):

we can just make an update commit at some point

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jan 12 2019 at 15:35):

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

view this post on Zulip Kenny Lau (Jan 12 2019 at 15:35):

changes

view this post on Zulip Kenny Lau (Jan 12 2019 at 15:35):

I'll just go back to 3.4.1 then

view this post on Zulip Mario Carneiro (Jan 12 2019 at 15:37):

I can't find a 3.4.2 on lean repo

view this post on Zulip Mario Carneiro (Jan 12 2019 at 15:37):

are you sure it's released?

view this post on Zulip Sebastian Ullrich (Jan 12 2019 at 15:37):

It's not. The nightly is.

view this post on Zulip Kenny Lau (Jan 12 2019 at 15:38):

I build Lean myself

view this post on Zulip 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 :) ...

view this post on Zulip Kenny Lau (Jan 12 2019 at 15:47):

oh man imagine when Lean 4 comes out

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jan 14 2019 at 01:26):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Mar 31 2019 at 19:35):

Fixed, thanks for pointing this out.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 01 2019 at 06:59):

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

view this post on Zulip Mario Carneiro (Apr 01 2019 at 07:00):

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

view this post on Zulip Johan Commelin (Apr 01 2019 at 07:03):

Ok, that's fine with me.

view this post on Zulip Johan Commelin (Apr 01 2019 at 07:03):

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

view this post on Zulip Johan Commelin (Apr 01 2019 at 07:03):

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

view this post on Zulip 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