Re: [ProofPower] Proofpower Digest, Vol 120, Issue 1

David, > On 25 Mar 2020, at 17:18, David Topham wrote: > > Rob, I got this, but I had 3 previous posts to mailing list that didn't make > it. > Were they inappropriate? Or lost? -Dave They must have got lost. Please do try to resend them. Regards, Rob. > > On Wed, Mar 25, 2020 at 9:00 AM

Re: [ProofPower] Proofpower Digest, Vol 120, Issue 1

Rob, I got this, but I had 3 previous posts to mailing list that didn't make it. Were they inappropriate? Or lost? -Dave On Wed, Mar 25, 2020 at 9:00 AM wrote: > Send Proofpower mailing list submissions to > proofpower@lemma-one.com > > To subscribe or unsubscribe via the World Wide Web,

Re: [ProofPower] Proofpower Digest, Vol 119, Issue 1

David, > On 1 Nov 2019, at 16:13, David Topham wrote: > > Ok, I can work within integers for awhile! I was trying to use the general > form of the geometric progression that may involve fractions, but I can > explore whole numbers more first. As an aside from what Roger has been trying to he

Re: [ProofPower] Proofpower Digest, Vol 119, Issue 1

David, On 01/11/2019 16:13, David Topham wrote: Ok, I can work within integers for awhile!  I was trying to use the general form of the geometric progression that may involve fractions, but I can explore whole numbers more first.  I see the "induction_thm" won't work with R anyway since it has

Re: [ProofPower] Proofpower Digest, Vol 119, Issue 1

Ok, I can work within integers for awhile! I was trying to use the general form of the geometric progression that may involve fractions, but I can explore whole numbers more first. I see the "induction_thm" won't work with R anyway since it has the base case as 0 and SML would expect 0.0 there fo

Re: [ProofPower] ProofPower and Discrete Math

David, On 28/10/2019 02:39, David Topham wrote: Hello Rob,Roger, et al. Hope you are doing well. I am still trying to apply ProofPower to forward proofs. Glad to hear that. I am working on proof by induction and came across this: induction_thm In the notes, there is an intriguing statement t

Re: [ProofPower] ProofPower output

Got it, thanks! On Fri, Feb 15, 2019 at 10:39 AM Rob Arthan wrote: > Dave, > > It's done using: > > =GFT ProofPower output > > "=GFT" stands for something like "General Formal Text". The text on the > GFT line is used for the label and the lines coming after a GFT directive > are > just formatte

Re: [ProofPower] ProofPower output

Dave, It's done using: =GFT ProofPower output "=GFT" stands for something like "General Formal Text". The text on the GFT line is used for the label and the lines coming after a GFT directive are just formatted like formal text in theLaTeX document, but not included by docsml. I would typically

[ProofPower] ProofPower output

I was reading an article by Rob Arthan about ProofPower Z and notice that the document shows SML input followed by ProofPower output. I have not seen how to automatically create that using xpp. e.g. I know that =SML produces the first label using doctex, but what produces the "ProofPower output" la

Re: [ProofPower] ProofPower and Discrete Math

> David, Good to hear you are still moving forward. If the transformation you seek is a propositional tautology, the following general prescription should work. 1. Formulate the transformation as an equivalence using propositional (Boolean) variables, with the starting point on the left of the

Re: [ProofPower] Proofpower Digest, Vol 110, Issue 4

Rob, Yes that little extra did it! Thanks for your help with this :) Steve > On 5/03/2017, at 6:00 AM, proofpower-requ...@lemma-one.com wrote: > > Send Proofpower mailing list submissions to > proofpower@lemma-one.com > > To subscribe or unsubscribe via the World Wide Web, visit >

Re: [ProofPower] ProofPower and Discrete Math

Roger, Thank you so much! I had not come across rewrite_rule in my reading. It works exactly as I need. -Dave On Tue, Feb 7, 2017 at 5:01 AM, Roger Bishop Jones wrote: > David, > > Of course, how to make a rule depends on what rule you are trying to make. > > ¬_∨_thm is an equivalence, i.e. a b

