Re: [Axiom-developer] Re: Pamphlets and LaTex

[Stephen Wilson]

C Y <address@hidden> writes:

> --- Stephen Wilson <address@hidden> wrote:
> 
> > What if \chunk{foo} resulted in referencing the Foo domain defined in
> > another file?
> 
> I personally didn't consider it desirable to reference chunks outside
> of a particular file - it makes it that much harder to understand.  If
> the idea is to tangle something, I don't really like the idea of
> tangling a source file out of multiple pamphlets.  In my opinion that
> level of complexity is always going to cause more difficulties than any
> advantages it might give.  I would be interested in use cases that can
> demonstrate the benefits of such an approach - just because I can't
> think of any certainly doesn't mean there aren't any.

Look at the algebra, for example.  Look at the interrelationships.  Do
you want to write your algebra for Boolean in the _same_ pamphlet for
the rest of the system which depends on it?  Do ( untested :)

     cd ./src/algebra && cat *.pamphlet > algebra.pamphlet

I expect that is the situation we would have.

[...]
> >     @
> >       Introduction.
> >     <<chunk1>>=
> >         (code here)
> >     <<chunk2>>=
> >         (more code)
> >     @
> >        Some documentation
> >     <<chunk3>>=
> >          (etc...)
> >      EOF
> 
> Erm.  Do we want to support a style like that?  My first thought upon
> seeing that would be to think "badly formatted, hard to understand."

Why?
          @
          The following two routines enables one to add integers, and
          subtract them.

          <<add>>=
              (defun add (x y) (+ x y))
          
          <<subtract>>=
              (defun subtract (x y) (- x y))

I gives you freedom to organize your code in a fashion which might be
suitable for your problem.  Note that there is absolutely no
requirement that you must format your code that way.  The point is
that you can, if needed.

> > The state machine hard wires code blocks:
> > 
> >       <<chunk>>=
> >           (code)
> >       @
> 
> Yes.  Personally I consider this a Good Thing - the visual signature of
> a chunk is always consistent and unique.  This makes for easier
> pamphlet editing, in my opinion - the above example would have me
> wondering if I was in chunk1 or chunk 2.

Its like as we have in LaTeX, \section{FOO}.  Its a header.  And as I
said, if you want to structure your code in a way which reads more
easily for you, there is nothing standing in your way.

> > State machines are fine if your modeling transistor networks.  Not
> > when parsing dirt simple noweb-like markup, IMHO.
> 
> Probably the Best Way to handle this would be to use some sort of BNF
> parser generator and define the pamphlet grammar - then let the parser
> generator write us a parser.  That would of course lose us some speed,
> but if we're opening up pamphlet syntax I would say the tradeoff would
> be well worth it.  Making a literate BNF tool might also be useful down
> the line for other applications in Axiom.

I would object to that.  This is very, very, simple syntax.  You can
parse the expressions involved by hand almost as easily as you could
specify them in BNF notation -- perhaps easier.

Of course, a BNF parser-generator would be useful for other problems.

[...]
> > Yes.  I am aware for that.  Note that you need cooperation from the
> > Lisp compiler.  Again, another non-latex component to the process.
> > Another reason not to have pamphlet markup masquerade as latex.
> 
> Sure :-).  But if you don't like the LaTeX syntax, just weave it into
> something else ;-).

I would rather weave the pamphlet syntax into LaTeX, if it is LaTeX I
am interested in.

If one is convinced that latex syntax is the best, then that is fine
with me.  I really do not care that much about the syntax.  Just dont
call the file a latex file.  Call it a pamphlet, which must be
explicitly woven to generate "real" latex.

[...]
> > I have some issues with the code in cl-web, as noted above,
> > unfortunately. (again, please dont take this personally!  These are
> > just dry technical observations!)
> 
> Of course - not a problem :-).  My only concern is that the
> documentation of cl-web was a non-trivial exercise (for me, at least
> :-/) and if we are going to have to re-do this again I want to make
> sure the direction chosen is the final direction. 

We can reuse a huge part of that documentation effort.  What I am
advocating does not conflict with the traditional noweb notion.  It
expands on it.  Thus, a great deal of what you wrote applies to this
situation equally well.  I am indebted to your efforts in this
respect, as it greatly eased the prototype tool I just started working
on.

[...]
> > The correct solution is to have a pamphlet command which can either:
> >    - executes the code and generates the appropriate latex as output
> >    - or replace the command with a simple latex expression without
> >      doing any on-the fly evaluation.
> > 
> > Either behavior, and perhaps others, can be specified to weave the
> > document.
> 
> Steve, are you thinking to have chunks identify their language to the
> scanner?  Otherwise I'm not sure how the scanner will distinguish
> between input, lisp, spad, etc. in the chunk and know to evaluate only
> the input expressions.

Well, for lisp it is easy.  

