Re: [ProofPower] help
On Wednesday 20 Oct 2010 10:14, Roger Bishop Jones wrote: ... > If you want to run through usr023_slides.doc, then do it > using the database "zed". > > xpp -f $PPHOME/doc/usr023_slides.doc -d example_zed That should have been: xpp -f $PPHOME/doc/usr023_slides.doc -d zed Roger Jones ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] help
On Tuesday 19 Oct 2010 23:13, Igorj V wrote: > this document is usefull > > usr011.pdf ProofPower Z Tutorial > > because i am trying to strugle with Z specification > language opening excercises Note that in usr011.pdf it says: (section 0.5 - Prerequisites) "We assume a working knowledge of Use of ProofPower as used for specification and proof in HOL" You may be OK going straight to proof in Z, but the Z tutorials are not written with that in mind, and assume that you have already done the HOL tutorials. (section 0.6 - How to use this tutorial) "you will find some of the material [in usr023.doc] will be rejected because definitions have already been made in this database. Alternatively you can work from a clean database (but then you may find problems if you miss out any of the material)." The database "example_zed" is the result of running the script usr023.doc. It is suitable for doing the exercises but if you try to reload the whole of usr023_slides.doc then you will get many failures because of actions which have already been done. To do the exercises in usr011 you should work from the file usr011X.doc, and produce something like usr011S.doc (which is a set of solutions to the exercises). If you want to run through usr023_slides.doc, then do it using the database "zed". xpp -f $PPHOME/doc/usr023_slides.doc -d example_zed Roger Jones ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] help
On Monday 18 Oct 2010 23:17, Igorj V wrote: > hello > after one year break i am trying to make some theory ; > (it is for university course ; ) > now reading proofpower_tutorial.pdf I'm not aware that there is such a document! The tutorial documents are: usr004.pdf ProofPower Tutorial usr011.pdf ProofPower Z Tutorial usr013.pdf ProofPower HOL Tutorial Notes usr022.pdf ProofPower Tutorial Transparencies Each of these documents contains material explaining how to use the tutorial: usr004 section 1 usr011 section 0.6 usr013 section 1 There are also instructions in usr022 which are intended for course students on machines which have been set up for the course, and so may not work on your machine. However, section 0.6 of usr013 says something about working through the course material. > one thing which i do not understand when opening example > from directory /opt/pp/doc/ from xpp how to lauch > something to prove?! when using pp -d demo i managed to > enter some simple examples (Peanissimo) Try following the instructions in section 0.6 of usr013 and let me know if you have a problem with that. Roger Jones ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] help
hello after one year break i am trying to make some theory ; (it is for university course ; ) now reading proofpower_tutorial.pdf one thing which i do not understand when opening example from directory /opt/pp/doc/ from xpp how to lauch something to prove?! when using pp -d demo i managed to enter some simple examples (Peanissimo) Igorj ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] help
Igor, The various tutorial manuals are the best place to start. Regards, Rob. On 19 Nov 2009, at 18:41, Igorj V wrote: > it seems after computer reboot error disappeared; > i have one training task to write a specification in Z language about course > register in university; also with a) ; b) additional tasks on proofpower; > just no idea what to read first from documentation on proofpower ?! > > 2009/11/18 Rob Arthan > Igorj, > > Can you try running it like this to give some more diagnostic output: > > PPENVDEBUG=y ../bin/pp_make_database -p hol demo > > Regards, > > Rob. > > On 18 Nov 2009, at 13:18, Igorj V wrote: > > > command pp_make_database -p hol receives such error ; what is missing?! > > > > ig...@igorj-laptop:/opt/pp/db$ ../bin/pp_make_database -p hol demo > > ../bin/pp_make_database: line 157: findfile: command not found > > ../bin/pp_make_database: line 158: findfile: command not found > > pp_make_database: database hol.polydb not found > > ig...@igorj-laptop:/opt/pp/db$ > > > > ___ > > Proofpower mailing list > > Proofpower@lemma-one.com > > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > > ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] help
Igorj, Can you try running it like this to give some more diagnostic output: PPENVDEBUG=y ../bin/pp_make_database -p hol demo Regards, Rob. On 18 Nov 2009, at 13:18, Igorj V wrote: > command pp_make_database -p hol receives such error ; what is missing?! > > ig...@igorj-laptop:/opt/pp/db$ ../bin/pp_make_database -p hol demo > ../bin/pp_make_database: line 157: findfile: command not found > ../bin/pp_make_database: line 158: findfile: command not found > pp_make_database: database hol.polydb not found > ig...@igorj-laptop:/opt/pp/db$ > > ___ > Proofpower mailing list > Proofpower@lemma-one.com > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] help
command pp_make_database -p hol receives such error ; what is missing?! ig...@igorj-laptop:/opt/pp/db$ ../bin/pp_make_database -p hol demo ../bin/pp_make_database: line 157: findfile: command not found ../bin/pp_make_database: line 158: findfile: command not found pp_make_database: database hol.polydb not found ig...@igorj-laptop:/opt/pp/db$ ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] help
Igor, You would need to use an old version (4.2) of Poly/ML for version 2.7.8 of ProofPower. Do you have a special reason for not using the latest version (2.8.1) of ProofPower? Regards, Rob. On 16 Nov 2009, at 19:44, Igorj V wrote: > when using polyML still some error; missing ML_dbase (tryed find -name > '*ML_dbase*') > > ig...@igorj-laptop:~/Desktop/OpenProofPower-2.7.8$ ./configure > Using /opt/pp as the installation target directory > Using Poly/ML > ERROR: The file "/usr/lib/poly/ML_dbase" does not exist > > > 2009/11/16 Rob Arthan > Igor, > > PS: the mailing list rejects posts with big attachments. If you need to send > a log file bigger than 30kb or so it is probably better to post an extract > first. In this case, the extract was all I needed to see. > > Regards, > > Rob. > > On 15 Nov 2009, at 18:32, Igorj V wrote: > >> thanx you are right; >> futher how to understand what is missing ?! >> >> file imp116.err contains (from programming languages am studing java ;) >> >> :1.278825 Error: overloaded variable not defined at type >> symbol: * >> type: INTEGER >> :1.278813 Error: overloaded variable not defined at type >> symbol: * >> type: INTEGER >> :1.279323 Error: overloaded variable not defined at type >> symbol: * >> type: INTEGER >> :1.279328 Error: overloaded variable not defined at type >> symbol: + >> type: INTEGER >> :1.279246 Error: overloaded variable not defined at type >> symbol: * >> type: INTEGER >> :1.280628 Error: overloaded variable not defined at type >> symbol: + >> type: INTEGER >> :1.280592 Error: overloaded variable not defined at type >> symbol: + >> type: INTEGER >> :1.280771 Error: overloaded variable not defined at type >> symbol: + >> type: INTEGER >> Exception+ (Exception: Error: Error) abandoning file imp116.sml at line 5682 >> *** (Exception: Stop: Stop) *** >> >> >> 2009/11/15 Rob Arthan >> >> On 14 Nov 2009, at 11:01, Igorj V wrote: >> >> > trying t install OpenProofPower-2.7.8 >> > appears some error >> > >> > how to read build.log file?! >> >> It is telling you that it failed while compiling file imp116.sml. The output >> from the compilation will be in the file src/imp116.err. Have a look at that. >> >> Regards, >> >> Rob. >> >> > ___ >> > Proofpower mailing list >> > Proofpower@lemma-one.com >> > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com >> >> >> > > > ___ > Proofpower mailing list > Proofpower@lemma-one.com > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] help
when using polyML still some error; missing ML_dbase (tryed find -name '*ML_dbase*') ig...@igorj-laptop:~/Desktop/OpenProofPower-2.7.8$ ./configure Using /opt/pp as the installation target directory Using Poly/ML ERROR: The file "/usr/lib/poly/ML_dbase" does not exist 2009/11/16 Rob Arthan > Igor, > > PS: the mailing list rejects posts with big attachments. If you need to > send a log file bigger than 30kb or so it is probably better to post an > extract first. In this case, the extract was all I needed to see. > > Regards, > > Rob. > > On 15 Nov 2009, at 18:32, Igorj V wrote: > > thanx you are right; > futher how to understand what is missing ?! > > file imp116.err contains (from programming languages am studing java ;) > > :1.278825 Error: overloaded variable not defined at type > symbol: * > type: INTEGER > :1.278813 Error: overloaded variable not defined at type > symbol: * > type: INTEGER > :1.279323 Error: overloaded variable not defined at type > symbol: * > type: INTEGER > :1.279328 Error: overloaded variable not defined at type > symbol: + > type: INTEGER > :1.279246 Error: overloaded variable not defined at type > symbol: * > type: INTEGER > :1.280628 Error: overloaded variable not defined at type > symbol: + > type: INTEGER > :1.280592 Error: overloaded variable not defined at type > symbol: + > type: INTEGER > :1.280771 Error: overloaded variable not defined at type > symbol: + > type: INTEGER > Exception+ (Exception: Error: Error) abandoning file imp116.sml at line > 5682 > *** (Exception: Stop: Stop) *** > > > 2009/11/15 Rob Arthan > >> >> On 14 Nov 2009, at 11:01, Igorj V wrote: >> >> > trying t install OpenProofPower-2.7.8 >> > appears some error >> > >> > how to read build.log file?! >> >> It is telling you that it failed while compiling file imp116.sml. The >> output from the compilation will be in the file src/imp116.err. Have a look >> at that. >> >> Regards, >> >> Rob. >> >> > ___ >> > Proofpower mailing list >> > Proofpower@lemma-one.com >> > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com >> >> > > > > ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] help
Igor, It looks like an incompatibility with SML/NJ has slipped through. I will correct this and supply a patch. In the mean time, I strongly recommend you to use Poly/ML rather than SML/NJ if you can. Poly/ML is much faster and uses a lot less memory than SML/NJ. It is also better supported these days. Regards, Rob. On 15 Nov 2009, at 18:32, Igorj V wrote: > thanx you are right; > futher how to understand what is missing ?! > > file imp116.err contains (from programming languages am studing java ;) > > :1.278825 Error: overloaded variable not defined at type > symbol: * > type: INTEGER > :1.278813 Error: overloaded variable not defined at type > symbol: * > type: INTEGER > :1.279323 Error: overloaded variable not defined at type > symbol: * > type: INTEGER > :1.279328 Error: overloaded variable not defined at type > symbol: + > type: INTEGER > :1.279246 Error: overloaded variable not defined at type > symbol: * > type: INTEGER > :1.280628 Error: overloaded variable not defined at type > symbol: + > type: INTEGER > :1.280592 Error: overloaded variable not defined at type > symbol: + > type: INTEGER > :1.280771 Error: overloaded variable not defined at type > symbol: + > type: INTEGER > Exception+ (Exception: Error: Error) abandoning file imp116.sml at line 5682 > *** (Exception: Stop: Stop) *** > > > 2009/11/15 Rob Arthan > > On 14 Nov 2009, at 11:01, Igorj V wrote: > > > trying t install OpenProofPower-2.7.8 > > appears some error > > > > how to read build.log file?! > > It is telling you that it failed while compiling file imp116.sml. The output > from the compilation will be in the file src/imp116.err. Have a look at that. > > Regards, > > Rob. > > > ___ > > Proofpower mailing list > > Proofpower@lemma-one.com > > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > > > ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] help
On 14 Nov 2009, at 11:01, Igorj V wrote: > trying t install OpenProofPower-2.7.8 > appears some error > > how to read build.log file?! It is telling you that it failed while compiling file imp116.sml. The output from the compilation will be in the file src/imp116.err. Have a look at that. Regards, Rob. > ___ > Proofpower mailing list > Proofpower@lemma-one.com > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] help
trying t install OpenProofPower-2.7.8 appears some error how to read build.log file?! build.log Description: Binary data ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] help
-- Forwarded message -- From: Date: 2009/11/10 Subject: Re: [ProofPower] help To: v.ig...@gmail.com You are not allowed to post to this mailing list, and your message has been automatically rejected. If you think that your messages are being rejected in error, contact the mailing list owner at mailman-ow...@blueberry.trouble-free.net. -- Пересылаемое сообщение -- From: Igorj V To: Roger Bishop Jones , mail...@lemma-one.com Date: Tue, 10 Nov 2009 21:25:07 +0200 Subject: Re: [ProofPower] help thanks; still install failed ; log in attach; ig...@igorj-laptop:~/Desktop/OpenProofPower-2.8.1p2$ ./install OpenProofPower installation begins [Tue Nov 10 21:22:48 2009] ... Moving to build directory /home/igorj/Desktop/OpenProofPower-2.8.1p2/src Building pptex xpp hol zed See /home/igorj/Desktop/OpenProofPower-2.8.1p2/build.log for messages install: installation failed; see /home/igorj/Desktop/OpenProofPower-2.8.1p2/build.log for more details ig...@igorj-laptop:~/Desktop/OpenProofPower-2.8.1p2$ 2009/11/9 Roger Bishop Jones > On Monday 09 November 2009 19:48:04 Igorj V wrote: > > > may be some one could explain me such error when installing proofpower?! > > > > troff: fatal error: can't find macro file s > > I had that problem, and the question has been asked and answered. > The answer is in the archive here: > > http://lemma-one.com/pipermail/proofpower_lemma-one.com/2009- > October/000576.html<http://lemma-one.com/pipermail/proofpower_lemma-one.com/2009-%0AOctober/000576.html> > > Roger Jones > > ___ > Proofpower mailing list > Proofpower@lemma-one.com > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com > build.log Description: Binary data ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] help
On Monday 09 November 2009 19:48:04 Igorj V wrote: > may be some one could explain me such error when installing proofpower?! > > troff: fatal error: can't find macro file s I had that problem, and the question has been asked and answered. The answer is in the archive here: http://lemma-one.com/pipermail/proofpower_lemma-one.com/2009- October/000576.html Roger Jones ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] help
-- Пересылаемое сообщение -- From: Igorj V To: mail...@lemma-one.com Date: Sun, 8 Nov 2009 22:41:05 +0200 Subject: Fwd: asking for assistance about proofpower hallo ; how to register one post ?! trying to install proofpower receive some error below; (whom to ask for some assistance?!) -- Forwarded message -- From: Igorj V Date: 2009/11/4 Subject: Fwd: asking for assistance about proofpower To: proofpower@lemma-one.com hello; may be some one could explain me such error when installing proofpower?! troff: fatal error: can't find macro file s 0 ? make[1]: *** [help.h] Error 1 make[1]: Leaving directory `/home/igorj/Desktop/OpenProofPower-2.8.1p2/src' make: *** [xpp] Error 2 hallo found your contacts here http://www.lemma-one.com/pipermail/proofpower_lemma-one.com/2009-January/000491.html maybe you could help me ;) it is my first step in Hoara logic; in specification languages Z; object Z; about Z language task is to try something to proof ; ( some tasks were given ; or by hand or using some soft ) found this tool Proof Power (sounds greate ); our lecturer only mentioned this tool (without any experience); because i am weak in this theory so decided to try some attempts with proof power ; all day long trying to configure proof power on ubunut 8.10; whom could i ask for assistance ?! (some fatal error takes place when installing prooffpower ) ./configure goes smoothly (but latex ; tex installed old versions ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
