Many thanks to Phil for this. I will try to devise a work-around for this bizarre behaviour of dash, which seems to be based on a misreading of the POSIX standard as far as I can see.



On 26 Jan 2009, at 16:25, Philip Clayton wrote:

We reproduced the same problem with Ubuntu 8.10 (Intrepid Ibex) on Paul's machine.

Thanks to Paul Whittaker who pointed out that, on Ubuntu, /bin/sh points to dash (a faster more cut-down POSIX-compliant shell) rather than bash, otherwise I could have wasted a fair bit of time debugging in the wrong shell! (This has been the case since Ubuntu 6.1, release in 2006.) Indeed this difference causes the difference in behaviour because particular lines in the pp script (possibly other scripts) are interpreted differently.

The problem is due to the use of the shell built-in eval on lines 222 and 225. Basically, in bash, the environment variable PPDATABASENAME is passed through by eval to its command but in dash it is not. Try the following commands on e.g. Fedora and Ubuntu:

 echo "#! /bin/sh" > echox
 echo "echo \$X" >> echox
 X=hello eval echox

On Fedora (where /bin/sh points to bash) you get 'hello' echoed back but on Ubuntu (where /bin/sh points to dash) you get nothing echoed back. I don't know what the correct semantics is.

One option is to do the equivalent of

 eval X=hello echox

which appears to give the same on each system.


Steven J. Ramsay wrote:
No problem.  I am on an old Pentium M processor (i.e. x86), with 1GB
of RAM.  The OS is Ubuntu 8.04 (Hardy Heron).



2009/1/24 Rob Arthan <>:


Thanks for that. What operating system and hardware are you running on?



On 24 Jan 2009, at 17:24, Steven J. Ramsay wrote:

2009/1/24 Rob Arthan <>:

What do the first few lines lok like? I expect they look something like:

val it = () : unit
val it = () : unit
=== ProofPower 2.8.1a10 [HOL Database]
=== Copyright (C) Lemma 1 Ltd. 2000-2008
Database name:

I.e., no database name (this is what Artur was seeing). Can you try the
following command after the failed build:

Yes, the first lines are the same (except the copyright is 2000-2009).

TESTVAR="testing" ./src/pp-ml ./src/zed.polydb

This should start an interactive session on your as yet incomplete zed
database. You should see something like this

val it = () : unit
val it = () : unit
=== ProofPower 2.8.1a10 [HOL/Z Database]
=== Copyright (C) Lemma 1 Ltd. 2000-2009
Database name:

In response to the ":)" prompt try:

get_shell_var "TESTVAR" ;

I get:

val it = "testing" : string

Now try:

OS.Process.getEnv "TESTVAR" ;

I get:

val it = SOME "testing" : string Option.option

Does this work the same for you?

Yes, all those tests delivered the same results.



Steven Ramsay
Research Student
Oxford University Computing Laboratory

Proofpower mailing list

The information contained in this E-Mail and any subsequent correspondence is private and is intended solely for the intended recipient(s). The information in this communication may be confidential and/or legally privileged. Nothing in this e-mail is intended to conclude a contract on behalf of QinetiQ or make QinetiQ subject to any other legally binding commitments, unless the e-mail contains an express statement to the contrary or incorporates a formal Purchase Order.

For those other than the recipient any disclosure, copying, distribution, or any action taken or omitted to be taken in reliance on such information is prohibited and may be unlawful.

Emails and other electronic communication with QinetiQ may be monitored and recorded for business purposes including security, audit and archival purposes. Any response to this email indicates consent to this.

Telephone calls to QinetiQ may be monitored or recorded for quality control, security and other business purposes.

QinetiQ Limited
Registered in England & Wales: Company Number:3796233
Registered office: 85 Buckingham Gate, London SW1E 6PD, United Kingdom
Trading address: Cody Technology Park, Cody Building, Ively Road, Farnborough, Hampshire, GU14 0LX, United Kingdom http://

Proofpower mailing list

Reply via email to