Hi Robert,
I am a PhD student in Edinburgh, Scotland who was first introduced to Logiweb
at MKM '07 [1]. Just this month, I have finally found time to start
investigating it.
Welcome to the list
To that end, I have begun to proceed through the tutorials
at logiweb.eu [2], and have encountered some strange behavior which I am
unable to duplicate predictably.
The same problem has appeared twice: After completing the Logiweb Submission
form [3], I submit the page (with the strings org="hwu" and name="rlamar", if
it helps) and receive the following error:
--------begin Logiwiki response--------
Frontend
Reverse lookup of
http://logiweb.eu/logiweb/wiki/hwu/rlamar/../../../page/check/latest/vector/page.lgw
Reverse lookup of
http://logiweb.eu/logiweb/wiki/hwu/rlamar/../../../page/Peano/latest/vector/page.lgw
Reverse lookup of
http://logiweb.eu/logiweb/wiki/hwu/rlamar/../../../page/base/latest/vector/page.lgw
Frontend: parsing associativity sections
Frontend: parsing body
Everything until this point looks fine
---
\section{Theorem}
We now state Lemma 3.2l of \cite{Mendelson87}:
"[ PA lemma 3.2|
---
l : all x : 0 * x = 0 end lemma ]"
\section{Proof}
"[ PA proof of 3.2l :
---
File Form input around line 153 char 16:
No interpretations
Goodbye
The "No interpretations, Goodbye" error message is one of the most common
error messages from the system, and it can be quite frustrating. Usually,
however, it is easy to locate the problem. The message means that the pyk
compiler (which is the one which generates the Logiwiki response) has
been able to parse everything up to line 153, character 15, but was
unable to parse character 16.
The error message consists of "---" followed by the last characters up to
line 153, character 15, followed by a vertical bar (so possible blanks at
the end of the line become visible) followed by "---" followed by some
line from line 153, character 16 and on, followed by "---" followed by the
error message.
So the compiler could parse
PA proof of 3.2
but could not parse
PA proof of 3.2l
In other words, the compiler knows something whose name starts with 3.2
but does not know something called 3.2l.
Your page references the Peano page which proves lemmas named 3.2a, 3.2b,
and so on, so that explains why the compiler can parse up to "3.2".
But the compiler does not know a construct named "3.2l".
The 3.2l construct is one you are supposed to introduce. To do so, add a
line saying
"" 3.2l
in the first PREASSOCIATIVE section in the upper window on the submission
form. The upper window should contain something like the following:
...
PREASSOCIATIVE
"check" check
"Peano" Peano
"base" base
"" 3.2l
PREASSOCIATIVE
"base" +"
...
where the 3.2l line is one you must type.
The 3.2l line comprises an empty string followed by the 3.2l construct.
The empty string indicates that the 3.2l construct is not imported from
any referenced page but, rather, is a construct you define. Tutorial
T05 gives a systematic treatment of how to introduce constructs.
I think I will just give answers to two obvious questions right ahead:
Q: Why doesn't the compiler give a better error message?
A: It can't. Compilers for languages with a fixed syntax can typically
give very precise error messages like "semicolon expected" or "3.2l
unknown". But the present language has no fixed syntax and that makes it
*extremely* difficult to give a better error message then the above when
something is unparsable. Fortunately, the system can give better error
messages in other situations. See Tutorial T05 for more on the syntax.
Q: Then, why doesn't the website or the tutorial give an explanation like
the one above.
A: That is because of lack of time. Sorry.
I am sorry that my query is verbose.
That was very helpful. In general, when asking questions, it is good to
have the complete output from the system as well as the input (the
contents of the upper and lower window of the submission form). Sometimes
even indivial switches and the "org" and "name" fields are useful to have.
I hope the answer helps. Else ask again.
Cheers,
Klaus
_______________________________________________
Logiweb mailing list
Logiweb@diku.dk
http://lists.diku.dk/mailman/listinfo/logiweb
(Web access from inside DIKUs LAN only)
