Re: [isabelle] Isabelle2016-RC5 available
On Tue, 16 Feb 2016, Gerwin Klein wrote:
On 13.02.2016, at 05:36, Makarius <makarius at sketis.net> wrote:
Isabelle2016-RC5 is now available for regular use in anticipation of official Isabelle2016:[
- Poly/ML: hardwired bash in OS.Process.system to help
Debian-testing-unstable with exported shell functions
Just wanted to confirm that this has avoided the problem in our setup as
Can you say where the bad dash-0.5.8 in your setup is coming from? So far
my impression it that only Debian-testing uses that.
We had some additional dash breakage in Makefiles that were using
"isabelle envâ, and the same change of âSHELL=bashâ works there as well.
The "make" tool is indeed another canonical source for /bin/sh
invocations. Even though "make" is obsolete for Isabelle, the concept of
the Isabelle process environment should allow going through /bin/sh, and
just avoiding that is no proper solution in the long term.
I have already plenty of ideas to make it once again more robust -- like
I've done several times in the past 1-2 decades. Nonetheless, it is sad
that Unix or POSIX has become such a fragile and hostile programming
environment. Windows is easier to tame in that respect, because we simply
ship a single well-defined version of Cygwin for the POSIX glue.
This archive was generated by a fusion of
Pipermail (Mailman edition) and