huffman at in.tum.de
Mon Jan 9 17:12:57 CET 2012
On Mon, Jan 9, 2012 at 4:04 PM, Makarius <makarius at sketis.net> wrote:
> Does the old src/HOLCF/IsaMakefile still have any purpose?
It is there so I can type "isabelle make all" in the HOLCF directory
to rebuild just those theories that depend on HOLCF, just as I could
before HOLCF was moved into src/HOL :)
I wouldn't mind getting rid of it, as long as we can have a build
target in src/HOL/IsaMakefile for HOLCF and all its dependencies.
Of course, I will be very happy when we can at last get rid of these
make files altogether.
> Ever since the inclusion of HOLCF within the regular HOL session library it
> should be subsumed by the main src/HOL/IsaMakefile. Some recent changes
> appy to both files nonetheless, see
> but the old HOLCF version probably has diverged from the HOL one already.
> (Makefiles are hard to maintain anyway.)
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev