Email Gateway (Aug 19 2022 at 11:56): Email Gateway (Aug 19 2022 at 11:56):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Developers,
a tiny remark, in the help-message of the components tool:
$ isabelle components -?
Usage: isabelle components [OPTIONS] [COMPONENTS ...]
Options are:
-I init user settings
-R URL component repository (default
$ISABELLE_COMPONENT_REPOSITORY)
-a all missing components
-l list status
Resolve Isabelle components via download and installation.
COMPONENTS are identified via base name.
ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"
"download all missing components" or something similar might be more
descriptive for the "-a" flag.
cheers
chris
Email Gateway (Aug 19 2022 at 11:56):From: Tjark Weber <webertj@in.tum.de>
Another tiny remark about help messages (and I may have raised this
before): I think it is unfortunate that the various Isabelle tools
complain about -? with, e.g.,
.../isabelle/lib/Tools/components: illegal option -- ?
Best,
Tjark
Email Gateway (Aug 19 2022 at 11:56):From: Christian Sternagel <c.sternagel@gmail.com>
You are not the only one ;), see for example (the latter part of) this
thread
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-February/msg00082.html
cheers
chris
Email Gateway (Aug 19 2022 at 11:56):From: Christian Sternagel <c.sternagel@gmail.com>
Since there are some blind alleys when staring from the message in the
above link, here is a more precise location:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-February/msg00090.html
Email Gateway (Aug 19 2022 at 11:56):From: Makarius <makarius@sketis.net>
I've tuned this a bit in Isabelle/2220f0fb5581.
The changeset also reveals that there is some documentation in the system
manual, even though the tool is mostly for administrative purposes --
actual users of Isabelle get a bundle with all components included.
Makarius
Email Gateway (Aug 19 2022 at 11:57):From: Makarius <makarius@sketis.net>
Can you say what is unfortunate here? By provoking a command line error
the tools print the "usage"; there is no explicit help option. This
should work uniformly for all Isabelle tools without special surprises.
When I worked out that scheme many years ago I was looking around how
Unix-oid tools usually do the help, with the main observation that there
are no standards for that, even until today.
So when I have an unknown Unix tool I feed variations of -? -h -help
--help to it to get some feedback, hoping that none of these options mean
"delete all files in the home directory".
Makarius
Email Gateway (Aug 19 2022 at 11:57):From: Tjark Weber <webertj@in.tum.de>
This is the special surprise. I do expect an explicit help option that
prints the usage message and is not considered an "illegal option."
Best,
Tjark
Email Gateway (Aug 19 2022 at 11:57):From: Makarius <makarius@sketis.net>
Digging up these old threads means I don't have to repeat everything
again. The initial confusion by these guys was caused by using odd
shells. Non-portable shells cause endless problems in the Unix-oid world,
and the "standard" /bin/sh is particularly non-portable. This is why
Isabelle has standardized on GNU bash a long time ago.
I've recently considered one more step in reducing the potential of
confusion: the Prover IDE could include some Isabelle system sub-plugin
for the jEdit Console. That would provide bash and only bash on all
platforms, including Windows. (De-facto there are more problems by users
on Mac OS X and Windows not knowing how to start a terminal, than by Linux
users with odd shells.)
Makarius
Email Gateway (Aug 19 2022 at 11:57):From: Makarius <makarius@sketis.net>
OK, so that is just a canonical case of changing the user expectation.
Makarius
Last updated: Apr 19 2024 at 04:17 UTC