Re: [isabelle] Presenting theories without running a session
On Mon, 14 Feb 2011, Robert Lamar wrote:
But you did get the usage, right? The error is a known feature,
because "?" is not an option.
With all due respect, if 'isabelle' (without any arguments) tells me
that I should add '-?' to a command to find out more, I should not get
an error message when I follow the instructions. If usage info is a
feature, the command-line option should exist. Otherwise it is
confusing, as a user.
There is a misunderstanding here. There is no option for help or usage,
but you get the latter whenever the command line is syntactically
malformed. Passing "-?" provokes such a syntax error, so you get the
usage of the command line as advertized. This was part of my minimalistic
design when I did this many years ago.
You can understand it as an instance of the original Unix attitude to
avoid extra features if the same can be achieved as a consequence of
existing functionality. Or as an instance of the principle in logic that
redundant axioms are avoided in favour of lemmas.
Anyway, I have now tried it myself with zsh (from Mac Ports). The shell
zsh: no matches found: -?
The reading of this message should be obvious to seasoned users of the
shell. And it also works directly when I pass "-?" for tool specific
help, with the literal quotes.
This archive was generated by a fusion of
Pipermail (Mailman edition) and