Zulip Chat Archive

Stream: maths

Topic: halting problem


view this post on Zulip Kenny Lau (May 23 2018 at 07:25):

https://github.com/leanprover/mathlib/commit/d62bf5605ec8971d446a01af40abf9183447cb42#diff-6650f7dae83be3a52c8eb036a23d7b26R175

view this post on Zulip Kenny Lau (May 23 2018 at 07:25):

holy mother you did it @Mario Carneiro

view this post on Zulip Kenny Lau (May 23 2018 at 07:25):

congratulations

view this post on Zulip Mario Carneiro (May 23 2018 at 07:25):

You can see it's just a corollary of a much stronger theorem

view this post on Zulip Kenny Lau (May 23 2018 at 07:26):

oh and which commit should i checkout?

view this post on Zulip Kenny Lau (May 23 2018 at 07:26):

you didn't bother to build any

view this post on Zulip Mario Carneiro (May 23 2018 at 07:26):

I think Rice's theorem is cool

view this post on Zulip Mario Carneiro (May 23 2018 at 07:26):

?

view this post on Zulip Kenny Lau (May 23 2018 at 07:26):

I eat them every day

view this post on Zulip Kenny Lau (May 23 2018 at 07:26):

https://github.com/leanprover/mathlib/commits

view this post on Zulip Kenny Lau (May 23 2018 at 07:26):

there are no green ticks after April 29

view this post on Zulip Mario Carneiro (May 23 2018 at 07:26):

that's weird

view this post on Zulip Mario Carneiro (May 23 2018 at 07:27):

travis usually kicks in automatically

view this post on Zulip Kenny Lau (May 23 2018 at 07:27):

so which commit should i use?

view this post on Zulip Mario Carneiro (May 23 2018 at 07:27):

I have been building locally so they should work, but I guess I should find out what's up with travis

view this post on Zulip Kenny Lau (May 23 2018 at 07:28):

and which lean version?

view this post on Zulip Mario Carneiro (May 23 2018 at 07:28):

3.4.1

view this post on Zulip Gabriel Ebner (May 23 2018 at 07:28):

Travis is broken on the other packages as well. "This is not an active repository
You don't have sufficient rights to enable this repo on Travis.
Please contact the admin to enable it or to receive admin rights yourself." @Sebastian Ullrich ?

view this post on Zulip Mario Carneiro (May 23 2018 at 07:28):

I always get that message, but it did not affect the build itself

view this post on Zulip Gabriel Ebner (May 23 2018 at 07:29):

Either way, super does not get built by travis either at the moment.

view this post on Zulip Sebastian Ullrich (May 23 2018 at 08:05):

I'll have to ask Leo

view this post on Zulip Kevin Buzzard (May 23 2018 at 08:06):

you have a halting problem

view this post on Zulip Sebastian Ullrich (May 23 2018 at 14:48):

https://travis-ci.org/leanprover/mathlib now looks more promising


Last updated: May 10 2021 at 06:13 UTC