[isabelle-dev] wwwfind

[Gerwin Klein]

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.

Cheers,
Gerwin