[Logiweb] New pyk/base/peano

[Klaus Ebbe Grue]

Hi logiweb at diku.dk

The local installation at Diku has been updated. The update concerns the 
pyk compiler, the base page, and the 'peano' page that defines Peano 
arithmetic.

Klaus

---

Pyk compiler:
----------------
A new version of the pyk compiler is available in ~grue/logiweb/20050603, 
so add the 20050603 in front of the 20050502 and 20050526 catalogues in 
your path.

An error in translation of http addresses in bibliographies has been 
fixed. From now on, the compiler prints a message when it translates an 
http address indicating which address it tries to resolve. The rules for 
http addresses are:

Full addresses like http://www.diku.dk/... are just looked up as they are.

Partial addresses like http:base/latest/vector/page.lgw are converted into 
<url>/base/latest/vector/page.lgw where <url> is the publication library 
set by "url=..." in the compiler command line or configuration files.

The error was that the pyk compiler prepended <url> even to full 
addresses.



Base page:
----------
An error in the definition of array assignment has been corrected.

The
   intro * index * pyk * tex * end intro
and
   intro * pyk * tex * end intro,
constructs have been moved from the peano page to the base page.

An error in the "intro" constructs above caused tex errors when 
typesetting the macro expanded version of a page. That has been corrected.

The
   line * because * indeed * cut *
construct has been changed to
   line * because * indeed * end line *
to increase compilation speed of "peano axioms" page. Reason: The pyk 
compiler considers *all* possible interpretations of a page. And having an 
operator named "* cut *" and another one named "... * cut *" may induce a 
long delay from
the "Frontend: parsing body" to the "Frontend: invoking priority rules" 
message.



Peano page:
-----------
"peano" page has been renamed to "peano axioms".

The peano page now defines two versions of Peano arithmetic and contains 
one correct proof for each theory.