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 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.


	Makarius


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