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

On Fri, 27 Jun 2014, Gottfried Barrow wrote:

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

By definition, when your are "using" an arbitrary repository snapshot, you are "testing" it. It can change rather quickly, as you have seen, and not always to the better. Serious work requires serious stable software releases.

We have this global trend, that many projects give up the principle of proper stable releases, and everyone is hooked on a repository for "latest and greatest snapshots". Isabelle is still in the furtunate situation of not following that.

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.

Systems extensions are perfectly normal for users, on normal stable releases. In some sense, all of Isabelle/HOL is just a user-space library, although a very big and complex one.

What makes you part of the development process is the "use" (i.e. "testing") of an arbtrary snapshot of the present state of the development.


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