If the code starts with a `(', it is Lisp :).

Seriously though.  My first response is to look at the pamphlet file
name itself.  foo.lisp.pamphlet denotes a lisp pamphlet, for example.
However, I certainly would want to be able to override the defaults
which a weave or tangle command would assume by convention.  So, yes,
I would like to have the option to say "<<chunk:boot>>=" or some such.


There is also a real advantage to be able to make these kinds of
specifications in the pamphlet file itself.

Consider how we do it today in make, where a pamphlet contains both
the boot code and the cached Lisp.  These are foo.boot.pamphlet files.
Currently, we lift the information that the root chunk <<*>> denotes
boot code and the root chunk <<clisp>> contains lisp into a the
makefiles.  Would it not be nice, for example, to have that
information available in the pamphlet itself and allow cooperation
between ASDF, say, and a Lisp based weave command to infer the the
situation itself?  Why code the same information in two places??

Note that this is not a pipe-dream.  I am working on real code which
does this reliably.

[...]
> > Axiom should be able to read pamphlets, and have them exist as
> > live objects in the system.  Should we actually require that axiom
> > write a file and call LaTeX to call itself in order to weave a
> > document?
> 
> I'm not sure what you mean by "live object".  I was viewing it as
> follows:
> 
> 1. .lisp.pamphlet and .spad.pamphlet files are loaded just as
> functionality is loaded now from these files.
> 
> 2. Axiom IO sessions inside LaTeX documents are typeset in a way
> similar to the way EMaxima handles things.  There could perhaps be an
> "evaluate all axiom expressions in this latex file" command or some
> such, but I'm not quite clear how this would make the document "live".

Consider this.  Someone is creating a new detailed algebra domain in a
fancy GUI interface which allows then to inspect and modify their
creation as they work.  This should be a familiar experience for
someone who codes in lisp or smalltalk or similar.

Our author gets their new domain working.  They click save.  A
"pamphlet" is written -- a representation of their efforts which can
be viewed just as easily in dome fancy GUI as it can in an Emacs
buffer.

In the above, where did the pamphlet originate?  I say it was a "live
object", capable of being modified and inspected by running code, by
dynamic human interaction.  The representation of a pamphlet as a file
is just a special case.

> > The Crystal, where we can view an object through a multitude of
> > facets.  We can see the API, the theorems and proofs, the category
> > hierarchy, the dependents and dependees, etc, etc...
> 
> Perhaps how we view these things is relevant to this.  For myself, most
> of these things are deduced and documents describing them can be
> generated "on the fly" with specific commands inside Axiom -
> GenerateProof(a=b,COQ) or CategoryTree(PositiveInteger) or )show api
> integrate or something like that.  I hadn't viewed the tangle/weave
> part of the system as directly having anything to do with it.

tangle/weave only have a small roll to play.  They just happen to be
the most familiar because the other operations (like dynamicly infering
the `types' of code chunks at build time),  have not yet been
invented yet.  But they will be, in time.

> > All these things have been discussed before, there are many other
> > options.  I mention these in particular because they are all
> > candidates for generating LaTeX output, but would ultimately be
> > inferred from a set of pamphlets.  You cant just run LaTeX on a
> > pamphlet and obtain that result, because pamphlets are not LaTeX.
> 
> Correct.  I would expect to do some interactive work to obtain those
> documents or at the very least run some special tools (not tangle or
> weave as such, maybe (prove-all "file.input.pamphlet") or some other
> command that builds on top of the basic scanner ability.)

Now your getting it! :)  This is precisely what I am saying.

> > Whats wrong with associating a documentation chunk as the formal
> > proof of a particular code chunks correctness?
> 
> My current (half formed) thought on that issue was to have
> pseudo-databases of the proofs themselves and get them at need (for
> generating an actual proof, or for insertion into some document).  I
> didn't figure to have every chunk and its correctness proof next to
> each other in the documents, simply because of the likely size of many
> of them (check out metamath).

How do you define the database?  How is it going to be constructed,
defined?  You need to write it down somewhere, and in the case of
axiom, it will be written down in a pamphlet.  May as well let the
pamphlets communicate the structure.

> > Or as the API doc which gets displayed when you pass the wrong type
> > to factorGroebnerBasis?
> 
> I thought API docs were very specificly terse, syntax focused messages
> that would have to be written with the idea of appearing as "error
> messages" rather than the more verbose research-paper style
> explanations.  (I'm probably missing something again, sorry...)

No, you are not missing anything.  Hence the idea of a documentation
`chunk'.  You will want to specify the API somewhere.  It could appear
in a research paper as an appendix or nowhere at all.  The very fact
that it is an option suggests to me that LaTeX is not the proper
primitive to encapsulate all that data.

For example, assume we can assign a type to a chunk, as I mentioned
above.  Then if the chunk type is Spad, feed it to the parser and ask
not for the AST, but for a list of export/documentation pairs,
extracted from the traditional +++ notation used in spad.  The +++
construct can be viewed as a special case of a "documentation chunk".

> > > Am I missing something here?  Help!
> > 
> > I hope that helps clarify my position a bit.  Lets keep discussing
> > this as I think it is of hugely important for Axiom!
> 
> It sounds like the design decision here is how much responsibility for
> processing do we specifically want to put into the weave tools.  My
> thought would be minimalist - strictly enforce the chunk style, and
> prepare additional tools/logic for operations beyond basic code
> extraction and LaTeX translation.  Which is not to say powerful tools
> aren't good, but I think they should either be inside Axiom or built as
> discrete functionality on top of the basic chunk style.

With some thought, we can define the primitives very specifically.
Indeed, weave and tangle might appear very 'high level'.

However, using just the raw notion of a `chunk' is not enough.  It
would be like trying to define mathematics using the single axiom "if
a < b and a > b, then a = b" (well, maybe not quite that extreme :).


Take care,
Steve