Dear All,
It is my pleasure to announce that an alpha version 2.8.1a10 of OpenProofPower
is now available that works with the version 5.2.1 of Poly/ML. New users are
strongly recommended to start with this version of OpenProofPower and old
users are advised to upgrade when convenient.
Note tha
Roger,
It seems to work for me. How is it failing?
Regards,
Rob.
On 20 Nov 2008, at 17:34, Roger Bishop Jones wrote:
> I tried out the new alpha of ProofPower this afternoon.
>
> It build OK (on openSUSE 11), but a builld of PPMathsEgs failed in
> wrk066.
> I used the latest version from lemm
Roger,
On Friday 21 Nov 2008 10:03 am, Roger Bishop Jones wrote:
> On Friday 21 November 2008 06:00:18 Rob Arthan wrote:
> > It seems to work for me. How is it failing?
>
> A rewrite failed.
>
> However, I went through it all again more carefully and it has now gone
> thr
On 22 Nov 2008, at 08:04, Roger Bishop Jones wrote:
> Rob,
>
> I had concluded that my knee jerk "fixing" of PPHOME should be
> irrelevant but
> anyway it works now and presumably it isn't worth chasing down exactly
> why it
> didn't work first time.
>
> I seem to have lost CTRL-F and CTRL-D as
On Thursday 04 Dec 2008 5:06 pm, Roger Bishop Jones wrote:
> On Saturday 22 November 2008 09:20:56 Rob Arthan wrote:
>
> (me)
>
> > > Can't find anything which suggests that these
> > > are configurable, any hints?
>
> (rob)
>
> > They are configu
Philip Clayton wrote:
Artur Oliveira Gomes wrote:
Hi there,
I'm trying to install the latest of ProofPower 2.8.1a10, but I got
some problems.
The last lines of build.log that I got is:
...
docsml -f hol.svf imp048
Compiling (code) imp048.sml
pp: "pp-ml
/home/artur/Proofpower/OpenProofPower-
Artur,
On Friday 19 Dec 2008 3:10 pm, Artur Oliveira Gomes wrote:
> Ops,
>
> I forgot to reply to all...
>
> Here follows the extract of imp048.err:
>
> val it = () : unit
> val it = () : unit
> === ProofPower 2.8.1a10 [HOL Database]
> === Copyright (C) Lemma 1 Ltd. 2000-2008
>
> Database name:
>
Artur,
What do the top 10 lines of src/dtd048.ldd say?
Regards,
Rob.
On Saturday 20 Dec 2008 12:53 pm, Artur Oliveira Gomes wrote:
> Rob,
>
> > The signature should have been defined when dtd048.sml was compiled. The
> > log
> > from compiling dtd048.sml should be in src/dtd048.ldd, so do you h
Artur,
On Saturday 20 Dec 2008 2:05 pm, Artur Oliveira Gomes wrote:
> Rob,
>
> val it = () : unit
> val it = () : unit
> === ProofPower 2.8.1a10 [HOL Database]
> === Copyright (C) Lemma 1 Ltd. 2000-2008
>
> Database name:
>...
This strongly suggests that you are somehow picking up an earlier vers
Artur,
On Tuesday 23 Dec 2008 8:40 am, Artur Oliveira Gomes wrote:
> Rob,
>
> This strongly suggests that you are somehow picking up an earlier version
> of
>
> > the pp script. You are using the "./configure; ./install" sequence to run
> > the
> > installation aren't you?
I take it that the answ
rrors (pass2)" raised abandoning file
> imp048.sml at line 521
> +++ Compiled imp048.sml: Failed (Compilation Run Complete) +++
>
>
> Any ideas?
>
> Best,
>
> Steven
>
> 2008/12/30 Rob Arthan :
> > Artur,
> >
> > On Tuesday 23 Dec 2008 8:40
Steve,
On Friday 23 Jan 2009 5:16 pm, Steven J. Ramsay wrote:
> After following your instructions, the build does not progress any
> further, the last output of build.log is:
>...
> Would you like to see any other output? It may or may not be helpful
> to know that my poly is not installed into th
Artur (& Steven),
On 23 Jan 2009, at 17:23, Artur Oliveira Gomes wrote:
Hi there,
Build.log output:
...
ar...@firebird:~/Proofpower/OpenProofPower-2.8.1a10$ cat src/
dtd048.log
cat: src/dtd048.log: No such file or directory
Sorry, I mean src/dtd048.ldd - what do you have in that?
Rega
On Friday 23 Jan 2009 9:53 pm, Steven J. Ramsay wrote:
> It ends with:
>
> val it = () : unit
> +++ Compiled dtd048.sml: OK (Compilation Run Complete) +++
> Exception Fail * The database name has not been set
> [save_and_exit.36010] * raised
What do the first few lines lok like? I expect they look
Steven,
Thanks for that. What operating system and hardware are you running on?
Regards,
Rob.
On 24 Jan 2009, at 17:24, Steven J. Ramsay wrote:
2009/1/24 Rob Arthan :
What do the first few lines lok like? I expect they look something
like:
val it = () : unit
val it = () : unit
old Pentium M processor (i.e. x86), with 1GB
> of RAM. The OS is Ubuntu 8.04 (Hardy Heron).
>
> Best,
>
> Steven
>
> 2009/1/24 Rob Arthan :
> > Steven,
> >
> > Thanks for that. What operating system and hardware are you running on?
> >
> > Regards,
&
Artur,
On Sunday 25 Jan 2009 12:22 pm, Rob Arthan wrote:
> Steven, Artur,
>
> I think it will probably be easiest if I try to build a Ubuntu 8.04 system
> and see if I can reproduce the problem. I will keep you posted.
>
> Artur: are you using Ubuntu too?
Supplementary quest
Phil
Steven J. Ramsay wrote:
No problem. I am on an old Pentium M processor (i.e. x86), with 1GB
of RAM. The OS is Ubuntu 8.04 (Hardy Heron).
Best,
Steven
2009/1/24 Rob Arthan :
Steven,
Thanks for that. What operating system and hardware are you
running on?
Regards,
Rob.
On 24 Jan
On 26 Jan 2009, at 19:34, Rob Arthan wrote:
Many thanks to Phil for this. I will try to devise a work-around
for this bizarre behaviour of dash, which seems to be based on a
misreading of the POSIX standard as far as I can see.
Further investigation reveals that it is POSIX that is
On 27 Jan 2009, at 21:54, Artur Oliveira Gomes wrote:
Rob,
I'll try to install this release on Ubuntu.
You mentioned Mac OS X. Do you have a tutorial, anything to help me
in order to install ProofPower on a Mac?
It is just like installing on Linux. You need to have installed the
Darwi
Dear All,
Phil Clayton reported a problem with 2.8.1a14 that I believe I have now fixed. I
have updated the tarball at:
http://www.lemma-one.com/ProofPower/getting/versions/OpenProofPower-2.8.1a14.tgz
The right one is dated 28th January not 27th.
Regards,
Rob.
___
Artur,
You may like to know that there is a so-called "component" proof context called
'z_reals which will make evaluation of real arithmetic expressions happen
automatically when you rewrite.
Try:
set_merge_pcs["'z_reals", "z_library"];
set_goal([], %SZT% real 30 %mem% real 20 ..%down%R re
Artur,
You can use:
a(conv_tac(ONCE_MAP_C z_float_conv));
to change things like "3.0" into "real 3" or "3.5" into "7/2" and then
rewriting in the proof context 'z_reals will do the arithmetic for you.
We don't do this automatically in the proof context 'z_reals in case
you have floating l
Frank,
On 7 Apr 2009, at 14:39, Frank Zeyda wrote:
Dear Roger,
Many thanks for the reply.
The additional feature of better error handling is easily supported
with another line of code handling possible exceptions.
The idea behind the caller parameter in many of these internal
funct
On 15 May 2009, at 04:49, Artur Oliveira Gomes wrote:
Hi there,
I am having a problem in rewriting using an assumption with
parenthesis.
For example:
(* 1 *) (\exists (SA AND SB)' · SAInit AND SBInit)
= ((\exists SA' · SAInit) AND (\exists SB' ·
SBInit))
(* |- *) \exist
On 18 May 2009, at 21:28, Artur Oliveira Gomes wrote:
Hi there,
It doesn't look like parentheses are the problem. It might be a
problem with types or something else that is not visible in the
pretty-printed Z that is stopping the LHS of he assumption matching
the conclusion of the goal.
On 18 May 2009, at 23:27, Artur Oliveira Gomes wrote:
Rob,
Can you tell me how can I increase the default subgoal limit when
stripping a goal?
In that proof I sent you an example, or me, the complete version
of the proof creates over 34 subgoals, then, ProofPower give me
a warning telling th
On 5 Jun 2009, at 08:35, Roger Bishop Jones wrote:
I quite often find that I want to use a new character in
ProofPower HOL.
However, ProofPower seems to be quite fussy about what
characters you use.
For example, there are three "spares" at the moment,
which would be useful for me. They wouldn
On 5 Jun 2009, at 08:35, Roger Bishop Jones wrote:
I quite often find that I want to use a new character in
ProofPower HOL.
However, ProofPower seems to be quite fussy about what
characters you use.
For example, there are three "spares" at the moment,
which would be useful for me. They wouldn
On 5 Jun 2009, at 08:35, Roger Bishop Jones wrote:
I quite often find that I want to use a new character in
ProofPower HOL.
However, ProofPower seems to be quite fussy about what
characters you use.
For example, there are three "spares" at the moment,
which would be useful for me. They wouldn
On 7 Jun 2009, at 11:39, Roger Bishop Jones wrote:
I have now a fairly complicated theory hierarchy
and its easy to mistakenly use a name which has already
been used somewhere.
I did this today and the resulting failure mode
seemed rather odd, so I wondered whether this is
how it is supposed t
Roger,
On 9 Jun 2009, at 07:23, Roger Bishop Jones wrote:
On Monday 08 June 2009 22:59:01 Rob Arthan wrote:
The name clash should definitely cause an error. Perhaps you are
catching the error somehow?
I don't think so.
Re-instating the error, I end up in a context in which
rbjmisc
On Tuesday 09 Jun 2009 2:28 pm, Roger Bishop Jones wrote:
> Rob,
>
>...
> In theory the attached tar file should enable you
> to reproduce the problem quickly.
And it did.
>
> ...
> It should fail in t018 after succeeding in building
> half a dozen other files.
>
> The two definitions of Set whic
Dear All,
I am happy to announce that OpenProofPower version 2.8.1 is now available from
the ProofPower web site:
http://www.lemma-one.com/ProofPower/getting/getting.html
Many thanks to all who helped with the new version and particularly Phil
Clayton of QinetiQ.
Regards,
Rob.
_
Dear All,
One of the changes in version 2.8.1 was a tidy-up of the holnormal
font, primarily intended to make tabs work nicely in xpp. I have just
discovered that this has a very useful side-effect: the font now works
properly in xterm, emacs, gvim and other programs with a traditional
te
Dear All,
I have just posted an update to version 2.8.1 of OpenProofPower that makes it
compatible with compilation systems that default to 64-bit architecture, e.g.
Apple's Xcode tools as supplied with Mac OS X 10.6 (Snow Leopard).
If xpp complains on start-up about invalid mnemonics for casca
Dear All,
Poly/ML 5.3 is likely to be released very soon. I have just posted a patch on
the ProofPower website that fixes a performance problem you will experience
if you compile using the latest development version of Poly/ML or with 5.3
when it is released.
As most people have fairly fast In
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.
>
On 14 Nov 2009, at 11:01, Igorj V wrote:
> trying t install OpenProofPower-2.7.8
> appears some error
>
> how to read build.log file?!
It is telling you that it failed while compiling file imp116.sml. The output
from the compilation will be in the file src/imp116.err. Have a look at that.
Re
t; symbol: +
> type: INTEGER
> :1.280771 Error: overloaded variable not defined at type
> symbol: +
> type: INTEGER
> Exception+ (Exception: Error: Error) abandoning file imp116.sml at line 5682
> *** (Exception: Stop: Stop) ***
>
>
> 2009/11/15 Rob Arthan
>
ase (tryed find -name
> '*ML_dbase*')
>
> ig...@igorj-laptop:~/Desktop/OpenProofPower-2.7.8$ ./configure
> Using /opt/pp as the installation target directory
> Using Poly/ML
> ERROR: The file "/usr/lib/poly/ML_dbase" does not exist
>
>
> 2009/1
Igorj,
Can you try running it like this to give some more diagnostic output:
PPENVDEBUG=y ../bin/pp_make_database -p hol demo
Regards,
Rob.
On 18 Nov 2009, at 13:18, Igorj V wrote:
> command pp_make_database -p hol receives such error ; what is missing?!
>
> ig...@igorj-laptop:/opt/pp/db$ .
th a) ; b) additional tasks on proofpower;
> just no idea what to read first from documentation on proofpower ?!
>
> 2009/11/18 Rob Arthan
> Igorj,
>
> Can you try running it like this to give some more diagnostic output:
>
> PPENVDEBUG=y ../bin/pp_make_database -
On 21 Nov 2009, at 04:40,
wrote:
> I've been trying to install ProofPower 2.8.1p2 on a very recent Ubuntu
> release (I'm sorry I don't have the precise release version right
> now).
Have a look at the file /etc/issue.
> So far I've just been trying to get 'xpp' installed. Having
> installe
On 21 Nov 2009, at 10:23, I wrote:
>
> On 21 Nov 2009, at 04:40,
> wrote:
>
>> I've been trying to install ProofPower 2.8.1p2 on a very recent Ubuntu
>> ...
>> So far I've just been trying to get 'xpp' installed. Having
>> installed tex, I tried configure:
>>
>> PPTARGETS="xpp" PPHOME=/
.
While this work was undertaken many years ago, it is a large-scale
example of a very direct and mathematically natural approach to
non-interference security properties that I believe still has many
features of interest.
Regards,
Rob Arthan
Frank Zeyda wrote:
Dear ProofPower Users,
I have the following problem, hope someone might be able to help.
At the moment I am trying to define a pretty printer "UTP" in order to
print certain terms in (mostly) Z expressions in a particular way. I
used the function set_printer from PrettyPrinter
Frank Zeyda wrote:
Hi Rob,
> As things stand it falls back to a default pretty-printer for HOL. I
> think the safest way to give you the facility you want would be to add
> an extra constructor (say PfRetry) to the data type PFUN_ANS allowing
> your pretty-printer to indicate explicitly tha
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?
Personally, I am happy with GPL (2 or 3).
Dear All,
Many thanks to Roger for making pp-contrib happen.
For reasons that I do not understand, the following reply to Phil's last
post arrived in the mailing list with "** SPAM **" in the subject line.
It is in the archive, but I expect it won't have got to many
subscribers. So I am tryin
Roger,
On 14/04/2010 15:12, 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).
On 14/04/2010 17:03, Roger Bishop Jones wrote:
On Wednesday 14 Apr 2010 16:07, Rob Arthan wrote:
Can you test texpdf on wrk066 from maths_egs? makeindex
produces some garbled entries resulting in LaTeX erros
when I try running it by hand.
No, doesn't work.
! Extra
On 6 Jul 2010, at 10:29, Roger Bishop Jones wrote:
> I find myself in puzzlement when trying to use the square
> subset symbol.
>
> When I use it I get an "Unknown extended character" error.
> If I try to add it (as if it were one of the unallocated
> codes) using "add_new_symbols" it complain
On 9 Aug 2010, at 19:20, Roger Bishop Jones wrote:
> ...The failure was connected with my trying (and failing) to
> redefine something defined in ProofPower.sty (instead of
> having my own special version of it).
> Does anyone know a way to override a definition in a style
> file (other than b
On 10 Aug 2010, at 17:08, Roger Bishop Jones wrote:
> ...
> \typeout{$Id: rbj.sty,v 1.2 2010-08-08 15:50:44 rbj Exp $}
> \NeedsTeXFormat{LaTeX2e}
> \ProvidesPackage{rbj}
> \RequirePackage{ProofPower}
> \RequirePackage{mathabx}
> \def\Zdef{\MMM{\corresponds}}
> \def\holindexon{\def\holin...@aux##1{
Roger,
On 17 Aug 2010, at 10:46, Roger Bishop Jones wrote:
> Here is a sequence of actions with ProofPower which is
> causing me puzzlement.
>
> :) set_merge_pcs ["unalg", "'latt2"];
>
> val it = () : unit
>
> :) add_%exists%_cd_thms [MkLat_recursion_lemma] "'latt2";
>
> val it = () : unit
>
Roger,
See attached.
Regards,
Rob.
rec.tgz
Description: Binary data
On 11 Jan 2011, at 09:14, Roger Bishop Jones wrote:
> Does anyone have a proof in ProofPower of a bijection
> between N and N x N.
> Or even an injection from N x N to N?
>
> Roger Jones
>
> __
As I thought, the mailing list scrubbed the attachment (at least in the
archive). If anyone else wants this, let me know and I will e-mail you direct.
Regards,
Rob.
On 11 Jan 2011, at 10:47, Rob Arthan wrote:
> Roger,
>
> See attached.
>
> Regards,
>
> Rob.
>
&g
Roger,
On 11 Jan 2011, at 12:03, Roger Bishop Jones wrote:
> Thanks Rob, that's great.
>
> Do you intend to add this to maths_egs?
It was originally destined for inclusion in ProofPower itself as part of a
recursive type definition package, but I keep failing to getting round to that.
Regards
On 18 Jan 2011, at 14:40, Roger Bishop Jones wrote:
> I am finding that if I give something the status of a binder
> before defining the constant, so that it can be used as a
> binder in the definition, the definition fails.
>
> The error message alleges that the binder occurs freely in
> the de
It is my pleasure to announce that the latest release of OpenProofPower,
version 2.9.1w2, is now available. The release incorporates bug fixes and
enhancements including the beginnings of support for higher-order matching in
the proof infrastructure and operation under the Cygwin platform on Mic
Oops! The URL should read:
http://www.lemma-one.com/ProofPower/getting/getting.html
and i forgot to mention find_thm (and associates) as a new feature that I have
been finding very useful.
Regards,
Rob.
On 1 Feb 2011, at 21:18, Rob Arthan wrote:
> It is my pleasure to announce that
Building OpenProofPower-2.9.1w2 has been found to fail on Cygwin on Vista: a
segmentation fault is reported in build.log and a stackdump pp-ml.exe.stackdump
is producied beginning with the line
Exception: STATUS_ACCESS_VIOLATION at eip=610E384A
If this happens to you, then first of all make sur
OpenProofPower version 2.9.1w2 incorporated a fix to a bug that made several of
the Z proof contexts fail to simplify certain expressions involving Z set
comprehensions. The PPRefinement example was sensitive to this fix. I have just
posted a replacement for PPRefinement.tgz that works with 2.9.
It is my plan to make some experimental releases of OpenProofPower leading
towards the next stable version over the next few months. I have just uploaded
an experimental release to:
http://www.lemma-one.com/ProofPower/getting/experimental/OpenProofPower-2.9.1w2.rda.110226.tgz
The idea is that
This really is me!
On 11 Mar 2011, at 12:46, Roger Bishop Jones wrote:
> It says you are missing the LaTeX epsf package.
> You could get that from ctan.org
Or on Ubuntu, install the package texlive-generic-recommended.
Regards,
Rob.
>
> Roger Jones
>
> __
Roger,
It works fine for me. What goes wrong?
Regards,
Rob.
On 27 Mar 2011, at 11:50, Roger Bishop Jones wrote:
> I have used today (possibly for the first time) the not a
> member of symbol in ProofPower HOL and find that it causes an
> error in pdflatex.
>
> The definition in ProofPower.s
Phil/Roger,
On 16 Apr 2011, at 02:55, Phil Clayton wrote:
> Roger,
>
> I think the short answer is to use the ProofPower exception mechanisms for
> readable exception messages.
>
Yes! Does this give you any problems, Roger?
> I presume you want e.g.
>
> raise General.Fail "%forall%";
>
>
Shu (with an aside to Phil, below),
Your answer's to Phil's questions make me suspect that this is a problem
specific to OpenMotif on Mac OS X. Here are a few more things to try:
a) To eliminate one small possibility can you check whether xpp still fails
with a segmentation fault if you run it
> seems it doesn't work :(
Regards,
Rob.
>
> Best Wishes!
>
> Shu
> On 17 Apr 2011, at 21:41, Rob Arthan wrote:
>
>> Shu (with an aside to Phil, below),
>>
>> Your answer's to Phil's questions make me suspect that this is a problem
On 12 Apr 2011, at 12:00, Phil Clayton wrote:
> 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 proo
Dear All,
I am looking at higher-order rewriting. The cleanest way to implement it will
involve adding an extra parameter to the functions prim_rewrite_conv,
prim_rewrite_rule and prim_rewrite_tac (which I suspect aren't very widely
used). The parameter value will be optional and supplying Nil
>
> I can see Z has complications for lambda abstractions not over U but
> expecting the domain condition as per z_%beta%_conv seems ok.
>
I think you will find there are several other complications - not least of
which will be working out what higher-order matching for Z ought to do.
Re
Phil,
On 5 Jun 2011, at 22:53, Phil Clayton wrote:
> 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
>
> E
Phil,
On 5 Jun 2011, at 12:10, Phil Clayton wrote:
> (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.
Phil,
The OpenMotif bug report suggests that if you use jpeg versions of the template
images, then things will work. You can find a tarball containing the jpegs you
need here:
http://dl.dropbox.com/u/34693999/ProofPower/template-jpegs.tgz
If you copy these into the bitmaps directory in the Pro
something different from what
LaTeX gives you out of the box. Note that \notin is not in the standard list of
mathematical symbols in the LaTeX User's Guide.
Regards,
Rob.
On 31 Mar 2011, at 14:26, Roger Bishop Jones wrote:
> On Tuesday 29 Mar 2011 16:48, Rob Arthan wrote:
>
>&
Roger,
On 10 Jul 2011, at 14:08, Roger Bishop Jones wrote:
> On Sunday 10 Jul 2011 12:22, Rob Arthan wrote:
>> Roger,
>>
>> I had put this on my list of things to fix by changing
>> \not\in in the style file to \notin, but I get exactly
>> the opposite probl
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 argument in a predicate stub (_?) isn't
>> implicitly converted to a predicate?
>>
>> A Z specification taking a Standard-compatible approach to booleans may
>> have:
>
treated as schema expressions. I think
the above slight complication (which is specific to conditionals or
user-defined things like them) is worth the improved uniformity of the new
approach.
Regards,
Rob.
On 11 Jul 2011, at 09:45, Rob Arthan wrote:
> Phil,
>
> On 6 Jul 2011, at
Roger,
On 10 Jul 2011, at 16:59, Roger Bishop Jones wrote:
> Rob,
>
> On Sunday 10 Jul 2011 15:59, you wrote:
>>
>> What happens if you just run doctex and then texdvi on
>> this file:
>>
>> http://dl.dropbox.com/u/34693999/ProofPower/rbj-not-in.te
>> x
>>
>> For me it fails on the second GFT
Phil,
On 12 Jul 2011, at 12:00, Phil Clayton wrote:
> I have updated mdt064.doc (attached) to add tests that demonstrate two
> printing issues relating to global variable names that contain strokes.
Many thanks for those. Good test cases are always appreciated.
>
>
> 1. Generic global variab
Phil,
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 to!)
>
> This issue was originall
I nearly always use Xpp with the following settings in $HOME/app-defaults/Xpp
Xpp*script.rows:32
Xpp*script.columns: 60
Xpp*script.background: white
Xpp*script.foreground: black
Xpp*journal.rows: 32
>
> Mark.
>
> on 22/7/11 3:10 PM, Rob Arthan wrote:
>
>> I nearly always use Xpp with the following settings in
>> $HOME/app-defaults/Xpp
>>
>> Xpp*script.rows:32
>> Xpp*script.columns: 60
Dear All,
It has taken a little bit longer than I would have hoped but I have just
completed a new experimental release of OpenProofPower. You can find it here:
http://www.lemma-one.com/ProofPower/getting/experimental/OpenProofPower-2.9.1w2.rda.110727.tgz
The idea is that an experimental releas
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 declaration.Yes. This needs to be fixed.I'm guessing this is the reason that stripping is not wo
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
>> s
Phil,
On 2 Aug 2011, at 16:26, Phil Clayton wrote:
> 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:
>>>
>>>>
Dear All,
I have just completed a new experimental release of OpenProofPower. You can
find it here:
http://www.lemma-one.com/ProofPower/getting/experimental/OpenProofPower-2.9.1w2.rda.110814.tgz
The idea is that an experimental release is a step toward the next stable
version (2.9.2 in this ca
Oops1
On 14 Aug 2011, at 16:18, Rob Arthan wrote:
> ...
> b) In xpp, you can now switch dynamically between the horizontal and vertical
> layout using a new item in the window geometry.
I meant "new item in the Window Menu&qu
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 sym
Phil,
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 is bad for peo
Phil,
On 17 Sep 2011, at 15:06, Phil Clayton wrote:
> 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] *
Begin forwarded message:
> From: ABZ2012
> Date: 22 December 2011 09:25:34 GMT
> To: Rob Arthan
> Subject: ABZ2012 remind deadline
>
> Dear Rob,
>
> I would like to recall you the ABZ submission deadline of Jan. 14th.
> I also kindly ask you, especially the tra
Begin forwarded message:
> From: ABZ2012
> Date: 9 January 2012 08:53:58 GMT
> To: Rob Arthan
> Subject: ABZ2012
>
> Dear Rob,
>
> after several requests, the ABZ deadline has been extended to Jan. 22.
> The conference web page will be updated soon.
> Pl
Begin forwarded message:
> From: ABZ2012
> Date: 31 January 2012 15:00:26 GMT
> To: Rob Arthan
> Subject: ABZ2012 short papers
>
> Dear Rob,
>
> this is a remind of the deadline, Feb. 3rd, for short paper submissions.
> Please, circulate this advertise among yo
On 31 Jan 2012, at 23:39, Phil Clayton wrote:
> Currently ProofPower doesn't build with SML/NJ. A patch is attached to fix
> this.
Thanks for that Phil. I will include this in the next release. Good to see that
the SML/NJ people seem to be active again.
Regards,
Rob.
__
Phil,
On 2 Feb 2012, at 19:36, Phil Clayton wrote:
> I meant to add that SML/NJ is 32 bit only so requires 32 bit libraries to
> build/run. On an x86_64 Fedora this can be achieved with
>
> yum install glibc-devel.i686 libgcc.i686
Thanks for the tip.
>
> Also, inside use_terminal (ProofPow
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
universal quantifier. Later on you w
1 - 100 of 221 matches
Mail list logo
