Zulip Chat Archive
Stream: maths
Topic: halting problem
Kenny Lau (May 23 2018 at 07:25):
Kenny Lau (May 23 2018 at 07:25):
holy mother you did it @Mario Carneiro
Kenny Lau (May 23 2018 at 07:25):
congratulations
Mario Carneiro (May 23 2018 at 07:25):
You can see it's just a corollary of a much stronger theorem
Kenny Lau (May 23 2018 at 07:26):
oh and which commit should i checkout?
Kenny Lau (May 23 2018 at 07:26):
you didn't bother to build any
Mario Carneiro (May 23 2018 at 07:26):
I think Rice's theorem is cool
Mario Carneiro (May 23 2018 at 07:26):
?
Kenny Lau (May 23 2018 at 07:26):
I eat them every day
Kenny Lau (May 23 2018 at 07:26):
https://github.com/leanprover/mathlib/commits
Kenny Lau (May 23 2018 at 07:26):
there are no green ticks after April 29
Mario Carneiro (May 23 2018 at 07:26):
that's weird
Mario Carneiro (May 23 2018 at 07:27):
travis usually kicks in automatically
Kenny Lau (May 23 2018 at 07:27):
so which commit should i use?
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
Kenny Lau (May 23 2018 at 07:28):
and which lean version?
Mario Carneiro (May 23 2018 at 07:28):
3.4.1
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 ?
Mario Carneiro (May 23 2018 at 07:28):
I always get that message, but it did not affect the build itself
Gabriel Ebner (May 23 2018 at 07:29):
Either way, super does not get built by travis either at the moment.
Sebastian Ullrich (May 23 2018 at 08:05):
I'll have to ask Leo
Kevin Buzzard (May 23 2018 at 08:06):
you have a halting problem
Sebastian Ullrich (May 23 2018 at 14:48):
https://travis-ci.org/leanprover/mathlib now looks more promising
Last updated: Dec 20 2023 at 11:08 UTC