Received! (By both my email addresses - it seems I am doubly subscribed!)
Phil
On 06/11/2023 00:54, Rob Arthan wrote:
This is an attempt to investigate what happened to the ProofPower mailing list
and to see if I can bring it back to life.
If you get this message please reply.
Best
The problem is that ⌜n + 1⌝ can't be matched with a numeric literal. It
may be possible to add such a matching capability but this is easily
worked around by converting the operand first. For a numeric literal,
as in your example, plus1_conv can be used. With this, you can build up
a
(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
** [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
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?
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
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
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
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
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
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
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
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
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 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
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:
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
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
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
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
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
. 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
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
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
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
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 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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
(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,
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
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
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
49 matches
Mail list logo
