mathlib broken?

Stream: general

[Scott Morrison]

Actually, it seems like the problem is just in mathlib.

[Scott Morrison]

Does anyone else get

/Users/scott/projects/lean/lean-category-theory/_target/deps/mathlib/data/nat/sqrt.lean:103:48: error: solve1 tactic failed, focused goal has not been solved

state:

n : ℕ,
sqrt_aux_is_sqrt :
 ∀ (m r : ℕ),
 r * r ≤ n →
 n < (r + 2 ^ (m + 1)) * (r + 2 ^ (m + 1)) → is_sqrt n (sqrt_aux (2 ^ m * 2 ^ m) (2 * r * 2 ^ m) (n - r * r)),
m r : ℕ,
h₁ : r * r ≤ n,
h₂ : n < (r + 2 ^ (m + 1 + 1)) * (r + 2 ^ (m + 1 + 1)),
a : n < (r + 2 ^ (m + 1)) * (r + 2 ^ (m + 1)),
this : is_sqrt n (sqrt_aux (2 ^ m * 2 ^ m) (r * 2 * 2 ^ m) (n - r * r))
⊢ is_sqrt n (sqrt_aux (2 ^ m * 2 ^ m) (r * (2 * 2 ^ m)) (n - r * r))
 ````

[Scott Morrison]

The finish here in mathlib/order/complete_boolean_algebra seems to take a long time to execute.

[Mario Carneiro]

mathlib is currently broken. I am working on a fix

[Kenny Lau]

actually what is the cause of the problem?

[Kenny Lau]

I roughly saw something to do with punit.eq

[Kenny Lau]

I checked the init and it is indeed there

[Mario Carneiro]

The biggest change was the has_pow typeclass, which changes the way power functions are used across the library

[Kenny Lau]

then why do I see punit.eq?

[Mario Carneiro]

group_power needed to be heavily edited, and that caused downstream changes

[Kenny Lau]

alright, good luck

[Mario Carneiro]

(plus I have some HW due tomorrow which is interfering with my maintenance work)

[Kenny Lau]

I see

[Scott Morrison]

Let us know if there is work that can be delegated. (Right now delegating might be more work than just fixing, but in the long run it may be worth thinking about sustainable models of mathlib maintenance.)

[Mario Carneiro]

For the moment I think I would rather do this work myself, and would indeed discourage others from trying to fix it on their own, because this creates merge headaches, especially in this sort of cross-library modification.

[Mario Carneiro]

I've got it 99% working, there's just one error in ordinal_notation that I need to check the original proof to fix. I could push it now, but it won't compile in travis

[Scott Morrison]

A 99% fix would still be helpful, as at the moment huge chunks of mathlib recompile every time I run leanpkg. This makes it almost impossible to work.

[Mario Carneiro]

I'll push a 99% fix if I can't get it working tonight.

[Scott Morrison]

no problem --- I'm managing as is, actually.

[Kevin Buzzard]

For the moment I think I would rather do this work myself, and would indeed discourage others from trying to fix it on their own, because this creates merge headaches, especially in this sort of cross-library modification.

The folly of youth :-)

[Kevin Buzzard]

"I am young and enthusiastic and I know I can fix it myself, so let me fix it myself"

[Kevin Buzzard]

I am just the opposite nowadays

[Kenny Lau]

a loucura da juventude

[Kevin Buzzard]

"I am old and busy, and I know I can do it, so sure go ahead and do it, and then I can remove it from my job list and furthermore I can blame you later ;-)"

[Mario Carneiro]

I see your point, but given that I've already done most of it, someone else jumping in at this point will only make things worse

[Mario Carneiro]

If I hadn't started the work I'd agree with you

[Kevin Buzzard]

I am sure you're right on this occasion.

[Kevin Buzzard]

If you're in the middle then it's surely easiest just to keep going.

[Kevin Buzzard]

I know now that the wise move is just to sit and wait and not upgrade Lean

[Kevin Buzzard]

see my comment in travis

[Mario Carneiro]

Indeed. My fix includes updating the leanpkg.toml file to explicitly reference the nightly it should work with, so hopefully going forward we shouldn't have the problem that updating breaks mathlib

[Kevin Buzzard]

I think that all this leanpkg.toml tinkering is a really good idea

[Kevin Buzzard]

because in the medium term future things will get more chaotic (when lean 4 appears)

[Kevin Buzzard]

and if we have some pretty robust stuff available for making lean and mathlib not break for people wanting to stay on the bleeding edge

[Kevin Buzzard]

this will be brilliant

[Mario Carneiro]

okay, I missed my self imposed deadline, have my 99% fix

[Kenny Lau]

e o teu HW?

[Mario Carneiro]

nao terminei

[Kenny Lau]

oh hey finalmente me falas em portugues

[Mario Carneiro]

lol

[Kenny Lau]

mdr

[Mario Carneiro]

@Sebastian Ullrich Could you troubleshoot the mathlib leanpkg.toml setup? Adding the lean_version just makes travis complain about it, and doesn't change the result.

[Sebastian Ullrich]

I'll try to build an MVP of leanup today that is sufficient for using it with Travis

[Mario Carneiro]

I think I've figured out the problem: Travis is using https://github.com/leanprover/lean-nightly/blob/gh-pages/build/lean-nightly-linux.tar.gz, which hasn't been updated in 15 days, presumably since the nightly publication process changed. Now I guess I have to go to https://github.com/leanprover/lean-nightly/releases and download the appropriate nightly, but that either requires parsing the TOML file or inserting the date in two more places in the travis.yml file. I assume this is what leanup is going to do?

[Gabriel Ebner]

Yes, see previous discussion here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/lean.20travis.20problems/near/124359348

[Sebastian Ullrich]

@Mario Carneiro Thanks for the quickfix :) . I'll have to supervise an exam today first, but after that I'll continue working on a proper leanup.