Stream: Archive Mirror: Isabelle Users Mailing List

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


view this post on Zulip Email Gateway (Aug 19 2022 at 10:26):

From: Rafal Kolanski <xs@xaph.net>
Hi,

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:
"/home/rafalk/wwwfind/isabelle-nicta/src/Tools/WWW_Find/ROOT.ML"
Exception- TOPLEVEL_ERROR raised
Error-Structure (YXML_Find_Theorems) has not been declared
Found near YXML_Find_Theorems.init ()
Static Errors
ML>

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?

Sincerely,

Rafal Kolanski.


Last updated: Mar 28 2024 at 16:17 UTC