Re: [ProofPower] Test

[Phil Clayton]

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 regards,

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


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

Re: [ProofPower] HOLCONST

[Phil Clayton]

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 conversion evaluate your summ function.  I've included my steps below 
to build up such a conversion.  Hopefully you can see what's going on at 
each step.


Phil


(* Use plus1_conv to get the operand in the right form *)

plus1_conv ⌜3⌝;
(*
 * val it = ⊢ 3 = 2 + 1: THM
 *)

(* Convert the argument if non-zero then rewrite *)

(RAND_C (TRY_C plus1_conv) THEN_C pure_once_rewrite_conv [get_spec 
⌜summ⌝]) ⌜summ 0⌝;
(RAND_C (TRY_C plus1_conv) THEN_C pure_once_rewrite_conv [get_spec 
⌜summ⌝]) ⌜summ 3⌝;

(*
 * val it = ⊢ summ 0 = 0: THM
 * val it = ⊢ summ 3 = summ 2 + 2 + 1: THM
 *)

(* Give this conversion a name and define a conversion that
 * recursively applies it to the left operand of the resulting
 * '+' term until is fails *)

val summ_step_conv =
  RAND_C (TRY_C plus1_conv) THEN_C pure_once_rewrite_conv [get_spec 
⌜summ⌝];

fun summ_conv t = (summ_step_conv THEN_TRY_C LEFT_C summ_conv) t;

summ_conv ⌜summ 0⌝;
summ_conv ⌜summ 3⌝;
(*
 * val it = ⊢ summ 0 = 0: THM
 * val it = ⊢ summ 3 = ((0 + 0 + 1) + 1 + 1) + 2 + 1: THM
 *)

(* Add up the resulting '+' tree *)

(summ_conv THEN_C MAP_C plus_conv) ⌜summ 3⌝;
(*
 * val it = ⊢ summ 3 = 6: THM
 *)


(* We want summ_conv to reduce the '+' terms so sum as we go.
 * Redefine the above. *)

val summ_step_conv =
  RAND_C (TRY_C plus1_conv) THEN_C pure_once_rewrite_conv [get_spec 
⌜summ⌝] THEN_C TRY_C (RIGHT_C plus_conv);


summ_step_conv ⌜summ 0⌝;
summ_step_conv ⌜summ 3⌝;
(*
 * val it = ⊢ summ 0 = 0: THM
 * val it = ⊢ summ 3 = summ 2 + 3: THM
 *)

fun summ_conv t =
  (summ_step_conv THEN_TRY_C (LEFT_C summ_conv THEN_C plus_conv)) t;

summ_conv ⌜summ 0⌝;
summ_conv ⌜summ 3⌝;
(*
 * val it = ⊢ summ 0 = 0: THM
 * val it = ⊢ summ 3 = 6: THM
 *)

map summ_conv (map (fn n => mk_app (⌜summ⌝, mk_ℕ (integer_of_int n))) 
(interval 0 50));

(*
 * val it =
 *[⊢ summ 0 = 0, ⊢ summ 1 = 1, ⊢ summ 2 = 3, ⊢ summ 3 = 6,
 * ⊢ summ 4 = 10, ⊢ summ 5 = 15, ⊢ summ 6 = 21, ⊢ summ 7 = 28,
 * ⊢ summ 8 = 36, ⊢ summ 9 = 45, ⊢ summ 10 = 55,
 * ⊢ summ 11 = 66, ⊢ summ 12 = 78, ⊢ summ 13 = 91,
 * ⊢ summ 14 = 105, ⊢ summ 15 = 120, ⊢ summ 16 = 136,
 * ⊢ summ 17 = 153, ⊢ summ 18 = 171, ⊢ summ 19 = 190,
 * ⊢ summ 20 = 210, ⊢ summ 21 = 231, ⊢ summ 22 = 253,
 * ⊢ summ 23 = 276, ⊢ summ 24 = 300, ⊢ summ 25 = 325,
 * ⊢ summ 26 = 351, ⊢ summ 27 = 378, ⊢ summ 28 = 406,
 * ⊢ summ 29 = 435, ⊢ summ 30 = 465, ⊢ summ 31 = 496,
 * ⊢ summ 32 = 528, ⊢ summ 33 = 561, ⊢ summ 34 = 595,
 * ⊢ summ 35 = 630, ⊢ summ 36 = 666, ⊢ summ 37 = 703,
 * ⊢ summ 38 = 741, ⊢ summ 39 = 780, ⊢ summ 40 = 820,
 * ⊢ summ 41 = 861, ⊢ summ 42 = 903, ⊢ summ 43 = 946,
 * ⊢ summ 44 = 990, ⊢ summ 45 = 1035, ⊢ summ 46 = 1081,
 * ⊢ summ 47 = 1128, ⊢ summ 48 = 1176, ⊢ summ 49 = 1225,
 * ⊢ summ 50 = 1275]: THM list
 *)


On 31/03/20 17:09, David Topham wrote:
I have  been able to get the length sample for HOLCONST from user013 to 
work, but when I try

my own function, I get an error.  Can anyone see what my problem is?
I suspect it may be setting the correct proof context since I needed to 
add set_pc "hol2"
to get the length function to work. I have tried several contexts such 
as "lin_arith", "R", "misc", but I have not seen how to find the correct 
one (if that is even the problem).


This one OK:
:) force_delete_theory "cs113" handle Fail _ => ();
val it = (): unit
:) open_theory "hol";  new_theory "cs113";
val it = (): unit
val it = (): unit
:) set_pc "hol2";
val it = (): unit
:) ⓈHOLCONST
:# │ length:'a LIST→ℕ
:# ├──
:# │           length [] = 0
:# │ ∧ ∀ h t⦁  length (Cons h t) = length t + 1
:# │
:# ■
val it = ⊢ length [] = 0 ∧ (∀ h t⦁ length (Cons h t) = length t + 1): THM
:) get_spec⌜length⌝;
val it = ⊢ length [] = 0 ∧ (∀ h t⦁ length (Cons h t) = length t + 1): THM
:) rewrite_conv[get_spec⌜length⌝] ⌜length [1;2;3;4]⌝;
val it = ⊢ length [1; 2; 3; 4] = 4: THM

But not this one:

:) ⓈHOLCONST
:# │ summ:ℕ→ℕ
:# ├──
:# │       summ 0 = 0
:# │ ∧ ∀n⦁ summ (n + 1) = (summ n) + (n + 1)
:# │
:# ■
val it = ⊢ summ 0 = 0 ∧ (∀ n⦁ summ (n + 1) = summ n + n + 1): THM
:# get_spec⌜summ⌝;
val it = ⊢ summ 0 = 0 ∧ (∀ n⦁ summ (n + 1) = summ n + n + 1): THM
:) rewrite_conv[get_spec⌜summ⌝] ⌜summ 2⌝;
Exception Fail * no rewriting occurred [rewrite_conv.26001] * raised



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



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

Re: [ProofPower] Distributed concatenation symbol

[Phil Clayton]

Rob,

[A somewhat belated response now.  I only noticed the delivery failure 
from December 2016 today!  Trying again...]


On 27/11/16 14:21, Rob Arthan wrote:

Dear All,

Roger Jones and I are doing some more work on Unicode and UTF-8 support 
in ProofPower.
We are currently considering two changes to the Unicode mapping as 
currently defined at:


http://www.lemma-one.com/ProofPower/unicode/pp-unicode.html

1) Supporting Unicode/UTF-8 in xpp and the various document-processing 
scripts would be
much simpler, if each character in the ProofPower extended character set 
mapped to a single
Unicode code point. Currently the only exception is the symbol for 
distributed concatenation
which has to be translated into two code points (a frown followed by a 
slash). Since frown-slash
is already accepted as a synonym for the single character for 
distributed concatenation we
would like to withdraw the single character mark-up from the ProofPower 
Z library.


I think this is a change for the better anyway.


2) We would like to use the MathML XML entity set as a standard set of 
human-readable
names for Unicode code points. However, there a few slight discrepancies 
that need to be resolved:
At Phil Clayton’s (nice) suggestion, the ProofPower mapping currently 
maps the greek
letters to the corresponding code points for Mathematical Alphanumeric 
Symbols in the range
1D400–1D7FF. The MathML entities use the code points for Greek in the 
range 0370–03FF.
The Mathematical Greek Symbols do look nice, but to gain compatibility 
with MathML,
we would like to revert to using the code points for Greek in the range 
0370-03FF.
This will also allow you to enter Greek by switching to a  standard 
Greek keyboard mapping.
In passing we will also use the right symbol for φ (the current mapping 
uses what LaTeX

calls \varphi rather than \phi).

Any comments on this would be appreciated.


I have no objection to this change but it doesn't appear that the 
mathematical Greek symbols are incompatible with MathML.  Looking at the 
MathML 3.0 standard, in particular section 7.5, doesn't MathML support 
the Mathematical Alphanumeric Symbols of Unicode using the mathvariant 
attribute?  That is, characters in the range 1D400–1D7FF are variants of 
corresponding unstyled characters in the BMP (plane 0).  Section 7.5 
also says:


  A MathML processor must treat a mathematical alphanumeric character
  (when it appears) as identical to the corresponding combination of
  the unstyled character and mathvariant attribute value.

Have I misunderstood?

Are you defining MathML markup for Z?

Regards,
Phil

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

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

