[isabelle-dev] isabelle build

[Johannes Hölzl]

Hi Makarius,

For the mkroot tool I would suggest that the layout looks more like a
AFP submission. The resulting directory should contain everything:

$ isabelle mkroot Project_X

Results in:
   
  Project_X/ROOT
  Project_X/Project_X.thy
  Project_X/document/root.tex

Also instead of calling the theory file "Ex.thy" I would call it like
the directory. This is quiet likely the name of the theory the user
wants for formalize. So if the user just has one theory file he does not
need to modify the ROOT file. And it allows the user to just pack the
directory Project_X and submit it as an AFP entry.

And I would suggest that isabelle mkroot tells the user to use version
control:

 * Use Mercurial to manage your project
   hg init Project_X
   hg add Project_X
   hg commit Project_X -m "initial commit"


- Johannes



Am Montag, den 06.08.2012, 19:24 +0200 schrieb Makarius:
> On Mon, 6 Aug 2012, Makarius wrote:
> 
> > In Isabelle/doc-src/ROOT there are some examples with document_dump and 
> > document_dump_mode that are leading into the direction to make typical 
> > configurations for papers based on regular sessions.
> >
> > I have my own traditional idioms here, but did not try to express them 
> > in the new way yet.  It will practially require some ./build script to 
> > wrap up the whole process as used to be done by several IsaMakefile 
> > command lines, but shell scripting is no longer built into the build 
> > tool.
> 
> I would like to encourage early adopters to post their favourite session 
> layout for individual documents (papers etc.).  So far there is a first 
> version of isabelle mkroot in eeb4480b5877, but it is still a bit awkward 
> -- too much influenced by the bounds of isabelle usedir.
> 
> The abstract specification for the result is like this:
> 
>    isabelle mkroot && ./build
> 
> It remains to figure out what mkroot generates in the directory, and what 
> the local build script looks like (based on isabelle build + isabelle 
> document etc.).
> 
> 
>  	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev