[Axiom-developer] Re: algebra Makefiles with explicit dependencies, bootstrap, fixed-points etc.

[root]

This is going to be painful to follow but:

Suppose 
a is a domain, b is a domain and 
b depends on a and
a depends on b.

Suppose
a'.lsp is the lisp code for a
b'.lsp is the lisp code for b

The .spad files contain

\section{a}
a
\section{a.bootstrap}
a'.lsp

\section{b}
b
\section{b.bootstrap}
b'.lsp

Now we compile this algebra
a'.lsp -> a.fasl
b'.lsp -> b.fasl
(load a)
(load b)
a  -> a.fasl
b  -> b.fasl

now we modify a and recompile it

a (mods to) A -> A'.lsp -> A.fasl

where A is the modified A and A'.lsp is the new lisp.

ASSUMING WE HAVE NOT CHANGED THE SIGNATURE OF a
then b will still compile and be valid code and we get:

\section{A}
A
\section{A.bootstrap}
A'.lsp

\section{b}
b
\section{b.bootstrap}
b'.lsp

and it all works. 

Now if we try to change the signature of a
so that it breaks b then we need to rewrite
b into B and recompile it with A loaded so we
start from scratch with

a'.lsp -> a.fasl
b'.lsp -> b.fasl
(load a)
(load b)
a  -> a.fasl
b  -> b.fasl
a  -> A
A  -> A'.lsp -> A.fasl
(load A)
b  -> B
B  -> B'.lsp -> B.fasl
(modfify .spad file bootstraps thus:
\section{A}
A
\section{A.bootstrap}
A'.lsp

\section{B}
B
\section{B.bootstrap}
B'.lsp

and now we rebuild the system from scratch
and it all works. Notice you have to co-modify
a -> A, b -> B in the same image and update the
.spad file and bootstrap code before rebuiding
from scratch.

Note that modifying a->A so it breaks b and
simultaneously modifying b->B so it breaks a
is left as an exercise. This kind of programming
is what got axiom into the state where it needed
a running axiom to build axiom.

Once you get past the circular dependency 
problem you no longer have a need for the
lisp bootstrap code. It is possible to modify 
non-bootstrap code and break the system build
but that's just a simple programming problem.

It is very tricky to modify the fundamental
cycles but it can be done. It has always been
true that you need a running axiom to rebuild 
axiom. My key breakthru was to make it possible
to build axiom from scratch. However it is not
true that you can randomly modify anything and
expect the algebra to build.

In general you would like the makefile to know
the dependency graph of algebra code. However
you'll find that make can't handle such a graph.

I tried another idea which was to decorate each
stanza from layer n with a ${LAYER(n-1)} but that
fails also.

However the fact that I failed is no reason not
to try because you  have a deeper understanding
of make so I'm willing to be convinced. My general
approach, when domain signatures change, is to do

make clean
make

The algebra hierarchy needs a future rewrite for
2 reasons, Provisos and ACL2 integration. Hopefully
we'll be smarter next time.

t