leeroy is down

[Matt Kaufmann]

Hi --

It looks to me like leeroy.defthm.com is down. It was up earlier this
afternoon. Because of my recent changes to *acl2-exports*, it might
be necessary to restart some jobs (not sure, maybe not).

Whoever can get leeroy going again.. that would be great. (Maybe
David Rager?) Not a true emergency, though.

Thanks --
-- Matt

[David L. Rager]

Hi,

We play a trick to obtain a significant discount on our cloud
computing. Specifically, we run what's called a "pre-emptible
instance." Such an instance costs ~25% of what a reliable instance
costs, and goes away when the cloud data center we use is heavily
loaded (resulting in leeroy being "down"). Thus far, this has seemed
okay, because our community is on a relatively small budget, and, in
some ways, we're lucky to have a build server at all. But, the
unfortunate consequence is that leeroy.defthm.com is down some
observable % of the time.

If this choice is particularly irksome, I'm willing to revisit it.
But, I'm guessing it's still okay -- you were just kindly letting me
know that it was down.

Thanks,
David

http://stackoverflow.com/questions/25223102/dynamically-deploying-jenkins-slaves-on-google-compute-engine-for-github-commits/33044106#33044106

> --
> --
> ACL2-books help:
> To post new messages: acl2-...@googlegroups.com
> To unsubscribe: acl2-books-...@googlegroups.com
> More options: http://groups.google.com/group/acl2-books?hl=en
>
> ---
> You received this message because you are subscribed to the Google Groups "acl2-books" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to acl2-books+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Matt Kaufmann]

Thanks, David! Now I know not to worry about leeroy right away when
it's unavailable. Is there any way for the rest of us to tell the
difference between this normal sort of "down" and something that
actually requires your intervention?

Thanks again --
-- Matt

[David L. Rager]

Hi Matt,

There's not really. Leeroy + linux historically seems pretty stable.
If it's down for a couple days, I'd find that a bit concerning. Also,
you're welcome to send me a gripe email about it being down too much
if it's bothersome. If enough people complain (and often enough),
maybe we can do something about it as a community.

Thanks,
David