[isabelle] RC4: sledgehammer on Cygwin crashed once; temp file not removed


I got the same failure I was getting with the pre-RC Isabelle2014, but, for now, it's doesn't appear to be of a catastrophic nature.

I attach a screen shot. It happened when I edited the timeout value. I've didn't test RC2/RC3, and I've only tested RC4 for several hours, to see what's up with the new Sledgehammer provers, and provers I haven't normally used.

It's only happened once, which indicates it'll be happening again occasionally, but if 3 hours is indicative of the future, it'll be tolerable. I'll find out, though not right away.

I've been out of the proving game, concerning myself with how I can attempt to conquer the future.

It turns out that in being overwhelmed, where I couldn't go forward, but wouldn't go back, I think I've strategized to where I haven't ended up wasting 2 years. In fact, I'm now not not two months behind, but a year or so ahead, because I've eliminating months of programming work. Hard work only gets a person so far. Some roads, they can't be traveled fast.

Acceptable solutions are all in the mind, the mind being the domain of many neurons, where neurons fight, one against the other, a brutal struggle for neuron supremacy, playing out, repeatedly, for hours on end, sometimes day after day, a struggle that is never a win-win struggle. At most, only a few neurons can win. It's even possible that all will lose, a most depressing thought, especially for those unfortunate neurons given the task of processing depressing thoughts.

The future is in parallel programming, and a full-blown general purpose GPU future, and general-purpose-massively-many-core-processor is getting closer all the time.

Nvidia played an important part in paving the wave, with CUDA, and turning GPUs into GPGPUs.

AMD nearly went out of business, but they aquired ATI, and now the boys are back in town. I had my credit card out, ready to buy a $650 AMD 8-core PC, but I decided to wait. For years, I haven't seen that AMD has had a CPU decently close in speed to a lower cost i7, but it could be AMD finally back in the game with a CPU like the FX-8320, along with their APUs.



At $1695 (full price), for a Intel Xeon Phi Coprocess 3120P, I'm thinking that the decently-cheap future is getting decently close. The Xeon Phi Coprocessor runs Linux, which is one of many examples that engineers and programmers are working hard to give us the use of a CPU and GPU, or Xeon, where we don't have to work so hard to make things happen fast.

For now, the present is continuing to extend the life of C and C++, in a big way, because the use GPGPUs is largely about having to use pointers. After many years of working hard to get away from manipulating memory directly, C is back in style, as if it ever went away.

But maybe things like ScalaCL will abstract us back up, by abstracting us away from all the messy details of OpenCL, when it's done in C and C++:


Being an expert in things related to proving math, namely, being an expert in programming, can be mutually exclusive with being an expert in proving math. I'm now of the mindset that, for myself, proof is optional. It's a fact, bug-ridden programs can be of great use to people. On the other hand, that which is logically correct, but of no use to anyone, is mostly, if not completely, ignored and forgotten.

In abandoning proof, I might have come up with a solution to not have to abandon proof. But it's too early to say, for sure.


Attachment: 140823__RC4 sledge crash.png
Description: PNG image

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.