Re: [ProofPower] ProofPower and Discrete Math

David, Of course, how to make a rule depends on what rule you are trying to make. ¬_∨_thm is an equivalence, i.e. a boolean equation, and the most common way of using equations is by rewriting. If you are doing forward proof then you can rewrite using rewrite_rule, so to use this theorem you m

Re: [ProofPower] ProofPower and Discrete Math

I have made some more progress in applying ProofPower to forward proofs in discrete math. e.g. I can prove DeMorgan's theorem successful (propositional calculus). I would like to use the newly proved theorem in other proofs now. What is the best strategy to do that? Is it to create an SML functi

Re: [ProofPower] ProofPower and Discrete Math

Thank you both (Rob and Roger) for your "above and beyond the call of duty" help in getting me through my attempts to approach using ProofPower to teach Discrete Math. I understand your comments that backward proof is more economical than forward proof. Yet, I don't think the students will learn ho

Re: [ProofPower] ProofPower and Discrete Math

David, I endorse what Roger said about forward v. backwards proof. There is definitely a tension between teaching proof theory and teaching practical mechanised proof. For the record, the problem was that you had the two theorem arguments of ∃_elim the wrong way round and you seemed to have misun

Re: [ProofPower] ProofPower and Discrete Math

David, There is a reason why the ProofPower tutorials don't say much about the forward proof tools you are trying to use. I have given courses on ProofPower HOL and on ProofPower Z and wrote the tutorials. What I did in the courses was to teach just enough about forward proof for the students

Re: [ProofPower] ProofPower and Discrete Math

Since the slides for this book use slightly different notation, I am back to trying to implement the proofs in the main book: UsingZ from www.usingz.com (in text link, it is zedbook) On page 42, the proof is using nested existentials, and I am trying to get past my lack of understanding in apply

Re: [ProofPower] ProofPower and Discrete Math

On 14/08/2016 08:44, David Topham wrote: Thanks Roger, I am using slides he distributes. He has false introduction rules starting on page 24 (attached). Sorry about my poor example, please ignore that since is a confused use of this technique anyway! -Dave Looks like he changed the name.

Re: [ProofPower] ProofPower and Discrete Math

David, I don't quite understand what you are trying to do here. On the face of it you want a rule: p -- false-intro false But this is not possible, because it is not sound. As far as I can see Woodcock does not have a false-intro rule, he has only a false-elim rule, is that what you

Re: [ProofPower] ProofPower on Ubuntu 16.04

Roger, Yes, thanks: there was a typo in my list of packages: I actually used: libmotif-dev polyml libpolyml-dev texlive-latex-recommended I expect texlive-generic-recommended would do too. Regards, Rob. > On 23 Jul 2016, at 08:14, Roger Bishop Jones wrote: >

Re: [ProofPower] ProofPower on Ubuntu 16.04

Thanks Rob for sorting this out for me. I now have ProofPower running on Ubuntu 16.04 (under VirtualBox on my macbook). (also under OS X, but I have other things which I can't get to work on OS X). 16.04 works on the 12" macbook under VirtualBox but not native, though it will boot from a flash

Re: [ProofPower] ProofPower on Ubuntu 16.04

Roger, I have now had time to build ProofPower on ubuntu 16.04. I needed to do the following: 1) Install the following packages: libmotif-dev poly libpoly-dev texlive-recommended 2) Change configure so that it doesn’t fail if libpolymain is in a subdirectory of

Re: [ProofPower] ProofPower on Ubuntu 16.04

Roger, > On 18 Jul 2016, at 22:15, Roger Bishop Jones wrote: > > I have been trying to install ProofPower on Ubuntu 16.04, without success. > > The stumbling block comes early, in the prerequisites for installing > OpenMotif, since some of these are not available in the usual repositories. Do

[ProofPower] ProofPower on Ubuntu 16.04

I have been trying to install ProofPower on Ubuntu 16.04, without success. The stumbling block comes early, in the prerequisites for installing OpenMotif, since some of these are not available in the usual repositories. If anyone figures out how to get ProofPower installed on Ubuntu 16.04 I s

