Dear list,

I have the same problem as Artur.  The machine that I am trying to
install to has never had a pp installation on it as far as I can
remember.

The first lines of pp read:

#! /bin/sh
#       pp   From: imp111.doc,v 1.57 2008/07/24 15:55:01 rda Exp %Z%
#
# Shell script to start a ProofPower session


To recap, imp048.err reads:

val it = () : unit
val it = () : unit
=== ProofPower 2.8.1a10 [HOL Database]
=== Copyright (C) Lemma 1 Ltd. 2000-2009
Database name:
:) Error-Signature (ZTypesAndTermsSupport) has not been declared   Found near
ZTypesAndTermsSupport
Exception Fail: Fail "Static errors (pass2)" raised abandoning file imp048.sml
 at line 521
+++ Compiled imp048.sml: Failed (Compilation Run Complete) +++


Any ideas?

Best,

Steven

2008/12/30 Rob Arthan <r...@lemma-one.com>:
> Artur,
>
> On Tuesday 23 Dec 2008 8:40 am, Artur Oliveira Gomes wrote:
>> Rob,
>>
>> This strongly suggests that you are somehow picking up an earlier version
>> of
>>
>> > the pp script. You are using the "./configure; ./install" sequence to run
>> > the
>> > installation aren't you?
>
> I take it that the answer is yes? I.e., you are using ./configure and
> ./install to run the installation.
>
>>> If so, you could try the replacement for
>> > src/zed.mkf
>> > that I have attached. Please compare it with what the file src/zed.mkf
>> > that you already have, the only difference is that this one calls "./pp"
>> > rather than "pp" - but that shouldn't be necessary because install puts
>> > the src directory at the top of the search path.
>>
>> It continues outputing the same things than before. I have compared the
>> output
>> before and after the replacement, it is the same. Looks like that the
>> replaced
>> file is not even readed by the script, or, the changes are not enough to
>> fix the problem.
>
> Thanks for persevering.  I wanted to make sure that the script pp was being
> picked up from the right place. There should be a version number and some
> other red tape in the first few lines of src/pp. It should look like this for
> version 2.8.1a10:
>
> #! /bin/sh
> #       pp   From: imp111.doc,v 1.57 2008/07/24 15:55:01 rda Exp %Z%
> #
>
> Is that what you have? If not let me know what you have got. If so, then I
> suggest you try again after doing ./distclean to tidy up. If it still fails,
> I will need to send you a modified version of imp111.doc to get some more
> diagnostic output.
>
> Regards,
>
> Rob.
>
>
>
>
>
> _______________________________________________
> Proofpower mailing list
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
>



-- 
Steven Ramsay
Research Student
Oxford University Computing Laboratory

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

Reply via email to