Re: [ProofPower] pp-contrib

2010-04-07 Thread Phil Clayton
Roger, This sounds like a good idea. As I understand it, this would be primarily intended for things built on top of ProofPower, e.g. new theories, but wouldn't exclude projects that contain the entire OpenProofPower source code base if, for example, they need lower-level integration with

Re: [ProofPower] pp-contrib

2010-04-13 Thread Phil Clayton
Rob Arthan wrote: On 12/04/2010 16:19, Phil Clayton wrote: Roger Bishop Jones wrote: ... Perhaps one directory for maths_eq-like contributions, one for contributions in the form of patches: What kind of patches are you envisaging? Do you have any examples in mind? (I'm not sure

Re: [ProofPower] Generating PDF files with texdvi and docdvi

2010-04-14 Thread Phil Clayton
Roger Bishop Jones wrote: On Wednesday 14 Apr 2010 13:23, Phil Clayton wrote: You can actually get docdvi and texdvi to generate PDF files straight up if you add \RequirePackage[pdftex,...]{hyperref} in the preamble (where ... represents other options). See attached example

Re: [ProofPower] Broken theory indexes

2010-08-08 Thread Phil Clayton
This looks like an issue involving blackboard bold S in indexes. I had an issue with this a few months ago and, after investigating, I recorded the following: The file sievekeyword should not have a \MMM{...} entry for %bbS%. Due to the presence of the \MMM{...}, LaTeX does not work when

Re: [ProofPower] Experimental OpenProofPower release 2.9.1w2.rda.110226.tgz

2011-04-12 Thread Phil Clayton
Rob Arthan wrote: a) Alongside the functions set_pc, set_merge_pcs, PC_T, MERGE_PCS_T, etc. there are now functions set_extend_pc, set_extend_pcs, EXTEND_PC_T, EXTEND_PCS_T etc., that extend the current proof context rather than overwrite it. This facilitates proof contexts that just change

Re: [ProofPower] xpp Segmentation fault

2011-04-17 Thread Phil Clayton
Hi Shu, We will need some more information about this... 1. Does pp -d database work? (Note pp not xpp.) This should give you the ProofPower session directly in the terminal. 2. What version of ProofPower are you using? If pp -d database worked above: The version printed by

Re: [ProofPower] xpp Segmentation fault

2011-04-17 Thread Phil Clayton
Rob Arthan wrote: b) Try running it under the gnu debugger, gdb. To do this run the command: gdb /usr/local/pp/bin/pp I'm guessing Rob meant /usr/local/pp/bin/xpp [Aside to Phil: when xpp runs in the background, gdb won't follow xpp through the fork unless you do clever things that have

[ProofPower] Type inference issue with characteristic tuples

2011-06-05 Thread Phil Clayton
(Examples also included in attached file char_tuple_issue.sml) After defining e.g. [T] S %def% [X : T] the type inference issue with characteristic tuples can be seen when the term {S; S'} occurs as a subterm. For example, the following terms fail when they are being constructed,

[ProofPower] Schema in a predicate stub

2011-06-21 Thread Phil Clayton
Is there any reason why a schema argument in a predicate stub (_?) isn't implicitly converted to a predicate? A Z specification taking a Standard-compatible approach to booleans may have: BOOL == P [] True == [| true] False == [| false] if True then X else Y However, this produces a type

[ProofPower] Xpp on Fedora 14 and later

2011-07-07 Thread Phil Clayton
On Fedora 14 and later, Xpp always produces a warning dialog on start up saying it can't find the bitmap images for the templates. (And the images don't appear in the templates window.) This appears to be due to the following: http://bugs.openmotif.org/long_list.cgi?buglist=1539 I haven't

Re: [ProofPower] Xpp on Fedora 14 and later

2011-07-09 Thread Phil Clayton
get on. Regards, Rob. On 8 Jul 2011, at 01:00, Phil Clayton wrote: On Fedora 14 and later, Xpp always produces a warning dialog on start up saying it can't find the bitmap images for the templates. (And the images don't appear in the templates window.) This appears to be due to the following

