Re: [isabelle] Presenting theories without running a session



On Mon, Feb 14, 2011 at 10:11 AM, Makarius <makarius at sketis.net> wrote:
>
> On Mon, 14 Feb 2011, Christian Sternagel wrote:
>
> > I think what Robert finds strange (and me too, by the way), is that even
> > if using an (due to the message) existing flag like "-?", Isabelle
> > produces an error message before giving the usage information. Typing
> > either of
> >
> > isabelle usedir -?
> > isabelle usedir "-?"
> > isabelle usedir '-?'
> >
> > in bash, using Isabelle2011 (down to at least Isabelle2007), I always
> > get the error message "illegal option -- ?".

This was exactly the point I was trying to bring up.

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

In the case of 'usedir', for instance, there is already a branch in
the case statement.  If '\?' was passed in as the value of '$OPT' on
line 95 of $ISABELLE_HOME/lib/Tools/usedir, it will be caught at line
171 and invoke the usage() function.  It looks to me that the
following is sufficient to make the error message disappear (Thanks to
Lars for pointing out that the error comes from getopts):

--- lib/Tools/usedir.OLD        2011-02-14 15:17:05.000000000 +0000
+++ lib/Tools/usedir    2011-02-14 15:18:20.000000000 +0000
@@ -90,7 +90,7 @@
 function getoptions()
 {
   OPTIND=1
-  while getopts "C:D:M:P:T:V:bd:f:g:i:m:p:q:rs:t:v:" OPT
+  while getopts "C:D:M:P:T:V:bd:f:g:i:m:p:q:rs:t:v:\?" OPT
   do
     case "$OPT" in
       C)

Many of the other tool scripts are in the same state, while others
(dimacs2hol, doc, env, make, makeall, and unsymbolize) handle the '-?'
option properly.

> Over many years Isabelle shell scripts have converged towards a certain
> standard form that minimizes various real problems, like spaces or unicode
> in directory names.  It all has become surprisingly complex, and indeed
> the semantics of bash is very complicated.  Any adhoc changes in the
> scripts to do not really make a fundamental difference are likely to
> increase the entropy.

I certainly understand that this is not an easy problem, and must be
secondary to developments in more interesting proof assistant work.
However, I humbly suggest, as I wrote in reply to Matthew, that
choosing an option like '-h' instead of '-?' might make the standard
form of expressions even more robust.  (Not to mention more consistent
with typical Linux command-line options.)

> Generally, there is a tendency to reduce traditional shell exposure of
> Isabelle more and more, as the Isabelle/Scala layer takes over the main
> responsibility of system integration.  (Many users on Mac OS X and Windows
> do not even know what a command-line based shell is and even failed to
> do the "tar" invokations on the download site.)

If command line users are in the minority (and shrinking), then the
status quo is probably fine.  I can certainly use the software right
now without too much trouble.  Thank you very much for your thoughts
on the situation!

-- Robert





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