Re: [ProofPower] Trouble Installing in cloud

2012-08-01 Thread Roger Bishop Jones 
On Thursday 02 Aug 2012 00:33, you wrote:
> On 01/08/12 14:35, Roger Bishop Jones wrote:
> > The real challenge (for me at least) is to get xpp
> > and/or emacs to run in the cloud with a display here
> > on earth, I don't have much clue how to do that.
> 
> I've been thinking about this.  To me, it seems
> conceptually wrong to be running Xpp remotely.

Mm.
I don't know about "conceptually", but there is a question 
here about what problem I am trying to solve.

> Would it
> not make more sense to run a local (earth-based) Xpp
> whose journal window contains a remote ProofPower shell
> (up in the cloud) via e.g. ssh?

If I were just interested in running ProofPower in the cloud 
then that would be correct. And this something that one 
might like to investigate.  However, my own primary interest 
is in whether I could export my entire development 
environment into the cloud so that I don't have to worry 
when I buy a device whether it will support LINUX and I get 
continuity of my development environment independently of 
what bits of kit I am buying or disposing of.

> Initially I tried
> testing
> 
>xpp -c ssh -Y user@host
> 
> but is seems that the capabilities of Xpp's pseudo
> terminal aren't up to ssh login interaction.  However,
> if you can automatically log in then all is fine.  I
> used the instructions here:
> http://docs.fedoraproject.org/en-US/Fedora/17/html/System
> _Administrators_Guide/s2-ssh-configuration-keypairs.html
> to create .ssh/authorized_keys on the remote account to
> allow automatic log in.

Aren't you heading for a situation in which the source files 
being edited by Xpp are local but the ProofPower database 
which you are augmenting is remote?

I don't see how that would make sense.

I am really looking for a complete X11 framebuffer (is that 
what they call it?) which  is is remote, so that not only 
Xpp but also other tools like emacs run remotely.
There does seem to be software which does that (e.g. using 
"VNC"), but the documentation seems to assume you know a lot 
more than I do.
Alternatively X11 forwarding over SSH looks like it allows 
any applications you open on the remote host to operate 
windows on the local machine (but this is not supposed to 
perform very well or to provide robust connections).  These 
are the two scenarios I am investigating at the moment, 
along with a third which I'm not sure where it fits but which 
might be what amazon best supports (because I can see it in 
their yum depositories. which seem light on X11 package 
groups) viz. Xephyr.

Roger



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

Re: [ProofPower] Trouble Installing on Windows

2012-08-01 Thread Phil Clayton 

Jon,

On 01/08/12 23:44, Jon Lockhart wrote:

I did run the yum install commands as you mentioned, but it is possible
I spelled it wrong. I will look into and get back to you.


You can copy and paste the required lines of the yum command from the 
email directly into a terminal.  A trailing backslash on a line means 
that the command is continued on the next line.  There is no problem 
copying and pasting the command in several pieces.


Note that in Linux, you can copy and paste just by selecting text to 
copy and middle-clicking where you want to paste.  (If middle-clicking 
in a terminal window, text is inserted at the cursor.)


Apologies if you're aware of these Linux basics.  Thought this may help 
to avoid spelling errors.


Phil


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

Re: [ProofPower] Trouble Installing in cloud

2012-08-01 Thread Phil Clayton 

On 01/08/12 14:35, Roger Bishop Jones wrote:

The real challenge (for me at least) is to get xpp and/or
emacs to run in the cloud with a display here on earth, I
don't have much clue how to do that.


I've been thinking about this.  To me, it seems conceptually wrong to be 
running Xpp remotely.  Would it not make more sense to run a local 
(earth-based) Xpp whose journal window contains a remote ProofPower 
shell (up in the cloud) via e.g. ssh?  Initially I tried testing


  xpp -c ssh -Y user@host

but is seems that the capabilities of Xpp's pseudo terminal aren't up to 
ssh login interaction.  However, if you can automatically log in then 
all is fine.  I used the instructions here:

http://docs.fedoraproject.org/en-US/Fedora/17/html/System_Administrators_Guide/s2-ssh-configuration-keypairs.html
to create .ssh/authorized_keys on the remote account to allow automatic 
log in.


