## Stream: general

### Topic: mathlib broken?

#### Scott Morrison (Apr 03 2018 at 23:35):

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

#### Scott Morrison (Apr 03 2018 at 23:36):

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 (Apr 03 2018 at 23:43):

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

#### Mario Carneiro (Apr 04 2018 at 00:47):

mathlib is currently broken. I am working on a fix

#### Kenny Lau (Apr 04 2018 at 00:47):

actually what is the cause of the problem?

#### Kenny Lau (Apr 04 2018 at 00:47):

I roughly saw something to do with punit.eq

#### Kenny Lau (Apr 04 2018 at 00:47):

I checked the init and it is indeed there

#### Mario Carneiro (Apr 04 2018 at 00:48):

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

#### Kenny Lau (Apr 04 2018 at 00:48):

then why do I see punit.eq?

#### Mario Carneiro (Apr 04 2018 at 00:48):

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

#### Kenny Lau (Apr 04 2018 at 00:49):

alright, good luck

#### Mario Carneiro (Apr 04 2018 at 00:50):

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

I see

#### Scott Morrison (Apr 04 2018 at 01:05):

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 (Apr 04 2018 at 01:25):

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 (Apr 04 2018 at 01:26):

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 (Apr 04 2018 at 04:59):

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 (Apr 04 2018 at 05:38):

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

#### Scott Morrison (Apr 04 2018 at 05:39):

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

#### Kevin Buzzard (Apr 04 2018 at 09:29):

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 (Apr 04 2018 at 09:29):

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

#### Kevin Buzzard (Apr 04 2018 at 09:30):

I am just the opposite nowadays

#### Kenny Lau (Apr 04 2018 at 09:30):

a loucura da juventude

#### Kevin Buzzard (Apr 04 2018 at 09:30):

"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 (Apr 04 2018 at 09:30):

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 (Apr 04 2018 at 09:31):

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

#### Kevin Buzzard (Apr 04 2018 at 09:31):

I am sure you're right on this occasion.

#### Kevin Buzzard (Apr 04 2018 at 09:31):

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

#### Kevin Buzzard (Apr 04 2018 at 09:31):

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

#### Kevin Buzzard (Apr 04 2018 at 09:31):

see my comment in travis

#### Mario Carneiro (Apr 04 2018 at 09:33):

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 (Apr 04 2018 at 09:35):

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

#### Kevin Buzzard (Apr 04 2018 at 09:36):

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

#### Kevin Buzzard (Apr 04 2018 at 09:36):

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 (Apr 04 2018 at 09:36):

this will be brilliant

#### Mario Carneiro (Apr 04 2018 at 10:12):

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

e o teu HW?

nao terminei

#### Kenny Lau (Apr 04 2018 at 10:15):

oh hey finalmente me falas em portugues

lol

mdr

#### Mario Carneiro (Apr 04 2018 at 11:07):

@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 (Apr 04 2018 at 11:13):

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

#### Mario Carneiro (Apr 05 2018 at 05:17):

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 (Apr 05 2018 at 07:26):

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

#### Sebastian Ullrich (Apr 05 2018 at 07:53):

@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.

Last updated: May 10 2021 at 00:31 UTC