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

Interesting.

Maybe it is better to convince Debian maintainers to regain some sanity? The testing of dash 0.5.8 has happened only last week: https://tracker.debian.org/news/744916

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


	Makarius


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