[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 
To: proofpower@lemma-one.com

Hi Mark,

On 15/06/17 10:29, Mark Adams wrote:

Hi Phil,

On 15/06/2017 10:24, Phil Clayton wrote:

...
Can you try the following to make
sure you have the required packages installed:

  dnf install \
gcc-c++ \
texlive-latex texlive-epsf \
ed \
motif motif-devel \
libXp-devel.x86_64 \
libXext-devel.x86_64 \
libXmu-devel.x86_64 \
libXt-devel.x86_64 \
xorg-x11-fonts-misc

and see how it goes with 3.1w7.


It all works now.  I was missing texlive-epsf.  I wonder whether/where 
it is documented anywhere that this is needed..


I think the system requirements just say that TeX/LaTeX is required and 
suggest Tex-Live or teTeX installations.  The issue here is that 
TeX-Live is provided by several Fedora packages, presumably because it 
is so large, that are not all installed by default.  If every Tex-Live 
package was installed, this wouldn't be an issue.  There should have 
been an error message saying "can't find espf.sty" or similar in the log 
file for dtd017.



Incidentally, if I try building ProofPower 3.1w6 with Poly/ML 5.6, I 
get further still in processing dev.mkf, but it fails this time with:


  Compiling (code) imp002.sml
  dev.mkf:349: recipe 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?


Which log file?


The one with the output from processing imp002.doc, which will probably 
be called imp002.ldd (as this is the target mentioned in the Make error 
above) but could be called imp002.err.  It should be the last modified 
file in the list given by

  ls -ltr src/*/* | tail

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 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/001178.html 
You would need to apply the patch in that message.


Poly/ML 5.6 should work though.

Poly/ML 5.5 is quite old and doesn't have polyc so I can't see how
ProofPower 3.1w7 can build with that version, even though the website
say that it does.  There are also versions 5.5.1 and 5.5.2 which do
provide polyc.

Poly/ML release dates are as follows:

  5.7 2017-05-12
  5.6 2016-01-25
  5.5.2   2014-05-13
  5.5.1   2013-11-18
  5.5 2012-09-14

See https://sourceforge.net/projects/polyml/files/polyml/

Phil


On 15/06/17 00:39, Mark Adams wrote:

Hi,

I'm getting problems installing ProofPower 3.1w7 on Fedora 24 with 
Poly/ML 5.7.


The first thing that looks wrong is that, even though I have 
OpenMotif installed, running ./configure complains that it can't 
find it.



yum install openmotif

...
Package motif-2.3.4-11.fc24.x86_64 is already installed, skipping.
Dependencies resolved.
Nothing to do.
Complete!


./distclean
PPHOME=`pwd` PPPOLYHOME=/usr/programs/polyml/polyml-5.7 ./configure

Using /usr/programs/pp/pp-3.1w7 as the installation target directory
Using Poly/ML from /usr/programs/polyml/polyml-5.7
Using dynamic linking for Motif
WARNING: Motif installation not found
Using 50 for the size of the labelled product cache
Generating code to install the following packages: pptex dev xpp 
hol zed daz
If you are happy with these settings, now run ./install to install 
ProofPower.


But ./install seems to fail for another reason:


./install

OpenProofPower installation begins [Wed Jun 14 21:41:19 2017] ...
Moving to build directory /usr/programs/pp/pp-3.1w7/src
Building pptex dev xpp hol zed daz
See /usr/programs/pp/pp-3.1w7/build.log for messages
install: installation failed; see 
/usr/programs/pp/pp-3.1w7/build.log for more details


Last few lines of build.log:

echo "use\"polyml-build.sml\";" | poly > slrp-bin.log 2>&1
polyc -o slrp-bin slrp-bin.o
Error: slrp-bin.o: No such file
Usage: polyc [OPTION]... [SOURCEFILE]
dev.mkf:174: recipe for target 'slrp-bin' failed
make: *** [slrp-bin] Error 1

I get the same problem if I use Poly/ML 5.5.

Regards,
Mark.

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


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




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

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

[Phil Clayton]

Hi Mark,

On 15/06/17 07:05, Mark Adams wrote:

Thanks very much for that Phil.

This definitely helps but I still get failure for Poly/ML 5.6..

Installing openmotif-devel clears up the Motif problem.

Regarding Poly/ML, yes when I look closer, the failure recorded in 
build.log is indeed different for Poly/ML 5.5:


  echo "use\"polyml-build.sml\";" | poly > slrp-bin.log 2>&1
  polyc -o slrp-bin slrp-bin.o
  make: polyc: Command not found
  dev.mkf:174: recipe for target 'slrp-bin' failed
  make: *** [slrp-bin] Error 127

So for 5.5 it's Error 127, but for 5.7 it's Error 1.


So Poly/ML 5.5 fails as expected: polyc not found.  That error code is 
probably from the shell.


For Poly/ML 5.7, polyc can't find the file slrp-bin.o specified as a 
argument.  That error code is probably from polyc.


There error codes aren't particularly useful.  There is usually an error 
message in the log file for the failing source file that gives more 
details about what went wrong.  This is usually the last file written, 
which you can find with

  ls -ltr src/*/* | tail


Anyway, Poly/ML 5.6 gets further in processing dev.mkf but still fails, 
this time with:


  doctex  dtd017.doc
  texdvi -b dtd017 > dtd017.dvi.ldd1 I haven't yet applied the patch for ProofPower 3.1.w7 (which shouldn't 
be necessary because I'm using Poly/ML 5.6).


Correct, Poly/ML 5.6 should work fine.  It looks like 5.6 is failing 
whilst building the documentation.  Can you try the following to make 
sure you have the required packages installed:


  dnf install \
gcc-c++ \
texlive-latex texlive-epsf \
ed \
motif motif-devel \
libXp-devel.x86_64 \
libXext-devel.x86_64 \
libXmu-devel.x86_64 \
libXt-devel.x86_64 \
xorg-x11-fonts-misc

and see how it goes with 3.1w7.


Incidentally, if I try building ProofPower 3.1w6 with Poly/ML 5.6, I get 
further still in processing dev.mkf, but it fails this time with:


  Compiling (code) imp002.sml
  dev.mkf:349: recipe 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 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/001178.html 


You would need to apply the patch in that message.

Poly/ML 5.6 should work though.

Poly/ML 5.5 is quite old and doesn't have polyc so I can't see how
ProofPower 3.1w7 can build with that version, even though the website
say that it does.  There are also versions 5.5.1 and 5.5.2 which do
provide polyc.

Poly/ML release dates are as follows:

  5.7 2017-05-12
  5.6 2016-01-25
  5.5.2   2014-05-13
  5.5.1   2013-11-18
  5.5 2012-09-14

See https://sourceforge.net/projects/polyml/files/polyml/

Phil


On 15/06/17 00:39, Mark Adams wrote:

Hi,

I'm getting problems installing ProofPower 3.1w7 on Fedora 24 with 
Poly/ML 5.7.


The first thing that looks wrong is that, even though I have 
OpenMotif installed, running ./configure complains that it can't find 
it.



yum install openmotif

...
Package motif-2.3.4-11.fc24.x86_64 is already installed, skipping.
Dependencies resolved.
Nothing to do.
Complete!


./distclean
PPHOME=`pwd` PPPOLYHOME=/usr/programs/polyml/polyml-5.7 ./configure

Using /usr/programs/pp/pp-3.1w7 as the installation target directory
Using Poly/ML from /usr/programs/polyml/polyml-5.7
Using dynamic linking for Motif
WARNING: Motif installation not found
Using 50 for the size of the labelled product cache
Generating code to install the following packages: pptex dev xpp hol 
zed daz
If you are happy with these settings, now run ./install to install 
ProofPower.


But ./install seems to fail for another reason:


./install

OpenProofPower installation begins [Wed Jun 14 21:41:19 2017] ...
Moving to build directory /usr/programs/pp/pp-3.1w7/src
Building pptex dev xpp hol zed daz
See /usr/programs/pp/pp-3.1w7/build.log for messages
install: installation failed; see /usr/programs/pp/pp-3.1w7/build.log 
for more details


Last few lines of build.log:

echo "use\"polyml-build.sml\";" | poly > slrp-bin.log 2>&1
polyc -o slrp-bin slrp-bin.o
Error: slrp-bin.o: No such file
Usage: polyc [OPTION]... [SOURCEFILE]
dev.mkf:174: recipe for target 'slrp-bin' failed
make: *** [slrp-bin] Error 1

I get the same problem if I use Poly/ML 5.5.

Regards,
Mark.

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

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

[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:

http://lemma-one.com/pipermail/proofpower_lemma-one.com/2017-May/001178.html
You would need to apply the patch in that message.

Poly/ML 5.6 should work though.

Poly/ML 5.5 is quite old and doesn't have polyc so I can't see how 
ProofPower 3.1w7 can build with that version, even though the website 
say that it does.  There are also versions 5.5.1 and 5.5.2 which do 
provide polyc.


Poly/ML release dates are as follows:

  5.7 2017-05-12
  5.6 2016-01-25
  5.5.2   2014-05-13
  5.5.1   2013-11-18
  5.5 2012-09-14

See https://sourceforge.net/projects/polyml/files/polyml/

Phil


On 15/06/17 00:39, Mark Adams wrote:

Hi,

I'm getting problems installing ProofPower 3.1w7 on Fedora 24 with 
Poly/ML 5.7.


The first thing that looks wrong is that, even though I have OpenMotif 
installed, running ./configure complains that it can't find it.



yum install openmotif

...
Package motif-2.3.4-11.fc24.x86_64 is already installed, skipping.
Dependencies resolved.
Nothing to do.
Complete!


./distclean
PPHOME=`pwd` PPPOLYHOME=/usr/programs/polyml/polyml-5.7 ./configure

Using /usr/programs/pp/pp-3.1w7 as the installation target directory
Using Poly/ML from /usr/programs/polyml/polyml-5.7
Using dynamic linking for Motif
WARNING: Motif installation not found
Using 50 for the size of the labelled product cache
Generating code to install the following packages: pptex dev xpp hol zed 
daz
If you are happy with these settings, now run ./install to install 
ProofPower.


But ./install seems to fail for another reason:


./install

OpenProofPower installation begins [Wed Jun 14 21:41:19 2017] ...
Moving to build directory /usr/programs/pp/pp-3.1w7/src
Building pptex dev xpp hol zed daz
See /usr/programs/pp/pp-3.1w7/build.log for messages
install: installation failed; see /usr/programs/pp/pp-3.1w7/build.log 
for more details


Last few lines of build.log:

echo "use\"polyml-build.sml\";" | poly > slrp-bin.log 2>&1
polyc -o slrp-bin slrp-bin.o
Error: slrp-bin.o: No such file
Usage: polyc [OPTION]... [SOURCEFILE]
dev.mkf:174: recipe for target 'slrp-bin' failed
make: *** [slrp-bin] Error 1

I get the same problem if I use Poly/ML 5.5.

Regards,
Mark.

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




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

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

[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?

Phil


On 13/05/17 04:44, Hugh Anderson wrote:


Hi - I just tried using SMLNJ instead of polyML, but I got the same 
error at the same place...


Cheers Hugh

On Sat, 13 May 2017, Hugh Anderson wrote:



Hi - I am trying to install ProofPower-Z using my new mac/Sierra machine,
using polyml, installed from brew: Poly/ML 5.7 Release RTS version: 
X86_64-5.6

  ...

Hugh Anderson E-mail: h...@comp.nus.edu.sg
SoC, National University of Singapore http://www.comp.nus.edu.sg/~hugh

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




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

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

[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, giving --enable-intinf-as-int as an argument 
to ./configure would avoid this issue.  However, I have just discovered 
that the build still won't work.  With Poly/ML 5.7, I get a build 
failure in imp108.sml because the types int and FixedInt.int are not the 
same.  This seems to be a change between Poly/ML 5.6.1 Testing and the 
final Poly/ML 5.7.


The attached patch should fix both issues and allow you to build with 
Poly/ML 5.7.  I have only tested on my Fedora machine.  Apply as usual, 
according to the instructions here:

http://www.lemma-one.com/ProofPower/patches/patches.html

Regards,
Phil

On 13/05/17 04:20, Hugh Anderson wrote:


Hi - I am trying to install ProofPower-Z using my new mac/Sierra machine,
using polyml, installed from brew: Poly/ML 5.7 Release RTS version: 
X86_64-5.6


I applied the MAC patch in the OpenProofPower-3.1w7 directory:

 Hughs-MacBook:OpenProofPower-3.1w7 hugh$ cat 
../patch-3.1.rda.20170310.diff| patch -p1 -b -B orig/

patching file configure
Hunk #1 FAILED at 25.
Hunk #3 FAILED at 71.
2 out of 6 hunks FAILED -- saving rejects to file configure.rej
patching file src/hol/hol.mkf
patching file src/pptex/imp096.doc
patching file src/xpp/imp096.doc
 Hughs-MacBook:OpenProofPower-3.1w7 hugh$

These two hunks did not seem important to me, so I carried on, but the 
configure failed. The offending part seemed to be attempting to build 
slrp-bin:


Hughs-MacBook:OpenProofPower-3.1w7 hugh$ tail -7 build.log
   docsml -f hol.svf imp018
   docsml -f hol.svf dtd017
   echo "use\"polyml-build.sml\";" | poly > slrp-bin.log 2>&1
   polyc -o slrp-bin slrp-bin.o
   Error: slrp-bin.o: No such file
   Usage: polyc [OPTION]... [SOURCEFILE]
   make: *** [slrp-bin] Error 1
 Hughs-MacBook:OpenProofPower-3.1w7 hugh$

I had a look at the src/dev/slrp-bin.log file, and found two errors like 
this:


imp001.sml:825: error: Type error in function application.
   Function: o : (int -> int) * (Time.time -> int) -> Time.time -> int
   Argument:
  (
 TimeInt.toInt,
 (
 case units of
Microseconds => Time.toMicroseconds |
Milliseconds => Time.toMilliseconds |
... => ...)
 ) : (int -> int) * (Time.time -> LargeInt.int)
   Reason:
  Can't unify int (*In Basis*) with LargeInt.int (*In Basis*)
 (Different type constructors)
Found near
  TimeInt.toInt o
  (
  case units of
 Microseconds => Time.toMicroseconds |
 Milliseconds => Time.toMilliseconds |
 Seconds => Time.toSeconds)
...
Exception- Fail "Static Errors" raised

So - is there some update or patch I can apply? This all worked fine for 
me on my old mac :) - maybe an  El Capitan / Sierra change? Or a change to

sml/time declarations?

Can anyone help? Cheers Hugh

Hugh Anderson E-mail: h...@comp.nus.edu.sg
SoC, National University of Singapore http://www.comp.nus.edu.sg/~hugh

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






patch-3.1w7-pbc-20170513.diff.gz
Description: application/gzip
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

[ProofPower] z_app_thm

[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 the domain of 
f, so the theorem could state


  ∀ a : 𝕌; f : 𝕌; x, y : 𝕌
⦁ (∀ f_a : 𝕌 | (a, f_a) ∈ f ⦁ f_a = x) ∧ (a, y) ∈ f ⇒ f a = x

As it stands, I suspect there could be some unnecessary proof overhead 
for users (and perhaps in the PP implementation) because it may be 
necessary to forward chain with the left antecedent, once established, 
and eliminate a variable to get the form required by z_app_thm.


I think other proof operations like z_app_eq_tac and z_app_λ_rule would 
naturally become simpler:


  - z_app_eq_tac could return a goal containing
  ... ∧ (∃ v : 𝕌 ⦁ (a, v) ∈ f)
so we can choose any v, instead of
  ... ∧ (a, v) ∈ f

  - z_app_λ_rule would not include the predicate V' = x in the
antecedents.

Phil

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

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

[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 
adding/stripping into the assumtions, e.g.

a (strip_asm_tac (z_%forall%_elim %SZT% y %>% z_id_%bij%_thm));

Phil


28/05/15 17:18, YuHui Lin wrote:

Dear all,

I get the following error when I tried to instantiated a forall quantifier in 
an assumption which I inserted using asm_tac.

   Exception Fail * Trying to instantiate type variable 'a, which occurs in 
assumption list [z_∀_elim.6006] * raised

The following dummy example can replay this error

set_goal ([], %SZT% %forall% x : %int%; y : %pset% %int% %=>% x %mem% y %or% x 
%notmem% y %>%);
a  (strip_tac);a  (strip_tac);a  (strip_tac);
a (asm_tac z_id_%bij%_thm);
a (z_spec_nth_asm_tac 1 %SZT% y %>%);


What does this error mean ? Where did I do wrong here ? Thanks in advance.


best,
Yuhui




-
We invite research leaders and ambitious early career researchers to
join us in leading and driving research in key inter-disciplinary themes.
Please see www.hw.ac.uk/researchleaders for further information and how
to apply.

Heriot-Watt University is a Scottish charity
registered under charity number SC000278.


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




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

Re: [ProofPower] OpenProofPower 3.1w5

[Phil Clayton]

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 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)
(Similarly for SLRPSTARTCMD in dev.mkf)
Is there any reason for that?


The idea of polyc was to prevent you having to do that
kind of thing.


polyc ducks the issue of the run path though.  I raised this with David 
when polyc first appeared - see the thread starting here:

http://lists.inf.ed.ac.uk/pipermail/polyml/2013-April/001216.html

David was concerned that some linkers may not support rpaths and did not 
know of any way to check with autotools.  Also, there was some concern 
about Linux distributions with objects to rpaths - for example see 
discussion starting "Libtool's use of `-rpath'..." at

https://www.sourceware.org/autobook/autobook/autobook_88.html
(where the authors of Libtool say "using rpath is a good thing".)



I don’t know how it achieves it because it doesn't set
LD_RUN_PATH (or Mac OS equivalent), but I don’t
have this problem on any system I have tried.
I have just installed it on Kubuntu 12.10 having made sure that
LD_RUN_PATH and LD_LIBRARY_PATH are not set and
it works.


Did you specify a prefix when you installed Poly/ML?  The problem occurs 
only when Poly/ML is installed to a non-system location, i.e. where the 
libraries are in a location not known to ld.




Unfortunately, because the makefiles defend themselves against polyc
not being there. it is a a bit difficult to tell exactly what happened
during the build. Can you unset LD_RUN_PATH and then
try this starting from  the build directory (assuming you have done
a build and haven’t cleaned up after it):

cd src/hol
polyc -o xyz pp-ml.o
xyz hol.polydb


[...@rizzo OpenProofPower-3.1w5]$ unset LD_RUN_PATH
[...@rizzo OpenProofPower-3.1w5]$ cd src/hol/
[...@rizzo hol]$ polyc -o xyz pp-ml.o
[...@rizzo hol]$ ./xyz hol.polydb
./xyz: error while loading shared libraries: libpolyml.so.6: cannot open 
shared object file: No such file or directory




That should start an HOL session. If it doesn’t then I think there
is a bug in polyc on your system and we should manufacture a
cut-down example and report it.


As noted, this behaviour of polyc is expected.  In fact, this is why 
--disable-shared became the default when building Poly/ML.  The upshot 
of the previous discussion was that users should either

 A. use the non-shared version
 B. add their installation to the ld config, /etc/ld.so.conf
or, as discussed
 C. set LD_LIBRARY_PATH if installed to a non-system location
(Are there any others?)

Whilst LD_RUN_PATH=... does work with polyc, I've now realized that that 
doesn't work for Mac OS X.  Possibly Mac OS X needs additional 
arguments, e.g. -Wl,-rpath,$(POLYML_LIBDIR), but polyc has no mechanism 
to pass additional arguments, if I remember correctly.


It's not a major issue for me - I can just build ProofPower with a 
static Poly/ML.  I just mentioned it to make ProofPower more portable.


Regards,
Phil


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

Re: [ProofPower] OpenProofPower 3.1w5

[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

  LD_RUN_PATH=$(LD_RUN_PATH)
(Similarly for SLRPSTARTCMD in dev.mkf)
Is there any reason for that?

Regards,

Phil


On 18/04/15 14:08, Rob Arthan wrote:

Dear All,

I am happy to announce that OpenProofPower version 3.1w5 is now available.
You can read about it and download it from:

http://www.lemma-one.com/ProofPower/getting/getting.html

The main change since version 3.1w4 is support for Unicode and UTF-8.
Setting the flag output_in_utf8 true in a ProofPower session, causes output
to use UTF-8 rather than the ProofPower extended character set. Likewise
setting the input_in_utf8 true makes the session expect subsequent input
to be UTF-8 encodings. The UTF-8 support is currently mainly targeted
at people who are programming their own GUIs and need to interface
to GUI toolkits using UTF-8. The document preparation system and xpp
do not yet support UTF-8.

Note that this version does not work with Standard ML of New Jersey,
due to a bug in that compiler’s handling of hexadecimal character
constants.

Regards,

Rob.


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




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

Re: [ProofPower] Updated Unicode translation scheme

[Phil Clayton]

  
  
On 30/03/15 22:15, Anthony Hall wrote:


  
  
  
  
Thanks
Rob

  
My problem
  is that I need a lexical translation scheme that is not
  just specific to Z, but one that makes sense for any of
  the open-ended set of languages that ProofPower supports.
  I certainly don’t want to translate ASCII characters to
  non-ASCII.
  
  
 
  
  
I just don’t
  think ISO Z got this right. 
I’m
certainly not going to disagree with you there!
  

  


I don't think ISO is quite right either.  Generally in text, I do
think the minus operator (whether prefix or infix) should be the '−'
character (0x2212 MINUS SIGN).  I've had the misfortune to write a
lot of technical documents with Word and a normal ASCII dash '-'
(0x2D HYPHEN-MINUS) just isn't wide enough for minus, so I am fairly
used to doing Insert -> Symbol -> Minus sign.  In OpenOffice,
ASCII dash is wide enough with a few fixed-width fonts (Courier,
Nimbus Mono L) however with others (Liberation Mono, DejaVu Sans
Mono) it is not and nor is it with variable-width fonts.

With Fuzz, it appers that ASCII '-' (0x2D HYPHEN-MINUS) is mark up
for a full width minus sign, so the problem with writing non-ASCII
is avoided.


  

  
It is easy
  to design a grammar that allows the same symbol (a minus
  sign) to function both as an infix operator and a prefix
  operator. However, I failed to realise the importance of
  this before the Standards committee ran off and committed
  to the backwards incompatible change that gave you “a lot
  of trouble".
I
do sometimes wonder what they thought they were up to. I
think sometimes people get so deep into solving a
problem that they can’t step back and see that the
problem isn’t real at all. As you say, a single symbol
can perfectly well be used – and is, by everyone else in
the world.
  

  


Spivey uses one symbol for both unary and binary minus but the unary
minus is an ordinary function.  Presumably the Standards committee
wanted a template for unary minus so that, for example,
  − − x
is not parsed as
  (− −) x
which seems sensible.  The Standard also requires that the mapping
from operator words in templates to tokens is a function.  This
prevents '−' from being both the PRE and I tokens, so can't be used
in both prefix and infix templates.  The reason for this, I suspect,
is all tied up with the Z concrete syntax: using '−' for both prefix
and infix minus would make
  f − x
ambiguous — is that
  App (f, − x)
or
  App (_ − _, (f, x))
?
Tightening up the concrete syntax to allow operator words to be
reused in templates would require a little thought.  Alternatively,
perhaps operator words could be reused by defining a fixed
precedence on operator word tokens with the same word, for example,
an I token takes priority over a PRE token.  After all,
  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 interoperability between
  ProofPower-Z and ISO Z at the same time. Inside
  ProofPower, interoperability with ISO Z and ProofPower-Z
  is best implemented using parsed syntax trees rather than
  lexical token streams. 
I
can see the force of that – in fact the “lot of trouble”
was precisely having to parse the specification rather
than just lex it.
 
Of course,
  perhaps one day, the Z Word Tools as a common front-end
  will also be an option.
The
trouble is that to go from ProofPower to ISO Z that
translation would have to be done, and again I would
have to have a parse tree from ProofPower to do it. I
haven’t thought any more since our conversations of
years ago about how a ZWT / Proofpower interface might
work (and maybe such a thing wouldn’t be useful anyway),
so my post was a bit of a knee-jerk reaction h

Re: [ProofPower] Unicode and ProofPower

[Phil Clayton]

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 underscores like the ProofPower
glyphs.  One option is
298B LEFT SQUARE BRACKET WITH UNDERBAR
298C RIGHT SQUARE BRACKET WITH UNDERBAR
They appear as ⦋ (298B) and ⦌ (298C) but I think they're too close to
refinement symbols.  I think this could be a case where you probably
want to combine another glyph with the existing parenthesis using the
combining diacritics.  I think the best options are
0331 COMBINING MACRON BELOW
which gives ̱( ̱)
These work in my email client and terminal.  Alternatively
0332 COMBINING LOW LINE
which gives (̲ )̲
These don't overlay correctly in my email client or terminal but are a
single wide character.


I am chary about using the COMBINING characters as it seems likely to
increase the chances that any given text-processing system will go wrong
in some way. The use of underlined brackets in the ProofPower font was a
bit of an arbitrary choice. So I have changed to the following which
look like the beginning and end of underlining.

2A3D RIGHTHAND INTERIOR PRODUCT: ⨽
2A3C INTERIOR PRODUCT: ⨼


I agree that it could be too soon to depend on combining characters. 
The less common ones aren't quite working on my 3-4 year old Linux 
installation.  These new characters don't sit quite as low as one would 
like, to emphasize underlining, but I can't suggest anything better 
without combining characters.




For epsilon, I can see why
03F5 GREEK LUNATE EPSILON SYMBOL
has been used instead of
03B5 GREEK SMALL LETTER EPSILON
- it is the correct shape for the equivalent LaTeX character.


I don’t know why we used \varepsilon in LaTeX rather than \epsilon for
this. (I think there is slight tendency to use the lunate epsilon for
the Hilbert choice operator in the literature, but the ordinary is often
used too and seems to be more common these days, and in Z you expect it
just to be the ordinary greek letter.)
l

 I was finding that the lunate epsilon is very similar to the
membership operator.  The lower case LaTeX mathematical greek letters
appear italicized so I wonder whether the standard should have used e.g.
𝜃 (1D703) instead of θ (03B8)
𝜆 (1D706) instead of λ (03BB)
𝜇 (1D707) instead of μ (03BC)
so you would have chosen
𝜖 (1D716) instead of ϵ (03F5)
That would have meant also that any Greek authors of Z don't find
themselves deprived of certain letters.  As things stand, I agree with
your choice.



I think it is an excellent idea to use the mathematical greek letters. I
have done that, fixing a mistake with 𝜓 in passing and treating epsilon
the same as all the others now.


I wasn't sure about the uppercase greek letters because the LaTeX 
counterparts are not italicized.  On reflection, I agree with your 
decision.  My main concern was that the following letters, now in 
italics, would look wrong for n-ary product and sum:

  𝛱 (1D6F1)
  𝛴 (1D6F4)
Of course, such operators should actually use the dedicated characters 
as follows:

  ∏ (220F N-ARY PRODUCT)
  ∑ (2211 N-ARY SUMMATION)



There are some multi-character operators that could be translated to a
single character operator that would result in Unicode documents more
in line with ISO Z.
\%down%s---> ⧹ (29F9) for schema hiding
%filter%%down%s ---> ⨡ (2A21) for schema projection
%rcomp%%down%s  ---> ⨟ (2A1F) for schema composition
This would require ProofPower-Z to be updated to add the new symbols.
 I mention it now because the transition to Unicode could be used as
an opportunity to eliminate the non-ISO forms from Unicode documents,
if you wished to transition to the ISO symbol.

Either way, you probably want to add schema projection and composition
to the ML function utf8_to_pp_replacement_data.



I don’t think you had updated your clone of the pputf8 contrib.
utf8_to_pp_replacement_data was a half-hearted attempt to introduce a
bit more compatibility with ISO Z that I decided to abandon. A proper
translation between ProofPower-Z and ISO Z needs to be on parse trees
rather than on streams of lexical tokens.


Yes, sorry, I hadn't updated my clone.

I notice in pp-contrib/src/pputf8 you have files
  a.txt
  t.tgz
Did you mean to commit those?



I agree that it would be good to start accepting keywords with
single-character Unicode equivalents for the Z operators as variant
syntax for the forms with subscripts.


There is also schema piping.  I assume that the existing operator '>>' 
can be dropped in favour of ⨠ (2A20 Z NOTATION SCHEMA PIPING) because, 
with only parser support existing, nobody would be using it to date.




The following are not well supported on my system:
01F13C SQUARED LATIN CAPITAL LETTER Mfor %SML%
01F143 SQUARED LATIN CAPITAL LETTER 

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

[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 thought I would go ahead and express my
appreciation anyway!

I have been using xpp to prepare notes and exercises for my discrete
math course this semester, and today after spending a couple of hours
working on a doc with some recursive functions in SML and inductive
proofs in Latex, my xpp froze up!  I don't know why, but I thought I was
doomed.  Then, magically, as I gave up and killed the process I saw the
wonderful message:
 xpp-panic-problem_3_1_10.doc-Dq6T0c
was being saved!

Thank you, thank you, whoever added in that code to automatically save
before dying!


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




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

Re: [ProofPower] Unicode and ProofPower

[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 doubt %xNN% occurs in any existing scripts, so I think that's fine.

Your Unicode values for %lseq% and %rseq% have not taken into account 
the correction to the Z Standard in Technical Corrigendum 1:

Page 24, in 6.4.6.5
In line 3, replace “ 3008 LEFT ANGLE BRACKET” by “ 27E8 
MATHEMATICAL LEFT ANGLE BRACKET”.
In line 4, replace “ 3009 RIGHT ANGLE BRACKET” by “ 27E9 
MATHEMATICAL RIGHT ANGLE BRACKET”.

So
   - 3008 should be 27E8
   - 3009 should be 27E9

You currently have
2588 FULL BLOCK
for %EFT%.  This renders quite large.   I'm guessing that the 
description 'full block' means that the intention is for the glyph to be 
entirely black.  This is larger that the square we're used to and it may 
not even be square.  I think

25A0 BLACK SQUARE
could be more suitable (and would be square!)
To compare in your email client:  █ (2588) and ■ (25A0)
What do you think?

You currently have
208D SUBSCRIPT LEFT PARENTHESIS for %ulbegin%
208E SUBSCRIPT RIGHT PARENTHESISfor %ulend%
but these parentheses don't have underscores like the ProofPower glyphs. 
 One option is

298B LEFT SQUARE BRACKET WITH UNDERBAR
298C RIGHT SQUARE BRACKET WITH UNDERBAR
They appear as ⦋ (298B) and ⦌ (298C) but I think they're too close to 
refinement symbols.  I think this could be a case where you probably 
want to combine another glyph with the existing parenthesis using the 
combining diacritics.  I think the best options are

0331 COMBINING MACRON BELOW
which gives ̱( ̱)
These work in my email client and terminal.  Alternatively
0332 COMBINING LOW LINE
which gives (̲ )̲
These don't overlay correctly in my email client or terminal but are a 
single wide character.


For epsilon, I can see why
03F5 GREEK LUNATE EPSILON SYMBOL
has been used instead of
03B5 GREEK SMALL LETTER EPSILON
 - it is the correct shape for the equivalent LaTeX character.  I was 
finding that the lunate epsilon is very similar to the membership 
operator.  The lower case LaTeX mathematical greek letters appear 
italicized so I wonder whether the standard should have used e.g.

𝜃 (1D703) instead of θ (03B8)
𝜆 (1D706) instead of λ (03BB)
𝜇 (1D707) instead of μ (03BC)
so you would have chosen
𝜖 (1D716) instead of ϵ (03F5)
That would have meant also that any Greek authors of Z don't find 
themselves deprived of certain letters.  As things stand, I agree with 
your choice.


There are some multi-character operators that could be translated to a 
single character operator that would result in Unicode documents more in 
line with ISO Z.

\%down%s---> ⧹ (29F9) for schema hiding
%filter%%down%s ---> ⨡ (2A21) for schema projection
%rcomp%%down%s  ---> ⨟ (2A1F) for schema composition
This would require ProofPower-Z to be updated to add the new symbols.  I 
mention it now because the transition to Unicode could be used as an 
opportunity to eliminate the non-ISO forms from Unicode documents, if 
you wished to transition to the ISO symbol.


Either way, you probably want to add schema projection and composition 
to the ML function utf8_to_pp_replacement_data.


The situation with hyphen minus is unfortunate.  I presume the issue is 
that you can't identify which instances of ASCII hyphen-minus are Z 
subtraction operators.


The following are not well supported on my system:
01F13C SQUARED LATIN CAPITAL LETTER Mfor %SML%
01F143 SQUARED LATIN CAPITAL LETTER Tfor %<:%
01F149 SQUARED LATIN CAPITAL LETTER Zfor %SZT%
What do you consider converting them to the expanded form, e.g.
  %SZT% ---> ⌜↘Z↕
?
I think a single character is preferable and ideally it would be somehow 
based on the opening corner '⌜'.  I wonder if there is a combining trick 
possible here.




I am particularly interested to know how good the coverage for the
Unicode characters needed is on different systems and on different
applications. You can see how good your web browser is just by looking
at the above Web page, which includes GIFs that show how LaTeX renders
the ProofPower symbols alongside the Unicode translation as rendered by
your browser. To see how good your mail client is, the following should
look something like the HOL definition of distributed union:

⌜∀ x a⦁ x ∈ ⋃ a ⇔ (∃ s⦁ x ∈ s ∧ s ∈ a)⌝


This is readable on my system - all glyphs are available.  The sizes are 
a little odd but that could be due to font substitution.




(There is a complete list of the symbols used at the end of this e-mail.)

Current indications are that Mac OS can do everything that is required,
but that recent Linux systems and MS Windows tend to miss one or two
glyphs: the squared upper case letters I am using for some of the
quotation symbols seem to be poorly supported, for example

Re: [ProofPower] (no subject)

[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 to make sure that ProofPower bin directory comes before the system bin 
directories in the
PATH environment variable.


Easy - by doing exactly that before you run xpp, e.g.

  PATH=/home/sarah/pp/bin:$PATH

Put this in

  /home/sarah/.bash_profile

to have this done automatically when you log in.  (That's for Fedora, at 
leats.  For other Linux distributions, it may go elsewhere e.g. .bashrc 
- I don't know.)


Phil


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

Re: [ProofPower] making new database

[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

http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
and use the button at the bottom to edit your options.)


On 17/02/13 17:03, khan khan wrote:

hi
i want to ask about that how to make the new database while working in
proofpower for zed...i am following proofpower tutorail for zed and it
says "For undertaking application work with ProofPower it is first
necessary to set up a new database as a child of the issued database ‘pp
zed’" .what is an issued database? how to use pp_make_database to make a
new database.  and kindly also tell me when i run the command  xpp
-d example_zed then it says "printer not found, aborting".
regards



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




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

Re: [ProofPower] templates activation problem

[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 is a known
issue that is easily worked around.)


I havn't used the templates for a long time, but I see now that I don't have
them either (in 2.9.1w5).
I have unhashed the template include line in Xpp but the Tools menu in Xpp
still has Templates greyed out.


On further investigation I do get the templates if I use an Xpp file in which
the include for the templates is omitted (hashed), but if I use an include
even with a full pathname it doesn't seem to pick up the template file.
This applies also to the XppKeyboard file as well, I can't get the include to
work, but if the include is omitted the behaviour corresponds to the issued
XppKeyboard file (so far as I can see).


In an X/Motif resource file, I believe '!' starts a comment and include 
is a macro so must have a '#' before it, as in the Xpp file distributed 
with ProofPower.  Roger - do you still get the issue with #include ?


To find out what is disabling the Templates menu item, it is worth trying

  PPENVDEBUG=1 xpp

and checking that the paths reported in the terminal look sensible.  In 
particular, what is given for XUSERFILESEARCHPATH ?  Also, if %N is 
replaced by XppTemplates does any element of the path refer to a file on 
the file system?


Phil


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

Re: [ProofPower] SML Loop Command

[Phil Clayton]

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" *** *)
a (...);
...

(* *** Goal "1.2" *** *)
a (...);

(* *** Goal "1.2.1" *** *)
a (...);

(* *** Goal "1.2.2" *** *)
a (...);

(* *** Goal "2" *** *)
a (...);

(* *** Goal "3" *** *)
a (...);

pop_thm ()
);

If a proof stops working for some reason, the comments above make it 
much easier to track down the reason because they indicate where each 
subgoal should be completed (unless set_labelled_goal was used to change 
goal).


I wouldn't really advocate e.g.

(* *** Goal "2" *** *)
(* *** Goal "3" *** *)
(* *** Goal "4" *** *)
(* *** Goal "5" *** *)
fun_pow 4 (fn () => a tac) ();

even though it is fairly obvious that tac is being used to finish the 
commented subgoals.  The reason is that you can't step through the goals 
one at a time when replaying.


Alternatively, if

  a tac1;

produces a number of subgoals that can be finished off by linear 
arithmetic, it may be preferable to stop those goals appearing in the 
first place by


  a (tac1 THEN_TRY PC_T1 "z_lin_arith" asm_prove_tac []);

However, this attempts lin arith on all subgoals produced by tac1 and 
this could be an issue if it does not fail quickly for subgoals that it 
does not prove.  I tend to do this but take care with how subgoals are 
broken down to avoid the issue.


Regards,

Phil


On 15/01/13 20:55, Jon Lockhart wrote:

Dear Community,

I was wondering if any of you knew of a command that could be used while
writing your ProofPower proofs for you HOL or Zed specifications that
would allow for the application of the apply_tactic or a command a
predetermined number of times? In my specifications I am running across
an instance where I need to repeat the same proof command for several
goal statements in a row. For example I could have 3 or 4 goals that all
require the command 'a (PC_T1 "z_lin_arith asm_prove_tac [])'. Rather
than repeating this multiple times I would like to encapsulate the whole
thing in a loop or a repeat function, similar to the use of REPEAT
within a goal to apply the tactic multiple times. Does such a function
exist within the ProofPower tool environment?

Regards,
Jon Lockhart


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




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

Re: [ProofPower] templates activation problem

[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 menu PPXpp-2.9.1w2
that i have installed it...the templates in the tools menu is not
active...could you please tell me that how to activate it...how to
customize xpp resource file (application defaults file) ???
The example resource file uses #include directives to include two
files XppKeyboard and XppTemplates in my case it is XppZTemplates which
define the keyboard layoiut and the behaviour of the Templates Tool.
XppKeyboard and XppTemplates are set up as symbolic links to other
resource files in the same directory.

now the problem is that i do not understand that how to include
XppKeyboard and XppZTemplates in the resource file for xpp so that the
templates get activated???

Thank you
Regards
Sarah



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






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

Re: [ProofPower] Initialisation convention

[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 operation which produces after
objects which are acceptable as starting values for the
persistent objects of the system.
Admittedly in this very simple case this seems a complicated
way of saying that the system must start with an empty
vocabulary."

(but note that they did not actually use an operation, the
initial state is defined as a bare after-state).

Possibly the priming of initial state began here.


By making initialization an operation without a before state, the 
initialization can be used with schema operators such as composition and 
pre, e.g.


  Init ⨟ Op

  pre Init

the latter being another way to write the following:
  ∃ Init ∙ true
  ∃ State' ∙ Init

Phil


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

Re: [ProofPower] Trying to Prove my Zed Specifications

[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 
was you meant pushed' = {}.


However, for initialization, you don't have an initial state, so your 
schema should just have

  State'
where you currently have
  Δ State

I strongly recommend reading chapter 12 of Using Z, available at 
http://www.usingz.com/




If this change is necessary, and of course I will apply it to the other
two init operations, would the pre operator then be more useful in being
applied to this operation?


pre Init is certainly worth establishing: it is useful to know whether 
the Init operation can be achieved.  Note that with the above change to 
use State', pre Init is either true or false as there are no unprimed 
variables.  You want to know that it is not false.  As there is no 
initial state, pre Init may be written

  ∃ State' ∙ Init

However, I see you're calculating
  pre Button_State
  pre Elevator_State
  pre Floor_State
which is pointless.  These schemas are not operations: they have no 
concept of before state and after state.  You'll see that none have 
primed variables.  Not surprisingly, you're finding

  pre X_State = X_State

I also recommend chapter 14 of Using Z.  The whole book is worth a read, 
in fact!


Phil


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

Re: [ProofPower] Trying to Prove my Zed Specifications

[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:


save_consistency_thm %SZT%masterStop%>% (pop_thm ());

I tend to write such proofs with the following form, for some global 
variable C:


save_consistency_thm %SZT%C%>% (
z_push_consistency_thm %SZT%C%>%;

(* proof steps here *)

pop_thm ()
);

Phil


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

Re: [ProofPower] Trying to Prove my Zed Specifications

[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 description defines several global
variables, the witness you need would be provided as a HOL tuple. As the
witnesses for the individual variables are likely to be Z terms, you are
already into some not entirely trivial mixed language working. I just
tried a Z axiomatic description declaring three integers x, y, and z
with defining property x > y > z > 0. Here is the tactic that proves the
consistency:

a(%exists%_tac %<%(%SZT%3%>%, %SZT%2%>%, %SZT%1%>%)%>% THEN PC_T1
"z_library"
 rewrite_tac[z'decl_def, z'dec_def]);


This has really confused me!  I get a Z existential quantifier for the 
initial goal.  Even when there are generic parameters, I still get a Z 
existential quantifier, it's just that the witness must be a HOL 
function.  Are you sure you used z_push_consistency goal rather than 
push_consistency_goal?  Perhaps there is a ProofPower issue on some 
platforms or am I just missing something?


A while ago, I had an issue with z_push_consistency_goal where it failed 
to produce the expected Z statement - I can't remember exactly what went 
wrong.  This issue was that the initial proof step it performs was 
sensitive to the environment - the proof context, I think.  However, I 
can't reproduce the issue.


Phil



Even when you translate that back into the extended character set (e.g.,
by pasting the bit between %<% and %>% into ProofPower), it is not very
nice. So on the whole I don't think doing consistency proofs is not a
good place to start learning proof in Z, because it will expose too much
HOL to you. If you have a strong interest in doing consistency proofs
later on, it would actually be quite easy to provide some tools to
protect you from the HOL.

Finally, there isn't a list flavour of %exists%_tac or z_%exists%_tac.
It would be a minor convenience in HOL (where existentials with a list
of bound variables are obtained by iterating existential quantifier over
a single variable), but MAP_EVERY %exists%_tac does what you want. It is
rarely what you want in Z, where you use a binding display as the
witness for an existential quantifier that binds several variables and
where iterated existential quantification is fairly rare.





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

Re: [ProofPower] Trying to Prove my Zed Specifications

[Phil Clayton]

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 else something very strange is occurring.


Phil


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

Re: [ProofPower] Trying to Prove my Zed Specifications

[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 from there. Thanks for the help.


You're welcome.  By the way, I don't think any dialect of Z allows 
multiple horizontal definitions in one paragraph.




As for the zipped file I used the gzip command, which is short for
gunzip. Was the first couple I sent you corrupted?


No, all the other GZ attachments have been fine - it must have been 
corrupted somewhere.


Phil


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

Re: [ProofPower] Trying to Prove my Zed Specifications

[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 file".  I managed to 
extract enough by renaming to .xz and extracting with 7za though.  (How 
did you create the .gz file?)


The issue is that there can only be one abbreviation definition per 
paragraph.  You can't lump BOOLEAN, True and False all together into one 
paragraph.  Apologies if I misled you with my email presentation.


Phil


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

Re: [ProofPower] Best platform for ProofPower?

[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 from
scratch.

So I revived an old server to try out a more up-to-date
context for running ProofPower.
(my efforts in the amazon cloud ran into the buffers some time
ago).

So far I'm not having much success on Ubuntu 12.04 (the
PolyML build doesn't seem to work for me).


What error message do you get?  I ask because David Matthews is about to 
release 5.5 so it would be worth resolving any issue there.




I'm interested to know what people are actually running
ProofPower on these days?


I'm using Fedora 16.  Generally I've had no issue installing on the 
Fedora series of Linux provided that all the prerequisite packages are 
installed - achieved with the following yum/rpm commands:


yum install \
  gcc-c++ \
  polyml \
  texlive-latex \
  libXp-devel \
  libXext-devel \
  libXmu-devel \
  libXt-devel \
  xorg-x11-fonts-misc

rpm -ivh \

http://motif.ics.com/sites/default/files/openmotif-2.3.3-1.fc12.x86_64.rpm \

http://motif.ics.com/sites/default/files/openmotif-devel-2.3.3-1.fc12.x86_64.rpm

The key bindings 'just work' with AltGr and Left Window as the modifiers.

However, many new distributions use Gnome 3 which causes screen redraw 
problems for Xpp (and Motif applications generally).  One simple 
work-around for Gnome 3 is to run in 'fallback mode' which avoids 
hardware acceleration.  That's what I do.  (There appear to be various 
discussions out there about this issue so it may be resolved now.)


Phil


P.S.  Also, I have an issue when using X in Depth30 mode, i.e. 10 bits 
per colour.  Unless Xpp is run as root, it fails to start.  Probably not 
an Xpp-specific issue.  I haven't bothered reporting that yet.  For now 
I just use Depth24, which is what most people without fancy displays are 
using.


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

Re: [ProofPower] Trying to Prove my Zed Specifications

[Phil Clayton]

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 variables. 
For example, the predicate


  masterStop = 0

must be changed to either

  ¬ masterStop

or

  masterStop = False



Seems odd to be to just
through True and False in there like that where I am describing sets but
if it works, then I am all for it, I just need to see or understand how
to use it properly.


To use this is very simple for the most part.  In a predicate context, 
just treat Boolean expressions as though they were predicates.  In an 
expression context, Boolean expressions can be combined to give other 
Boolean expressions as you would expect, e.g. a ∧ b.  However, to create 
a Boolean expression from a predicate p, you need to write


  [ | p]

It is probably worth understanding what is going on at least once.  It 
is easiest to think in terms of sets.  A schema is just a set of 
bindings.  The empty schema [], which is the same as [ | true], is a set 
containing just the empty binding, i.e. {()}.  So [] is much like the 
SML type 'unit', a type that has only one value.  Thus Boolean is the 
set {{}, {()}} where {} represents false and {()} represents true, hence 
our definition of True and False.  So an expression of type Boolean is a 
schema.  When a schema S is used as a predicate, the predicate is θS ∈ 
S.  For one of our Boolean expressions B as a predicate, the predicate 
is θB ∈ B which is equivalent to () ∈ B.  So you can see how the 
corresponding predicate is derived.




As for the version of ProofPower, I have version 2.9.1w2, which is what
you were saying does not support ==. Looks like I might have to update
here when the latest stable version is released on the site.


If you feel inclined to try the latest patch, it is here, with instructions:
http://www.lemma-one.com/ProofPower/patches/patches.html

I'm fairly familiar with the installation process, so it only takes me a 
few minutes to build a patched version.  However, a new release may be 
around the corner - I don't know what Rob's plans are there.




What I was saying on the masterStop / masterReset axiom, along with the
minNumberFloors, maxNumberFloors, etc axioms, since I am using those as
global variables essentially, is how do I prove them and preconditions
on them like I have down for my States so far? Is is necessary too, or
if I just get the spec of them they are already shown to be theorems?


I see what you mean.  Yes, for an axiomatic description, one wants to be 
sure that it is not introducing a contradiction into the theory, making 
the theory inconsistent.  ProofPower has a mode of operation where it 
does not assume such axioms are consistent until they have been proved 
consistent.  This works by showing that each axiom is a conservative 
extension to the theory, i.e. does not introduce an inconsistency.


For Z, at the start of your theory, you would do

  set_flag ("z_use_axioms", false);

Note, then, that z_get_spec does not simply give you the axiom as a 
theorem.  After an axiomatic description paragraph, start a consistency 
proof with e.g.


  z_push_consistency_goal %SZT%minNumberFloors%>%;

See section 5.3, page 93, of usr011.dvi for examples.

Phil


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

Re: [ProofPower] Trying to Prove my Zed Specifications

[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] Trying to Prove my Zed Specifications

[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
cleared by FUZZ and CZT through Anthony's Z Word Tools. Unfortunately
ProofPower doesn't allow me to do such a thing and I am wondering what
would be the proper protocol for adding such sets to a specification in
ProofPower.


These work in the version I have, 2.9.1w2.rda.120805, the latest patch 
which fixes the recent Xpp issue.  (Generally it would be useful to see 
the error message you get.)  ProofPower used to require ≜ (hat-equals) 
for an abbreviation definition but a recent patch allows the standard == 
to be used.  If you are using the 'current release' 2.9.1w2, == is not 
supported.  Can you check the version of ProofPower in the banner that 
is shown when it starts?




My second question derives from this where right after the
sets I list some axioms which are used to hold globals which I use in
operations throughout the rest of my specification. They rely on the
boolean set I just created or are just parameters for the sets in
general. How would one go about proofing these or is it even necessary?


I'm not sure I understand the question.  The axiomatic description 
involving masterStop and masterReset is referring to the global variable 
BOOLEAN that was defined to be 0 .. 5 earlier.  The constraint holds 
throughout the theory and is obtained as a theorem by

  z_get_spec %SZT%masterStop%>%

Phil

P.S. A better way to define booleans in Z is as follows:

BOOLEAN == ℙ []
True == [ | true]
False == [ | false]

This is standard Z.  I don't know whether FuZZ accepts empty schemas. 
The main advantage is that the usual logical connectives can be used 
with such boolean expressions and the implicit conversion of schemas as 
predicates allows such a boolean expressions to be used where a 
predicate is required, and giving the expected predicate value.  The 
specification is more readable as a result.  For example, your expression


  if (elevatorRightHeading? = 1 ∧ elevatorGoingToFloor? = 1) then ...

could just be

  if elevatorRightHeading? ∧ elevatorGoingToFloor? then ...

To negate a value one can write

  ¬ elevatorRightHeading?

rather than encouraging numerical tricks like

  (1 - elevatorRightHeading?)

Note also that [] is a maximal set, so ℙ [] is too.  Consequently type 
checking ensures that such boolean values can take no other values. 
Using BOOLEAN == {0, 1}, the constraint is a semantic one: type checking 
will not reject e.g.


  elevatorRightHeading? = 2

which, presumably, would be a mistake.


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

Re: [ProofPower] Trying to Prove my Zed Specifications

[Phil Clayton]

Hi John,

That sounds strange.  It's probably easiest if you can cut your example 
down to a short script that produces the error, say containing just a 
single paragraph, and send a zipped version of that to the list.


Phil


On 03/09/12 01:47, Jon Lockhart wrote:

Phil,

Thanks for the 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" mailto:phil.clay...@lineone.net>> wrote:

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 language. The PP system comes
back with
expection 62000 of the Z-Parser, saying that the union symbol
from the
palette is a free variable and those are not permitted in Z
paragraphs.


If ProofPower says that ∪ is a variable then the Z toolkit theory
"z_sets" that defines the Z global variable (_ ∪ _) is not in scope,
i.e. "z_sets" is not an ancestor theory of your current theory.

Generally, Z specifications should always have the theory
"z_library" as an ancestor, which brings all Z toolkit theories into
scope.  Typically your theory would start

   open_theory "z_library";
   new_theory "some_new_theory";
   ...

If you need other theories in scope, add them as parents e.g.

   new_parent "z_reals";

Phil



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




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

Re: [ProofPower] Trying to Prove my Zed Specifications

[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 language. The PP system comes back with
expection 62000 of the Z-Parser, saying that the union symbol from the
palette is a free variable and those are not permitted in Z paragraphs.


If ProofPower says that ∪ is a variable then the Z toolkit theory 
"z_sets" that defines the Z global variable (_ ∪ _) is not in scope, 
i.e. "z_sets" is not an ancestor theory of your current theory.


Generally, Z specifications should always have the theory "z_library" as 
an ancestor, which brings all Z toolkit theories into scope.  Typically 
your theory would start


  open_theory "z_library";
  new_theory "some_new_theory";
  ...

If you need other theories in scope, add them as parents e.g.

  new_parent "z_reals";

Phil


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

Re: [ProofPower] ProofPower RCS Repository

[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 to $PPDEVHOME rather than $PPDEVHOME/pp .


Phil


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

Re: [ProofPower] ProofPower RCS Repository

[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 to be able to map
between Mercurial or Git and RCS. Any feedback on this
would be gratefully received.


I tried it but failed to build xpp.
Lots of undefined references:

/usr/lib/gcc/i486-linux-
gnu/4.4.3/../../../../lib/libXm.a(TextIn.o): In function


Thanks for the prompt feedback.

I am assuming this is on a platform where you can build from the OpenProofPower 
distribution. If so, my first guess is that you don't have the libraries in the 
form you need to link xpp statically, which (confusingly) is the default in the 
xpp makefile but not the default when you build with configure. Could you try 
again with PPMOTIFLINKING=dynamic ?


I too required PPMOTIFLINKING=dynamic too.  I don't think the problem is 
OpenMotif itself (the -devel package includes libXm.a) but the libraries 
it depends on.  Many of the undefined references start Xft... and 
neither libXft nor libXft-devel provide a .a file on my system.


I also required PPPOLYHOME=... because I have Poly/ML installed in a 
non-standard location.


Attached is a modified script that adds comments for PPPOLYHOME and 
PPMOTIFLINKING (copied from configure).


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.  Also, it looks like the default for PPRCSDIR 
is not

  $PPDEVHOME/pp/OpenProofPower/RCS
(as documented) but
  $PPDEVHOME/OpenProofPower/RCS
so I changed that comment.

Phil



opp-developer-setup.sh.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trouble Installing in cloud

[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 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.

>

Well actually, it is exactly what was expected to happen in the original
X Windows concept - run applications (called X clients, because they are
clients of the local GUI services) remotely and have the GUI appear on
local machine (running an X server, because it supplies GUI services to
the remote applications). In that model, the client connects to the
server using the standard network protocols for client-server
connection. But this model is fine on a well-managed intranet but raises
a lot of security issues in the wild world of the Internet.


We often made use of X Windows' network transparency to run Xpp remotely 
over a LAN, without issue.  My views were less security-related and more 
concerned with usability given the likely longer latencies to a remote 
host in the cloud.




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


Exactly.  This is the old debate about thick clients v. fat client. Both
have there merits, but it depends what your are trying to achieve.


Right, I now understand Roger's motivation is to avoid installing 
ProofPower on various devices, rather than taking advantage of the 
resources offered by the cloud.




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




If I were just interested in running ProofPower in the cloud
then that would be correct. And this something that one
might like to investigate.


Unfortunately with things stand, Phil's fat clients would hold the
user's source files locally while the ProofPower theory database is held
remotely. That makes sense if you just want the server to offer a
stateless service whereby you uploaded your specs and proofs each time,
It would also make sense for collaborative work, but to make that really
work, you would want to adapt ProofPower to have a model supporting
multiple concurrent users accessing a shared database.

I don't see how that would make sense.


Such a fat client can easily work with remote source files, if a user so 
wishes - just use sshfs to make the remote account's filesystem appear 
local via ssh with e.g.


  sshfs user@host:dir localdir


It will be interesting to see how running Xpp remotely works out.  If I 
get a chance, I'll try it over a long distance SSH connection (with X11 
forwarding).


Phil


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

Re: [ProofPower] Trouble Installing on Windows

[Phil Clayton]

Jon,

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

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


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


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


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


Phil


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

Re: [ProofPower] Trouble Installing in cloud

[Phil Clayton]

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

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


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


  xpp -c ssh -Y user@host

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

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


However,

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

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


1. Specify full remote path, e.g.

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

where REMOTEPPHOME is the ProofPower home directory in the cloud.

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

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

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


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

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

Regards,

Phil


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

Re: [ProofPower] Trouble Installing on Windows

[Phil Clayton]

Jon,

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

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


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




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


The missing file is

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

On my machine, the command

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

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




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


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


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


Regards,

Phil


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

Re: [ProofPower] Trouble Installing in cloud

[Phil Clayton]

Roger,

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


  rpm -ql openmotif-devel

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

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

In that message, I see that I also noted

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

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

Phil


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

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

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

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

Here's is what rpm says about it:

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

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

Roger Jones

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





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

Re: [ProofPower] Trouble Installing on Windows

[Phil Clayton]

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

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

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


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

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

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

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

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


Regards,

Phil


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

Re: [ProofPower] Trouble Installing on Windows

[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 never installs the package polyml from any repo by 
adding polyml to the line starting


  exclude=

in /etc/yum.conf , e.g.

  exclude=polyml

In my case, I have

  exclude=openmotif*,lesstif*,polyml,mlton,ocaml*

Phil


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

Re: [ProofPower] Trouble Installing on Windows

[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 install \
  gcc-c++ \
  polyml \
  texlive-latex \
  libXp-devel \
  libXext-devel \
  libXmu-devel \
  libXt-devel \
  xorg-x11-fonts-misc

It would be useful to know if anything is missing after entering this 
command, which you need to run as root.  (I believe the package gcc-c++ 
will give you g++.)


There are a couple of things Fedora users need to know though.

1. OpenMotif is available via yum from the RPM Fusion repository.  If 
you add the RPM Fusion repository to your system, you mustn't use the 
version of OpenMotif that it supplies - see my previous message here for 
details:

http://lemma-one.com/pipermail/proofpower_lemma-one.com/2010-January/000592.html
If you don't use RPM Fusion, don't worry about this!

2. With Fedora 16 and later, the GNOME 3 shell is the default and this 
breaks the Motif Text widget, making Xpp very cumbersome to use.  (At 
least on x86-64 platforms.)  The solution is to use fallback mode: in 
'System Settings' -> 'System Info' -> 'Graphics', set 'Forced Fallback 
Mode' to 'On'.  This issue has now been officially noted as an OpenMotif 
bug here:

http://bugs.motifzone.net/long_list.cgi?buglist=1551

Regards,

Phil


On 31/07/12 21:35, Jon Lockhart wrote:

Hey Rob,

Thanks for the link to motifzone, that worked immediately and I was able
to get the latest binary for open motif installed on my Fedora 17 image.

I am now currently having trouble with getting polyml to install.

After running the config file I try to run the make file and it says
that command g++ is not found. I did a yum install of gcc and gpp to
make sure I had a c and c++ compiler installed on my fedora and it
appeared to have installed both packages fine. Any thoughts on this?
Sorry for asking for all the help, my linux is pretty rusty.

Thanks,
Jon Lockhart


On Mon, Jul 30, 2012 at 2:58 AM, Jon Lockhart mailto:jal...@bucknell.edu>> wrote:

Rob,

Thank you very much for the site. I will give it a try as soon as i can.

Regards,
Jon

On Jul 30, 2012 2:48 AM, mailto:r...@lemma-one.com>> wrote:

Jon,

 > Rob,
 >
 > I was wondering, you know of any problems with the download
site for
 > OpenMotif?
 >
 > I got Virtual Box and Fedora 17 working on my desktop, my
laptop did not
 > have enough RAM to run it, and I got ProofPower and ML
downloaded no
 > problems, but seems you get a blank page when getting
OpenMotif 2.3.3. I
 > contacted there list but have not heard back all week.
 >
 > Any ideas?

Try motifzone.net  rather than
www.openmotif.org 

Regards,

Rob.





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




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

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

[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 outputs, I just cannot choose"
  "I have the sensation
  Of just a relation"
  "I'll wait to see where I am used!"

I doubt Norman Douglas would be impressed but if that's your sort of 
thing, there's always FM2011's field day:

http://sites.lero.ie/fm2011/limerickscompetition.html

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

Re: [ProofPower] Scope of variables in Z declaration

[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 under certain desirable transformations. In
particular, the standard account of how to normalise a schema fails.
If you try to normalise S, you get the ill-typed schema [A : Z x Z | A
in A x A /\ (_+_) A< 10]. In this example, you can expand the
definition of A, but if A were loosely specified, I don't see any
clean way of describing the normalised version.


Whilst horizontal schemas are not closed under normalization, we can write

[A' : A × A | (_ + _) A' < 10][A / A']


Oops, that should have been

  [A' : ℤ × ℤ | A' ∈ A × A ∧ (_ + _) A' < 10][A / A']


so at least schemas are closed. For practical purposes, that seems
sufficient.


GIven its provenance in academia, it amazes me how many design
decisions in Z make it harder to teach, typically, as here, by making
useful rules of thumb fail to work in edge cases.


Yes, another headache for teachers and students.

Phil


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

Re: [ProofPower] Scope of variables in Z declaration

[Phil Clayton]

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. In particular, the standard 
account of how to normalise a schema fails. If you try to normalise S, you get the 
ill-typed schema [A : Z x Z | A in A x A /\ (_+_) A<  10]. In this example, you 
can expand the definition of A, but if A were loosely specified, I don't see any 
clean way of describing the normalised version.


Whilst horizontal schemas are not closed under normalization, we can write

  [A' : A × A | (_ + _) A' < 10][A / A']

so at least schemas are closed.  For practical purposes, that seems 
sufficient.



GIven its provenance in academia, it amazes me how many design decisions in Z 
make it harder to teach, typically,  as here, by making useful rules of thumb 
fail to work in edge cases.


Yes, another headache for teachers and students.

Phil

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

Re: [ProofPower] Scope of variables in Z declaration

[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" alternative, for
reasons I will come to shortly, but I think it possible that
in coming to the decision I was partly influenced by a
misreading of the passage you quoted from the ZRM.

I thought Spivey was saying that the names bound by the
schema declaration could not be used in the declaration.
Whereas you read him as saying that they can be used but
fall outside the scope of the declaration.
Of course he does say explicitly that they fall outside the
scope, but that is consistent with the prohibition.


Regarding Spivey Z, I am reading the second edition ZRM (1998).  It 
could be that the first edition (1992) was stricter, in line with your 
understanding.  (I have no way of finding out.)


Addressing the question of what Spivey and Standard Z allow now, I have 
tried type checking some examples with Fuzz and CZT for the two 
dialects, respectively.  Both accept the following pathological 
axiomatic description:


│ e : ℙ ℤ
├
│ ∀ e : e ⦁ e < e

and they both reject the following as type incorrect:

│ e : ℙ ℤ
├
│ ∀ e : {e} ⦁ e < e

which is consistent with my understanding.



In the context of that possible misunderstanding, one may
imagine there to be a little scope for discretion in how to
deal with a specification which seems to be formally outside
the scope of Z.  One might then implement the (semantics of)
mapping into HOL with a different scope rule and then debate
about whether an error report should be raised if the
prohibition is violated.

I did consider the merits of the two alternatives, and I was
then and am now still strongly in favour of the existing
behaviour.
As to the opportunities for writing obscure specifications,
they are ample whichever choice is made, and my opinion was
then that the decision should be made not on the basis of
bad practice but on the basis of good practice.
The only cases of good practice which came to mind in which
a variable is used in a declaration which binds it are cases
in which the variable is used in a subsequent part of the
declaration to the one in which it is bound,
In these cases it is often the case that the specification
can be made both more concise and more easily understood by
allowing the use.

I did not think of any examples in which the use of a
variable from an outside scope in a declaration which binds
it would be a good thing.


For hand-written Z, I cannot think of any examples where it offers any 
benefit.


It is perhaps worth considering another use of Z though - as an 
intermediate language, e.g. to capture the semantics of some other 
notation according to some recursive translation/mapping scheme.  In 
such a scheme that I was working on (to embed another notation), there 
was extensive use of schemas that contained free variables.  (I doubt 
that this would occur much in hand-written Z.)  With the alternative 
scoping behaviour, the translation scheme can construct such schemas and 
use them in declarations without needing to adjust for any overlap 
between the free variables and component names of such a schema.




Another consideration is the effect of the scope rules on
proof.
This is connected with the way in which the scope rules
influence the mapping into HOL (and this is the case even if
you are not implementing in HOL).
There can be no doubt that I was influenced by the fact that
it is much more straighforward to implement the mapping if
the predicate implicit in the declaration is in the scope of
the bindings.
This is reflected in a simpler description of how to obtain
the implicit predicate from the declaration, the nub of
which is that one simply replaces the colons by membership
signs.
This effects the proof behaviour, for one then expects that
to prove a universally quantified predicate one can just drop
the universal quantifier and replace the declaration with is
implicit predicate on the LHS of an implication.

Of course, if there are name clashes then then there will
have to be renamings, but they are at least uniform.
If the other scope rule is used, then partial renaming is
necessary just to give the implicit predicate, and hence
also in any context in which the proof requires the
declaration to be eliminated but not the predicate.
I too am now curious about how other proof tools handle such
situations (there were no others to refer to when
ProofPower-Z was being designed).


So with the alternative scoping, it seems that additional variable 
renaming would occur during proof compared with the ProofPower scoping 
but, presumably, that because the ProofPower scoping ensures that a 
non-clashing name is used when writing Z in the first place.


As a user, the existing renamings to avoid clashes and the additional 
"

[ProofPower] Scope of variables in Z declaration

[Phil Clayton]

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 
constructing Z terms.  I was proving something like


  y = 3 ⇒ (∃ [x : ℤ | x = y - 1] ⦁ x = 2)

which is fine.  Then a slight variant

  y = 3 ⇒ (∃ [x : ℤ | x = y - 1][y / x] ⦁ y = 2)

which isn't provable.  Although the schema

  [x : ℤ | x = y - 1][y / x]

has a free variable y that is (necessarily) distinct from the schema 
component y (even though they are the same type), the free y becomes 
bound by its schema component y when appearing in a Decl.


I'm fairly familiar with the ProofPower-Z behaviour but, clearly, not 
enough and this issue got me wondering what other Z dialects do about 
the scope of variables declared in a declaration.


For Spivey-Z, see last para section 3.4 of ZRM: "the scope never include 
the declaration itself: variables may not be used on the right of a 
colon...".


For the Z Standard, looking at the semantic relations in section 15, I 
believe that the scope never includes the declaration itself.  (The 
semantic value for a declaration expression is always derived from an M 
∈ Model that is not extended with the bindings from the declaration.) 
Is that right?


Thinking about the relative merits of the ProofPower-Z behaviour, I can 
see that it could perhaps make schemas slightly more succinct but opens 
the door to obfuscation, e.g.


  ∀ i : i .. j ⦁ P

instead of the equivalent

  ∀ i : ℤ | i ≤ j ⦁ P

and possible confusion due to a bound variable being referenced before 
(in a textual sense) it has appeared bound.  Is there any particular 
reason ProofPower-Z behaves like it does?


Phil

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

Re: [ProofPower] Theorem QA

[Phil Clayton]

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 "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 will be puzzled when tools
like the rewriting tools think you don't want the free variables to
be instantiated.

b) Theorems with variables bound by logical quantifiers (universal,
existential and unique existential) that are not used in the body
of the abstraction. This happens for various reasons (often hand in
hand with (a)). It is misleading for the reader and can be
confusing when you try to use the theorem.

It outputs a little report on any problems it finds.

I am considering putting a bug-fixed and documented version of
check_thms in the next working release of ProofPower. Any comments
or suggestions for other things to check for would be welcome.


I am wondering about a stronger version of check b for individual
conjuncts of a theorem. In the past, I have found that e.g.
rewriting can be awkward when an equational conjunct of a theorem
does not mention a universally quantified variable (that is
mentioned by other conjuncts). I think the issue was when the
unmentioned variable was quantified over a non-maximal set, so this
is probably most relevant to Z. For example, given

│ _ ^ _ : ℤ × ℕ → ℤ
├──
│ ∀ i : ℤ; j : ℕ ⦁ i ^ 0 = 1 ∧ i ^ (j + 1) = i * i ^ j

I think rewriting with the base case requires manual intervention to
provide a value for j,


Indeed. ∀ i : ℤ; j : X ⦁ i ^ 0 = 1 amounts to a convoluted way of
saying "either X is empty or ∀ i : ℤ ^ 0 = 1".


so the following would be preferable:

├──
│ ∀ i : ℤ ⦁ i ^ 0 = 1 ∧ (∀ j : ℕ ⦁ i ^ (j + 1) = i * i ^ j)




I expect that this sort of check would be dependent on the current
proof context (perhaps making use of canonicalization support) so
may not be desirable as part of the same utility.


I think a simple heuristic would work. I think is reasonable to say
that in a predicate of the form:

∀ ... x : X | P ⦁ Q1 ∧ Q2 ∧ ...

If there is an i such that x doesn't appear free in P or Qi, then
report a possible problem. There are many cases (e.g., law of
transivity) where a theorem has an implication with an antecedent
that contains variables that are not in the succedent, but it is a
reasonable style rule in Z not to disguise such an implication by
burying the antecedent in an implication.


That sounds reasonable to me.

There is also the possibility of a schema declaration in the
quantification which presents various options. For e.g. a schema
reference:

∀ S; ... | P ⦁ Q1 ∧ Q2 ∧ ...

would it make sense for the heuristic warn if there is an i such that
frees(P) ∪ frees (Qi) does not mention any variable bound by S?


Yes that makes sense.


Also, for a horizontal schema declaration, there is the question of
whether to destruct it, i.e. expand out its contents, or treat it like
any other schema.


Do you mean a declaration in a quantifier of the form [Declaration |
Predicate]?


Yes.



Do you use that idiom much?


No.  (Although I am generating Z systematically which can result in a 
horizontal schema, I can't foresee any need to quantify such a 
horizontal schema in a theorem.)




I can't see the point, so I don't have any views on how to handle it.


I don't have any views either but thought I would mention it in case 
anyone did.


Regards,

Phil

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

Re: [ProofPower] Theorem QA

[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. It checks against:

a) Theorems with free variables. Typically this means you forgot an outer 
universal quantifier. Later on you will be puzzled when tools like the 
rewriting tools think you don't want the free variables to be instantiated.

b) Theorems with variables bound by logical quantifiers (universal, existential 
and unique existential) that are not used in the body of the abstraction. This 
happens for various reasons (often hand in hand with (a)). It is misleading for 
the reader and can be confusing when you try to use the theorem.

It outputs a little report on any problems it finds.

I am considering putting a bug-fixed and documented version of check_thms in 
the next working release of ProofPower. Any comments or suggestions for other 
things to check for would be welcome.


I am wondering about a stronger version of check b for individual conjuncts of 
a theorem.  In the past, I have found that e.g. rewriting can be awkward when 
an equational conjunct of a theorem does not mention a universally quantified 
variable (that is mentioned by other conjuncts).  I think the issue was when 
the unmentioned variable was quantified over a non-maximal set, so this is 
probably most relevant to Z.  For example, given

│ _ ^ _ : ℤ × ℕ → ℤ
├──
│ ∀ i : ℤ; j : ℕ ⦁ i ^ 0 = 1 ∧ i ^ (j + 1) = i * i ^ j

I think rewriting with the base case requires manual intervention to provide a 
value for j,


Indeed. ∀ i : ℤ; j : X ⦁ i ^ 0 = 1  amounts to a convoluted way of saying "either X 
is empty or ∀ i : ℤ ^ 0 = 1".


so the following would be preferable:

├──
│ ∀ i : ℤ ⦁ i ^ 0 = 1 ∧ (∀ j : ℕ ⦁ i ^ (j + 1) = i * i ^ j)




I expect that this sort of check would be dependent on the current proof 
context (perhaps making use of canonicalization support) so may not be 
desirable as part of the same utility.


I think a simple heuristic would work. I think is reasonable to say that in a 
predicate of the form:

∀ ...  x : X  | P ⦁ Q1 ∧ Q2 ∧ ...

If there is an i such that x doesn't appear free in P or Qi, then report a 
possible problem. There are many cases (e.g., law of transivity) where a 
theorem has an implication with an antecedent that contains variables that are 
not in the succedent, but it is a reasonable style rule in Z not to disguise 
such an implication by burying the antecedent in an implication.


That sounds reasonable to me.

There is also the possibility of a schema declaration in the 
quantification which presents various options.  For e.g. a schema reference:


  ∀ S; ... | P ⦁ Q1 ∧ Q2 ∧ ...

would it make sense for the heuristic warn if there is an i such that 
frees(P) ∪ frees (Qi) does not mention any variable bound by S?


Also, for a horizontal schema declaration, there is the question of 
whether to destruct it, i.e. expand out its contents, or treat it like 
any other schema.


Phil

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

Re: [ProofPower] Theorem QA

[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 
universal quantifier. Later on you will be puzzled when tools like the 
rewriting tools think you don't want the free variables to be instantiated.

b) Theorems with variables bound by logical quantifiers (universal, existential 
and unique existential) that are not used in the body of the abstraction. This 
happens for various reasons (often hand in hand with (a)). It is misleading for 
the reader and can be confusing when you try to use the theorem.

It outputs a little report on any problems it finds.

I am considering putting a bug-fixed and documented version of check_thms in 
the next working release of ProofPower. Any comments or suggestions for other 
things to check for would be welcome.


I am wondering about a stronger version of check b for individual 
conjuncts of a theorem.  In the past, I have found that e.g. rewriting 
can be awkward when an equational conjunct of a theorem does not mention 
a universally quantified variable (that is mentioned by other 
conjuncts).  I think the issue was when the unmentioned variable was 
quantified over a non-maximal set, so this is probably most relevant to 
Z.  For example, given


│ _ ^ _ : ℤ × ℕ → ℤ
├──
│ ∀ i : ℤ; j : ℕ ⦁ i ^ 0 = 1 ∧ i ^ (j + 1) = i * i ^ j

I think rewriting with the base case requires manual intervention to 
provide a value for j, so the following would be preferable:


├──
│ ∀ i : ℤ ⦁ i ^ 0 = 1 ∧ (∀ j : ℕ ⦁ i ^ (j + 1) = i * i ^ j)

I expect that this sort of check would be dependent on the current proof 
context (perhaps making use of canonicalization support) so may not be 
desirable as part of the same utility.




This is currently just for HOL, but I could do something similar for Z too.


Certainly this would be a useful facility for HOL users but I could only 
make use of a Z version.


Regards,

Phil


P.S.  The above formal text is UTF8 encoded!  Hopefully that is not a 
problem these days.  It would be useful to know if any mail systems 
aren't displaying it properly.


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

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

[Phil Clayton]

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

Also, inside use_terminal (ProofPower's real-eval-print loop), SML/NJ 
appears to require an additional semicolon 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 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.



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



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

[ProofPower] Fixes for building with SML/NJ

[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 
compiler-specific loopholes to circumvent proof.


Anyone following the Isabelle mailing list recently will note that this 
provides little additional assurance when operating in a zero-trust 
environment: running with both compilers only helps with item 2d on 
Mark's list:

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-January/msg00085.html
Still, every little helps...

Phil


patch-2.9.1w2.rda.110814.pbc.120131.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Writing Z schema predicates with decorations

[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
inconsistently. So perhaps renaming is useful?


I'm sure it is.

But I doubt that it is sensible in the mapping of a
decorated schema reference.
In this case the same decoration is applied to all
components.

As to the merits of the design of z_schema_pred, it seems to
me that the mapping is not only simpler but works more as
one would expect if a decorated schema reference uses the
decoration parameter as intended.

In that case, simply rewriting with the definition of
Z'SchemaPred (which is just membership) yields the statement
that the binding with decorated variable names (but
undecorated component names) is a member of the schema
(undecorated).
This is as close as you get to asserting that the decorated
theta term is a member of the schema (which might possibly
have been even better in some ways, though less "efficient").

My guess is that it probably was done that way in the
prototype embedding of Z into the prototype ICL HOL (I did
the specifications and explained them to Geoff Scullard who
implemented them), but that when this was all re-implemented
for the "product version", the implementation fell out
without using it (I don't think either Geoff or myself had
much involvement at that stage, so the reason for using it
got lost).


I wondered whether the original design intended to map decoration
differently for predicates and expressions? Then the user could
determine the mapping of e.g. S' as either
mk_z_schema_pred (S, "'")
mk_z_schema_pred (mk_z_decor%down%s (S, "'"), "")
by controlling predicate/expression parsing modes as usual. (As Rob
points out, the second is always used currently.)


To answer my own question: from what Roger is saying, this must have 
been the intention as Z'SchemaPred can only occur in a predicate and 
Z'Decor only in an expression.


Phil



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

Re: [ProofPower] Writing Z schema predicates with decorations

[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?


I'm sure it is.

But I doubt that it is sensible in the mapping of a
decorated schema reference.
In this case the same decoration is applied to all
components.

As to the merits of the design of z_schema_pred, it seems to
me that the mapping is not only simpler but works more as
one would expect if a decorated schema reference uses the
decoration parameter as intended.

In that case, simply rewriting with the definition of
Z'SchemaPred (which is just membership) yields the statement
that the binding with decorated variable names (but
undecorated component names) is a member of the schema
(undecorated).
This is as close as you get to asserting that the decorated
theta term is a member of the schema (which might possibly
have been even better in some ways, though less "efficient").

My guess is that it probably was done that way in the
prototype embedding of Z into the prototype ICL HOL (I did
the specifications and explained them to Geoff Scullard who
implemented them), but that when this was all re-implemented
for the "product version", the implementation fell out
without using it (I don't think either Geoff or myself had
much involvement at that stage, so the reason for using it
got lost).


I wondered whether the original design intended to map decoration 
differently for predicates and expressions?  Then the user could 
determine the mapping of e.g. S' as either

  mk_z_schema_pred (S, "'")
  mk_z_schema_pred (mk_z_decor%down%s (S, "'"), "")
by controlling predicate/expression parsing modes as usual.  (As Rob 
points out, the second is always used currently.)


A better answer as to why Z'SchemaPred needs to support decoration is to 
allow e.g. predicate S' to match with S, for e.g. forward chaining, with 
such an S' being a valid Z term.  (Currently, when a schema predicate is 
stripped in the subgoal package with the proof context 'z_schemas, any 
top-level Z'Decor is converted to decoration on the Z'SchemaPred binding 
variables.)


My suggestion regarding renaming was not about the mapping of Z into HOL 
but about what Z proof operations could do to avoid "not Z" HOL terms. 
That is actually a separate issue/discussion.  Sorry for the confusion.


Phil



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

Re: [ProofPower] Writing Z schema predicates with decorations

[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 exactly
what the decoration in mk_z_schema_pred is for (I know
what the semantics is intended to be but I can't
recall why we have it). Perhaps Roger can cast his
mind back to this.


My memory is pretty bad on the history.

I expect that I started out with the syntax in Spivey's
"The Z Notation" (It was the only game in town at the
time). But then you might expect to see "gen actuals"
and "renaming!" there.


A better answer is as follows.

We were making the Spivey syntax more "orthogonal" by
allowing schema expressions in places where only schemas
were previously allowed, and in that context there was no
benefit in putting actual parameters or renamings into the
predication operation, since they could be implemented
using the normal schema expression operations.

However, decoration is another matter.
Decoration during schema-predication requires only that the
free variables in the covert theta term be decorated.
Decorating the schema(expression) is a more horrible
operation and is unnecessary.
So the parameter would enable a more efficient mapping of the
Z into HOL, if it had actually been used!
Presumably the implementation (of z_schema_pred) does just
decorate the theta term not the schema expression.


I have just found section 4.3.7 in ZED003 and it appears to say that.

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?


Phil



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

Re: [ProofPower] Writing Z schema predicates with decorations

[Phil Clayton]

My guess would be that a non-empty decoration is possible for 
Z'SchemaPred to allow for variable decoration during proof operations: 
if all variables in the characteristic binding are consistently 
decorated, the resulting term is still Z.


However, not all Z proof operations consistently 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 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 way to write a Z term quotation equal to tm1 as follows:

val tm1 = mk_z_schema_pred (S, "'");

? (I can do so in HOL using Z'SchemaPred directly.)



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 what the decoration in mk_z_schema_pred is for (I know what the
semantics is intended to be but I can't recall why we have it). Perhaps
Roger can cast his mind back to this.

This reminds me that I always meant to make the Z specifications of the
Z to HOL mapping available. As a quick fix, I have put the documents here:

http://dl.dropbox.com/u/34693999/zed002.pdf
http://dl.dropbox.com/u/34693999/zed003.pdf
http://dl.dropbox.com/u/34693999/zed005.pdf

I will make sure they typecheck presently and include them in the doc
directory in future builds.

Regards,

Rob.



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





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

[ProofPower] Writing Z schema predicates with decorations

[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 way to write a Z term quotation equal to tm1 as follows:

  val tm1 = mk_z_schema_pred (S, "'");

?  (I can do so in HOL using Z'SchemaPred directly.)

All my attempts result in a term equal to tm2 as follows:

  val tm2 = mk_z_schema_pred (mk_z_decor%down%s (S, "'"), "");

tm1 and tm2 are equivalent so this is hardly an issue for writing Z 
specifications but can make quoting terms awkward.  In the end, I just 
referred to the assumption by index.


Phil



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

[ProofPower] Denormalized Z terms

[Phil Clayton]

(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 rather more than I would hope 
and causing me problems.  I have found them occurring in two ways:

1. ML quotations nested in Z terms;
2. when avoiding variable capture, primarily z_%forall%_elim etc.
The attached script gives an account of these issues.

Is the intention that Z proof operations always produce (valid) Z terms?

Phil

P.S. I have noticed that inst [] [] is not an identity operation, which 
may be related to item 1 above.


denormalized_z_egs.sml.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

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

[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 is bad for people who like to
use the horizontal layout even on smallish screens. The only way to
keep everybody happy is to have separate resources for the width and
height of an edit-only session.


The extra configuration would be appreciated by me but, while I'm the
only one, perhaps it is not worth doing.


It seemed the right thing to do, so it's done and will be in the next
experimental release.


Thanks - I look forward to it!

Phil



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

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

[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, a symbol for unary
minus in Z has been added to the font and defined as a synonym of the
unary minus written as a tilde in the theory z_numbers. The symbol
displays and typesets as short minus sign. %cat%/ (i.e., a frown
followed by a backslash) is now defined as an alias for distributed
concatenation written %dcat% in the theory z_sequences.


The new minus sign appears to be missing from the palette.  (Am I going blind?)


It should be at row 6 column 3, just right of greater-than-or-equals.


My fault.  For some reason I failed to merge that line of the new Xpp 
file into the one in my home directory.  (Normally I merge in the 
opposite direction to avoid this happening.)




b) In xpp, you can now switch dynamically between the horizontal and
vertical layout using a new item in the window geometry. N.b., this is
accompanied by a change in the way you specify the initial layout and
geometry in app-defaults/Xpp. See the CHANGES file for more details.


The switching is useful.  A few observations:

1. When there is no journal window, Show Geometry causes a crash:
xpp: fatal error: signal 11: memory fault: ...
(It may not crash the first time.)  Also, Ctrl+T causes a crash, even though 
there is no menu item Toggle Geometry without a journal window.


I have attached a patch that fixes these two (which were intermittent/system 
dependent).


Thanks, that fixes it.



2. I have an issue with the design when using horizontal mode.  My 
app-defaults/Xpp sets column widths assuming there will be a journal window.  
However, I am often opening file just to view/edit, i.e. no journal window, and 
always have to resize the window which is far too wide.


But you "far too wide" may be another user's "very nice" (see below).


If there are users who want as much width as possible, then I suppose so.



  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 people who like to use the 
horizontal layout even on smallish screens. The only way to keep everybody 
happy is to have separate resources for the width and height of an edit-only 
session.


The extra configuration would be appreciated by me but, while I'm the 
only one, perhaps it is not worth doing.




For vertical mode, the current behaviour seems preferable.  I think different 
behaviour for the different orientations makes sense because of the asymmetric 
nature of documents: bounded width, unbounded height.


That's not really a valid assumption: you may worry about keeping your source 
files within a fixed width. but many people don't. When entering text, it is 
quite common to use carriage-returns only to separate paragraphs or sentences 
and this logical arrangement is convenient for many reasons, e.g., when 
searching for phrases. Likewise, in code, many people prefer long lines to 
artificially inserted line breaks with no logical significance. (A 
line-wrapping mode for formal text in ProofPower documents is on my wish-list).


There are pros and cons.  I find it useful to make the text fit e.g. 80 
columns not just for general readability but to get a decent view of two 
source files on the screen at once.  This especially helps 
comparing/merging side by side and working with a journal window (which 
has sizeable output).


(Even with a line wrapping mode for formal text, I would stick to N 
columns because other tools, e.g. visual diff programs, would not have 
such a line wrapping mode.)




3. Given the above observation about document shape, should toggling attempt to 
maintain width by resizing the Xpp window? I have had various ideas along these 
lines.  Have you thought about that?


Aside from my reservations above, it is generally considered to be bad practice 
for X applications to resize or move top-level windows programmatically once 
they are created unless there is some really compelling reason in the 
application logic for doing this. The results of trying to do so are dependent 
on the window manager and many window managers will just ignore resize requests 
from the program.


Yes, I wondered if it was bad practice for the window to resize itself.

Phil



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

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

[Phil Clayton]

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 symbol for unary
minus in Z has been added to the font and defined as a synonym of the
unary minus written as a tilde in the theory z_numbers. The symbol
displays and typesets as short minus sign. %cat%/ (i.e., a frown
followed by a backslash) is now defined as an alias for distributed
concatenation written %dcat% in the theory z_sequences.


The new minus sign appears to be missing from the palette.  (Am I going 
blind?)




b) In xpp, you can now switch dynamically between the horizontal and
vertical layout using a new item in the window geometry. N.b., this is
accompanied by a change in the way you specify the initial layout and
geometry in app-defaults/Xpp. See the CHANGES file for more details.


The switching is useful.  A few observations:

1. When there is no journal window, Show Geometry causes a crash:
xpp: fatal error: signal 11: memory fault: ...
(It may not crash the first time.)  Also, Ctrl+T causes a crash, even 
though there is no menu item Toggle Geometry without a journal window.


2. I have an issue with the design when using horizontal mode.  My 
app-defaults/Xpp sets column widths assuming there will be a journal 
window.  However, I am often opening file just to view/edit, i.e. no 
journal window, and always have to resize the window which is far too 
wide.  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?


For vertical mode, the current behaviour seems preferable.  I think 
different behaviour for the different orientations makes sense because 
of the asymmetric nature of documents: bounded width, unbounded height.


3. Given the above observation about document shape, should toggling 
attempt to maintain width by resizing the Xpp window?  I have had 
various ideas along these lines.  Have you thought about that?




c) z_%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 either failed or produced a result that was
not fully simplified.


Thanks, this is working now.

Phil



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

Re: [ProofPower] z_%mem%_seta_conv issue

[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 declaration.


Yes. This needs to be fixed.


I hope the work-around I posted was useful.


Yes, thanks - I have that working.

Phil



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

Re: [ProofPower] z_%mem%_seta_conv issue

[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 declaration.


Yes. This needs to be fixed.


I hope the work-around I posted was useful.

I have been thinking about how to fix z_%mem%_seta_conv and can do so,
but I don't like the fix much, so I thought I would share it with you
(and the list) to see if we can come up with something neater. The
fundamental problem is with the conversion z_%exists%_intro_conv1...


My current understanding is that z_%exists%_intro_conv1 is being passed 
a denormalized Z term.  Are conversions supposed to handle denormalized 
Z terms?  Thinking that they weren't, I was going to look into a fix to 
seq_binder_simple_%alpha%_conv or prot_%alpha%_conv to prevent this 
happening in the first place.  If it can be made to work, is that an 
acceptable solution?


Phil



...that
turns HOL existentials of a suitable form (specifically the form
returned by z_%exists%_elim_conv2) into Z existentials.
z_%exists%_intro_conv1 doesn't know how to deal with the case when
substitutions have caused bound variables to be renamed - but that case
can fairly easily be fixed using z_dec_rename%down%s_conv. Unfortunately
z_dec_rename%down%s_conv depends on z_rename%down%s_conv which is
defined in the DTD043 module which depends on DTD042 (where
z_%mem%_seta_conv lieves) and DTD041 (where z_%exists%_intro_conv1 lives).

Teasing out the dependencies so that z_rename%down%s_conv can be moved
into DTD041 doesn't look very promising, but maybe I haven't tried hard
enough. There may be something I could do with the hated functors, but I
don't know what. So the only option is to have a hook in DTD041 for
setting a conversion that z_%exists%_intro_conv1 uses where
z_dec_rename%down%s_conv is needed and calling that hook (and then
filtering it out of the signature) at the end of DTD041.

Regards,

Rob.



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





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

[ProofPower] z_%mem%_seta_conv issue

[Phil Clayton]

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 a way to finish 
it without getting stuck into the HOL embedding.  (As shown, renaming 
the schema components partially helps.)  Can anyone think of a Z 
work-around for now?


Thanks,
Phil


z_%mem%_seta_conv_issue.sml.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] How do you arrange Xpp?

[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 change this.

People like Mark with smallish screens should be aware that the window
menu now has a Show/Hide Journal item as well as Show/Hide Script. Even
when I using a big screen, I use these a lot when I am doing proofs (I
set PPLINELENGTH so that ProofPower formats things to use the full width
of the journal window when the script window is hidden).

What I may do in a forthcoming version is add a toggle geometry item to
the window menu so that the horizontal/vertical distinction can be made
dynamically.

Regards,

Rob.

On 22 Jul 2011, at 16:03, Mark wrote:


I use Xpp in 1-window mode for general text editing, and I also 2-window
mode for developing scripts. I want to develop my text with 80-character
width, which is the industry standard. Like many, I only have a 1280x800
screen, and so horizontal mode means that the journal window is very
squashed up if the script window stays at 80. So I prefer vertical.

I bet Phil is now going to show off about his new, super-hidef screen
laptop
and suggest horizontal mode... :)

Mark.

on 22/7/11 3:10 PM, Rob Arthan mailto:r...@lemma-one.com>> wrote:


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
Xpp*journal.columns: 60
Xpp*namestring.columns: 24
Xpp*journal.background: light blue
Xpp*journal.foreground: black
Xpp*journal.editable: true
Xpp*mainpanes.orientation: HORIZONTAL

This differs from the "out of the box" default in laying out the windows
side-by-side and letting you bring up the command dialogue by trying to

type

into the journal window. I am tempted to change the default settings to

the

above - it looks a bit less like a standard Motif application, but it

makes

much better use of modern screens (or at least modern screens that have a
landscape aspect ratio).

It would be nice to know what other people do before I commit to this
change. So please let me know your preferences.

Regards,

Rob.



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







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





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

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

[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 to!)

This issue was originally noticed because the following term prints
back without parentheses around the body of the lambda expression:

%SZT% %lambda% x : X
%spot% (%exists% [y : Y | p y]
%spot% [x : X; y : Y | q x y]) %>%; (1)


I.e., (for those who don't have the time to parse this in and pick it
apart), you have a lambda abstraction whose body is a schema expression
formed using the schema existential quantifier.


Consequently, the printed term does not re-parse. (Similarly for a mu
expression but let-expressions are ok.) In the printer module imp064,
it looks like parentheses would get inserted in (1): the precedence
for lambda and mu expressions is set to pc_expr0_%lambda%_%mu%_let.
However, the function do_binder_aux overrides the precedence with
PcLowest, inhibiting the parentheses. (Note pc_expr0_%lambda%_%mu%_let
is not used for let expressions, although its name suggests it is.)

Now, I think the issue is with the parser and parentheses should not
be required in (1) The definition of ProofPower-Z in usr005 (def007A)
appears to say that parentheses are not required: for non-terminal
Expr0, Expr in the lambda expression can be Schema.

A possible fix is to update the grammar in dtd061 by moving lambda and
mu expressions along side the current let/quantification expressions.
However, in doing this, I've noticed discrepancies between the syntax
in def007A and the grammar, so I'm not really sure whether this is ok.
See below.


To help the uninitiated, when Phil writes def007A he is referring to the
description of the ProofPower-Z language in part II of the manual USR005
"ProofPower Description".


Yes, def0070A.doc is the source file providing that part of USR005.



USR005 is just plain wrong about let-expressions/let-predicates. It
should do for them what it does for quantifiers, i.e., they should
appear twice: once as as a form of expression and once as a form of
predicate (as an extra alternative for Pred1) - the existing
disambiguation rules in section 6.4.14 of USR005 serve to resolve the
resulting ambiguity. This is what the parser implements for
let-expressions and let-predicates.



Phil


def007A allows a predicate as the body of a lambda expression but it
must be enclosed in parentheses as follows:

%lambda% x : X %spot% (x %mem% S)


Note that this example is not ISO Z, because it is not first order. An
analogous example that is standard Z is when the thing inside the
brackets is a schema-expression as in your original example above.


This was deliberately non-Standard because I thought a schema quantifier 
is already allowed without parentheses in the body by USR005 (because 
Expr can be Schema, even with the fix below).  (In Spivey, Expression 
can be Schema-Ref.)




However, the current implementation in dtd061 doesn't require the
parentheses, which seems to contradict def007A:

%lambda% x : X %spot% x %mem% S (* ok *)


USR005 (or def007A as you keep calling it) appears to have been trying
to follow Spivey Z here. Unfortunately it contains a very significant
typo: when it defines Expr = Expr0, it should say Expr = Expr1. With
this correction, USR005 is trying to give the same effect as Spivey
whereby lambda-, mu- and let-expressions have to appear in brackets.


Presumably Expr4 would be updated accordingly (by separating the 
singleton tuple case to allow Expr0 in a parenthesized expression).  It 
might be worth considering allowing Expr0 in other lowest-precedence 
contexts such as tuple/set/sequence display elements and 'inner' 
template arguments (as Spivey hardwires for the relational image set).




Somewhat to my surprise the Spivey rules require the brackets even after
the bullet in another lambda-, mu or let-expression. I.e., you can't
omit the brackets from:

let inc == 1 in (\lamda a : Z @ a + inc)

The ProofPower-Z parser corrects what I just consider to be errors in
USR005 and in Spivey's grammar: the symbol after the bullet in a
lambda-, mu- and let-expression should be Expr0 and not Expr.


That seems a sensible change to Spivey.



Now bearing in mind that the thing after the bullet in a lambda- and
mu-expression can sensibly be a schema-expression (even in first-order
ISO Z), it would make sense to allow arbitrary schema expressions
without brackets. This would amount to changing the symbol after the
bullet in USR005 from Expr to Schema. Here are two completely different
Z predicates.

val pred1 = %SZT%{} = (%fn%x: %bbZ%%spot% ([y: %bbZ% | x < y] %or% [y:
%bbZ% | y > x]))%>%;
val pred2 = %SZT%{} = (%fn%x: %bbZ%%spot% [y: %bbZ% | x < y]) %or% [y:
%bbZ% | y > x]%>%;

pred1 has no free variab

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

[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 with minimal parentheses, using the current
theory to determine whether parentheses are necessary, i.e. print C'
for (C)' if C' is not the name of a global variable.

B. Print in Standard-Z by always using enclosing parentheses for
decoration, i.e. print (C)' even if it is valid to print C'.

I think B can be achieved by simply dropping the ZLVar and ZGVar cases
on lines 670 and 671 of imp064.


I think B is not very nice for those used to Spivey Z. The following
heuristic seems good to me (and also fixes the remaining failures in
your new tests).


I have no objections here - I don't need Standard-form printed out - 
happy to see it fixed either way!




C. Add brackets if any of the following hold: (1) the operand is not a
variable (as now), (2) the operand is a local variable,
(3) the operand is a global variable whose name ends in a decoration
character, or (4) the operand is a global variable called N and there is
non-empty prefix P of the decoration such that N^P is declared as a
global variable.

Here (2) is the case when a local variable of schema type is decorated.
(4) is for the obscure case when, for example, the user has declared
schemas ABS and ABC!? and then says something like (ABC)!?! which the
parser will interpret as (ABC!?)! if you leave the brackets out.


I can't think of any case where this wouldn't work.  As long as 
unpack_ident and pack_ident are used in cases 3 and 4 (e.g. to test 
whether a name ends in a decoration character) there shouldn't be a 
problem with template forms.


I note that, as ProofPower stands, given

generic (ab _)

ab X == [a, b : X]

then

ab' X

prints back as

(ab X)'

To get the first form (which is in the spirit of your proposal) would 
need a change that is more than simply changing the condition for 
need_brackets in do_decor.


Phil



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

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

[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 parentheses around the body of the lambda expression:


%SZT% %lambda% x : X
%spot% (%exists% [y : Y | p y]
  %spot% [x : X; y : Y | q x y]) %>%;(1)

Consequently, the printed term does not re-parse.  (Similarly for a mu 
expression but let-expressions are ok.)  In the printer module imp064, 
it looks like parentheses would get inserted in (1): the precedence for 
lambda and mu expressions is set to pc_expr0_%lambda%_%mu%_let. However, 
the function do_binder_aux overrides the precedence with PcLowest, 
inhibiting the parentheses.  (Note pc_expr0_%lambda%_%mu%_let is not 
used for let expressions, although its name suggests it is.)


Now, I think the issue is with the parser and parentheses should not be 
required in (1)  The definition of ProofPower-Z in usr005 (def007A) 
appears to say that parentheses are not required: for non-terminal 
Expr0, Expr in the lambda expression can be Schema.


A possible fix is to update the grammar in dtd061 by moving lambda and 
mu expressions along side the current let/quantification expressions. 
However, in doing this, I've noticed discrepancies between the syntax in 
def007A and the grammar, so I'm not really sure whether this is ok.  See 
below.


Phil


def007A allows a predicate as the body of a lambda expression but it 
must be enclosed in parentheses as follows:


%lambda% x : X %spot% (x %mem% S)

However, the current implementation in dtd061 doesn't require the 
parentheses, which seems to contradict def007A:


 %lambda% x : X %spot% x %mem% S(*  ok  *)

ProofPower-Z does allow a predicate in the body of a let expression (an 
earlier design decision) but def007A has not yet been updated, e.g. it 
does not appear to permit


 let x %def% 2 %spot% x %mem% S

because it requires parentheses around the body.




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

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

[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 particular, this 
affects generic global variables that are not "template forms with one 
or more non-%bbU% generic actual parameters".)


In imp064, function do_generic, I believe references to 'name' on lines 
1350 and 1353 should refer to 'fullname'.  That change fixes most of the 
test failures.



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 with minimal parentheses, using the current theory 
to determine whether parentheses are necessary, i.e. print C' for (C)' 
if C' is not the name of a global variable.


B. Print in Standard-Z by always using enclosing parentheses for 
decoration, i.e. print (C)' even if it is valid to print C'.


I think B can be achieved by simply dropping the ZLVar and ZGVar cases 
on lines 670 and 671 of imp064.


Phil



mdt064.doc.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Schema in a predicate stub

[Phil Clayton]

Rob,

On 11/07/11 13:37, Rob Arthan wrote:

Further to my earlier reply to Phil's suggestion (outlined below), I
have looked into implementing it and it all looks good to me.


That's good - I was poised to have a go myself!



There is
only one consequence that I can see that looks a little strange at
first, but makes sense when you think about it. This is the treatment of
conditionals in quotations. If you enter:

%SZT% if 1 = 2 then 3 else 4 %>%

it will fail, because the top level of a Z quotation is a predicate
context (but not an operand of a stub, so non-predicates are allowed).
To get this to work you have to force an expression context:

%SZT% (if 1 = 2 then 3 else 4) %bigcolon% %bbU %>%

Arguably we should have a separate quotation symbol to introduce a Z
expression. The justification for the quotation to default to predicate
is easy to see when you think about entering ordinary logical
expressions: it would be very painful if they defaulted to being 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.


I agree with your view.  Although it may be necessary to force an 
expression for such terms, overall I think the behaviour is clearer 
because it's more uniform.


Whether to have a separate expression quotations is an interesting 
question.  The need to force an expression is not that common so 
%bigcolon% %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 there any reason why a schema argument in a predicate stub (_?) isn't
implicitly converted to a predicate? ...


There is also the question of whether context stubs (_!) should be
checked as predicates when the context is a predicate. Given

function (op2 _!)

would we expect

%SZT% [ | op2 2] %>%

to fail because 2 is not a predicate? (Irrespective of any definition
op2 may have.) I think I would. (This looks more effort to implement.)


I will look into implementing something along these lines.

Regards,

Rob.


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




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





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

Re: [ProofPower] Xpp on Fedora 14 and later

[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 executable, i.e. a long string in argv[0], at run-time.


On my machine, when argv[0] (incl. null terminator) is more than 78 
characters, xpp crashes.  I can reproduce it simply by copying my 
existing pp installation to a new directory as follows:


  cp -a /opt/pp/pp-2.9.1w2.rda.110226 
/tmp/ppxxx


Then argv is
/tmp/ppxxx/bin/xpp
which is 79 characters (incl. null terminator) and this makes xpp crash.

Unfortunately all my builds since moving to Fedora 15 were temporary 
builds to test patches which were located somewhere deep in the 
directory hierarchy.


Phil

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

Re: [ProofPower] Xpp on Fedora 14 and later

[Phil Clayton]

Rob,

Thanks - using jpegs solves the issue.

Phil


On 09/07/11 15:28, Rob Arthan wrote:

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 ProofPower
installation directory (or your own bitmaps directory if you have one)
and change all the ".bmp" file extensions in app-defaults/Xpp to ".jpg",
that should give you a workaround. Please 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.) This appears to be due
to the following:
http://bugs.openmotif.org/long_list.cgi?buglist=1539
I haven't looked into any work-around.

On Fedora 15, building Xpp works but it seg faults when I run it - see
attached xpp_output.log. I can run a version built elsewhere but it
has serious issues not updating the text windows when scrolling under
certain circumstances, which may be related to Gnome 3 - I don't know.

Anyone unfortunate enough to be using Gnome 3 as well will find that
the left window key (Super_L) is now used by Gnome. There is a simple
work-around apart from the obvious using another modifier key. For
Shift+Super_L make sure you press Shift first
Super_L press X; press Super_L; release X
where X is any benign key. I use Shift (as I'm already in the habit of
pressing Shift+Super_L).

Phil - wishing I had stuck with Fedora 13 for now...
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com




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



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

[ProofPower] Empty schema paragraphs

[Phil Clayton]

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 as the 
corresponding Z constraint paragraph.  (In the processing of terms, 
there were many places where an axiomatic description with an empty 
declaration could be mapped to the existing constraint paragraph 
support, if at all.  I took the view that the distinction between 
axiomatic descriptions and constraints was useful at the abstract level 
because they work differently with the ProofPower theory support so that 
support for constraints would probably remain.  However, the 
concrete-level support (parsing, syntax trees) is now redundant and, not 
being in the Standard, I thought it may become deprecated at some point. 
 Thus the implementation only uses the existing abstract level support 
for constraints.)


Note that this patch is relative to my earlier patch pbc.110605 as they 
involve changes to the same files.


Phil



patch-2.9.1w2.rda.110226.pbc.110605.pbc.110706.txt.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

[ProofPower] Xpp on Fedora 14 and later

[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 looked into any work-around.

On Fedora 15, building Xpp works but it seg faults when I run it - see 
attached xpp_output.log.  I can run a version built elsewhere but it has 
serious issues not updating the text windows when scrolling under 
certain circumstances, which may be related to Gnome 3 - I don't know.


Anyone unfortunate enough to be using Gnome 3 as well will find that the 
left window key (Super_L) is now used by Gnome.  There is a simple 
work-around apart from the obvious using another modifier key.  For

  Shift+Super_L  make sure you press Shift first
  Super_Lpress X; press Super_L; release X
where X is any benign key.  I use Shift (as I'm already in the habit of 
pressing Shift+Super_L).


Phil - wishing I had stuck with Fedora 13 for now...


xpp_output.log.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Schema in a predicate stub

[Phil Clayton]

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 then X else Y

However, this produces a type error: we must explicitly say that True is
to be taken as a predicate, i.e.

if %Pi% True then X else Y

which seems unnecessary.


I note that the built-in function %Pi% (that forces its argument to be 
taken as a predicate) is defined using a predicate stub (_?) but _does_ 
convert schemas to schemas as predicates.  It is the special handling of 
%Pi% during type-checking that achieves this conversion, not the 
predicate stub.


It would certainly make sense for predicate stubs to be type-checked as 
predicates.  (I was about to modify the type-checker to do that, which 
looks fairly simple.)  Thus, given


function (op1 _?)

I would expect

%SZT% [ | op1 2] %>%

to fail because 2 is not a predicate, irrespective of any definition op1 
may have.  Is there any reason ProofPower-Z does not want this behaviour?


There is also the question of whether context stubs (_!) should be 
checked as predicates when the context is a predicate.  Given


function (op2 _!)

would we expect

 %SZT% [ | op2 2] %>%

to fail because 2 is not a predicate?  (Irrespective of any definition 
op2 may have.)  I think I would.  (This looks more effort to implement.)


Phil



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

Re: [ProofPower] z_%mu%_eq_tac?

[Phil Clayton]

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 to break
the goal into a forall and exists subgoal. This often removes the need
to explicitly mention %mu% TERMs (to apply to z_%mu%_rule) making proofs
more tolerant to changes.

Incase it's useful to anyone (I know Steve King has been fiddling with
%mu%s) I've attached my implementation --- called z_%mu%_eq_tac.

Would there be any value in adding such a tactic to ProofPower?
(Possibly even as a stripping tactic?)

Phil


patch-2.9.1w2.rda.110226.pbc.110705.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] v_%exists%_intro efficiency

[Phil Clayton]

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 anymore - see test below. It
looks like simple_%exists%_intro has undergone an enhancement but no
corresponding modification was made to v_%exists%_intro.
(v_%exists%_intro follows precisely the `old style imlementation' of
simple_%exists%_intro without the costly initial term_match but with a
more general %beta%_conv for pair quantification.)


Well, nearly 7 years on, v_%exists%_intro is still slower than 
simple_%exists%_intro, though not as much as it was.




It looks to be a simple fix to base v_%exists%_intro on the new
implementation of simple_%exists%_intro - see attachment - given the
availability of simple_%exists%_intro_thm from imp007. Any improvement
would have knock-on effects in some other functions e.g.
%exists%_reorder_conv.


A patch for this is attached.  It is relative to 2.9.1w2.rda.110226 
rather than the latest working release 2.9.1w2 to make it easier to 
apply.  Most of the changes relate to exposing the theorem 
simple_%exists%_intro_thm, which I renamed to %exists%_intro_thm as it 
is not limited to simple quantification.


See following tests for performance improvement.


(* test values *)
val tm = %<%%exists% b c x y %spot% f (x + y + z) (y * 234 - a) %or% g b 
(c - 100)%>%;

val v = %<%a : %bbN%%>%;
val thm = asm_rule tm;
val %exists%_tm = mk_%exists% (v, tm);

PolyML.timing true;

(* test simple_%exists%_intro *)
val c = ref 50;
while !c > 0 do (
   simple_%exists%_intro %exists%_tm thm;
   c := !c - 1
);
(* ~3.5s *)

(* test v_%exists%_intro *)
val c = ref 50;
while !c > 0 do (
   v_%exists%_intro v thm;
   c := !c - 1
);
(* ProofPower 2.9.1w2.rda.110226:~5.0s *)
(* ProofPower 2.9.1w2.rda.110226.pbc.110704: ~1.1s *)


Note that my computer is just over 10 times faster than the one I was 
using 7 years ago for the above tests!  More interestingly, that is 
significantly less than 2^(7/1.5) times... I suppose that begs the 
question: where does concurrency feature on the ProofPower roadmap?


Phil


patch-2.9.1w2.rda.110226.pbc.110704.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

[ProofPower] Schema in a predicate stub

[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 error: we must explicitly say that True is 
to be taken as a predicate, i.e.


  if %Pi% True then X else Y

which seems unnecessary.  Above example attached.

Phil


schema_in_pred_stub.sml.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Type inference issue with characteristic tuples

[Phil Clayton]

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 reference S.  This avoids the question of what 
happens when both S and S' are global variable names.




Yes. Horrible isn't it. The space is barbaric by usual mathematical 
typographical standards and is an incompatibility with Spivey Z.


Horrible, it is, and I am in favour of supporting Spivey-Z except as in 
point 2 below.



2. Should ProofPower-Z allow S ' to be interpreted as the name S', 
i.e. ignoring space between the two tokens and taking them as one 
token?  I would never expect e.g. abc def to be taken as the name abcdef.


Apart from the above comment about _mathematical_ typography rather than 
programming language practice, I really don't want to get into a debate 
about why it should or should not be as it is, since I went into this 
kind of question very carefully and at some length during the Z 
standardisation process (see the document Issues for Concrete Syntax 
at http://www.lemma-one.com/zstan_docs/zstan_docs.html). ProofPower-Z 
implements the scheme described there that is backwards compatible with 
Spivey in all but very obscure cases. This was a typical case where one 
existing tool implemented a thought-through approach which gave the 
desired new semantics using a syntax that was designed to be compatible 
with Spivey at least in typical cases, but, while no other tool 
supported either the desired semantics or the syntax, the standards 
committee chose a different and incompatible approach.


On practical grounds, I'm not a huge fan of the choice made (Decor.3) 
either.


I'll just summarize my point in relation to Spivey-Z.  Lexing S ' as two 
separate tokens in ProofPower-Z would cause ' to be parsed as a schema 
decoration so type checking would require S to have schema type.  This 
would:


1. Rule out Spivey-Z specifications where identifiers contain white 
space before any decoration, e.g.

  x '
which would need to be written as
  x'
Hopefully nobody does or would want to write identifiers in such a way. 
 I think it's really horrible to see x ' for the identifier x' where 
the ' has no special significance - just the last character of the name. 
 In fact, it doesn't even have to be on the same line:

  0 < x
  '

2. Give compatibility with Standard-Z in the following obscure case:

 Note that when both S and S' are global variable names, S ' is a 
reference to S' in ProofPower-Z, not the schema decoration of S.  Not 
only is this surprising, it is different to Standard-Z.  (Section 7.3 
in Z Standard.)


Of course, only the seriously crazed declare global variables with 
decoration on them.


I agree, it's best avoided.


Currently, my thinking is that a separate Standard-Z compatible parser 
would be a useful adjunct to ProofPower-Z, but I am still much 
interested in some level of backwards compatibility with Spivey Z, 
because all the significant specs I have come across in industry are in 
Spivey Z. So I have no plans to throw away the existing parser.


I don't think the impact on Spivey-Z is too bad but understand your 
reasons for keeping it this way.  I'm not hell bent on conforming to the 
Standard though - I really don't like the way the language allows an 
identifier to be input containing white space!


Phil




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

[ProofPower] Characteristic function construction?

[Phil Clayton]

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" raised

because there is no support for generating the characteristic tuple of a 
lambda expression.


Is/was there some intention of allowing lambda expressions without a 
spot to construct an identity function?  I can't see that this is much 
use because the toolkit function "id" is just as good and in some cases, 
better, e.g.


  (%lambda% x : X | p x) = id {x : X | p x}
  (%lambda% x : X)   = id X

Attached is a fairly mundane patch that adapts the grammar for lambda 
expressions.  Then e.g.


  (%lambda% x : X)

produces a regular syntax error.

Phil


patch-2.9.1w2.pbc.110605.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

[ProofPower] Type inference issue with characteristic tuples

[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, due to an internal type mismatch:


  {{S; S'}}
  {S; S'} = A

The type of {S; S'} should be the same as for {S; (S)'}, i.e.

  [X : T] %rel% [X : T]

However, type inference incorrectly computes the type of {S; S'} as

  [X : T] %rel% [X' : T]

- the type of the different term {S; (S ')}.  When terms are constructed 
after type inference, construction of the characteristic tuple has the 
correct type.  However, incorrect type annotations can be present 
elsewhere in the term from type inference, causing the type mismatch 
when building terms.


The problem is that type inference generates the characteristic tuple 
for the schema text, e.g. S; S', before type checking the schema text. 
Consequently S' has not been converted from a local variable to a 
decorated global variable when the characteristic tuple is generated, so 
the characteristic tuple (effectively) contains


  %theta% (S ')

rather than

  %theta% S '

I think this is fairly simple to fix - see attached patch.  Note that 
there is no problem with


  {S; (S)'}

because there is no local variable S' to cause the problem.  (This can 
be used as a work-around.)


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 reference S.  This avoids the question of what 
happens when both S and S' are global variable names.


2. Should ProofPower-Z allow S ' to be interpreted as the name S', i.e. 
ignoring space between the two tokens and taking them as one token?  I 
would never expect e.g. abc def to be taken as the name abcdef.  Note 
that when both S and S' are global variable names, S ' is a reference to 
S' in ProofPower-Z, not the schema decoration of S.  Not only is this 
surprising, it is different to Standard-Z.  (Section 7.3 in Z Standard.)


Phil


char_tuple_issue.sml.gz
Description: GNU Zip compressed data


imp062.doc.patch.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] prim_rewrite_conv etc.

[Phil Clayton]

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 matching/rewriting facilities be implemented 
for Z also? If not, does the updated rewriting infrastructure support 
a corresponding implementation for ProofPower-Z?


The infrastructure will support any way of turning a theorem into a pair 
comprising a pattern term and a conversion to apply to terms that match 
the pattern. But bear in mind that higher-order matching for HOL just 
won't work for Z.


Yes, I don't expect it to given that HOL lambda is totally different to 
Z lambda.



If you are designing theorems specifically for use as 
higher-order rewrite rules, it might be simpler to write them in a 
mixture of HOL and Z so you can use higher-order matching.


I'm guessing you mean use e.g. HOL function application instead of Z 
function application, HOL for all instead of Z for all etc. as required? 
 I may well take up that idea if a theorem exposes the underlying HOL 
anyway but probably wouldn't want to 'dirty' otherwise pure Z theorems.



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.


I may have a think about that once I've had a look at your HOL version!

Phil



Rob Arthan wrote:

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 will give the same behaviour as currently. 
If anybody has code that would be badly affected by this, please let 
me know.

Regards,
Rob.

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





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





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





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

Re: [ProofPower] prim_rewrite_conv etc.

[Phil Clayton]

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 implementation for ProofPower-Z?


I can see Z has complications for lambda abstractions not over U but 
expecting the domain condition as per z_%beta%_conv seems ok.


Phil


Rob Arthan wrote:

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 will give the same behaviour as currently. If anybody 
has code that would be badly affected by this, please let me know.


Regards,

Rob.




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





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

Re: [ProofPower] xpp Segmentation fault

[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 never worked for me: it will just say that the 
process exited normally. As it is fairly rare that running in the background makes any 
difference, I usually try debugging with "-b" first. You don't need to single 
step with gdb if the failure you are expecting is a signal like a segmentation fault, gdb 
will trap the signal and prompt for commands.]


Thanks, that's useful to know.

Phil




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

Re: [ProofPower] xpp Segmentation fault

[Phil Clayton]

Hi Shu,

Unfortunately, I don't have any Mac OSes available to me, so I can't try 
anything out myself.  All I can suggest at this stage is to


1. Have a look at build.log to see whether the compiling/linking of xpp 
produced any warnings etc.  (You'll have to search for the place that 
builds xpp.)


2. Run the program through gdb (the GNU debugger) to see if that can 
shed any more light on the seg fault, e.g.


  gdb xpp
  (gdb) start
  (gdb) continue

Even better would be to find the line in the C source code on which it 
seg faults, e.g.


  gdb xpp
  (gdb) start
  (gdb) step
  ...
  etc.

(I am assuming gdb is available on the Mac.  Also, you may have a better 
debugger to hand, e.g. a graphical one.)


This isn't ideal.  Hopefully one of the Mac users can shed more light on 
this issue!


Phil


Shu Cheng wrote:

Hi Phil,

Thanks very much for your reply.

1 Yes, pp -d  is work well.

2 I downloaded the latest version of ProofPower, which is ProofPower 
2.9.1w2 [HOL/Z Database]


3 I am using Mac OS X version 10.6. "uname -a" reports
"Darwin Shu-Chengs-MacBook-Pro.local 10.0.0 Darwin Kernel Version 
10.0.0: Fri Jul 31 22:47:34 PDT 2009; root:xnu-1456.1.25~1/RELEASE_I386 
i386"


4 Yes, I built it on this machine yesterday.

5 "PPENVDEBUG=1 xpp" reports

xpp: invoked as /usr/local/pp/bin/xpp
xpp: using PPHOME=/usr/local/pp
xpp: using 
PATH=/usr/local/pp/bin:/opt/local/bin:/opt/local/sbin:/usr/bin:/bin:/usr/sbin:/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 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.
  Otherwise:
The ProofPower version is contained in the
file $PPHOME/VERSION where PPHOME is such that
  "which xpp"
returns $PPHOME/bin/xpp.
Also, in this case, the Poly/ML version will be useful.
What does "ldd `which pp-ml`" say for libpolyml
and what version is Poly/ML in that directory.

3. What OS (incl. version) are you using?
  What does "uname -a" report?

4. Are you running xpp (or pp) on the machine that
  it was built on?
  If not:
What does "file `which xpp`" report?
If you can, what does "uname -a" give for the
machine that built it?

5. Does "PPENVDEBUG=1 xpp" produce any more output?

That's probably enough to start with!

Phil


Shu Cheng wrote:

Hello everyone,
I am a fresher here.
When I try to use "xpp -d database" to open an xpp session in X11, I 
get an error message -- Segmentation fault. Is anyone have any idea 
for this?

Thanks a lot!
Shu Cheng
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com







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






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

Re: [ProofPower] xpp Segmentation fault

[Phil Clayton]

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.
   Otherwise:
 The ProofPower version is contained in the
 file $PPHOME/VERSION where PPHOME is such that
   "which xpp"
 returns $PPHOME/bin/xpp.
 Also, in this case, the Poly/ML version will be useful.
 What does "ldd `which pp-ml`" say for libpolyml
 and what version is Poly/ML in that directory.

3. What OS (incl. version) are you using?
   What does "uname -a" report?

4. Are you running xpp (or pp) on the machine that
   it was built on?
   If not:
 What does "file `which xpp`" report?
 If you can, what does "uname -a" give for the
 machine that built it?

5. Does "PPENVDEBUG=1 xpp" produce any more output?

That's probably enough to start with!

Phil


Shu Cheng wrote:

Hello everyone,

I am a fresher here.

When I try to use "xpp -d database" to open an xpp session in X11, I get 
an error message -- Segmentation fault. Is anyone have any idea for this?


Thanks a lot!

Shu Cheng

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






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

[ProofPower] Exceptions not translated for output - raw_diag_string in imp110?

[Phil Clayton]

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 occurrences to use diag_string instead (see 
patch) and this seemed to solve the issue this those cases.


A more interesting example is

   use_string "plus_conv %SZT%Q%>%;";

The patch reduces the number of Qs in the exception message from 16 to 4 
but would we expect the 4 Qs to reduce to 1?  As ordinary users _must_ 
be aware that Q in a string is escaped as , perhaps not?


Phil


patch-imp110.txt.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Extended characters in exceptions

[Phil Clayton]

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 to specify their own writer functions for writing 
text output from the compiler, these user-supplied writers are 
bypassed for the exception text output.  Therefore the ProofPower 
writer can't be used here and, unfortunately. Poly/ML thinks \181 is 
unprintable so escapes it.


That is not exactly what happens, but the effect is the same. The 
ProofPower reader/writer is calling the compiler and handling any 
exceptions raised. If it gets an exception defined by ProofPower, like 
BasicError.Fail - the one raised by the function fail - then it can take 
special action. If it gets some other exception, it calls 
General.exnMessage from the standard basis library to find out what to 
print, and the Poly/ML implementation of General.exnMessage just formats 
the exception as if it were about to print it in its read/eval/print 
loop. ProofPower could treat General.Fail specially, but that probably 
isn't what Roger wants (is it?).


Good point - I forgot that the read/eval/print loop is catching all 
exceptions.  It looks like exnMessage is just creating strings with 
PolyML.makestring which (I think) is using String.toString to print the 
body of strings (see basis/String.sml, lines 882-886.)  I was going to 
suggest just installing a new printer for the type string that does not 
escape the ProofPower printable characters - I tried it and it works - 
but have been sidetracked looking into the writer side of things.


Phil




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

Re: [ProofPower] New Languages in ProofPower

[Phil Clayton]

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 lexer/parser - I assume you're ok with that.


If you are producing a new object language, it is probably best to use 
HOL_reader.  (One reason not to is if your language has any white space 
oddities.)  HOL_reader is used for Z quotations in ProofPower-Z, for 
example.


If your object language allows nested term quotations, your lexer will 
need a token for terms that is produced when a Lex.Term input is 
encountered.


Regards,

Phil


Roger Bishop Jones wrote:
Does anyone have a small/simple example of how to add a new 
language to ProofPower?


Roger Jones




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




reader.sml.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Extended characters in exceptions

[Phil Clayton]

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 compiler interface 
allows applications to specify their own writer functions for writing 
text output from the compiler, these user-supplied writers are bypassed 
for the exception text output.  Therefore the ProofPower writer can't be 
used here and, unfortunately. Poly/ML thinks \181 is unprintable so 
escapes it.


If you process the supporting SML at the end of this message, you will 
see when the user-supplied writers are used by Poly/ML:


  compileString "\"abc\";";
(* CPOutStream writer used for normal text output *)

  compileString "PolyML.print \"abc\";";
(* CPPrintStream writer used for PolyML.print output *)

  compileString "raise General.Fail \"abc\";";
(* Note that exception message does not go via
   either CPOutStream or CPPrintStream writers *)

I think Rob may have more info on why Poly/ML is like this.

Phil


(* Supporting SML *)

local
  val input = ref ""
  val pos = ref 0

  fun setInput s = (input := s; pos := 0)
  fun readInput () =
SOME (String.sub (!input, !pos)) before pos := !pos + 1
  handle
Subscript => NONE

  open PolyML.Compiler
in
  fun compileString s = (
setInput s;
PolyML.compiler
  (readInput,
   [CPOutStream (fn s => app print ["\nCPOutStream[", s, "]"]),
CPPrintStream (fn s => app print ["\nCPPrintStream[", s, "]"])])
()
  )
end;

(* End of supporting SML *)


Roger Bishop Jones wrote:

-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1

Is there a way to get string valued exceptions to print 
extended characters correctly?


Roger Jones
-BEGIN PGP SIGNATURE-
Version: GnuPG v1.4.10 (GNU/Linux)

iEYEARECAAYFAk2op9wACgkQpS+qcQX1oA+2vQCdEqFqkt4z1U3ZVJsF5TLxUy9f
vMkAoJcf2wlbyiygoHi0FteGVWAaFYsP
=LuxB
-END PGP SIGNATURE-

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






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

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

[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 the 
behaviour of particular proof procedures like forward chaining.


I've noticed some change to the proof context output of print_status (as
supplied by get_current_pc):

1. The output of print_status now includes the all proof contexts
implicitly included by the specified proof context.  For example, for

  set_pc "z_library"

print_status produces

  Current proof context name(s): ['z_predicates, 'z_decl,
   z_predicates, 'z_%mem%_set_lang, 'z_bindings, 'z_schemas,
   'z_tuples, z_language, 'z_normal, 'z_%mem%_set_lib,
   'z_sets_alg, z_sets_alg, 'z_rel_alg, 'z_fun_alg,
   'z_numbers, z_library];

2. If a proof context is requested more than once, explicitly or
implicitly, it appears more than once in the list printed by
print_status.  For example, for

  set_merge_pcs ["z_library", "z_predicates"];

print_status produces

  Current proof context name(s): ['z_predicates, 'z_decl,
   z_predicates, 'z_%mem%_set_lang, 'z_bindings, 'z_schemas,
   'z_tuples, z_language, 'z_normal, 'z_%mem%_set_lib,
   'z_sets_alg, z_sets_alg, 'z_rel_alg, 'z_fun_alg,
   'z_numbers, z_library, 'z_predicates, 'z_decl,
   z_predicates];

I suspect 1 and 2 are really the same thing.  I presume this is
unintended as it does not fit the behaviour described for get_current_pc
in the manual.  I actually found it quite useful to see the component
parts of the proof context without having to refer to the manual, though
I think the old behaviour should still be present for print_status, i.e.
telling the user what they specified.


Regarding this new capability, given a current proof context e.g.
["z_library", "'z_reals"], is it more efficient to do e.g.
  set_extend_pcs ["a", "b"];
than
  set_merge_pcs ["z_library", "'z_reals", "a", "b"]
?  It looks like it is from reading the source code but I didn't fully
digest everything.

Also I noticed imp051.doc, line 1594:
fun Ûset_extend_pcsÝ ([]: string list): unit = fail "set_merge_pcs" 51020 []
should probably not say "set_merge_pcs".


b) A variable capture problem in %implies%_match_mp_rule1 that made 
forward chaining fail has been addressed in a new rule 
%implies%_match_mp_rule2. The new behaviour has been adopted as the 
default, but this can make some existing proofs break. Component proof 
contexts "'mmp1" and "'mmp2" are provided that let you switch between 
the new and old behaviour. Using, set_extend_pc"'mmp1" or EXTEND_PC_T 
"'mmp1" will revert to the old behaviour and gives a quick way of fixing 
any broken proof scripts.


Glad to see that has been fixed.  I have stumbled on that one every so
often for years but never got around to looking into it.

Phil





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

[ProofPower] Check for normal Z terms when printing?

[Phil Clayton]

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 bound variable in the underlying HOL 
representation of the Z term, leading to a 'denormalized' Z term.  There 
is no issue with the logic for mechanized proof, though it could well 
cause some confusion when reading the printed version.


On the few occasions I have seen this before, it has been during 
interactive proof.  I assume that %alpha%_to_z_conv/%alpha%_to_z will be 
used in future to avoid this sort of thing in Z variants of HOL proof 
support.  However, I'm not sure that you can, or would want to, use the 
above functions to adjust the Z parts of a term when reading quotations.


Should these 'denormalized' Z terms be rejected as Z terms, thus printed 
as plain HOL?  The documentation for %alpha%_to_z_conv/%alpha%_to_z 
suggests that such terms "fail to be Z", if I understand it correctly.


On the other hand, it is useful to see Z syntax so perhaps the Z printer 
should somehow warn that it is printing a 'denormalized' Z (sub)term?


Also, for the offending subterm

  [x' : 1 .. 2]

basic_dest_z_term returns BdzOk ... - should it?  (Would it be useful 
for datatype BDZ to have another category, e.g. BdzDenorm ?)


Phil




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

Re: [ProofPower] Broken theory indexes

[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 %bbS% occurs 
in a section heading, consequently e.g. dtd052.dvi does not build.


So perhaps making that change to the sievekeyword file fixes it. 
However, I can't remember the precise error I got so this may be nothing 
to do with your issue.


Phil


Roger Bishop Jones wrote:

I am now running ProofPower on Ubuntu 10.04 LTS.

In the last couple of days something has been automatically 
upgraded which has broken the processing of indexes on 
ProofPower documents (I believe this because when I roll 
back my ProofPower work several weeks I still have the 
problem which only appeared today.)


Has anyone else experienced this?

This is a sample of the kind of error I am getting (while 
LaTeX is processing a .sid file).


! Extra }, or forgotten $.
 ...\mathgroup \symAMSb \relax S\egroup 
  $\leaders 
\hbox to 0.5em{\...

l.30 ...up \mathgroup \symAMSb \relax S\egroup }{}
  }
{\hyperpage{206}}

Roger Jones

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






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

Re: [ProofPower] Cut and Paste problem

[Phil Clayton]

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 detail, just follow the 
commands at the bottom.  I can't say what the OpenMotif situation is for 
non-Fedora Linux distributions or where to get an appropriate version.


Phil


Roger Bishop Jones wrote:

I have one other problem with my present set-up.

In xpp cut and paste don't work, neither by keyboard nor by 
menu.


If anyone else has come across this and can help that would 
be appreciated.


Roger Jones

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






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

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

[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.  This is generally useful anyway

 as it makes the references in a document hyperlinks.


I do have these things in my documents, but at the time I 
started doing PDFs they did not have that effect.


The main problem I had at the time was in getting 
hyperlinked indexes to work,
ProofPower at the time had its own way of doing indexes 
which did not use makeindex, and this didn't work out with 
the hyperlinks.
In the end I decided that the best way to get the hyperlinks 
to work was to change texpdf to use makeindex instead of 
whatever it was then doing.


So, are you telling me that I can now get pdf files with 
hyperlinked indexes without any changes to the ProofPower 
document preparation scripts?


No, I was just talking about the links within a document using \label 
and \ref and things like the contents page.  That's all pure LaTeX so is 
bound to work.  I'd forgotten that hyperref breaks the index support.


Phil



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

[ProofPower] Generating PDF files with texdvi and docdvi

[Phil Clayton]

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 first,
but then it will invoke texpdf and fail to find it.
I suppose I could put "./texpdf in docpdf.
In rbj.src.tgz these are supplied but unless you put "." in 
the path it doesn't work.

Any ideas how to do this kind of thing?


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 generally useful anyway as it makes the references in 
a document hyperlinks.


I believe that this works on my Linux installations (Fedora >= 10) 
because latex and pdflatex are just symbolic links to pdftex and pdftex 
(presumably) has some logic to determine what to behaviour is required. 
 Presumably many things could trigger the production of a PDF file 
rather than a DVI.  As you can see, I don't really know why this works...


Ideally one wouldn't specify the pdftex option above because that forces 
a PDF file to be generated.  Perhaps latex or pdflatex would be invoked 
depending on an environment variable e.g. PPDOCFORMAT?


Regards,

Phil



eg.doc.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] pp-contrib

[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 if that was a question for Roger or me.)  For me, an 
example is extending proof support for Z sequences.  This involves 
significant changes to the structure ZSequences1 and associated theory 
in dtd107 and imp107.  There are likely to be changes for knock-on 
effects but I haven't got that far yet.




Personally, I am happy with GPL (2 or 3).


Well, so far it looks like GPL3 on google with mercurial.


GPL 3 would rule out the ProofPower code base as that is GPL 2.  GPL 2 
and 3 are 'incompatible': http://www.gnu.org/licenses/rms-why-gplv3.html

So, whilst ProofPower is GPL 2, my preference would actually be GPL 2.
(Note ProofPower does not specify "any later version" regarding GPL.)

That would be about redistribution. You won't be redistributing 
OpenProofPower on pp-contrib. I am considering the "any later version" 
option, but don't consider it a big issue at the moment because I don't 
think anybody will want to do redistribute OpenProofPower other than 
perhaps as a freestanding whole so that it can be freely combined with 
other GPL 2 and GPL 3 offerings regardless of which I use.


For changes to the OPP code base like above, a baseline version of the 
OPP source really needs to be in the repository.  There is no intention 
to be redistributing OPP, just making the changes available, however 
someone would get everything in the repository when cloned.  What do you 
think of that set up?



In fact, this may be an issue for the sort of contributions you are 
talking about too.  On the one hand, one could view ProofPower like a 
compiler that processes theories and these theories could be viewed as 
works in their own right, so they could have whatever licence the 
author wants.  On the other hand, one could view these theories as ML 
programs that make calls to the ProofPower library of ML functions so 
would need to be available under GPL 2:

http://www.gnu.org/licenses/old-licenses/gpl-2.0-faq.html#IfLibraryIsGPL
http://www.gnu.org/licenses/old-licenses/gpl-2.0-faq.html#LinkingWithGPL
That does not stop them also being made available under a 'compatible' 
licence, i.e. one that is upstream from GPL 2 in the following diagram:
http://www.gnu.org/licenses/quick-guide-gplv3.html#new-compatible-licenses 

Under the latter interpretation, which is probably the right one, I 
don't think it would be possible to make the contributions available 
under GPL 3 as it stands.



Please bear in mind that an open source licence is simply a public 
statement that the copyright holder won't take legal action against 
users of their software who haven't bought a licence but do conform with 
a given set of rules. It isn't a contract. It is the copyright holder 
who is going to assess conformance with the rules and decide whether to 
take action against a user. If that every happened, then no doubt a 
court would take the terms of the open source licence into account.


 In this case, the copyright holder is Lemma 1 and my position is 
essentially like that of Larry Wall on Perl scripts and the GPL (see 
http://dev.perl.org/licenses). That means that I will always take your 
first interpretation for scripts that are distributed separately from 
OpenProofPower. I would be very happy to make a similar public statement 
about this to clarify the position and would it make it clear that 
distributing theory scripts under GPL3 is OK. The only thing I really 
want to prevent is someone shrink-wrapping OpenProofPower inside their 
own packaging and selling the result (i.e., unlike Perl, I definitely 
don't want to use something like the Artistic Licence).


Thanks for explaining that.  I think it is important to clarify you 
interpretation on the ProofPower licence web page and in the LICENCE 
file.  Unless stated, nobody will ever really know.  For example, it 
wasn't clear whether you take Larry Wall's position on object code too. 
 Under GPL, someone can pass on a binary release of OpenProofPower, as 
long as they (offer to) provide the source.  Can they provide a 
proprietary child database or is that within your definition of 
shrink-wrapping?


Phil



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

Re: [ProofPower] pp-contrib

[Phil Clayton]

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 things which don't 
fit into that.


Perhaps one directory for "maths_eq"-like contributions, one 
for contributions in the form of patches, and another for 
other kinds of things.  The first two having some rules to 
provide uniform installation, the last consisting of 
contributions each of which makes up its own rules.


That sounds flexible enough.  Does this all go into one repository?  (I 
don't know what is possible or most suitable using Mercurial on google 
code.)




Personally, I am happy with GPL (2 or 3).


Well, so far it looks like GPL3 on google with mercurial.


GPL 3 would rule out the ProofPower code base as that is GPL 2.  GPL 2 
and 3 are 'incompatible': http://www.gnu.org/licenses/rms-why-gplv3.html

So, whilst ProofPower is GPL 2, my preference would actually be GPL 2.
(Note ProofPower does not specify "any later version" regarding GPL.)

In fact, this may be an issue for the sort of contributions you are 
talking about too.  On the one hand, one could view ProofPower like a 
compiler that processes theories and these theories could be viewed as 
works in their own right, so they could have whatever licence the author 
wants.  On the other hand, one could view these theories as ML programs 
that make calls to the ProofPower library of ML functions so would need 
to be available under GPL 2:

http://www.gnu.org/licenses/old-licenses/gpl-2.0-faq.html#IfLibraryIsGPL
http://www.gnu.org/licenses/old-licenses/gpl-2.0-faq.html#LinkingWithGPL
That does not stop them also being made available under a 'compatible' 
licence, i.e. one that is upstream from GPL 2 in the following diagram:

http://www.gnu.org/licenses/quick-guide-gplv3.html#new-compatible-licenses
Under the latter interpretation, which is probably the right one, I 
don't think it would be possible to make the contributions available 
under GPL 3 as it stands.



On google you can have a different licence for documentation, 
one of the creative commons licences. Does anyone think that 
would be a good idea?


I don't know much about the creative commons licence - what are the 
benefits and drawbacks for documentation?




I have used Subversion on a few projects and found it too
 inflexible. Without access to the Subversion repository
 a number of things aren't possible.
 (Simply being
 connected to the internet doesn't necessarily solve
 this: in my case, the Subversion server was only visible
 from an internal company network.)


I don't understand the distinctions you are making here, and 
think that I need to.



 Whilst the
 Subversion working copy is local to a machine, without
 visibility of the repository I couldn't see the log of
 previous commits, nor make any commits.  Working on more
 than one commit was a pain.  (Sometimes, I found that a
 particular enhancement required a logically separate
 enhancement to be made first...) Fortunately the
 Git-Subversion interface worked quite well and I was
 able to use Git locally to prepare a series of commits
 and upload them once I was connected to the Subversion
 repository.


I'm not convinced that the problems you are experiencing 
reflect what would happen if we had a properly set up 
subversion repository.


For this I think you need to have the repository on a server 
which runs a subversion service.  Having a repository which 
is visible across the network by other means is not the 
same.
I have a subversion repository at rbjones.com, but cannot 
provide a general service because rbjones.com is on a 
virtual host so all access to the repository has to be 
through my username.


Sorry, all I was saying is that when one doesn't have access to the 
Subversion repository (for whatever reason), any operation that requires 
access to the Subversion repository won't work, which includes various 
operations that I would do normally during the course of development, 
e.g. looking at the previous log messages or previous revisions or 
making commits.


Wherever the repository is, or however it is set up, if you don't have 
access, you can get stuck.  Whilst a repository on Google Code would be 
quite accessible, I do a lot of development on the move and wouldn't 
even want to be dependent on an internet connection.


With a distributed VCS, you have your own local repository, so access is 
not a problem.



Also I don't understand your commit problem, why was it 
desirable to have a series of commits rather than just one?


If I'm making three separate changes that are totally unrelated, it's 
better for these to be separate commits, in my view.  For example, it is 
easier for people to understand the changes if they're separated out. 
Also, it would allow someone else to pull one of the c