Ops, I forgot to reply to all...
Here follows the extract of imp048.err: val it = () : unit val it = () : unit === ProofPower 2.8.1a10 [HOL Database] === Copyright (C) Lemma 1 Ltd. 2000-2008 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) +++ Artur 2008/12/19 Philip Clayton <pclay...@taz.qinetiq.com> > Artur Oliveira Gomes wrote: > >> Hi there, >> >> I'm trying to install the latest of ProofPower 2.8.1a10, but I got some >> problems. >> The last lines of build.log that I got is: >> >> ... >> docsml -f hol.svf imp048 >> Compiling (code) imp048.sml >> pp: "pp-ml /home/artur/Proofpower/OpenProofPower-2.8.1a10/src/zed.polydb" >> exited with status 1 >> make[1]: *** [imp048.ldd] Error 1 >> make[1]: Leaving directory >> `/home/artur/Proofpower/OpenProofPower-2.8.1a10/src' >> make: *** [zed_build] Error 2 >> >> Is this extract enough to see what is going on? >> > Hi Artur, > > The actual error will probably be in 'src/imp048.err'. > > Phil > > > 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://www.qinetiq.com/home/notices/legal.html > -- Artur Oliveira Gomes
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
