[Logiweb] Curious Logiwiki behavior

[Klaus Ebbe Grue]

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