Email Gateway (Aug 18 2022 at 17:02): Email Gateway (Aug 18 2022 at 17:02):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 17:03):From: Robert Lamar <rlamar@stetson.edu>
On Tue, Feb 15, 2011 at 11:52 AM, Makarius <makarius@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
Email Gateway (Aug 18 2022 at 17:03):From: Timothy McKenzie <tjm1983@gmail.com>
Is guess this partly depends on what you mean by "feature", and
more specifically, whether you consider error messages to be
ordinary features. It seems strange to me that you're inviting
users to obtain usage information by provoking an error, rather
than by invoking a help or usage option. You said yourself that
"There is no option for help or usage". I think this is what
seemed strange to Robert, too.
Of course, it's not a big problem, because the usage information
is available, but it could easily confuse users who are not used
to having computer programs invite them to deliberately provoke
errors.
Tim
<><
signature.asc
Email Gateway (Aug 18 2022 at 17:15):From: Robert Lamar <rlamar@stetson.edu>
Hello, Isabelle users,
I am curious about converting .thy files to .tex files without running a
session to verify the document (with Isabelle 2011). Is this possible? I
have been looking at the documentation for 'isabelle make', 'isabelle
usedir', 'isabelle document', and 'isabelle latex', but I cannot conclude if
producing LaTeX code depends on processing the documents, producing the
heap, and so on. Clearly, running the following is sufficient to produce
the .tex files. What is necessary?
isabelle usedir -D generated HOL Foo
>
As an aside, here is something I noticed about the behavior of the isabelle
command line tool. I can work around it, I am just sharing it for your
information as a possible bug: typing 'isabelle' at a command prompt gives
usage information, and includes the message 'pass "-?" for tool specific
help.' But if I type, say, 'isabelle usedir -?', it gives the following
message along with the expected usage info for usedir:
/scratch/usr/Isabelle2011/lib/Tools/usedir: illegal option -- ?
>
That is in bash. In my favored shell, zsh, the shell gives an error because
it thinks the ? is a wildcard.
Take care,
Robert
Email Gateway (Aug 18 2022 at 17:15):From: Brian Huffman <brianh@cs.pdx.edu>
Hi Robert,
Due to the possibility of document antiquotations like @{thm foo},
generating the .tex file for a given .thy file is not trivial, and
depends on having access to the current theory database. So you will
need to run an Isabelle session.
You can speed things up a bit by running Isabelle in "skip proofs"
mode. Try adding commands to set the following two references before
"use_thys" in ROOT.ML:
quick_and_dirty := true;
Toplevel.skip_proofs := true;
use_thys ["MyTheory"];
This will cut running time by a fair amount. I do not know whether
there is a command-line option to do the same thing. (Although you can
make a separate copy of ROOT.ML file and select it with a "-f"
option.)
You can also save time by not saving a heap image. Run isabelle usedir
without the "-b" option (note that you may have to run "isabelle
usedir" from the parent directory for this to work).
Email Gateway (Aug 18 2022 at 17:16):From: Robert Lamar <rlamar@stetson.edu>
Hello Brian,
Very interesting. Thank you for your thoughts on the matter.
As I think about it, the Isabelle session will also determine the
dependencies between theories, and thus the order that they will appear in
session.tex. I am not suprised to hear that the document preparation system
relies heavily on the results of an Isabelle session; I suppose I was just
writing in to confirm that this was the case.
Robert
Email Gateway (Aug 18 2022 at 17:16):From: Makarius <makarius@sketis.net>
I've seen this effect for the last time with tcsh, many many years ago.
The usage message of the Isabelle scripts is correct in asking for "-?"
but it depends on the context how you need to produce that externally.
Here the context is prose English, so I have some quotes around it. Bash
will accept it without quotes. Other shells will have there own idea.
Makarius
Email Gateway (Aug 18 2022 at 17:16):From: Makarius <makarius@sketis.net>
The main idea behind the Isabelle document preparation system is to
produce a pinted "proof" of your formal development, using standard
typesetting technology. This explains some biases towards properly
checked sources, although there are numerous ways to print anything you
want, rearrange the order of theories etc. There are open-ended
possibilities that some users have turned this into an art in itself.
There are alternative ways to make simple draft printouts of the sources,
notable the 'display_drafs' command (the the isar-ref manual) or the
standard File/Print operation of Isabelle/jEdit. The latter works
surpringly well together with the IsabelleText font.
Makarius
Email Gateway (Aug 18 2022 at 17:16):From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
-\? does the trick in zsh, Robert.
Matthew.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 18 2022 at 17:17):From: Lars Noschinski <noschinl@in.tum.de>
On 13.02.2011 15:16, Makarius wrote:
On Thu, 10 Feb 2011, Robert Lamar wrote:
/scratch/usr/Isabelle2011/lib/Tools/usedir: illegal option -- ?
That is in bash. In my favored shell, zsh, the shell gives an error
because it thinks the ? is a wildcard.
It is a wildcard, so you will get strange effects if you've got a file
named e.g. "-b" in your current directory ;)
I've seen this effect for the last time with tcsh, many many years ago.
I can reproduce this error message with bash 4.1.5(1); on a Debian
system. This is a warning output by getopts, as "?" is not in the list
of valid arguments (nor ":" is given as first element in the optstring,
to enable silent error reporting).
-- Lars
Email Gateway (Aug 18 2022 at 17:17):From: Makarius <makarius@sketis.net>
But you did get the usage, right? The error is a known feature, because
"?" is not an option.
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.
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.)
Makarius
Email Gateway (Aug 18 2022 at 17:17):From: Robert Lamar <rlamar@stetson.edu>
Thanks, but actually I realized that. (I had been getting around it by
using double-quotes: "-?".) I suppose that my point was, implicitly,
that it might be better to use a character which is never used as a
wildcard. For instance, '-h' is common for many commands in the Linux
userspace. I will acknowledge that if you are coming from the Windows
command shell, '-?' makes good sense.
Alternatively, Isabelle could use a scheme like certain version
control systems use: type "isabelle help" for general guidance and
"isabelle help TOOL" for guidance on the tool mentioned. (Subversion
is an example of such a system.)
Email Gateway (Aug 18 2022 at 17:17):From: Robert Lamar <rlamar@stetson.edu>
On Mon, Feb 14, 2011 at 10:11 AM, Makarius <makarius@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 ofisabelle 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
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
Email Gateway (Aug 18 2022 at 17:17):From: Robert Lamar <rlamar@stetson.edu>
On Mon, Feb 14, 2011 at 9:17 AM, Lars Noschinski <noschinl@in.tum.de> wrote:
On 13.02.2011 15:16, Makarius wrote:
On Thu, 10 Feb 2011, Robert Lamar wrote:
/scratch/usr/Isabelle2011/lib/Tools/usedir: illegal option -- ?
That is in bash. In my favored shell, zsh, the shell gives an error
because it thinks the ? is a wildcard.It is a wildcard, so you will get strange effects if you've got a file
named e.g. "-b" in your current directory ;)
Indeed! I was merely suggesting that it would be even better to use
a character that is not a wildcard. :c) I propos '-h', as it does
not seem to be used as an option by any of the tools.
I've seen this effect for the last time with tcsh, many many years ago.
I can reproduce this error message with bash 4.1.5(1); on a Debian
system. This is a warning output by getopts, as "?" is not in the list
of valid arguments (nor ":" is given as first element in the optstring,
to enable silent error reporting).
Very interesting. I had not dug quite that deeply. It looks to me
that appending '\?' to the lists of getopts options (for instance,
line 93 in lib/Tools/usedir) would make the error go away. Can you
see any problem with this?
Email Gateway (Aug 18 2022 at 17:17):From: Robert Lamar <rlamar@stetson.edu>
Thank you very much for these pointers. I will give them a closer look.
Last updated: Apr 20 2024 at 12:26 UTC