Re: [isabelle] Presenting theories without running a session



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

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






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