Re: [isabelle] Isabelleʼs getsettings somehow broken
On Wed, 10 Feb 2016, Joachim Breitner wrote:
dashâs upstream (Erik Blake) says this is not a bug and POSIX conform:
http://www.mail-archive.com/dash at vger.kernel.org/msg01147.html
Maybe it is better to convince Debian maintainers to regain some sanity?
The testing of dash 0.5.8 has happened only last week:
I don't mind people inventing strange shells. I do mind if they make that
/bin/sh and pretend that they have the real thing (at version 0.5.x).
I've spent some years on variations on all that already, refining it overÂ
and over again.
Isabelle exclusively uses bash wherever possible. Sometimes other systemÂ
function sneak-in unreliable /bin/sh.
In my naivety, I would immediately scold such code: Really, one should
not use the system-family of calls that needlessly go via a shell, with
all the worrying quoting involved. But, judging from a very brief web
search (http://sml-family.org/Basis/os-process.html), it seems that SML
does not provide the safe form taking a list of arguments, instead of a
single string, that I have seen in most other languages. Is there really
no way of executing a program from SML that does not go via the shell?
It is not just Poly/ML (or SML/NJ) but also the Java runtime.
I need to correct myself: I am working on the problem for decades,
starting about 1996.
The intersection of all these platforms and programs is a null-set. The
current solution is as stable as I can currently imagine -- the peak of
stability in Isabelle history so far. It certainly cannot be changed
within a few days for Isabelle2016.
In the worst case, I will just add to
http://isabelle.in.tum.de/installation.html another entry like "Linux /
Requirements: A version of /bin/sh that works".
This archive was generated by a fusion of
Pipermail (Mailman edition) and