Steven,

Can you try it with the replacement for src/imp111.doc contained in the 
attachement. Run ./distclean to tidy up, then run ./configure as you did 
before then install using

PPENVDEBUG=y ./install

This should give us some more diagnostics in build.log. Look for 
lines beginning "Using PPDATABASENAME" and see if they give any clues. Let me 
know how you get on.

Regards,

Rob.



On Friday 23 Jan 2009 4:40 pm, Steven J. Ramsay wrote:
> 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

Attachment: src-imp111.tgz
Description: application/tgz

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

Reply via email to