|Logiweb system pages|
|Tutorial T01: Hello world|
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'.
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:
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:
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.
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.
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.
You have now produced your first Logiweb page.