Email Gateway (Aug 19 2022 at 10:26): 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: Nov 21 2024 at 12:39 UTC