Re: [ProofPower] Xpp on Fedora 14 and later

2011-07-10 Thread Phil Clayton
On 08/07/11 01:00, Phil Clayton wrote: On Fedora 15, building Xpp works but it seg faults when I run it - see attached xpp_output.log. On further investigation, I may have unfairly attributed this to using Fedora 15. The cause of the issue appears to be having a long path to the xpp

Re: [ProofPower] Schema in a predicate stub

2011-07-11 Thread Phil Clayton
right. It just takes getting used to. Expression quotations would be clearer and more intuitive though. Phil Regards, Rob. On 11 Jul 2011, at 09:45, Rob Arthan wrote: Phil, On 6 Jul 2011, at 16:15, Phil Clayton wrote: On 21/06/11 16:58, Phil Clayton wrote: Is there any reason why a schema

[ProofPower] Z pretty printing issue with strokes in global variable names

2011-07-12 Thread Phil Clayton
I have updated mdt064.doc (attached) to add tests that demonstrate two printing issues relating to global variable names that contain strokes. 1. Generic global variables Under certain conditions, strokes in the names of generic global variables (other than %bbU%) are not printed. (In

[ProofPower] Z parser/pretty printer issue with precedence of lambda and mu

2011-07-15 Thread Phil Clayton
I was going to leave this issue for now but I bumped into it again today, so I've had a look into it. (It's not something that is holding me up, just forcing me to put in parentheses where I don't want to!) This issue was originally noticed because the following term prints back without

Re: [ProofPower] Z pretty printing issue with strokes in global variable names

2011-07-15 Thread Phil Clayton
On 14/07/11 17:57, Rob Arthan wrote: 2. Decorated global variable name clash When both C and C' are schema references, (C)' is printed as C' which is a different term. In imp064, the problem appears to be in function do_decor. There appear to be two routes to fixing this: A. Print in Spivey-Z

Re: [ProofPower] Z parser/pretty printer issue with precedence of lambda and mu

2011-07-17 Thread Phil Clayton
On 16/07/11 16:02, Rob Arthan wrote: On 15 Jul 2011, at 15:29, Phil Clayton wrote: I was going to leave this issue for now but I bumped into it again today, so I've had a look into it. (It's not something that is holding me up, just forcing me to put in parentheses where I don't want

Re: [ProofPower] How do you arrange Xpp?

2011-07-27 Thread Phil Clayton
I meant to add that I always use horizontal mode, so that would have got my vote as Mark predicted! A dynamic toggle would be very useful, I think. Phil On 27/07/11 13:37, Rob Arthan wrote: Thanks to Mark and Artur for their feedback. We have one vote each way, so for the time being I won't

Re: [ProofPower] z_%mem%_seta_conv issue

2011-08-02 Thread Phil Clayton
On 31/07/11 16:33, Rob Arthan wrote: Phil, On 30 Jul 2011, at 17:18, Rob Arthan wrote: On 28 Jul 2011, at 18:10, Phil Clayton wrote: There appears to be a bug in z_%mem%_seta_conv (see attached) when renaming of bound variables is required but the bound variables are introduced by a schema

Re: [ProofPower] Experimental OpenProofPower release 2.9.1w2.rda.110814

2011-09-06 Thread Phil Clayton
Rob, On 04/09/11 11:49, Rob Arthan wrote: Phil, On 3 Sep 2011, at 20:01, Phil Clayton wrote: Rob, Thanks for the latest release. I have been using this for a while now and have a few comments. On 14/08/11 16:18, Rob Arthan wrote: a) For visual compatibility with the ISO standard

Re: [ProofPower] Experimental OpenProofPower release 2.9.1w2.rda.110814

