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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