However,

  xpp -c ssh -Y user@host "pp -d zed"

fails to find pp when attempting to run on the remote host, even though 
the remote account adds the ProofPower home directory to the path in 
.bash_profile.  The issue is that the remote shell is not an interactive 
shell, so .bash_profile does not get run.  Many options here:


1. Specify full remote path, e.g.

  xpp -c ssh -Y user@host \
"$REMOTEPPHOME/bin/pp -d $REMOTEPPHOME/db/zed"

where REMOTEPPHOME is the ProofPower home directory in the cloud.

2. Source the required environment as part of the command, e.g.

  xpp -c ssh -Y user@host "source .bash_profile; pp -d zed"

3. Add the ProofPower home directory to the path in an rc file (e.g. 
.bashrc) instead of in a profile file (such as .bash_profile), then just use


  xpp -c ssh -Y user@host "pp -d zed"

For a cloud service, option 3 looks like the best set up.

Regards,

Phil


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

Re: [ProofPower] Trouble Installing on Windows

2012-08-01 Thread Jon Lockhart 
Phil,

I will certainly look into what you mentioned after dinner.

I did run the yum install commands as you mentioned, but it is possible I
spelled it wrong. I will look into and get back to you.

Thanks,
Jon


On Wed, Aug 1, 2012 at 6:35 PM, Phil Clayton wrote:

