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

-- 
Robert





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.