2011-09-13 Thread Phil Clayton
On 08/09/11 10:41, Rob Arthan wrote: On 6 Sep 2011, at 15:19, Phil Clayton wrote: I would have a similar issue the other way around. Is it possible for the width of the editor window to be the same whether or not Xpp is started with a journal window? That is exactly the old behaviour which

[ProofPower] Writing Z schema predicates with decorations

2011-09-17 Thread Phil Clayton
Using the subgoal package, I have just been trying to quote an assumption (as a term quotation) but couldn't. On the assumption term, dest_z_term returns the form ZSchemaPred (..., ') Given, e.g. (* S : P [a, b : Z] *) val S = %SZT% S %bigcolon% %bbP% [a, b : %bbZ%] %%; is there a

Re: [ProofPower] Writing Z schema predicates with decorations

2011-09-25 Thread Phil Clayton
decorate the variables in the characteristic binding, so the semantic constant Z'SchemaPred is exposed fairly often. (This could be avoided with schema renaming as already done recently.) Phil On 24/09/11 13:09, Rob Arthan wrote: Phil, On 17 Sep 2011, at 15:06, Phil Clayton wrote: Using

Re: [ProofPower] Writing Z schema predicates with decorations

2011-09-25 Thread Phil Clayton
On 25/09/11 10:04, Roger Bishop Jones wrote: On Saturday 24 Sep 2011 22:53, Roger Bishop Jones wrote: On Saturday 24 Sep 2011 13:09, Rob Arthan wrote: The quick answer is no - the term generator (imp063.doc) never calls mk_z_schema_pred with non-empty decoration. I need to remind myself

Re: [ProofPower] Writing Z schema predicates with decorations

2011-09-28 Thread Phil Clayton
On 27/09/11 13:25, Roger Bishop Jones wrote: On Sunday 25 Sep 2011 16:20, Phil Clayton wrote: Although the Z'SchemaPred semantic constant enables renaming to be avoided, Z'SchemaPred HOL terms are not Z when the schema components are decorated inconsistently. So perhaps renaming is useful

Re: [ProofPower] Writing Z schema predicates with decorations

2011-09-28 Thread Phil Clayton
On 28/09/11 13:40, Phil Clayton wrote: On 27/09/11 13:25, Roger Bishop Jones wrote: On Sunday 25 Sep 2011 16:20, Phil Clayton wrote: Although the Z'SchemaPred semantic constant enables renaming to be avoided, Z'SchemaPred HOL terms are not Z when the schema components are decorated

[ProofPower] Fixes for building with SML/NJ

2012-01-31 Thread Phil Clayton
Currently ProofPower doesn't build with SML/NJ. A patch is attached to fix this. Although working with Poly/ML is recommended, any (less-trusting) users building on theories of others may wish to check, by running with both compilers, that the supplied proof scripts do not exploit

Re: [ProofPower] Fixes for building with SML/NJ

2012-02-02 Thread Phil Clayton
before the standard output is flushed to the screen. It's only an issue if people are actually using SML/NJ interactively. Phil On 02/02/12 11:52, Rob Arthan wrote: On 31 Jan 2012, at 23:39, Phil Clayton wrote: Currently ProofPower doesn't build with SML/NJ. A patch is attached to fix

Re: [ProofPower] Theorem QA

2012-03-25 Thread Phil Clayton
On 24/03/12 09:32, Rob Arthan wrote: The scripts for the ProofPower mathematical case studies have a little tool called check_thms which does a quality assurance check on the the theorems in a theory. It checks against: a) Theorems with free variables. Typically this means you forgot an outer

Re: [ProofPower] Theorem QA

2012-03-29 Thread Phil Clayton
On 27/03/12 08:36, Rob Arthan wrote: On 25 Mar 2012, at 12:31, Phil Clayton wrote: On 24/03/12 09:32, Rob Arthan wrote: The scripts for the ProofPower mathematical case studies have a little tool called check_thms which does a quality assurance check on the the theorems in a theory

Re: [ProofPower] Scope of variables in Z declaration

