[isabelle-dev] isabelle build
Makarius
makarius at sketis.net
Tue Aug 7 16:14:07 CEST 2012
On Tue, 7 Aug 2012, Johannes Hölzl wrote:
> isabelle mkroot shouldn't be about build only.
> I think it is a good idea to propose some best practices, like
>
> * you can use a ROOT file to check your theories with isabelle build
>
> * you can use LaTex to document your theories (document/root.tex)
>
> * you can use version control the same way as with regular source code
>
> Of course, it shouldn't be condescending. But why shouldn't we give a
> beginner some kind of guidelines?
So far we are just collecting wild ideas.
In principle, what used to be "isabelle mkdir" and is "isabelle mkroot" at
the moment is the tool to set up a "project".
David Aspinall had already added his "isabelle mkproject" for PG/Eclipse
in changeset cb0c4bd149a6, but that is also obsolete. So we could hijack
that name, or just call it "isabelle project".
So the example invocation becomes:
isabelle project && ./build
isabelle project Test && ./build
Potentially with some more options for the project setup.
Makarius
More information about the isabelle-dev
mailing list