[isabelle-dev] src/HOLCF/IsaMakefile

[Brian Huffman]

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.

- Brian

>
> 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
> http://isabelle.in.tum.de/repos/isabelle/log/f363e5a2f8e8/src/HOL/HOLCF/IsaMakefile
> but the old HOLCF version probably has diverged from the HOL one already.
> (Makefiles are hard to maintain anyway.)
>
>
>        Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev