[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