Re: [isabelle] Presenting theories without running a session
On Tue, Feb 15, 2011 at 11:52 AM, Makarius <makarius at sketis.net> wrote:
> 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.
Yes, I clearly misunderstood. When I ran 'isabelle' with no
arguments, it told me,
Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
And I assumed that "-?" had a special status, where it is simply one
of many strings which will cause the command line arguments to be
malformed. My mistake.
I perceived that there was some inconsistency in the documentation,
and was mentioning these things in a helpful effort to provide a bug
report. But I can see that my understanding of the system design was
flawed, so there is no bug and nothing to fix.
> Anyway, I have now tried it myself with zsh (from Mac Ports). The shell
> clearly reports:
> 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.
I would not yet call myself a 'seasoned' user of zsh, but I did
understand the above meaning for the message. I deeply regret not
saying so in my initial email. I got that error, and it did not
confuse me: I mentioned it because the choice of "-?" caused different
behaviors in different shells, and I thought that the developers might
like to know this so that users could have a more uniform experience
across systems. I really expressed this poorly.
But as we established above, "-?" does not actually have a
distinguished status, so I can use any of the following, so long as
there is no filename match:
isabelle usedir "-?"
isabelle usedir -h
isabelle usedir --help
isabelle usedir help
isabelle usedir foobarbaz
This archive was generated by a fusion of
Pipermail (Mailman edition) and