On Friday 23 Jan 2009 9:53 pm, Steven J. Ramsay wrote:
> It ends with:
>
> val it = () : unit
> +++ Compiled dtd048.sml: OK (Compilation Run Complete) +++
> Exception Fail * The database name has not been set
> [save_and_exit.36010] * raised

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:

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?

(Use Ctrl+D to exit the interaction system).

Regards,

Rob.


_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to