After following your instructions, the build does not progress any
further, the last output of build.log is:
Compiling (code) dtd048.sml
pp: PPHOME set by caller to /usr/local/pp
pp: PATH set by caller to /usr/local/src/OpenProofPower-2.8.1a10/src:/usr/bin:/u
sr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/local/src/OpenPr
oofPower-2.8.1a10/src:.
pp: PPDATABASEPATH set by caller to /usr/local/src/OpenProofPower-2.8.1a10/src
pp: PPCOMPILER set by caller to POLYML
pp: Using PPDATABASENAME /usr/local/src/OpenProofPower-2.8.1a10/src/zed
pp: Calling "echo let val reset_quiet = set_flag("subgoal_package_quiet",get_fla
g("subgoal_package_quiet")) handle Fail _ => false; val ok = HOLSystem.load_file
s ("dtd048.sml"::nil); val _ = false handle Fail _ => false; in if ok then if tr
ue then save_and_exit 0 else exit 0 else if false then save_and_exit 1 else exit
1 end; | PPDATABASENAME=/usr/local/src/OpenProofPower-2.8.1a10/src/zed eval pp-
ml "/usr/local/src/OpenProofPower-2.8.1a10/src/zed.polydb" 2>&1"
docsml -f hol.svf imp048
docsml: PPHOME set by caller to /usr/local/pp
docsml: PATH set by caller to
/usr/local/src/OpenProofPower-2.8.1a10/src:/usr/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/local/src/OpenProofPower-2.8.1a10/src:.
docsml: PPETCPATH set by caller to /usr/local/src/OpenProofPower-2.8.1a10/src
sieve: using keyword file sievekeyword
sieve: using keyword file hol.svf
sieve: using keyword file sievekeyword
sieve: using keyword file hol.svf
Compiling (code) imp048.sml
pp: PPHOME set by caller to /usr/local/pp
pp: PATH set by caller to
/usr/local/src/OpenProofPower-2.8.1a10/src:/usr/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/local/src/OpenProofPower-2.8.1a10/src:.
pp: PPDATABASEPATH set by caller to /usr/local/src/OpenProofPower-2.8.1a10/src
pp: PPCOMPILER set by caller to POLYML
pp: Using PPDATABASENAME /usr/local/src/OpenProofPower-2.8.1a10/src/zed
pp: Calling "echo let val reset_quiet =
set_flag("subgoal_package_quiet",get_flag("subgoal_package_quiet"))
handle Fail _ => false; val ok = HOLSystem.load_files
("imp048.sml"::nil); val _ = false handle Fail _ => false; in if ok
then if true then save_and_exit 0 else exit 0 else if false then
save_and_exit 1 else exit 1 end; |
PPDATABASENAME=/usr/local/src/OpenProofPower-2.8.1a10/src/zed eval
pp-ml "/usr/local/src/OpenProofPower-2.8.1a10/src/zed.polydb" 2>&1"
pp: "pp-ml /usr/local/src/OpenProofPower-2.8.1a10/src/zed.polydb"
exited with status 1
make[1]: *** [imp048.ldd] Error 1
make[1]: Leaving directory `/usr/local/src/OpenProofPower-2.8.1a10/src'
make: *** [zed_build] Error 2
The contents of imp048.err is the same.
Would you like to see any other output? It may or may not be helpful
to know that my poly is not installed into the default location, I had
to set PPPOLYHOME; but otherwise I think everything is fairly
standard.
Best,
Steven
2009/1/23 Rob Arthan <r...@lemma-one.com>:
> 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
>
--
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
