[isabelle] Isabelle2013-RC1 Sledge output finicky



I finally got some good data.

I attach 3 screenshots for a total of 135+154+159 KB. Not bad for capturing a lot of screen space.

Here's the story: I had two views open, a left view and a right view.

1) I did a CNTL-V to insert what I call the "sledge_long" command. (Why use 1 when you can use 18, although there's a few I leave out.)

2) Sledgehammer finished after only a few seconds and didn't give me any feedback. That's shown in the 1st screenshot.

3) I clicked into the other view and switched to the file with the sledgehammer command. It automatically started running sledgehammer, but quit after a few seconds, without giving any real feedback in the output panel. I didn't capture that screenshot.

4) I clicked back into the left view and switched to a file which the sTs.thy file imports. That caused the right view to start running Sledgehammer again, but this time Sledgehammer worked right. The 2nd screen capture shows the right view running Sledgehammer.

5) The right view finished running Sledgehammer after a couple of minutes, I clicked back into the right view, and I scrolled down to the bottom of the output panel. The 3rd screen shot shows the right view finished, with the last of the Sledgehammer results. It finished normally given the 90 second timeout.

Here is my cheap seats observation: With Sledgehammer and parallel processing, nothing ever happens exactly the same twice. I hope that helps.

That parallel processing, it's tricky stuff, and I've now noticed that one of those processes didn't get terminated, at the expense of 25% of the CPU processing. Icon meters in the taskbar. Necessary, very necessary.

Just now getting back to jEdit, the Sledgehammer command was still there. I clicked back and forth between the two windows, it kicked out fast without proving anything, and after more clicking around, it started running right and was visible in both views.

Regards,
GB

Attachment: 1_sledge quit after a few seconds.png
Description: PNG image

Attachment: 2_sledge running in right view.png
Description: PNG image

Attachment: 3_sledge finished in right view.png
Description: PNG image



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