[isabelle-dev] wwwfind

[Lawrence Paulson]

It sounds like a useful thing to have, especially for beginners who may not be aware of what is in the library.

Maybe we need a web interface so that users can invoke it without having to install special software. At Cambridge at least, users would have to tangle with our system administrators for each and every machine that needs to have lighttpd installed. This is quite a deterrent :-(

Larry

On 19 Jan 2010, at 22:11, Gerwin Klein wrote:

> 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