Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] document preparation query


view this post on Zulip Email Gateway (Aug 19 2022 at 11:49):

From: Leo Freitas <leo.freitas@newcastle.ac.uk>
Hi

I am struggling a bit with the document preparation options, mostly because of
the many variations and consequences of their (mis)use.

The one I found easier to use was having a ROOT file with the sessions of interest,
and just use "isabelle build". I think I managed to make it work reasonably well.

I also saw the other options with mkdir/usedir, which uses ROOT.ml ad IsaMakeFile.
I think I understood the difference, yet wasn't quite sure which one is best/current practice.

Is there a tutorial on such things? Looking at Isabelle's own ROOT file it was good, if a bit complex.

Any hints / pointers / best-practices would be appreciated.

Best,
Leo

view this post on Zulip Email Gateway (Aug 19 2022 at 11:49):

From: Lars Hupel <hupel@in.tum.de>
Hi Leo,

The one I found easier to use was having a ROOT file with the sessions of
interest,
and just use "isabelle build". I think I managed to make it work
reasonably well.

isabelle build is indeed used for document preparation since
Isabelle2013. The old mkdir/usedir tools have been discontinued (cf
the NEWS file).

Is there a tutorial on such things? Looking at Isabelle's own ROOT file it
was good, if a bit complex.

I don't know whether there's a tutorial for document preparation, but you
can have a look at the AFP <http://afp.sourceforge.net/> for examples of
ROOT files. The source code is browsable via SourceForge:
<http://sourceforge.net/p/afp/code/ci/default/tree/thys/>.

Cheers
Lars

view this post on Zulip Email Gateway (Aug 19 2022 at 11:50):

From: Makarius <makarius@sketis.net>
On Mon, 23 Sep 2013, Leo Freitas wrote:

I am struggling a bit with the document preparation options, mostly
because of the many variations and consequences of their (mis)use.

Both the "system" and "isar-ref" cover document preparation, including
minimal examples to get an idea how things are done in Isabelle2013.

There is also "isabelle mkroot" to make default session directories with
document preparation.

I also saw the other options with mkdir/usedir, which uses ROOT.ml ad
IsaMakeFile. I think I understood the difference, yet wasn't quite sure
which one is best/current practice.

Just forget that ROOT.ML and IsaMakefile ever existed. Isabelle2013 is
the last Isabelle release where this old stuff from 1996 is still there as
legacy feature.

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 11:50):

From: Makarius <makarius@sketis.net>
Note that the latest Isabelle release (which is Isabelle2013) mentions
mkdir and usedir as "legacy", but it is still there. They will disappear
in the coming release -- release candidates will become publicly
available in 1-2 weeks.

Isabelle is a professional application with proper releases -- this should
not be confused with ever changing repository snapshots.

Makarius


Last updated: Apr 25 2024 at 20:15 UTC