Re: [ProofPower] ProofPower build on OS X

Magic. Build complete. I just had to change the path. xpp seems to come up ok. Thanks, I’ll post a resume. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] ProofPower build on OS X

Roger, > On 30 Apr 2016, at 15:55, Roger Bishop Jones wrote: > > Rob, > > Now failing to find mkfontdir. > > PATH=/opt/local/bin:/opt/local/sbin:/usr/bin:/bin:/usr/sbin:/sbin:/Applications/Emacs.app/Contents/MacOS/bin-x86_64-10_9:/Applications/Emacs.app/Contents/MacOS/libexec-x86_64-10_9 > >

Re: [ProofPower] ProofPower build on OS X

Rob, Now failing to find mkfontdir. PATH=/opt/local/bin:/opt/local/sbin:/usr/bin:/bin:/usr/sbin:/sbin:/Applications/Emacs.app/Contents/MacOS/bin-x86_64-10_9:/Applications/Emacs.app/Contents/MacOS/libexec-x86_64-10_9 Am I missing something from the PATH or do I need to install something else? Ro

Re: [ProofPower] ProofPower build on OS X

Roger, > On 30 Apr 2016, at 10:43, Roger Bishop Jones wrote: > > Rob, > > Thanks for you continuing support. Not a problem. Thank you for persisting with this bit of the installation, because I have a bit of difficulty testing it on Mac OS in a clean environment. I will look into improving the

Re: [ProofPower] ProofPower build on OS X

Rob, Thanks for you continuing support. > On 30 Apr 2016, at 10:16, Rob Arthan wrote: > > ... > Try it in in src/dev. I think it will fail. If so, try it without the > obsolete options: > > polyc -o pp-ml pp-ml.o > Here are the results: bash-3.2$ polyc -segprot POLY rwx rwx -o pp-

Re: [ProofPower] ProofPower build on OS X

Roger, > On 29 Apr 2016, at 23:16, Roger Bishop Jones wrote: > > Rob, > >> On 29 Apr 2016, at 20:31, Rob Arthan wrote: >> >> >> The linker can’t find the gmp library. What version of Poly/ML are you >> using? Did you build >> it yourself or download it ready-made from somewhere? >> > > I

Re: [ProofPower] ProofPower build on OS X

Rob, > On 29 Apr 2016, at 20:31, Rob Arthan wrote: > > > The linker can’t find the gmp library. What version of Poly/ML are you using? > Did you build > it yourself or download it ready-made from somewhere? > I did: port install polymer poly -v gives Poly/ML 5.5.2 ReleaseRTS ve

Re: [ProofPower] ProofPower build on OS X