2012-04-20 Thread Phil Clayton
Roger, Thanks for the background and explanation. I have added responses below. On 15/04/12 15:21, Roger Bishop Jones wrote: Thanks for your comments on the ProofPower-Z scope rules Phil. I personally believe that the ProofPower position on the scope of variables is preferable to the

Re: [ProofPower] Scope of variables in Z declaration

2012-04-20 Thread Phil Clayton
On 20/04/12 18:48, Phil Clayton wrote: On 20/04/12 11:19, Rob Arthan wrote: ... A == 1 .. 10 S ^= [A : A x A | (_+_)A 10] ... And as so often, language decisions that are bad for proof are often bad for pedagogical and other reasons too. In this case, it stops the language being closed

[ProofPower] Continuing the theme of terrible formal methods limericks...

2012-04-21 Thread Phil Clayton
After reading a book on limericks, one came to me this morning. Bizarrely, it was about function application in Z. (I can't explain that. Obviously I need to get out more.) The greatest chance of amusing anyone is probably here, so here it is. A function said, feeling confused Some

Re: [ProofPower] Trouble Installing on Windows

2012-07-31 Thread Phil Clayton
Jon, I have been running ProofPower under Fedora for many years now. A long time ago, Rob and I established that the following yum command gave us the prerequisites needed for ProofPower (apart from OpenMotif itself, which is not properly open source) after a standard Fedora install: yum

Re: [ProofPower] Trouble Installing on Windows

2012-07-31 Thread Phil Clayton
On 01/08/12 00:07, Phil Clayton wrote: yum install \ gcc-c++ \ polyml \ Of course, you can leave the package polyml out if you're building it yourself. I believe the Fedora 17 repo supplies 5.4.1. If you always want to manage your own versions of Poly/ML, you can ensure that yum

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

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

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

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.

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

Re: [ProofPower] Trouble Installing in cloud

2012-08-03 Thread Phil Clayton
On 02/08/12 10:40, Rob Arthan wrote: On 2 Aug 2012, at 06:52, Roger Bishop Jones wrote: 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

Re: [ProofPower] ProofPower RCS Repository

2012-08-17 Thread Phil Clayton
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

Re: [ProofPower] ProofPower RCS Repository

2012-08-17 Thread Phil Clayton
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

Re: [ProofPower] Trying to Prove my Zed Specifications

2012-09-02 Thread Phil Clayton
Hi John, On 02/09/12 23:59, Jon Lockhart wrote: The problem I am having is this. I am trying to use the union operator in my specification. More specifically I am trying to and a individual item to a set in the predicate of a specification paragraph in z, which is allowed by the rules of the

Re: [ProofPower] Trying to Prove my Zed Specifications

2012-09-02 Thread Phil Clayton
. I have set it so up like that where the parent theory is z_library and my new theory is named something else. Just ran the print status again and that is what it says as well. Could it be one more minor thing is not loaded? Regards, Jon On Sep 2, 2012 8:43 PM, Phil Clayton phil.clay

Re: [ProofPower] Trying to Prove my Zed Specifications

2012-09-12 Thread Phil Clayton
Jon, On 13/09/12 00:24, Jon Lockhart wrote: Unfortunately the two extra sets I want to declare and add to the spec are causing parser errors in ProofPower. The sets I am trying to declare are TIMER == 0..5 and BOOLEAN == {0, 1} which is allowed in the normal standard and has been syntactically

Re: [ProofPower] Trying to Prove my Zed Specifications

2012-09-12 Thread Phil Clayton
On 13/09/12 02:47, Phil Clayton wrote: BOOLEAN that was defined to be 0 .. 5 I meant to say {0, 1}, of course! ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Best platform for ProofPower?

2012-09-13 Thread Phil Clayton
On 12/09/12 21:05, Roger Bishop Jones wrote: I'm having bad luck lately getting suitable environments for running ProofPower. My laptop is on Ubuntu 10.4, and that is fine for ProofPower, but is now so out of date that I can't upgrade it, I would have to install a more recent version of Ubuntu

Re: [ProofPower] Trying to Prove my Zed Specifications

2012-09-13 Thread Phil Clayton
On 13/09/12 21:32, Jon Lockhart wrote: I tried performing the change you prescribed in my ProofPower spec and it fails to parse. I have included the attachment for your reference. I think the attachment has a strange compression format or has been corrupted - gunzip reports unexpected end of

Re: [ProofPower] Trying to Prove my Zed Specifications

2012-09-13 Thread Phil Clayton
On 13/09/12 23:48, Jon Lockhart wrote: I see now, I did not know that. You can lump them together in the Word document when I am using those tools but that is b/c when it is parsed each is separated into its own paragraph on the back end. I will be sure to correct that and see where I can get

Re: [ProofPower] Trying to Prove my Zed Specifications

2012-09-14 Thread Phil Clayton
On 14/09/12 15:50, Rob Arthan wrote: When you set up the consistency goal for a Z axiomatic description, what you see is a mixture of HOL and Z and the existential quantifier is an HOL quantifier not a Z one. So you would need to use %exists%_tac rather than z_%exists%_tac. If the axiomatic

Re: [ProofPower] Trying to Prove my Zed Specifications

2012-09-14 Thread Phil Clayton
On 14/09/12 18:48, Roger Bishop Jones wrote: (I attach a revised version of your document with the proof fixed). In order for z_get_spec to drop the consistency hypothesis, it is necessary to use save_consistency_thm on the resulting theorem. So after the proof you need a line like:

Re: [ProofPower] Trying to Prove my Zed Specifications

2012-09-20 Thread Phil Clayton
Jon, On 20/09/12 17:59, Jon Lockhart wrote: So based on what you have said does that mean then that pushed = {} should be changed to pushed' = {} since it would be a consequence of the Init operation running at start up? I had a quick read yesterday but no time to reply. My initial reaction

Re: [ProofPower] Initialisation convention

2012-09-23 Thread Phil Clayton
On 22/09/12 10:45, Roger Bishop Jones wrote: I see that Potter Sinclair and Till An Introduction to Formal Specification Using Z 1991 use the primed version of the convention, and offer the following rationale (p43): Here we use Vocab' as the variable to suggest that initialisation is like an

Re: [ProofPower] templates activation problem

2013-01-14 Thread Phil Clayton
Hi Sarah, When you select Tools-Templates, do you see the templates dialog box (with very small buttons) or does nothing happen? (The first is a known issue that is easily worked around.) Phil On 15/01/13 05:33, khan khan wrote: Hi i have a problem in activating templates in the tools

Re: [ProofPower] templates activation problem

2013-01-15 Thread Phil Clayton
On 15/01/13 21:39, Roger Bishop Jones wrote: On Tuesday 15 Jan 2013 09:27:06 Roger Bishop Jones wrote: On Tuesday 15 Jan 2013 07:43:30 Phil Clayton wrote: When you select Tools-Templates, do you see the templates dialog box (with very small buttons) or does nothing happen? (The first

Re: [ProofPower] making new database

2013-02-17 Thread Phil Clayton
This question was answered yesterday: http://lemma-one.com/pipermail/proofpower_lemma-one.com/2013-February/000980.html Your chances of spotting replies to the list may be increased if you change your mailing list options to be a non-digested member. (Do this at

Re: [ProofPower] (no subject)

2013-02-18 Thread Phil Clayton
On 18/02/13 15:39, khan khan wrote: 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

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

2015-03-30 Thread Phil Clayton
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

Re: [ProofPower] Unicode and ProofPower

2015-03-27 Thread Phil Clayton
Rob, 12/03/15 12:31, Rob Arthan wrote: I am currently working on support for input and output using Unicode into ProofPower. I would appreciate any feedback on the translation scheme I am proposing to use, which is described here: http://www.lemma-one.com/ProofPower/unicode/pp-unicode.html I

Re: [ProofPower] Unicode and ProofPower

2015-04-08 Thread Phil Clayton
Rob, 28/03/15 16:03, Rob Arthan wrote: On 27 Mar 2015, at 14:41, Phil Clayton phil.clay...@lineone.net mailto:phil.clay...@lineone.net wrote: You currently have 208D SUBSCRIPT LEFT PARENTHESIS for %ulbegin% 208E SUBSCRIPT RIGHT PARENTHESISfor %ulend% but these parentheses don't have

Re: [ProofPower] Updated Unicode translation scheme

2015-04-18 Thread Phil Clayton
said in a recent post to Phil Clayton, I abandoned my half-hearted hopes of providing Unicode support for ProofPower in general and some level of interoperability between ProofPower-Z and ISO Z at the same time. Inside ProofPower, interoperab

Re: [ProofPower] OpenProofPower 3.1w5

2015-04-18 Thread Phil Clayton
Rob, I have build 3.1w5 and am seeing Z characters in the terminal which is great! I find that I need to set LD_LIBRARY_PATH for the Poly/ML libraries when running. I suspect that this is because the polyc command in HOLSTARTCMD in hol.mkf does does not include

Re: [ProofPower] error msg when instantiating quantifier in asm

2015-05-28 Thread Phil Clayton
Hi Yuhui, I asked a similar question some years ago here: http://lemma-one.com/pipermail/proofpower_lemma-one.com/2004-September/000235.html See the replies for an explanation of the issue, in particular Roger's emails. In your case, you need to specialize the theorem z_id_%bij%_thm before

[ProofPower] z_app_thm

2015-09-08 Thread Phil Clayton
In z_app_thm, which states ∀ a : 핌; f : 핌; x : 핌 ⦁ (∀ f_a : 핌 | (a, f_a) ∈ f ⦁ f_a = x) ∧ (a, x) ∈ f ⇒ f a = x I notice that the antecedent (a, x) ∈ f does not actually need to map a to x because that is already captured in the first antecedent. It only needs to say that a is in

Re: [ProofPower] Setting up on macosx Sierra fails...

2017-05-13 Thread Phil Clayton
I have successfully built ProofPower with SML/NJ 110.81 which was recently released. (That was on Fedora but any SML type errors should be the same on different platforms.) I haven't tried earlier versions. In the ProofPower source directory, did you run ./distclean before rebuilding?

Re: [ProofPower] Setting up on macosx Sierra fails...

2017-05-13 Thread Phil Clayton
Hi Hugh, In brief, try the attached patch. As of Poly/ML 5.7, the types int and LargeInt.int are no longer the same, hence your error: Reason: Can't unify int (*In Basis*) with LargeInt.int (*In Basis*) (Different type constructors) When building Poly/ML 5.7,

Re: [ProofPower] PP 3.1w7 installation problems with Fedora 24

2017-06-14 Thread Phil Clayton
Hi Mark, You probably need to do yum install openmotif-devel to ensure that the Motif C header files are also installed. ProofPower 3.1w7 doesn't build with Poly/ML 5.7 due to a change in the integer types described here:

Re: [ProofPower] PP 3.1w7 installation problems with Fedora 24

2017-06-15 Thread Phil Clayton
** [imp002.ldd] Error 1 I don't know why 3.1w6 doesn't build with Poly/ML 5.6. What does the log file for imp002 say? Phil Cheers, Mark. On 15/06/2017 02:27, Phil Clayton wrote: Hi Mark, You probably need to do yum install openmotif-devel to ensure that the Motif C header files are

Re: [ProofPower] PP 3.1w7 installation problems with Fedora 24

2017-06-16 Thread Phil Clayton
(I replied from the wrong email address which silently fails, trying again...) Forwarded Message Subject: Re: [ProofPower] PP 3.1w7 installation problems with Fedora 24 Date: Thu, 15 Jun 2017 16:31:29 +0100 From: Phil Clayton <phil.clay...@lineone.net> To: proofpower