Users of Fedora 10, 11 or 12 will find that the openmotif-devel package
from the RPM Fusion repository causes a problem for building
ProofPower. The version of the package provided by MotifZone works fine.
As the Fedora distribution contains only those packages that are truly
open source, man
Here is a small patch that adds the power operator to the theory
z_numbers and adds the obvious theorem about the finiteness and size of
a powerset (of a finite set) to the theory z_numbers1. (There could be
scope for improving the proof.)
Before I do more on this I wondered
- has anyone alre
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 Pr
Roger Bishop Jones wrote:
...
We could have one directory for such things, with
subdirectories for each "contribution" and some rules for
these to permit a uniform and simple way of installing
whatever selection a user wants to make use of, and then
have different top level directories for t
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 n
Roger,
[Subject changed for the mailing list.]
Roger Bishop Jones wrote:
However I actually have a small problem which I don't know
how to solve without a patch.
All of my stuff depends upon the use of docpdf and texpdf for
documentation.
I could put "./docpdf" in the makefile to invoke the f
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. This is
This has been the subject of much discussion in the past... The
solution should be as simple as using OpenMotif 2.3.1.
If you're a Fedora user see my previous post:
http://lemma-one.com/pipermail/proofpower_lemma-one.com/2010-January/000592.html
and if you don't want to wade through all the det
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 %bb
When entering a mixed HOL and Z term as follows:
%<%%lambda% dummy %spot%
%SZT%[[x : 1 .. 2] | 3 < x']%>%
%>%;
the Z part of the term is printed back as
[[x' : 1 .. 2] | 3 < x']
- note the extra prime. This is nothing new - just a consequence of
HOL term operations renaming a boun
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 the
Roger,
I think the short answer is to use the ProofPower exception mechanisms
for readable exception messages.
I presume you want e.g.
raise General.Fail "%forall%";
to show the for all symbol rather than \181. Unfortunately it seems
Poly/ML does not allow this. Whilst the Poly/ML compi
Roger,
See attached for an example of adding a new object language (that can be
mixed with existing HOL and Z terms). This makes use of HOL_reader
which saves having to write a new reader but requires your lexer to
consume Lex.INPUT values. The attached example does not actually
provide the
Rob Arthan wrote:
On 16 Apr 2011, at 02:55, Phil Clayton wrote:
I presume you want e.g.
raise General.Fail "%forall%";
to show the for all symbol rather than \181. Unfortunately it seems
Poly/ML does not allow this. Whilst the Poly/ML compiler interface
allows applications
Whilst looking at imp110, I see that the caught exception messages are
printed using raw_diag_string. As these are not printed from within
compile[12], their output does not go via writer, consequently text is
not translated for output, e.g.
plus_conv %SZT%Q%>%;
I tried changing a few occ
Hi Shu,
We will need some more information about this...
1. Does "pp -d " 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 " worked above:
The version printed by ProofPower.
sbin:/usr/local/bin:/usr/texbin:/usr/X11/bin
xpp: using
XUSERFILESEARCHPATH=/Users/shucheng/app-defaults/%N:/Users/shucheng/%N:/usr/local/pp/app-defaults/%N
Segmentation fault
Thanks very much for helping
Shu
On 17 Apr 2011, at 19:15, Phil Clayton wrote:
Hi Shu,
We will need some mor
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 nev
This sounds very useful - only today I was having to introduce lambda
terms for rewriting to match with... but in Z, not HOL. Will these
higher-order matching/rewriting facilities be implemented for Z also?
If not, does the updated rewriting infrastructure support a
corresponding implementatio
Rob,
Rob Arthan wrote:
On 15 May 2011, at 19:28, Phil Clayton wrote:
This sounds very useful - only today I was having to introduce lambda
terms for rewriting to match with... but in Z, not HOL.
Presumably this is to use theorems involving Z applications?
Yes.
Will these higher-order
(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, d
I've noticed that the ProofPower-Z grammar accepts lambda expressions
without a spot, e.g.
(%lambda% x : X)
because it uses the same grammar rules as for mu expressions. Such
expressions always produce the error message
Exception PARSER_ERROR: PARSER_ERROR "invalid PredLambda arguments" r
Rob Arthan wrote:
On 5 Jun 2011, at 12:10, Phil Clayton wrote:
I suppose this is a good opportunity to raise item 219, i.e.
1. Should the Spivey-Z schema decoration S' be supported in
ProofPower-Z? I believe Standard-Z requires one of
(S)'
S '
to decorate a schema ref
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
On 26/08/04 10:43, Philip Clayton wrote:
Rob and others who are interested in efficiency,
For v_%exists%_intro the manual states
"If the functionality is sufficient, this is superior in efficiency to
both %exists%_intro and simple_%exists%_intro."
However this doesn't seem to be the case anymor
A proper patch that provides z_%mu%_eq_tac is attached. (The
implementation is simpler than what I sent before.)
Phil
On 16/08/04 13:49, Philip Clayton wrote:
Given a subgoal conclusion (%mu% D | P %spot% V) = x or similar, I've
found that it's helpful to have a tactic that uses z_%mu%_rule
On 21/06/11 16:58, Phil Clayton wrote:
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 t
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 loo
A patch that adds support for empty schema paragraphs is attached. This
allows schema definitions and axiomatic descriptions to have an empty
declaration. (The present support for empty schemas does not extend to
paragraphs.)
An axiomatic description with no declaration has the same effect a
ease let me know how you 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.)
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
olon% %bbU% seems all 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 t
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 partic
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 paren
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
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
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
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 declaration.
I'm guessing this is the reason that stripping is not working in my
proof (see attached). It looks trivial but I can't see
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
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
%forall%_intro_conv1 and z_%exists%_intro_conv1 no longer fail if
bound variables declared by schemas-as-declarations had been renamed.
Instead they introduce schema renamings as necessary to convert the
declarations back into valid Z. This fixes a bug reported by Phil
Clayton whereby stripping
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, a
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
(By 'denormalized Z term', I mean a term that is not Z but is
alpha-convertible to a Z term, so could be fixed to be a Z term. I
can't remember if we decided on better word than 'denormalized' - I will
happily use some other word if one exists.)
I have found denormalized terms popping up rath
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
ently 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:
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 exactly
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 perhap
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 comp
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
compiler-s
colon 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 attac
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 oute
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
On 29/03/12 16:59, Rob Arthan wrote:
On 29 Mar 2012, at 15:02, Phil Clayton wrote:
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
In ProofPower-Z, the scope of a variable declared in the Decl part of a
SchemaText includes all expressions in the Decl, for example, in
x : E1; y : E2
any free occurrence of x or y in E1 or E2 is the bound x or y.
I recently got caught out by a subtle case whilst systematically
constructin
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" alter
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 under certain desirable transformations.
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 clo
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 out
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 in
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 tha
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
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 O
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
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.
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 backs
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 d
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
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 relati
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 lan
reply. 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" m
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
c
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
Jon,
On 13/09/12 04:16, Jon Lockhart wrote:
Are you saying then for the Boolean block I have to just replace it with
the one that you have provided in the email?
Not only would you have to replace the Boolean block but also remove the
integer comparison around the references to Boolean global
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 f
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
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 fro
On 14/09/12 10:05, Roger Bishop Jones wrote:
I had a brief look at the last spec that you posted.
I also had a problem unzipping it, ...
This doesn't surprise me because the attachment was byte for byte the
same as the previous attachment that didn't unzip! I guess Jon sent the
wrong file or
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 descr
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:
save_c
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
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
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 m
Hi Jon,
To keep proof scripts maintainable, I always strictly adhere to a format
where an SML comment is inserted each time the name of the goal changes.
For example:
val some_thm = (
push_goal ([], ...);
a (REPEAT z_strip_tac);
(* *** Goal "1" *** *)
a (...);
...
(* *** Goal "1.1" *** *)
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 i
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
http://lemma-one.com/mailman/
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"
ho
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
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
Rob,
28/03/15 16:03, Rob Arthan wrote:
On 27 Mar 2015, at 14:41, Phil Clayton 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 underscor
f − x
should never be parsed as
f (− x)
Regards,
Phil
As I 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 inter
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
LD_RUN_PATH=$(LD_RUN_PATH)
Rob,
On 19/04/15 17:16, Rob Arthan wrote:
Phil,
On 18 Apr 2015, at 18:19, Phil Clayton mailto:phil.clay...@lineone.net>> wrote:
Rob,
I have build 3.1w5 and am seeing Z characters in the terminal which is
great!
Glad you like it!
I find that I need to set LD_LIBRARY_PATH for the P
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
ad
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 the
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, gi
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?
Phil
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:
http://lemma-one.com/pipermail/proofpower_lemma-one.com/2017-May/001
cipe for target 'imp002.ldd' failed
make: *** [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 inst
(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
To: proofpower@lemma-one.com
Hi Mark,
On 15/06
1 - 100 of 103 matches
Mail list logo
