4.11 External interfaces

Prev Up Next Page 37 of 800 Search internet

Once upon a time, Logiweb had features for generating XML, MathML, Lisp S-expressions, Mizar source code, and other formats. Now, Logiweb has a Turing complete rendering facility, and it is up to you, the author of Logiweb pages, to decide what formats you want to support.

Logiweb still has special support for TeX in that the rendering machinery is able to invoke LaTeX, BibTeX, makeindex, and dvipdfm. Furthermore, Logiweb has special support for C in that Logiweb machines are able to invoke a C compiler and load the resulting Dynamic Link Library (DLL).

If you want to interface Logiweb to some other system, first consider the option to port that system into Logiweb.

If porting to Logiweb is not an option, and if you just want to transfer data from Logiweb to the other system, you should consider writing a rendering function which renders the Logiweb data you want in the format required by the other system.

As an alternative, your can write a program which can read the binary 'rack' format of Logiweb pages. That format is simple, easy to parse, and contains a lot of information in a lot of versions organized in a lot of different ways, so chances are that it contains something you can use.

Transferring data into Logiweb

If you want to transfer data from some other system to Logiweb, chances are that you are doing something you should not do.

Logiweb is a system for archiving and publishing eternal truths. An eternal truth can be a theorem which will stay true forever. Or, more dull, an eternal truth can be that a particular version of a particular program is defined in a particular way. Or that a particular version of a particular paper contains a particular text.

As a non-trivial example, the Peano page proves a number of theorems and store them together with their proofs, the axioms used and the proof checker used. If you change the axioms or the proof checker, the theorem may not be true relative to the new axioms or proof checker. But the fact that a given theorem is true for given axioms, a given proof, and a given proof checker is an eternal truth and that truth is what Logiweb can archive and publish.

If you have verified a proof on some other proof system and want Logiweb to archive and publish that, forget it. You can only record that fact faithfully on Logiweb if you put the foreign proof checker under Logiweb version control, i.e. if you port the foreign system to Logiweb.

The only way to transfer information from a foreign proof system to Logiweb without porting that foreign proof system is to let the foreign proof system generate a Logiweb source (lgs) file which you can then run through the Logiweb compiler (lgc).

Prev Up Next Page 37 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05