Zulip Chat Archive

Stream: general

Topic: mathlib broken?


view this post on Zulip Scott Morrison (Apr 03 2018 at 23:35):

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

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

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

view this post on Zulip Mario Carneiro (Apr 04 2018 at 00:47):

mathlib is currently broken. I am working on a fix

view this post on Zulip Kenny Lau (Apr 04 2018 at 00:47):

actually what is the cause of the problem?

view this post on Zulip Kenny Lau (Apr 04 2018 at 00:47):

I roughly saw something to do with punit.eq

view this post on Zulip Kenny Lau (Apr 04 2018 at 00:47):

I checked the init and it is indeed there

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

view this post on Zulip Kenny Lau (Apr 04 2018 at 00:48):

then why do I see punit.eq?

view this post on Zulip Mario Carneiro (Apr 04 2018 at 00:48):

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

view this post on Zulip Kenny Lau (Apr 04 2018 at 00:49):

alright, good luck

view this post on Zulip Mario Carneiro (Apr 04 2018 at 00:50):

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

view this post on Zulip Kenny Lau (Apr 04 2018 at 00:50):

I see

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

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

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

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

view this post on Zulip Mario Carneiro (Apr 04 2018 at 05:38):

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

view this post on Zulip Scott Morrison (Apr 04 2018 at 05:39):

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

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

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

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 09:30):

I am just the opposite nowadays

view this post on Zulip Kenny Lau (Apr 04 2018 at 09:30):

a loucura da juventude

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

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

view this post on Zulip Mario Carneiro (Apr 04 2018 at 09:31):

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

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 09:31):

I am sure you're right on this occasion.

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 09:31):

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

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

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 09:31):

see my comment in travis

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

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 09:35):

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

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 09:36):

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

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

view this post on Zulip Kevin Buzzard (Apr 04 2018 at 09:36):

this will be brilliant

view this post on Zulip Mario Carneiro (Apr 04 2018 at 10:12):

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

view this post on Zulip Kenny Lau (Apr 04 2018 at 10:12):

e o teu HW?

view this post on Zulip Mario Carneiro (Apr 04 2018 at 10:14):

nao terminei

view this post on Zulip Kenny Lau (Apr 04 2018 at 10:15):

oh hey finalmente me falas em portugues

view this post on Zulip Mario Carneiro (Apr 04 2018 at 10:15):

lol

view this post on Zulip Kenny Lau (Apr 04 2018 at 10:15):

mdr

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

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

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

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

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