[isabelle-dev] isabelle build

Johannes Hölzl hoelzl at in.tum.de
Tue Aug 7 10:25:11 CEST 2012


Am Dienstag, den 07.08.2012, 09:03 +0200 schrieb Tobias Nipkow:
> Am 07/08/2012 09:00, schrieb Jasmin Christian Blanchette:
> > Am 07.08.2012 um 00:15 schrieb Johannes Hölzl:
> > 
> >> 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"
> > 
> > Isn't that condescending?
> 
> Worse, it has nothing to do with "build".
> 
> Tobias


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?

  - Johannes







More information about the isabelle-dev mailing list