Roger, > On 29 Apr 2016, at 17:17, Roger Bishop Jones wrote: > > Rob, > > OK, so now I am through to the ProofPower build, which fails pretty fast, > just after compiling dtd108. > > Here’s the tail of the log: > > rm -f hol.polydb > Compiling dtd108.sml and imp108.sml > { { echo "val sy

[ProofPower] ProofPower build on OS X

Rob, OK, so now I am through to the ProofPower build, which fails pretty fast, just after compiling dtd108. Here’s the tail of the log: rm -f hol.polydb Compiling dtd108.sml and imp108.sml { { echo "val system_version : string = \"3.1w7\"; val build_date : Date.date = Date.fromTimeLocal(

Re: [ProofPower] ProofPower on OS X

> On 29 Apr 2016, at 10:24, Roger Bishop Jones wrote: > > > That seems to be necessary, but the port of openmotif nevertheless fails. > port complains that: > > xorg-libXt must be installed with +flat_namespace > I found the fix to that, so I am progressing, Will post an upgraded recipe if an

Re: [ProofPower] ProofPower on OS X

Thanks for your help so far Rob. > On 28 Apr 2016, at 22:01, Rob Arthan wrote: > >> I have managed to get Xcode installed now, > > Good. > >> but fail on step 2 of your prescription because the preferences in Xcode >> doesn’t seem to have a download option. > > I am not sure an analogue of t

Re: [ProofPower] ProofPower on OS X

Roger, > On 28 Apr 2016, at 21:32, Roger Bishop Jones wrote: > > >> On 28 Apr 2016, at 11:57, Rob Arthan wrote: >> >> >> Can you point me at the recipe, so I can see what is likely to be >> out of date. > > http://lemma-one.com/pipermail/proofpower_lemma-one.com/2012-December/000955.html >

Re: [ProofPower] ProofPower on OS X

> On 28 Apr 2016, at 11:57, Rob Arthan wrote: > > > Can you point me at the recipe, so I can see what is likely to be > out of date. http://lemma-one.com/pipermail/proofpower_lemma-one.com/2012-December/000955.html

[ProofPower] ProofPower on OS X

I would appreciate advice on how to run ProofPower on OS X El Capitain (10.11.4). I tried a rather dated recipe posted by Rob a while back but find that there is problem installing Xcode (it hangs up in the installation). If I have to resort to running Linux is VirtualBox the best way to do that

Re: [ProofPower] Proofpower Digest, Vol 91, Issue 10

0:35 +0100 From: Rob Arthan To: David Topham Cc: ProofPower List Subject: Re: [ProofPower] ProofPower (and xpp) is a great program! Message-ID: Content-Type: text/plain; charset="windows-1252" David, On 30 Mar 2015, at 06:05, David Topham wrote: > I know I am preaching to th

Re: [ProofPower] ProofPower (and xpp) is a great program!

David, On 30 Mar 2015, at 06:05, David Topham wrote: > I know I am preaching to the choir here, but I was so impressed by the > behavior of ProofPower today I thought I would go ahead and express my > appreciation anyway! > > I have been using xpp to prepare notes and exercises for my discre

Re: [ProofPower] ProofPower (and xpp) is a great program!

I had similar thoughts last week when having to use Gedit to prepare an email with Unicode characters. The X server gave up and there was no panic file... 30/03/15 06:05, David Topham wrote: I know I am preaching to the choir here, but I was so impressed by the behavior of ProofPower today I

[ProofPower] ProofPower (and xpp) is a great program!

I know I am preaching to the choir here, but I was so impressed by the behavior of ProofPower today I thought I would go ahead and express my appreciation anyway! I have been using xpp to prepare notes and exercises for my discrete math course this semester, and today after spending a couple of ho

Re: [ProofPower] ProofPower and Discrete Math

------ >> >> Message: 1 >> Date: Wed, 4 Feb 2015 12:49:47 -0800 >> From: David Topham >> To: Roger Bishop Jones >> Cc: ProofPower List >> Subject: Re: [ProofPower] ProofPower and Discrete Math &g

Re: [ProofPower] ProofPower PrettyPrinter

Rob, That works great! Thanks so much, Dave On Sun, Feb 22, 2015 at 9:08 AM, Rob Arthan wrote: > David, > > On 22 Feb 2015, at 16:47, David Topham wrote: > > I am trying to get a proof listing (of hypothetical syllogism) for > teaching purposes. > > Thanks to help from Roger, I have the proof w

Re: [ProofPower] ProofPower PrettyPrinter

David, On 22 Feb 2015, at 16:47, David Topham wrote: > I am trying to get a proof listing (of hypothetical syllogism) for teaching > purposes. > > Thanks to help from Roger, I have the proof working, but would like to use > PrettyPrinter to put each step of proof on different line. I almost h

Re: [ProofPower] ProofPower and Discrete Math

On 3 Feb 2015, at 21:16, Roger Bishop Jones wrote: > On 03/02/15 13:55, David Topham wrote: >> >> >> I am interested in using ProofPower to aid in the teaching of Discrete >> Math. I would like to assist the students in developing proofs using >> specific rules of inference. e.g. in the attach

Re: [ProofPower] ProofPower and Discrete Math

Roger, Thank you very much! This example got me past my mental block and I see how to work with these proofs much better now. I appreciate your time in helping me. Now I see one of my tasks is to map the names I use (such as hypothetical syllogism) to the names used within ProofPower (such as =>_tr

Re: [ProofPower] ProofPower and Discrete Math

On 03/02/15 13:55, David Topham wrote: > > > I am interested in using ProofPower to aid in the teaching of Discrete > Math. I would like to assist the students in developing proofs using > specific rules of inference. e.g. in the attached proof from our > textbook the proof uses Hypothetical Syllog

[ProofPower] ProofPower and Discrete Math

I am interested in using ProofPower to aid in the teaching of Discrete Math. I would like to assist the students in developing proofs using specific rules of inference. e.g. in the attached proof from our textbook the proof uses Hypothetical Syllogism to prove a Propositional expression. I don't qu

Re: [ProofPower] Proofpower Digest, Vol 88, Issue 8

Thank you Rob, I just tried this and it works perfectly! It is a testament to the quality of the design of ProofPower that it is so versatile and adaptable. I see you got QCheck to work too; It looks very promising to create unit tests easily. I hadn't known that you could choose to run different i

Re: [ProofPower] ProofPower build problems

David, On 21 Dec 2014, at 19:25, David Topham wrote: > Rob, I am really enjoying learning about ProofPower and so impressed at the > amount of documentation and extra facilities that I didn't even know were > part of this program. e.g. I have long been interested in "literate > programming"

Re: [ProofPower] ProofPower build problems

Rob, I am really enjoying learning about ProofPower and so impressed at the amount of documentation and extra facilities that I didn't even know were part of this program. e.g. I have long been interested in "literate programming" and find your approach using =SML and =TEX to be very efficient. I

[ProofPower] ProofPower build problems

Rob, Fantastic! That was the key! I reinstalled PolyML just to be sure and checked that poly and polyc worked OK, but still got same error building ProofPower. But I made the changes to the mkf (just xpp and hol, not zed) as you suggested and now it completed successfully. I had to install the st

Re: [ProofPower] ProofPower build problems (was, Re: GUI Interface (Motif))

David, > On 17 Dec 2014, at 00:19, David Topham wrote: > > Maybe another non-Posix issue? Attached is latest build attempt. This time > it fails > trying to build processes.cpp because pthread functions are undefined... > (setting OS=linux made progress, then I had to install mkfontdir utility

Re: [ProofPower] ProofPower build problems (was, Re: GUI Interface (Motif))

Maybe another non-Posix issue? Attached is latest build attempt. This time it fails trying to build processes.cpp because pthread functions are undefined... (setting OS=linux made progress, then I had to install mkfontdir utility and load the Xp libraries as well before getting to the current erro

Re: [ProofPower] ProofPower build problems (was, Re: GUI Interface (Motif))

David, On 16 Dec 2014, at 16:25, David Topham wrote: > Thanks for helping Rob, TinyCore does have uname, and that command returns > "Linux". > > It uses BusyBox for shell commands and a subset of dd is supported which does > not have the lcase option! > Ah! I try to make the ProofPower bui

Re: [ProofPower] ProofPower build problems (was, Re: GUI Interface (Motif))

Thanks for helping Rob, TinyCore does have uname, and that command returns "Linux". It uses BusyBox for shell commands and a subset of dd is supported which does not have the lcase option! (see attached) -Dave On Tue, Dec 16, 2014 at 2:02 AM, Rob Arthan wrote: > > David, > > > On 15 Dec 2014,

[ProofPower] ProofPower build problems (was, Re: GUI Interface (Motif))

David, > On 15 Dec 2014, at 23:43, David Topham wrote: > > It is version 2.9.1w8... and here is the latest attempt (attached). > > > I notice that SOLARIS is on the compile line which is not true..should be > LINUX perhaps? > but how do I influence that? The relevant makefile (src/xpp.mkf)

[ProofPower] ProofPower source on GitHub

Dear All, I am happy to announce that I have now ported the ProofPower source from RCS to git. The source is available on GitHub. The URL is: http://github.com/RobArthan/pp This seemed like a timely moment to include PPDaz in the open source offering. So ProofPower and OpenProofPower ar

Re: [ProofPower] proofpower

Sarah, Why do you keep repeating your questions? If you do not understand the replies that Phil Clayton or Roger Jones provided then respond to their posts and make sure you copy your replies to the mailing list. Also, you have been trying to make a post with a screenshot attached. Please do n

[ProofPower] proofpower

first of all when i enter /home/sarah/pp/bin/xpp it opens xpp and second command that you tell me to try was PPENVDEBUG=y /home/sarah/pp/bin/xpp it also open xpp...so then why when i enter the command xpp -d example_zed  says "printer not found, aborting" how to make sure that ProofPower bin dir

Re: [ProofPower] ProofPower Update

Rob, Sorry for the slow response. I have thought quite a bit about this, but these days such cogitations don't always go anywhere useful. On Thursday 30 Aug 2012 21:58, Rob Arthan wrote: > On 11 Aug 2012, at 15:07, Roger Bishop Jones wrote: > > and a number of cases where identifiers which I ha

Re: [ProofPower] ProofPower Update

On 11 Aug 2012, at 15:07, Roger Bishop Jones wrote: > I have now managed to build my theories on the new > ProofPower and MathsEgs. > > I had to modify 13 source files to get them through. > > It seems probable that the changes all resulted from the new > MathsEgs, and primarily were changes

Re: [ProofPower] ProofPower RCS Repository

On 17/08/12 15:12, Phil Clayton wrote: Also, I encountered some confusing behaviour in that if PPRCSDIR is relative, it must be relative to PPDEVHOME, not the current directory, so I updated the comment. I failed to read the notes below where that was documented. But I think it's relative to

Re: [ProofPower] ProofPower RCS Repository

On 06/08/12 19:40, Rob Arthan wrote: roger, On 6 Aug 2012, at 14:08, Roger Bishop Jones wrote: On Sunday 05 Aug 2012 15:36, Rob Arthan wrote: If anyone feels minded to look at this and advise how it could be adapted to work with Mercurial or Git, I would be very grateful. My ideal would be t

Re: [ProofPower] ProofPower Update

I have now managed to build my theories on the new ProofPower and MathsEgs. I had to modify 13 source files to get them through. It seems probable that the changes all resulted from the new MathsEgs, and primarily were changes to names. These include the changes to theorems "plus" => "additive"

Re: [ProofPower] ProofPower Update

Roger, On 10 Aug 2012, at 14:11, Roger Bishop Jones wrote: > The new version of ProofPower breaks a differential geometry > proof (probably one of yours!) in my t003. > > Were you expecting this to happen at this stage, I thought I > had already sucessfully built all my stuff on the version >

Re: [ProofPower] ProofPower Update

The new version of ProofPower breaks a differential geometry proof (probably one of yours!) in my t003. Were you expecting this to happen at this stage, I thought I had already sucessfully built all my stuff on the version with the higher order rewriting? The changes history does not seem to b

Re: [ProofPower] ProofPower Update

Roger, On 9 Aug 2012, at 12:07, Roger Bishop Jones wrote: > Rob, > > On Thursday 09 Aug 2012 10:26, Rob Arthan wrote: > >> I plan to make a new ProofPower release shortly. In the >> meantime, if you want the state of the art, I uploaded >> an experimental version built from the latest source. >

Re: [ProofPower] ProofPower Update

Roger, On 9 Aug 2012, at 20:28, Roger Bishop Jones wrote: > Rob, > > My theories fail to build on the latest version of maths_egs > because I have been using "R_plus_ops_thm" and > "R_plus_group_thm" which were in wrk068 but are no longer. > > Looks like you have just changed some names, is t

Re: [ProofPower] ProofPower Update

Rob, My theories fail to build on the latest version of maths_egs because I have been using "R_plus_ops_thm" and "R_plus_group_thm" which were in wrk068 but are no longer. Looks like you have just changed some names, is that right? Roger Jones ___ P

Re: [ProofPower] ProofPower Update

Rob, On Thursday 09 Aug 2012 10:26, Rob Arthan wrote: > I plan to make a new ProofPower release shortly. In the > meantime, if you want the state of the art, I uploaded > an experimental version built from the latest source. > You can find this here: > > http://www.lemma-one.com/ProofPower/getti

[ProofPower] ProofPower Update

Dear All, I plan to make a new ProofPower release shortly. In the meantime, if you want the state of the art, I uploaded an experimental version built from the latest source. You can find this here: http://www.lemma-one.com/ProofPower/getting/experimental/ The main reason for the experimental

Re: [ProofPower] ProofPower RCS Repository

On Monday 06 Aug 2012 19:40, Rob Arthan wrote: > Could you try again with > PPMOTIFLINKING=dynamic ? That worked fine. I'm afraid I can't help with mercurial or git, but I am due for a new development regime so I will be following you closely. Roger __

Re: [ProofPower] ProofPower RCS Repository

roger, On 6 Aug 2012, at 14:08, Roger Bishop Jones wrote: > On Sunday 05 Aug 2012 15:36, Rob Arthan wrote: > >> If anyone feels minded to look at this and advise how it >> could be adapted to work with Mercurial or Git, I would >> be very grateful. My ideal would be to be able to map >> between

Re: [ProofPower] ProofPower RCS Repository

On Sunday 05 Aug 2012 15:36, Rob Arthan wrote: > If anyone feels minded to look at this and advise how it > could be adapted to work with Mercurial or Git, I would > be very grateful. My ideal would be to be able to map > between Mercurial or Git and RCS. Any feedback on this > would be gratefully

[ProofPower] ProofPower RCS Repository

There were some discussions last year about making the ProofPower source repository available online, but this didn't come to anything. The main problem I have is that the popular version control systems (CVS, SVN, Git, Mercurial) don't seem to fit very well with what I have always done once-up-

[ProofPower] ProofPower on AWS EC2

Thanks to Phil, Rob and Wolfram for help so far. I was completely distracted yesterday by the delivery of a new keyboard (7-octave variety), but seem to have made some progress. Phil's Yum prescription was helpful. The amazon repositories don't have SML, but do contain a satisfactory openmotif.

Re: [ProofPower] ProofPower in the cloud?

I have a Linux instance running up there in the Amazon "elastic cloud" and will see if I can install ProofPower. There doesn't seem to be much software installed, not even "make", but "yum" seems to be working fine. I'll report back if I get anywhere. Roger Jones

Re: [ProofPower] ProofPower in the cloud?

On Friday 27 Jul 2012 09:45, Rob Arthan wrote: > What is the AWS pricing model? See: http://aws.amazon.com/ec2/pricing/ Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] ProofPower in the cloud?

Roger, On 22 Jul 2012, at 10:23, Roger Bishop Jones wrote: > Has anyone tried, or even considered, running ProoPower in > the Amazon "cloud" (AWS they call it "Amazon Web Services")? > > They offer a number of Linux images which might be used as > starting points. > Presumably one could run Pr

[ProofPower] ProofPower in the cloud?

Has anyone tried, or even considered, running ProoPower in the Amazon "cloud" (AWS they call it "Amazon Web Services")? They offer a number of Linux images which might be used as starting points. Presumably one could run ProofPower and xpp in the cloud and access it using an X-client on cygwin

[ProofPower] ProofPower install script for Ubuntu Linux

Dear all, I'm sending you a very basic shell script that I made to help Marcel while trying to install ProofPower this week. It downloads the required packages via APT, also the last version of ProofPower and PolyML, and install it in the default directories. It is a suggestion for new users that

Re: [ProofPower] ProofPower on Ubuntu 9.04

On Tuesday 13 Oct 2009 1:15 pm, Roger Bishop Jones wrote: > I have tried to build ProofPower on Ubuntu 9.04, > but it failed so I was wondering whether anyone > else has succeeded and if they have any helpful > hints. > > I used the lastest "p2" sources, which build OK > for me on openSUSE 10.3. >

[ProofPower] ProofPower on Ubuntu 9.04

I have tried to build ProofPower on Ubuntu 9.04, but it failed so I was wondering whether anyone else has succeeded and if they have any helpful hints. I used the lastest "p2" sources, which build OK for me on openSUSE 10.3. On Ubuntu the build fails pretty quickly in makehelp.sh with the message