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
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
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and