[isabelle] Can't get wwwfind to work in RC2


At first I thought it was my mistake, but then I consistently keep
getting this in the logs no matter what I do:

> val it = (): unit
val commit = fn: unit -> bool
*** No such file:
Exception- TOPLEVEL_ERROR raised
Error-Structure (YXML_Find_Theorems) has not been declared
Found near YXML_Find_Theorems.init ()
Static Errors

Which appears in the log like this (after everything appears to
successfully load):

SCGI server started.
  with handlers:
    - echo
    - find_theorems
    - yxml_find_theorems
/home/rafalk/wwwfind/isabelle-nicta/lib/scripts/run-polyml: line 77:
21662 Terminated              "$POLY" -q $ML_OPTIONS

I presume these two are related, but I can't find where the remaining
ROOT.ML reference is. The documentation (doc/design.tex) says:

"The module is built by using a \texttt{ROOT.ML} file inside a heap that
contains the theories to be searched."

So how do I get it to work? Did anyone else succeed in getting it to work?


Rafal Kolanski.

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