System pages
Site pages

Introduction...
Showroom
Tutorials
Man pages
Help
Download
Wiki...
Wiki submission
Background
Machine room...
Contact

T01: Hello world
T02: Programming
T03: Proving
T04: Googling
T05: Syntax

Hints for administrators
Syntax of references
Road map
Explanation of output

Up. Submission form.

Introduction

Logiweb is a system for distribution of definitions, lemmas, and proofs. It is also a system for electronic publishing of high quality journal papers. Journal papers constitute the normal medium for distribution of definitions, lemmas, and proofs, so the two statements above are more or less equivalent.

As an analogy to 'html pages', papers published on Logiweb are called 'Logiweb pages' in Logiweb terminology.

The present tutorial teaches how to publish a Logiweb page containing the immortal words 'Hello world'.

Prerequisites

• You must know LaTeX.
• The present site must support a Logiwiki. If it doesn't, you get an 'Error 404: Object not found' when you try to submit a page.
• You must adjust the width of your browser window to make the lines of the present tutorial short enough to be readable.

The header creation form

Open the header creation form in a separate window (in most browsers: right click the link and select something like 'open in new window').

The form has a 'Suggest Header' button and two big text windows.

Start making your page

Enter the following in the upper text window:

PAGE my page
BIBLIOGRAPHY
"check" "http:../../../page/check/latest/vector/page.lgw".
"base" "http:../../../page/base/latest/vector/page.lgw".

The lines above assign the name 'my page' to your page. Furthermore, they state that all constructs defined on the 'check' and 'base' pages are available for use on your page.

A bibliographic entry consists of a name and a reference:

"check" "http:../../../page/check/latest/vector/page.lgw"

The reference above is relative to your publication directory. You can read more about references here.

The name can be used for refering to the page locally inside your source text. You can choose the name freely, but I suggest you use the name of the page unless forced to do otherwise (e.g. if you reference two distinct pages who happen to have identical names).

Generate associativity sections

All constructs defined on the 'check' and 'base' pages have to be 'imported'. How they are imported may affect the priority and associativity of the imported constructs. We shall not care about that now, so we just ask the system to suggest how to import all constructs:

• Click 'Suggest Header'.

Clicking 'Suggest Header' is supposed to send your source text (known as a 'pyk' source text) through the pyk compiler. If you install Logiweb on your own computer, you can invoke the pyk compiler directly from a command line.

The response from pyk

If you got an 'Error 404: Object not found': move to a site such as logiweb.eu which supports a Logiwiki.

If you are a system administrator desperately trying to make the present tutorial work, try to go here.

If you got no 404 then chances are you got a Logiwiki submission form

The form has a 'Submit' button, some controls, and two big text windows. The upper window contains something like this:

PAGE my page
BIBLIOGRAPHY
"check" "http:../../../page/check/latest/vector/page.lgw".
"base" "http:../../../page/base/latest/vector/page.lgw".
PREASSOCIATIVE
"check" check
"base" base
PREASSOCIATIVE
"base" +"
...
PREASSOCIATIVE
"base" " \\ "

This is a suggestion from pyk on how you could import all constructs defined on the check and base pages. Pyk suggests that the 'check' and 'base' constructs get highest priority and that the 'x \\ y' construct gets lowest priority. It also suggests some constructs to be pre- and some to be post-associative.

A 'preassociative' construct is left-associative in text which runs left-to-right, right-associative in text which runs right-to-left, and counter-clockwise-associative in text written in clockwise spirals. As an example, 12 \\ 34 \\ 56 means ( 12 \\ 34 ) \\ 56 because x \\ y is preassociative. +12 \\ 34 means ( +12 ) \\ 34 because +x has higher priority than x \\ y.

Pyk does not necessarily guess what priorities and associativities you want to assign to the constructs. But pyk does its best. Priority, associativity, and other syntactic issues are covered in more detail in Tutorial T05: The pyk syntax.

Publication directory

Enter some strings in the 'org=' and 'name=' fields.

Your page will end up in a directory named org/name/ inside the Logiwiki. The 'org' and 'name' fields have no other purpose than picking a name for the publication directory.

Produce a 'Hello world' page

Put the following in the lower text window:

BODY
page ( Pyk , Priority )
title "My page"
bib ""
main text "Hello world"
appendix "This is my appendix"
end page

The pyk compiler simply appends the text in the upper and lower text window before translation. The pyk compiler does not even put a newline character between the text of the upper and lower text window, so be sure to end the upper text window and/or begin the lower text window with a newline character.

• Press 'Submit'.

Viewing your page

The response from pyk contained a line saying

Rendering page here

Click the 'here' link in the response to get to a page saying something like

Logiweb main menu of my page

Logiweb can be implemented as a browser plug-in but, until further, the burden of installation is put on Logiweb site maintainers rather than casual Logiweb readers. For that reason, pyk is constructed such that it generates a number of ordinary html and PDF pages which allow a reader to view Logiweb pages without any other software than a PDF enabled web browser.

But rush to see your masterpiece: click the 'Body' link on the main menu page to get to a page saying something like

Logiweb body of my page

Then click the Pdf link on that page to see your page.

When you have finished admiring your page, click 'back' to get to back to this window:

Logiweb body of my page

Then click Toc (Table Of Contents) to get to a page with links to 'main text', 'appendix', and 'chores'. If you click 'main text' you get to the page you admired above. If you click 'appendix' you come to the appendix you defined in your body section. If you click 'chores' you get to a page generated on basis of the header of your page. Section 1 of chores lists the constructs you have defined. Your page only defines a 'my page' construct which represents your page. Section 2 contains a complete priority and associativity table which lists the hundreds of constructs you have imported from the check and base pages.

The 'body' of a page is the thing you want your readers to see. Other things like the 'bibliography', 'dictionary', 'codex', and so on is useful for advanced readers who want to build on top of your results. Those other things may also be useful for yourself if the page does not behave as you expect and you want to debug your pyk source.

If you are curious about what the 'bibliography', 'dictionary', etc. contain, click here.

Conclusion

You have now produced your first Logiweb page.

Up. Submission form.