Re: [Axiom-developer] LogiWeb

[Klaus Ebbe Grue]

Hi Ralf,

> http://axiom-developer.org/
>
> But I guess, the information there is not organized enough for everyones
> taste. So if you don't understand something, it's probably better to ask
> on the axiom-dev list.
>
> Maybe a good start would be to download the Axiom book (it's free) or try out 
> AXIOM online inside the WIKI.

Thanks. I printed out (part of) the Axiom book and will take a look at it.

> Oh, that sounds even more interesting that you can already compile
> programs that are hidden in papers. In fact, currently a pamphlet file
> is nothing else than an ordinary input file for noweb
> (http://www.eecs.harvard.edu/~nr/noweb/). They contain the programs and
> Makefiles are used to extract and build the program. In fact, one
> pamphlet contains only a part of the whole AXIOM CAS.

I just took a quick look at noweb. Maybe if you have an example of a 
pamphlet file, then I could run acrosss that also.

> BTW, what tool to you use to translate TeX into HTML?

I don't. After considering lots of alternatives, including MathML, I ended 
up translating TeX to PDF. At the time I investigated the alternatives, a 
latex|dvipdfm pipeline was the only combination of programs which (1) 
could reliably mix TeX and http-references and (2) gave rise to acceptable 
response times. There is a bug in dvipdfm which has the effect that some 
pages get magnified so that one has to click fit-to-width to get them back 
in reasonable size. I have complained to the dvipdfm maintainers about 
this, but I don't think anything will happen. I suppose there are many 
more options than latex|dvipdfm today, but until further I stick to that 
solution.

> I completely understand your decision, but now it might be time to open
> it up. Which means more people than just you need to understand the
> scary details. LogiWeb would be dead immediately if there happens
> something dragically to you. How much is LogiWeb already in use
> somewhere? What would be a good start to read about the overall
> infrastructure and the internals? Any linearly readable text available?

The decision on making Logiweb a one-man project has fulfilled its 
purpose (to make Logiweb small and coherent), so I have no problems 
opening the sources. Actually, I am in the process of documenting the 
system to a degree where others could implement it from scratch. As a 
first step, the internal protocol is documented in

ftp://ftp.rfc-editor.org/in-notes/internet-drafts/
draft-grue-logiweb-protocol-1-00.txt

But that is not a good place for starting to learn about Logiweb.

> How much is LogiWeb already in use
> somewhere?

The release of Logiweb is rather new. Right now it is only installed three 
places. I hope to add Bialystok soon.

> What would be a good start to read about the overall
> infrastructure and the internals? Any linearly readable text available?

A good start is the 'Logiweb base page' which is the page which 
'bootstraps' Logiweb. It is at
http://logiweb.eu/logiweb/page/base/fixed/body/tex/page.pdf

Section 2 in principle tells all there is to tell about programming in 
lambda calculus. Section 3 defines addition, exceptions, and so on. 
Section 4 defines a self-evaluator and, as a side effect, explains some of 
the central data structures. Section 5 defines macro expansion. Without
macros, Logiweb is difficult to live with. Macros are not used much on the 
base page itself, but if you replace 'base' by 'check' in the URL above, 
you get to the page which defines Logiwebs 'own' proof checker. Section 6 
explains how to compile Logiweb programs into stand-alone programs.

Another linear source could be 
http://logiweb.eu/logiweb/doc/browser/loading.html

That reference is *much* shorter than the base page, and more technical 
in nature. I think it is a good place to get information for anyone who 
already has a picture of what Logiweb looks like.

> > But from now on, anyone can continue the developement of the system 
> > without touching the source code: Anyone can add facilities to
> > Logiweb by publishing Logiweb pages containing the facilities. I
> > intend to continue doing bugfixes, minor updates, and porting (and I
> > would not mind getting help on that:-)
>
> Does LogiWeb have some features like WEB, i.e. change files by which one
> can modify the originally published program? (Honestly, I don't really
> understand the details of Knuth's .ch files, but it sounds to me like a
> necessary feature to remove bugs without touching the original sources.

No. The sources of Logiweb are never touched when changing Logiweb. 
New features are published on Logiweb pages and are available to anyone 
who reference them. That should work since Logiweb itself is rather 
neutral and just allows people to publish features. Logiwebs 'own' proof 
checker is an example: it is just a feature published on a Logiweb page, 
and those who want to use it, reference it, and those who don't, don't. In 
that way I avoid forcing my own proof checker upon other people.

> I very much hope that this will become a fruitful 
> cooperation.

The same to you. I have taken the liberty to sign up to the 
axiom-developer mailing list. I hope that is ok.

Best regards,
Klaus