Re: [Axiom-developer] ProofGeneral

[Bill Page]

Quoting Ralf Hemmecke <address@hidden>:

> Could someone have a look at
> http://proofgeneral.inf.ed.ac.uk/kit
>
> Eclipse-Plugin at:
> http://proofgeneral.inf.ed.ac.uk/eclipse
>
> Bill, that is from the answer of Christoph Lüth whom I asked about
> the project http://www.informatik.uni-bremen.de/~cxl/eig/index.html.
> You sent me that that link recently in connection with literate
> programming in eclipse.
>
> I currently have no time. Is there some stuff in this plugin that is
> connected with literate programming?

Short answer: Yes. But my ultimate conclusion is that this is not
something new for us.

As a starting point I read the document:

  Assisted Proof Document Authoring.
  by David Aspinall, Christoph Lüth  and Burkhart Wolff.

at http://proofgeneral.inf.ed.ac.uk/Kit/docs/pgauthor.pdf

I think it is clear that the "document-centric" approach advocated by
the authors of this paper for creating human-readable large-scale proofs
using automated theorem provers (e.g. the famous proof of the 4-color
theorem) is very similar to the type of interaction that we have envisaged
for the interaction of mathematicians with computer algebra systems.
It is essentially the same problem. This does have some things in
common with what is conventionally known as literate programming,
hence "literate theorem proving" and "literate computer algebra", etc.
but this is not a new paradigm for literate programming.

I found the discussion of "backflow" also very relevant to the way we
hope to use computer algebra. Backflow is the substitution of output
generated by an external system back into the actual literate document.
The result is then woven (in the sense of literate programming) into a
LaTeX file and rendered as PDF.  Exactly this is possible now on the
Axiom Wiki when using the interface to Sage. See for example:

http://wiki.axiom-developer.org/SandBoxSageAxiomInterface
http://wiki.axiom-developer.org/SandBoxSagePamphlet

Something very similar to this also an integral part of the Axiom Wiki
website at a deeper level since it directly supports "backflow" from the
Axiom Interpreter, the Aldor, Spad, Boot and Lisp compilers (in the
context of Axiom) as well as Reduce and Maxima into a the contents
of a wiki page. In MathAction such code chunks are delimited by
LaTeX pseudo-environment markers like:

  \begin{axiom}
  integrate(sin(x)*cos(x),x)
  \end{axiom}

Thus the Axiom Wiki (or more generally, the MathAction extension
of ZWiki) is already a "literate" environment for the use of computer
algebra in this sense.

In principle I think it would be quite easy to develop plug-ins for both
emacs and eclipse based on the example of Proof General.

Regards,
Bill Page.