[isabelle-dev] wwwfind

Gerwin Klein gerwin.klein at nicta.com.au
Tue Jan 19 23:11:46 CET 2010

On 19/01/2010, at 9:33 PM, Lawrence Paulson wrote:
> We advertise wwwfind as the leading new feature of Isabelle 2009-1. But how is it actually invoked?
> I could find no mention of it in PG. On my Mac, it does this:
> ~: isabelle wwwfind
> Platform Darwin currently not supported by wwwfind component.
> On a Linux workstation, it does this:
> rhee: isabelle wwwfind start
> lighttpd not found at /usr/sbin/lighttpd
> I think we should publish a small tutorial somewhere.

Well, it does say in the NEWS file:

* Isabelle tool "wwwfind" provides web interface for 'find_theorems'
on a given logic image.  This requires the lighttpd webserver and is
currently supported on Linux only.

If these two preconditions are there, the tool should run out of the box without further configuration (just as you invoked it).

We should probably have put the requirements on the advertising as well, they are admittedly easy to overlook.


More information about the isabelle-dev mailing list