Email Gateway (Aug 22 2022 at 12:38): Email Gateway (Aug 22 2022 at 12:38):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
Isabelle2016-RC5 is now available for regular use in anticipation of
official Isabelle2016:
http://isabelle.in.tum.de/website-Isabelle2016-RC5
This corresponds to the repository versions
https://bitbucket.org/isabelle_project/isabelle-release/commits/Isabelle2016-RC5
and https://bitbucket.org/isa-afp/afp-devel/commits/7a23f634aef3
Notable changes:
- isar-ref: more material on Isar language updates
- Poly/ML: hardwired bash in OS.Process.system to help
Debian-testing-unstable with exported shell functions
After 6 weeks of testing by reletively few people, very few problems have
been exposed. This is the last chance to point out problems, before
Isabelle2016 becomes final next week.
People who have used earlier release candidates should upgrade now. Local
settings can be preserved by copying $ISABELLE_HOME_USER in a suitable
manner: renaming the last component of the directory name to
Isabelle2016-RC5 before starting the new version.
When discussing problems, observations, suggestions, etc. the mail subject
line should be changed to something informative (but the release candidate
number still given in the message body).
Makarius
Email Gateway (Aug 22 2022 at 12:39):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
On 13.02.2016, at 05:36, Makarius <makarius@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 well.
We had some additional dash breakage in Makefiles that were using "isabelle env”, and the same change of “SHELL=bash” works there as well.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 12:39):From: Makarius <makarius@sketis.net>
On Tue, 16 Feb 2016, Gerwin Klein wrote:
On 13.02.2016, at 05:36, Makarius <makarius@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 functionsJust wanted to confirm that this has avoided the problem in our setup as
well.
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.
Makarius
Email Gateway (Aug 22 2022 at 12:39):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
On 16 Feb 2016, at 21:42, Makarius <makarius@sketis.net> wrote:
On Tue, 16 Feb 2016, Gerwin Klein wrote:
On 13.02.2016, at 05:36, Makarius <makarius@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 functionsJust wanted to confirm that this has avoided the problem in our setup as well.
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.
The main (surprising) case happened to be a manual dash update on Ubuntu. Not something you’d currently encounter by default, but potentially an issue in the next few Ubuntu releases.
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.
Indeed.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Apr 19 2024 at 04:17 UTC