Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2015-RC5 - minor feature request


view this post on Zulip Email Gateway (Aug 22 2022 at 09:54):

From: "C. Diekmann" <diekmann@in.tum.de>
Dear Makarius,

I know it is a bit late for a feature request for the upcoming
release, but this one is really uncritical.

Is it possible to add an example to the build usage? I always need to
look up its usage. In particular, the current usage description does
not directly tell how to generate a proof document.

=== What I wish for ==
$ isabelle build --help
[...]Isabelle2015-RC5/lib/Tools/build: illegal option -- -

Usage: isabelle build [OPTIONS] [SESSIONS ...]

Options are:
[...]

Example:
Build the session with the name `Session_Name' in the current
directory and generate a pdf proof document.

$ isabelle build -v -o document=pdf -d . Session_Name
=== End what I wish for ==

Regards,
Cornelius

view this post on Zulip Email Gateway (Aug 22 2022 at 09:54):

From: Makarius <makarius@sketis.net>
In the "system" manual there is section 2.3 "Invoking the build process",
which starts with a copy of the command-line usage, with some extra
explanations. (This is a general principle for most Isabelle command-line
tools.)

Moreover, at the end of the section there are various examples.

The subsequent chapter in the manual is then about the whole complex of
document preparation.

Makarius


Last updated: Apr 24 2024 at 08:20 UTC