Re: [isabelle] Cygwin Isabelle2014 sledgehammer libwww-perl missing

On 14-06-26 07:31, Makarius wrote:
Thanks for testing that unofficial integration-test snapshot. It shows that there was something wrong with the integration, namely the cygwin component.

As it turns out, I'm not really testing it, I'm using it.

Everything seems to work good. When my CPU meter is at 100% for too long, when it doesn't seem it should be, my first tendency was, and can be, to think that it's gone into a bad, deep loop, and that something's wrong.

I now try remember to first ask, "Is one of the auto tools that I have enabled causing this?" I think that when I have incomplete, error causing syntax, that auto Nitpick will go into heavy usage for a longer than normal time, but I'm not sure.

I don't use "Auto Sledgehammer", and I see that "Auto Time Limit" is only 2 seconds, but when I'm getting that long CPU heavy, when I don't think I should be, when I disable all the auto tools, that seems to eliminate the heavy CPU usage.

I mention this because a person, me and probably others too, can think there's a problem when some features just need to be disabled. I have a keyboard shortcut to quickly enable and disable continuous proving, but I don't think I can assign keyboard shortcuts to options in "Plugin Options/ Isabelle / General / Automatically tried tools".

Part of the heavy usage can sometimes come from my using split screens, so sometimes I need to change what file is being displayed in an edit buffer I'm not working in.

This thread should have remained on isabelle-dev, though, where the development process happens, and everything is constantly moving -- hopefully forwards and usually quite fast. See also this change from 3 weeks ago: Public testing of isabelle-users of Isabelle2014-RC0 should start at the end of next week. Until then the continued development happens at isabelle-dev.

There's not really a problem here, other than my problem, and my problems aren't necessarily other people's problems.

Because of search engines, I compartmentalize on the Web, and I don't want a profile on isabelle-dev. Unfortunately, I've created a small one there, even though it was my intention for that not to happen.

My pointing out the failure of Sledgehammer shows the value of watching that list and saying things, and I foresee a reason, maybe once a year, to say something similar. The only solution is to send in an email under a different handle, so if someone who appears to be me does that, it could be me, it could be someone else, or it could be someone who can neither confirm nor deny that it's me. I partly say this to show that I'm willing to create another email account to abide by the list etiquette that you want. A better solution could be just to live with problems, for however long they exist.

Contrary to any possible appearance, I haven't been involved in any of the development process, though it may be that I extend Isabelle in ways that nobody else is extending it, which could be perceived as development. I'm an independent operator, and it's too easy to get a higher profile than I warrant due to light traffic on isabelle-dev.

That's where professionals with connections to big name institutions operate.


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