> Jon,
>
>
> On 01/08/12 22:43, Jon Lockhart wrote:
>
>> I forgot to grab the devel rpm when I was on the download site. I had
>> olbly grabbed the OpenMotif rpm. That did the trick on the configuration
>> file.
>>
>
> devel packages are easily overlooked!  Usually, when you have source code
> with a build dependency on X, you need X's devel package.
>
>
>
>  Now I am running into the issue on the install. I have attached the
>> build log for your convienece. The install is failing b/c the file
>> Print.h is not available in the X11 folder, and I have tried
>> reinstalling with yum several times. Is there another package from yum
>> that I have possibly missed downloading?
>>
>
> The missing file is
>
>   /usr/include/X11/extensions/**Print.h
>
> On my machine, the command
>
>   rpm -q --whatprovides /usr/include/X11/extensions/**Print.h
>
> indicates that the package libXp-devel provides this file.  This should
> have been installed by the yum command I quoted previously, which included
> libXp-devel.  Can you double check that you entered the command exactly,
> omitting only the line containing polyml?  (I checked the fc17 package, and
> it does appear to provide this file.)
>
>
>
>  I just want to take the time now to thank you and Rob for all the help
>> you been providing me on getting PP up and running. It has been a long
>> time since I used a Linux system, and having to relearn all this
>> material I go is frustrating, along with trying to get a tool installed
>> that I really want to try and use with my formal specification writing.
>> I appreciate everything I have been provided.
>>
>
> Glad to help.  With Linux distributions these days, package management
> support takes most of the pain out of fetching/installing prerequisites.
>  But you still need to know which packages to install...
>
> It's a pity that 90% of the installation effort is just to get Xpp
> working.  I'm working on a GTK-based replacement to Xpp but it's not quite
> ready yet.
>
> Regards,
>
> Phil
>
>
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trouble Installing on Windows

2012-08-01 Thread Phil Clayton 

Jon,

On 01/08/12 22:43, Jon Lockhart wrote:

I forgot to grab the devel rpm when I was on the download site. I had
olbly grabbed the OpenMotif rpm. That did the trick on the configuration
file.


devel packages are easily overlooked!  Usually, when you have source 
code with a build dependency on X, you need X's devel package.




Now I am running into the issue on the install. I have attached the
build log for your convienece. The install is failing b/c the file
Print.h is not available in the X11 folder, and I have tried
reinstalling with yum several times. Is there another package from yum
that I have possibly missed downloading?


The missing file is

  /usr/include/X11/extensions/Print.h

On my machine, the command

  rpm -q --whatprovides /usr/include/X11/extensions/Print.h

indicates that the package libXp-devel provides this file.  This should 
have been installed by the yum command I quoted previously, which 
included libXp-devel.  Can you double check that you entered the command 
exactly, omitting only the line containing polyml?  (I checked the fc17 
package, and it does appear to provide this file.)




I just want to take the time now to thank you and Rob for all the help
you been providing me on getting PP up and running. It has been a long
time since I used a Linux system, and having to relearn all this
material I go is frustrating, along with trying to get a tool installed
that I really want to try and use with my formal specification writing.
I appreciate everything I have been provided.


Glad to help.  With Linux distributions these days, package management 
support takes most of the pain out of fetching/installing prerequisites. 
 But you still need to know which packages to install...


It's a pity that 90% of the installation effort is just to get Xpp 
working.  I'm working on a GTK-based replacement to Xpp but it's not 
quite ready yet.


Regards,

Phil


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

Re: [ProofPower] Trouble Installing on Windows

2012-08-01 Thread Jon Lockhart 
Phil,

I forgot to grab the devel rpm when I was on the download site. I had olbly
grabbed the OpenMotif rpm. That did the trick on the configuration file.

Now I am running into the issue on the install. I have attached the build
log for your convienece. The install is failing b/c the file Print.h is not
available in the X11 folder, and I have tried reinstalling with yum several
times. Is there another package from yum that I have possibly missed
downloading?

I just want to take the time now to thank you and Rob for all the help you
been providing me on getting PP up and running. It has been a long time
since I used a Linux system, and having to relearn all this material I go
is frustrating, along with trying to get a tool installed that I really
want to try and use with my formal specification writing. I appreciate
everything I have been provided.

Regards,
Jon


On Wed, Aug 1, 2012 at 5:36 AM, Phil Clayton wrote:

> On 01/08/12 06:40, Jon Lockhart wrote:
>
>> I will try the rpm inquiry and see what i come up with.
>>
>> I remember seeing that in the README. Guess it will be necessary to set
>> those config variables.
>>
>
> I have never found it necessary to set the PPMOTIFHOME environment
> variable.  I believe I am currently using
>   openmotif-2.3.3-1.fc12.x86_64.**rpm
>   openmotif-devel-2.3.3-1.fc12.**x86_64.rpm
> as obtained from
>
> http://www.motifzone.org/**files/public_downloads/**
> openmotif/2.3/2.3.3/openmotif-**2.3.3-1.fc12.x86_64.rpm
>
> http://www.motifzone.org/**files/public_downloads/**
> openmotif/2.3/2.3.3/openmotif-**devel-2.3.3-1.fc12.x86_64.rpm
>
> Note that you need the devel package which provides the C header files
> required for building Motif applications.  (I suspect it certain header
> files that configure is looking for.)
>
> Regards,
>
>
> Phil
>
>
> __**_
> 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] Trouble Installing in cloud

2012-08-01 Thread Roger Bishop Jones 
Phil,

On Wednesday 01 Aug 2012 14:06, Phil Clayton wrote:
> Can you
> provide the output of
> 
>rpm -ql openmotif-devel

It had to be something really stupid, I don't do enough of 
this kind of thing.

I didn't install openmotif-devel.

Now I have, and the configure script does find it.
I have now installed ProofPower.

I shall try and get the rest of my build system in place, 
which should be just a question of remembering what else 
needs to be installed to run my builds.

The real challenge (for me at least) is to get xpp and/or 
emacs to run in the cloud with a display here on earth, I 
don't have much clue how to do that.

Roger

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

Re: [ProofPower] Trouble Installing in cloud

2012-08-01 Thread Phil Clayton 

Roger,

From the reported package name openmotif-2.3.3-4.6.amzn1.x86_64 I can 
see that you're not using the packages from motifzone.net.  Can you 
provide the output of


  rpm -ql openmotif-devel

It could be that the Amazon 'amzn1' packages for OpenMotif have the same 
issue as the RPM Fusion OpenMotif packages that I describe here:

http://lemma-one.com/pipermail/proofpower_lemma-one.com/2010-January/000592.html

In that message, I see that I also noted

  "I think there could be an issue beyond the configure
   script because PPMOTIFHOME doesn't seem to be used
   anywhere, namely in any include paths for compilation
   or linking."

So I don't even know whether setting PPMOTIFHOME does anything!

Phil


On 01/08/12 13:10, Roger Bishop Jones wrote:

I seem to have the same problem as John in a different place.
i.e. in a linux image in the amazon cloud.

I followed Phil's Yum list to get me started, which worked
apart from failing to find polyml.
I successfully built polyml from the sources.
Then I checked with yum and found that the openmotif in the
amazon repositories seemed to be the right one, and
installed openmotif.

However, the ProofPower configure script can't find it.

Here's is what rpm says about it:

[ec2-user@domU-12-31-39-05-56-E9 ~]$ rpm -q openmotif
openmotif-2.3.3-4.6.amzn1.x86_64
[ec2-user@domU-12-31-39-05-56-E9 ~]$ rpm -ql openmotif
/etc/X11/mwm/system.mwmrc
/etc/X11/xinit/xinitrc.d/xmbind.sh
/usr/bin/mwm
/usr/bin/xmbind
/usr/include/X11/bitmaps/xm_error
/usr/include/X11/bitmaps/xm_hour16
/usr/include/X11/bitmaps/xm_hour16m
/usr/include/X11/bitmaps/xm_hour32
/usr/include/X11/bitmaps/xm_hour32m
/usr/include/X11/bitmaps/xm_information
/usr/include/X11/bitmaps/xm_noenter16
/usr/include/X11/bitmaps/xm_noenter16m
/usr/include/X11/bitmaps/xm_noenter32
/usr/include/X11/bitmaps/xm_noenter32m
/usr/include/X11/bitmaps/xm_question
/usr/include/X11/bitmaps/xm_warning
/usr/include/X11/bitmaps/xm_working
/usr/lib64/libMrm.so.4
/usr/lib64/libMrm.so.4.0.3
/usr/lib64/libUil.so.4
/usr/lib64/libUil.so.4.0.3
/usr/lib64/libXm.so.4
/usr/lib64/libXm.so.4.0.3
/usr/share/X11/bindings
/usr/share/X11/bindings/acorn
/usr/share/X11/bindings/apollo
/usr/share/X11/bindings/dec
/usr/share/X11/bindings/dg_AViiON
/usr/share/X11/bindings/doubleclick
/usr/share/X11/bindings/hal
/usr/share/X11/bindings/hitachi
/usr/share/X11/bindings/hp
/usr/share/X11/bindings/ibm
/usr/share/X11/bindings/intergraph
/usr/share/X11/bindings/intergraph17
/usr/share/X11/bindings/megatek
/usr/share/X11/bindings/motorola
/usr/share/X11/bindings/ncr_at
/usr/share/X11/bindings/ncr_vt
/usr/share/X11/bindings/pc
/usr/share/X11/bindings/sgi
/usr/share/X11/bindings/siemens_9733
/usr/share/X11/bindings/siemens_wx200
/usr/share/X11/bindings/sni
/usr/share/X11/bindings/sni_97801
/usr/share/X11/bindings/sony
/usr/share/X11/bindings/sun
/usr/share/X11/bindings/sun_at
/usr/share/X11/bindings/tek
/usr/share/X11/bindings/xmbind.alias
/usr/share/doc/openmotif-2.3.3
/usr/share/doc/openmotif-2.3.3/COPYRIGHT.MOTIF
/usr/share/doc/openmotif-2.3.3/README
/usr/share/doc/openmotif-2.3.3/RELEASE
/usr/share/doc/openmotif-2.3.3/RELNOTES
/usr/share/man/man1/mwm.1.gz
/usr/share/man/man1/xmbind.1.gz
/usr/share/man/man4/mwmrc.4.gz

Should I be setting OPENMOTIFHOME?
If so, to what, surely ProofPower looks in /usr/bin

Roger Jones

___
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] Trouble Installing in cloud

2012-08-01 Thread Roger Bishop Jones 
I seem to have the same problem as John in a different place.
i.e. in a linux image in the amazon cloud.

I followed Phil's Yum list to get me started, which worked 
apart from failing to find polyml.
I successfully built polyml from the sources.
Then I checked with yum and found that the openmotif in the 
amazon repositories seemed to be the right one, and 
installed openmotif.

However, the ProofPower configure script can't find it.

Here's is what rpm says about it:

[ec2-user@domU-12-31-39-05-56-E9 ~]$ rpm -q openmotif
openmotif-2.3.3-4.6.amzn1.x86_64
[ec2-user@domU-12-31-39-05-56-E9 ~]$ rpm -ql openmotif
/etc/X11/mwm/system.mwmrc
/etc/X11/xinit/xinitrc.d/xmbind.sh
/usr/bin/mwm
/usr/bin/xmbind
/usr/include/X11/bitmaps/xm_error
/usr/include/X11/bitmaps/xm_hour16
/usr/include/X11/bitmaps/xm_hour16m
/usr/include/X11/bitmaps/xm_hour32
/usr/include/X11/bitmaps/xm_hour32m
/usr/include/X11/bitmaps/xm_information
/usr/include/X11/bitmaps/xm_noenter16
/usr/include/X11/bitmaps/xm_noenter16m
/usr/include/X11/bitmaps/xm_noenter32
/usr/include/X11/bitmaps/xm_noenter32m
/usr/include/X11/bitmaps/xm_question
/usr/include/X11/bitmaps/xm_warning
/usr/include/X11/bitmaps/xm_working
/usr/lib64/libMrm.so.4
/usr/lib64/libMrm.so.4.0.3
/usr/lib64/libUil.so.4
/usr/lib64/libUil.so.4.0.3
/usr/lib64/libXm.so.4
/usr/lib64/libXm.so.4.0.3
/usr/share/X11/bindings
/usr/share/X11/bindings/acorn
/usr/share/X11/bindings/apollo
/usr/share/X11/bindings/dec
/usr/share/X11/bindings/dg_AViiON
/usr/share/X11/bindings/doubleclick
/usr/share/X11/bindings/hal
/usr/share/X11/bindings/hitachi
/usr/share/X11/bindings/hp
/usr/share/X11/bindings/ibm
/usr/share/X11/bindings/intergraph
/usr/share/X11/bindings/intergraph17
/usr/share/X11/bindings/megatek
/usr/share/X11/bindings/motorola
/usr/share/X11/bindings/ncr_at
/usr/share/X11/bindings/ncr_vt
/usr/share/X11/bindings/pc
/usr/share/X11/bindings/sgi
/usr/share/X11/bindings/siemens_9733
/usr/share/X11/bindings/siemens_wx200
/usr/share/X11/bindings/sni
/usr/share/X11/bindings/sni_97801
/usr/share/X11/bindings/sony
/usr/share/X11/bindings/sun
/usr/share/X11/bindings/sun_at
/usr/share/X11/bindings/tek
/usr/share/X11/bindings/xmbind.alias
/usr/share/doc/openmotif-2.3.3
/usr/share/doc/openmotif-2.3.3/COPYRIGHT.MOTIF
/usr/share/doc/openmotif-2.3.3/README
/usr/share/doc/openmotif-2.3.3/RELEASE
/usr/share/doc/openmotif-2.3.3/RELNOTES
/usr/share/man/man1/mwm.1.gz
/usr/share/man/man1/xmbind.1.gz
/usr/share/man/man4/mwmrc.4.gz

Should I be setting OPENMOTIFHOME?
If so, to what, surely ProofPower looks in /usr/bin

Roger Jones

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

Re: [ProofPower] Trouble Installing on Windows

2012-08-01 Thread Phil Clayton 

On 01/08/12 06:40, Jon Lockhart wrote:

I will try the rpm inquiry and see what i come up with.

I remember seeing that in the README. Guess it will be necessary to set
those config variables.


I have never found it necessary to set the PPMOTIFHOME environment 
variable.  I believe I am currently using

  openmotif-2.3.3-1.fc12.x86_64.rpm
  openmotif-devel-2.3.3-1.fc12.x86_64.rpm
as obtained from

http://www.motifzone.org/files/public_downloads/openmotif/2.3/2.3.3/openmotif-2.3.3-1.fc12.x86_64.rpm

http://www.motifzone.org/files/public_downloads/openmotif/2.3/2.3.3/openmotif-devel-2.3.3-1.fc12.x86_64.rpm

Note that you need the devel package which provides the C header files 
required for building Motif applications.  (I suspect it certain header 
files that configure is looking for.)


Regards,

Phil


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