Re: [ProofPower] "Unicode" vs. UTF8

[Rob Arthan]

Makarius,

Good to hear from you.


> On 7 Nov 2023, at 10:09, Makarius  wrote:
> 
> On 06/11/2023 02:19, Rob Arthan wrote:
>> One bit of burrowing inside instigated by the developers rather than the 
>> users began a few years ago: an experimental port of ProofPower to use 
>> Unicode and UTF-8 for mathematical symbols in place of the ad hoc character 
>> set that we had to invent for ourselves years ago. Roger Jones did some 
>> excellent work towards this end and made a version of the document 
>> processing tools that would compile all the ML code from UTF-8 sources using 
>> the old character set as an intermediary. I ported the user interface 
>> program xpp based on his work, but it has proved problematic to port all 
>> that we did to Linux: we were developing on Mac OS and, sadly, the Free BSD 
>> wchar_t libraries are much less restrictive than the Gnu libraries and it 
>> seems to need a lot more work on the document processing utilities (that are 
>> written in C) to get round this.
> 
> I first heard of "Unicode" approx. 1990. Everybody was talking about "wide 
> charaters" (16bit) and made moves to support them (e.g. major Unix vendors 
> and MicroSoft). That was the time of now obsolete UCS16: "16bit should be 
> sufficient for everyone, i.e. every imaginable character on the planet".

With ProofPower, we were just a year or two earlier, when "8-bit clean”, i.e. 
compatibility with iso8859 was the name of the game. None of the iso8559 
encodings covered the mathematical symbols that we needed so we rolled our own 
encoding that covered the symbols we needed.

> 
> Many years later, everybody started to use UTF-8 and the meaning "Unicode" 
> changed quite a bit. The "UTF-8 manifesto" http://utf8everywhere.org helps to 
> understand the situation in retrospective. In particular, "wide characters" 
> are now mostly obsolete, although we still see them as building blocks for 
> UTF-16 (which is not the same sas 16-bit Unicode). Programming languages with 
> wide characters carry unnecessary baggage. E.g. see this side remark 
> (concerning Python) in the text:
> 
> """
> Furthermore, we would like to suggest that counting or otherwise iterating 
> over Unicode code points should not be seen as a particularly important task 
> in text processing scenarios. Many developers mistakenly see code points as a 
> kind of a successor to ASCII characters. This lead to software design 
> decisions such as Python’s string O(1) code point access. The truth, however, 
> is that Unicode is inherently more complicated and there is no universal 
> definition of such thing as Unicode character. We see no particular reason to 
> favor Unicode code points over Unicode grapheme clusters, code units or 
> perhaps even words in a language for that. On the other hand, seeing UTF-8 
> code units (bytes) as a basic unit of text seems particularly useful for many 
> tasks, such as parsing commonly used textual data formats. This is due to a 
> particular feature of this encoding. Graphemes, code units, code points and 
> other relevant Unicode terms are explained in Section 5. Operations on 
> encoded text strings are discussed in Section 7.
> """
> 

The way this pans out in C (and in particular in the OpenMotif libraries) is 
that you can either work with UTF-8 encodings as strings of bytes or with 
wchar_t encodings where a wchar_t is a number representing a Unicode code 
point. On Mac OS, this is no problem, because the wchar_t type comprises 32-bit 
integers and that is plenty to cover all the Unicode code points. Alas, that 
doesn’t work on MS Windows if you need to use symbols outside the Basic 
Multilingual Plane (i.e., with code points >= 2^16). I don’t agree with the 
thinking behind thje UTF-8 manifesto: it seems to be telling us that we 
shouldn’t be using a conceptually simple model of strings of symbols drawn from 
a finite alphabet of known size just because certain parties underestimated the 
required size.

The particular programming problem we have in ProofPower with this is that (to 
allow transition from the old world to the knew and vice versa) we need to 
convert an 8-bit clean encoding to a UTF-8 encoding and vice versa. This 
involves a great deal of work as the C locale mechanisms aren’t very helpful 
with this.

> (Maybe this helps to prove that the mailing list is alive.)
> 

Let’s hope so!

Best,

Rob

> 
>   Makarius

> 
> 
> ___
> 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] Test

[Rob Arthan]

I received my test post to the ProofPower mailing list, so I better do myself 
what I asked everyone else to do! So here is my reply! Perhaps I should give a 
brief update on events since the list started to malfunction:

ProofPower is alive and well and in use by D-RisQ and others. It has reached 
that rare state for a software system of becoming relatively stable: by and 
large, it does what the current user community want and they are mostly 
building on top of it rather than needing to burrow inside it. (It is a sad 
comment on software engineering that stable is considered by many to imply 
moribund. I do not share that opinion.)

One bit of burrowing inside instigated by the developers rather than the users 
began a few years ago: an experimental port of ProofPower to use Unicode and 
UTF-8 for mathematical symbols in place of the ad hoc character set that we had 
to invent for ourselves years ago. Roger Jones did some excellent work towards 
this end and made a version of the document processing tools that would compile 
all the ML code from UTF-8 sources using the old character set as an 
intermediary. I ported the user interface program xpp based on his work, but it 
has proved problematic to port all that we did to Linux: we were developing on 
Mac OS and, sadly, the Free BSD wchar_t libraries are much less restrictive 
than the Gnu libraries and it seems to need a lot more work on the document 
processing utilities (that are written in C) to get round this. [As an aside: I 
wanted to continue to support the Cygwin platform and there seems to be little 
hope for full support for UTF-8 on gcc in Cygwin.] I have more r
 ecently got the xpp port working on Linux, but not the rest of the system. So 
that development is in abeyance. I hope to lock horns with this strand of work 
again in the not too distant future.

Best regards,

Rob.

> On 6 Nov 2023, at 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

[ProofPower] Test

[Rob Arthan]

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

Re: [ProofPower] Law of Cases

[Rob Arthan]

David,

I think you got some help with this from Roger off the list. I am replying on 
the list in case you still haven't solved your problem.

It looks like you want your law of cases to be a rule that given  훤 ⊢ p ⇒ r and 
훥 ⊢ q ⇒ r infers 훤, 훥 ⊢ p ∨ q ⇒ r. Your proposed implementation doesn't use any 
rules that "know" about disjunction. The rule that corresponds to this law of 
cases is ∨_elim, which states the law of implication elimination in the sequent 
calculus presentation of natural deduction in the usual way (using the 
turnstile rather than ⇒ to represent the implications). You can implement your 
law of cases using ∨_elim as shown below.

Regards,

Rob.

fun law_of_cases th1 th2 = (* 훤 ⊢ p ⇒ r, 훥 ⊢ q ⇒ r *) 
let val (p, _) = (dest_⇒ o concl) th1;
val (q, _) = (dest_⇒ o concl) th2;
val p_or_q = mk_∨(p, q); (* p ∨ q *)
val th3 = asm_rule p_or_q; (* p ∨ q ⊢ p ∨ q *)
val th4 = undisch_rule th1; (* 훤, p ⊢ r,*)
val th5 = undisch_rule th2; (* 훥, q ⊢ r *)
val th6 = ∨_elim th3 th4 th5; (* 훤, 훥, p ∨ q ⊢ r *)
val th7 = disch_rule p_or_q th6;  (* 훤, 훥 ⊢ p ∨ q ⇒ r *)
in  th7
end;

val L1 = asm_rule ⌜p ⇒ r⌝;
val L2 = asm_rule ⌜q ⇒ r⌝;

law_of_cases L1 L2;
(*
Result:
val it = p ⇒ r, q ⇒ r ⊢ p ∨ q ⇒ r: THM
*)


> On 31 Mar 2020, at 17:10, David Topham  wrote:
> 
> I was hoping this would work for applying the Law of Cases to a proof, but it 
> adds q to the list of premises.
> What could I do to remove that?
> 
> =SML
> fun law_of_cases th1 th2 =
> let
> val D⇒ (tm,_) = dest_term (concl th1)
> in asm_elim tm (undisch_rule th1)(undisch_rule th2)
> end;
> val L0 = asm_rule ⌜p ∨ q⌝;
> val L1 = asm_rule ⌜p⇒r⌝;
> val L2 = asm_rule ⌜q⇒r⌝;
> law_of_cases L1 L2;
> =GFT
> :) val L0 = p ∨ q ⊢ p ∨ q: THM
> :) val L1 = p ⇒ r ⊢ p ⇒ r: THM
> :) val L2 = q ⇒ r ⊢ q ⇒ r: THM
> :) val it = p ⇒ r, q ⇒ r, q ⊢ r: THM
> ___
> 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

[Rob Arthan]

David, Phil,

Phil's post gives a nice little introduction to programming with conversions 
(things like plus_1_conv) and conversionals (functions that create new 
conversions from old like THEN_C). Phil's conversion is focussed and efficient.

Going for comfort rather than speed, an alternative is to prove a theorem that 
recasts the recursion equations into a form that can be used as a rewrite rule. 
This gives a cheap and cheerful solution which isn't much more complicated to 
code than rewriting with the definition of the length function (where the the 
problem with numeric literals doesn't arise, because despite appearances[1; 2; 
3] does match the pattern Cons h t). See my code below.
 
Regards,

Rob.

open_theory "hol";  new_theory "t";
set_pc"basic_hol1"; (* say, see comments on all_summ_conv below *)
(*
Define summ as David did.
*)

ⓈHOLCONST
│ summ : ℕ → ℕ 
├──
│   summ 0 = 0
│ ∧ ∀n⦁ summ (n + 1) = summ n + n + 1
■

(*
Get an ML name for the defining theorem.
*)

val summ_def = get_spec⌜summ⌝;

(*
Prove a theorem recasting the recursion equations as a rewrite rule.
*)

set_goal([], ⌜∀n⦁ summ n = if n = 0 then 0 else summ (n - 1)  + n⌝);
a(REPEAT strip_tac);
a(induction_tac⌜n:ℕ⌝ THEN rewrite_tac[summ_def]);
val summ_thm = save_thm("summ_thm", pop_thm());

(*
Result:
val summ_thm = ⊢ ∀ n⦁ summ n = (if n = 0 then 0 else summ (n - 1) + n): THM
*)

(*
The following conversion will simplify all subterms of the form ⌜summ n⌝
where n is a numeric literal on the assumption that the current proof context
(like basic_hol1) includes 'ℕ_lit (so it simplifies natural number arithmetic
expressions involving literals automatically).

The conversion repeatedly attempts to use summ_thm once as a rewrite rule
followed by rewriting with what is built into the proof context (to perform
arithmetic simplications and to simplify the if-then-else terms).

(You can use PC_C1 to force the conversion to use your choice of proof context,
if you want something that is a bit more general-purpose.)
*)

val all_summ_conv = REPEAT_C (once_rewrite_conv[summ_thm] THEN_C 
rewrite_conv[]);

val egs =  map all_summ_conv [⌜summ 0⌝, ⌜summ 1⌝, ⌜summ 2⌝, ⌜summ 42 + summ 
99⌝];

(*
Result:
val egs = [⊢ summ 0 = 0, ⊢ summ 1 = 1, ⊢ summ 2 = 3, ⊢ summ 42 + summ 99 = 
5853]: THM list
*)


> On 31 Mar 2020, at 20:36, Phil Clayton  wrote:
> 
> 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, ⊢ 

Re: [ProofPower] Proofpower Digest, Vol 120, Issue 1

[Rob Arthan]

David,


> On 25 Mar 2020, at 17:18, David Topham  wrote:
> 
> Rob, I got this, but I had 3 previous posts to mailing list that didn't make 
> it.
> Were they inappropriate? Or lost? -Dave

They must have got lost. Please do try to resend them.

Regards,

Rob.
> 
> On Wed, Mar 25, 2020 at 9:00 AM  wrote:
> Send Proofpower mailing list submissions to
> proofpower@lemma-one.com
> 
> To subscribe or unsubscribe via the World Wide Web, visit
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
> or, via email, send a message with subject or body 'help' to
> proofpower-requ...@lemma-one.com
> 
> You can reach the person managing the list at
> proofpower-ow...@lemma-one.com
> 
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Proofpower digest..."
> 
> 
> Today's Topics:
> 
>1. Testing, testing (Rob Arthan)
> 
> 
> ----------
> 
> Message: 1
> Date: Wed, 25 Mar 2020 15:10:15 +
> From: Rob Arthan 
> To: ProofPower List 
> Subject: [ProofPower] Testing, testing
> Message-ID: 
> Content-Type: text/plain;   charset=us-ascii
> 
> This is a test. If you receive it, please ignore it.
> 
> Regards,
> 
> Rob.
> 
> 
> 
> --
> 
> Subject: Digest Footer
> 
> ___
> Proofpower mailing list
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
> 
> 
> --
> 
> End of Proofpower Digest, Vol 120, Issue 1
> **
> ___
> 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] Testing, testing

[Rob Arthan]

This is a test. If you receive it, please ignore it.

Regards,

Rob.

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

Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math

[Rob Arthan]

Roger, David,

> On 2 Nov 2019, at 18:45, Roger Bishop Jones  wrote:
> 
> Oops.
> 
> On 02/11/2019 17:25, Roger Bishop Jones wrote:
>> How about working in theory "ℚ"?
> Great idea, apart from the fact that it doesn't exist!

That's right: we don't provide a type ℚ of rationals. The approach I took
to defining the type ℝ of reals doesn't construct the rationals first. A type
of rationals could easily be provided as a subtype of the reals, but I have
never felt the need for it: if I need to work with the rationals I just treat
them as a subset of the reals.

Regards,

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

Re: [ProofPower] Proofpower Digest, Vol 119, Issue 1

[Rob Arthan]

David,

> On 1 Nov 2019, at 16:13, David Topham  wrote:
> 
> Ok, I can work within integers for awhile!  I was trying to use the general 
> form of the geometric progression that may involve fractions, but I can 
> explore whole numbers more first.

As an aside from what Roger has been trying to help with, you may also like to 
look at the treatment of sequences and series in the document wrk066.doc in the 
mathematical case studies that deals with some basic analysis. Sequences are 
modelled as functions ℕ → ℝ. The following function is defined to convert a 
sequence s into the series comprising the sequence of partial sums s_0 + s_1 + 
… + s_n.

ⓈHOLCONST
│ ⦏Sigma⦎ : (ℕ → ℝ) → (ℕ → ℝ)
├──
│   (∀s⦁ Sigma s 0 = ℕℝ 0)
│ ∧ (∀s n⦁ Sigma s (n+1) = Sigma s n + s n)
■

In a similar vein, a function that maps a sequence of coefficients to the 
corresponding power series is defined as follows:

ⓈHOLCONST
│ ⦏PowerSeries⦎ : (ℕ → ℝ) → (ℕ → ℝ → ℝ)
├──
│ ∀s n⦁ PowerSeries s n = PolyEval (s To n)
■

where s To n is the list comprising the first n elements of the sequence s and 
PolyEval maps a list of coefficients to the corresponding polynomial function:

ⓈHOLCONST
│ ⦏PolyEval⦎ : ℝ LIST → (ℝ → ℝ)
├──
│   (∀x⦁ PolyEval [] x = ℕℝ 0)
│∧  (∀c l x⦁ PolyEval (Cons c l) x = c + x * PolyEval l x)
■

When you are reasoning about these things, you can do induction over the index 
of a sequence, because that’s a natural number. The theory includes the usual 
results on geometric series:

:) geometric_sum_thm;
val it = ⊢ ∀ n x⦁ ¬ x = 1. ⇒ Sigma (휆 m⦁ x ^ m) (n + 1) = (1. - x ^ (n + 1)) / 
(1. - x): THM

:) geometric_series_thm;
val it = ⊢ ∀ x⦁ ~ 1. < x ∧ x < 1. ⇒ (휆 n⦁ PowerSeries (휆 m⦁ 1.) n x) -> 1. / 
(1. - x): THM

Regards,

Rob





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

Re: [ProofPower] Distributed concatenation symbol

[Rob Arthan]

Phil,


> On 26 Mar 2019, at 17:49, Phil Clayton  wrote:
> 
> Rob,
> 
> [A somewhat belated response now.  I only noticed the delivery failure from 
> December 2016 today!  Trying again...]

Better late than never!

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

Thanks for the endorsement.

> 
> 
>> 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 ç.
>> 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.
> 
We aren't defining a MathML processor.

[As an aside: does MathML really achieve this? If so, it presumably arranges
for maths bold, fraktur and ordinary Roman letters to be treated differently
somehow.]

> Have I misunderstood?
> 
> Are you defining MathML markup for Z?

We aren't defining MathML markup for Z. What we are doing is closer
to the Z Standard's identify markup. However we want to use
MathML's entity set as the basis for the naming scheme for
the symbols, since the UCS/Unicode names are unintuitive and
unwieldy. We do need to define what Unicode code points the entity names map to
(as, without a great deal of work, ProofPower will need to fix on one code 
point for each entity name
for use on output). The code points in the 0370-03FF range have the advantage 
of being
supported in a great number of fonts.

Regards,

Rob.




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

Re: [ProofPower] ProofPower output

[Rob Arthan]

Dave,

It's done using:

=GFT ProofPower output

"=GFT" stands for something like "General Formal Text". The text on the
GFT line is used for the label and the lines coming after a GFT directive are
just formatted like formal text in theLaTeX document, but not included by 
docsml.
I would typically copy text out of the journal window and paste it into the 
script
window while writing the document and processing the SML that produces
the output interactively.

Regards,

Rob.

> On 15 Feb 2019, at 18:17, David Topham  wrote:
> 
> I was reading an article by Rob Arthan about ProofPower Z and notice that the 
> document shows SML input followed by ProofPower output. I have not seen how 
> to automatically create that using xpp. e.g. I know that
> =SML
> produces the first label using doctex, but what produces the "ProofPower 
> output" label in the tex file?
> 
> So far, I have been using screenshot images of what I see in xpp and using 
> \includegraphics under =TEX
> -- 
> -Dave
> ___
> 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...

[Rob Arthan]

Hugh,

> On 14 May 2017, at 03:21, Hugh Anderson  wrote:
> 
> 
> Hi Phil,
> 
> That does the trick! With polyml it now compiles and installs correctly on my 
> up-to-date sierra, and the version of Poly/ML that brew installs (5.7).

The folk who maintain brew must be very quick off the mark: Poly/ML 5.7 was only
announced as released on 12th May. 

I have been working on making ProofPower compatible with Poly/ML 5.7
compiled with or without --enable-intinf-as-int. This isn't fully tested yet,
but it will be in the next release.

Thanks to Phil for supplying a work-around.

Regards,

Rob.

> I also tried using smlnj (On a mac at the moment, brew installs 110.80), and 
> this also installed perfectly.
> 
> Thanks very much for your patch...
> 
> Cheers Hugh
> 
> On Sun, 14 May 2017, Phil Clayton wrote:
> 
>> 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
>> 
>> 
>> 
> 
> 
> 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
> 

Re: [ProofPower] Is this a MacOs 10.12 problem?

[Rob Arthan]

Steve,Not your ignorance at all. It was a change in clang that came in with Mac OS 10.11.I’d been meaning to issue a fix. I’ve attached a patch. To apply it do:	patch -p1 -b -B orig/ < patch-3.1.rda.20170301in the OpenProofPower-3.1w7 directory. Let me know if you have any more problems.Regards,Rob.

patch-3.1.rda.20170301
Description: Binary data
On 1 Mar 2017, at 05:19, Steve Reeves  wrote:I couldn’t find anything later than November and about 10.11….so perhaps this is new…or more likely my ignorance!Anyhow, I’m trying to install the latest PP and on running install I got this in the build.log file:Building pptex dev xpp hol zed dazif [ "${PPTARGETDIR:-}" = "" ]; \	then \		rm -rf "/Users/stever/pp"; \	fi[ -d   "/Users/stever/pp" ] || mkdir "/Users/stever/pp"[ -d   "/Users/stever/pp"/bin ] || mkdir "/Users/stever/pp"/bin[ -d   "/Users/stever/pp"/etc ] || mkdir "/Users/stever/pp"/etc[ -d   "/Users/stever/pp"/tex ] || mkdir "/Users/stever/pp"/texrm -f imp096.cln -s imp096.doc imp096.cgcc -o sieve -DVERSION="\"3.1w7\""  imp096.cimp096.c:60:1: warning: '/*' within block comment [-Wcomment]/* From: imp096.doc   @(#) 94/04/06 1.3 imp096.doc^In file included from imp096.c:5151:/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX10.12.sdk/usr/include/unistd.h:508:6: error: cannot apply asm label to function after its first useint      getopt(int, char * const [], const char *) __DARWIN_ALIAS(getopt);         ^                                          ~~imp096.c:5323:1: warning: '/*' within block comment [-Wcomment]/*^2 warnings and 1 error generated.make: *** [sieve] Error 1Seems to be a problem in an Xcode file….Any help grateful received!Steve___Proofpower mailing listProofpower@lemma-one.comhttp://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] Distributed concatenation symbol

[Rob Arthan]

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.

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.

Regards,

Rob.

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

Re: [ProofPower] Font for SML

[Rob Arthan]

David,

The ProofPower environments use \obeyspaces to persuade LaTeX to honour the 
spaces
in ML code etc. The ffslides package is doing something that is stopping 
\obeyspaces
working properly. A quick fix would be to edit the .tex file (lab.tex in your 
example) to replace
spaces between \begin{GFT} and \end{GFT} with tildes.

Regards,

Rob.

> On 5 Oct 2016, at 20:55, David Topham  wrote:
> 
> ...forgot to mention...need to go through postscript, so
> latex lab.tex
> dvipdf lab.dvi
> 
> On Wed, Oct 5, 2016 at 12:28 PM, David Topham  > wrote:
> Thanks Roger, In case you wish to see the problem more exactly attached is 
> the doc file and the ffslides.cls  (which you could also get at CTAN).  It 
> seems that for SML, the spaces are all removed!  I will look into GFT to see 
> how spaces are inserted. One issue might be if verbatim environment is used?  
> -Dave
> 
> 
> On Wed, Oct 5, 2016 at 8:35 AM, Roger Bishop Jones  > wrote:
> David,
> 
> Doctex doesn't chose a font, it just generates LaTeX commands for the formal 
> text and any font changing is up to the rest of the document (that you 
> provide in the =TEX sections of the .doc file).
> 
> It does generate tex for the HOL and ZED paragraphs which is intended to 
> force the layout in the printed version to follow the layout in the source, 
> which tex would not normally do, so I guess the ffslides package is 
> interfering with the way that works.
> The formal text is translated into tex using an environment GFT which is 
> defined in ProofPower.sty, but its beyond my tex expertise to understand how 
> it works or why ffslides is interfering.
> 
> It is possible to get slides made with ProofPower formal text in them, the 
> tutorial slides in the ProofPower distribution are examples of how this can 
> be done, though the method used for them is probably rather ancient by now.
> 
> Roger
>  
> 
> On 04/10/2016 20:14, David Topham wrote:
>> I am exploring a not often used but nice Latex package named ffslides. It 
>> has several advantages in exact control of where things are placed on the 
>> page using postscript (actually pstricks) behind the scenes.  But, one 
>> problem is that the SML in my doc file is getting scrunched together like 
>> this:
>> 
>> funsubset([],[])=true
>> 
>> Is there a way for me to choose a different font when doctex extracts the 
>> SML? 
>> Maybe I could find an alternative that would not squash?
>> 
>> -Dave
>> 
>> 
>> ,
>> [])=
>> true
>> 
>> 
>> ___
>> Proofpower mailing list
>> Proofpower@lemma-one.com 
>> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com 
>> 
> 
> 
> 
> This message did not originate from Ohlone College and must be viewed with 
> caution. Viruses and phishing attempts can be transmitted via email. E-mail 
> transmission cannot be guaranteed to be secure or error-free as information 
> could be intercepted, corrupted, lost, destroyed, arrive late or incomplete, 
> or contain viruses. If you have any concerns, please contact the Ohlone 
> College IT Service Desk at itserviced...@ohlone.edu 
>  or (510) 659-7333 
> .
> 
> 
> ___
> 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] ProofPower and Discrete Math

[Rob Arthan]

David,

I endorse what Roger said about forward v. backwards proof.
There is definitely a tension between teaching proof theory
and teaching practical mechanised proof.

For the record, the problem was that you had the two theorem
arguments of ∃_elim the wrong way round and you seemed
to have misunderstood the role of the term argument: it is
the variable that is free in the assumption of the second theorem
that is going to be discharged by the first theorem (the one
with the existential conclusion). Here is the complete proof
with the output you should see in the comments.

val L1 = asm_rule ⌜p(x,y):BOOL⌝;
(* val L1 = p (x, y) ⊢ p (x, y): THM *)
val L2 = ⌜∃x:'a⦁p(x,y)⌝;
(* val L2 = ⌜∃ x⦁ p (x, y)⌝: TERM *)
val L3 = ∃_intro L2 L1;
(* val L3 = p (x, y) ⊢ ∃ x⦁ p (x, y): THM *)
val L4 = ⌜∃y:'b⦁∃x:'a⦁p(x,y)⌝;
(* val L4 = ⌜∃ y x⦁ p (x, y)⌝: TERM *)
val L5 = ∃_intro L4 L3;
(* val L5 = p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *)
val L6 = asm_rule ⌜∃y:'b⦁p(x,y)⌝;
(* val L6 = ∃ y⦁ p (x, y) ⊢ ∃ y⦁ p (x, y): THM *)
val L7 = ∃_elim ⌜y:'b⌝ L6 L5;
(* val L7 = ∃ y⦁ p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *)
val L8 = asm_rule ⌜∃x:'a⦁ ∃y:'b⦁p(x,y)⌝;
(* val L8 = ∃ x y⦁ p (x, y) ⊢ ∃ x y⦁ p (x, y): THM *)
val L9 = ∃_elim ⌜x:'a⌝ L8 L7;
(* val L9 = ∃ x y⦁ p (x, y) ⊢ ∃ y x⦁ p (x, y): THM *)
val L10 = ⇒_intro ⌜∃x:'a⦁ ∃y:'b⦁p(x,y)⌝ L9;
(* val L10 = ⊢ (∃ x y⦁ p (x, y)) ⇒ (∃ y x⦁ p (x, y)): THM *)

The documentation and the error messages talk about varstructs
meaning either variables or  things formed from variables using pairing
(like ∃_elim will work on theorems with conclusions like ∃(x, y)⦁ p (x, y)).
You can just read “variable” for “varstruct” in simple examples.

Regards,

Rob.

> On 16 Aug 2016, at 21:24, David Topham  wrote:
> 
> Since the slides for this book use slightly different notation, I am back to 
> trying to implement the proofs in the main book:  UsingZ from
> www.usingz.com   (in text link, it is zedbook)
> 
> On page 42, the proof is using nested existentials, and I am trying
> to get past my lack of understanding in applying E-elim
> (Roger already helped me with E-intro)
> 
> Here are two of my attempts (using ASCII since I can't attach pdf here)
> val L1 = asm_rule %<%p(x,y):BOOL%>%;
> val L2 = %<%%exists%x:'a%spot%p(x,y)%>%;
> val L3 = %exists%_intro L2 L1;
> val L4 = %<%%exists%y:'b%spot%%exists%x:'a%spot%p(x,y)%>%;
> val L5 = %exists%_intro L4 L3;
> val L6 = asm_rule %<%%exists%y:'b%spot%p(x,y)%>%;
> val L7 = %exists%_elim L4 L5 L6; 
> 
> val L1 = asm_rule %<%p:BOOL%>%;
> val L2 = %<%%exists%x:'a%spot%p%>%;
> val L3 = %exists%_intro L2 L1;
> val L4 = %<%%exists%y:'b%spot%%exists%x:'a%spot%p%>%;
> val L5 = %exists%_intro L4 L3;
> val L6 = asm_rule %<%%exists%y:'b%spot%p%>%;
> val L7 = %exists%_elim L4 L5 L6; 
> 
> The error I get is "does not match the bound varstruct" 
> 
> Does anyone have a suggestion to get me past this roadblock?
> 
> -Dave
> 
> On Sun, Aug 14, 2016 at 2:21 AM, Roger Bishop Jones  > wrote:
> 
> On 14/08/2016 08:44, David Topham wrote:
> Thanks Roger, I am using slides he distributes.  He  has false introduction 
> rules starting on page 24 (attached).
> Sorry about my poor example, please ignore that since is a confused use of 
> this technique anyway!  -Dave
> 
> Looks like he changed the name.
> 
> In fact the original name (the one he uses in the book) is good in ProofPower.
> ¬_elim is available in ProofPower and does what you want (though it is 
> sligftly more general, it proves anything from a contradiction so you have to 
> tell it what result you are after).
> Details in reference manual.
> 
> Roger
> 
> 
> This message did not originate from Ohlone College  and must be viewed with 
> caution. Viruses and phishing attempts can be transmitted via email.
> E-mail transmission cannot be guaranteed to be secure or error-free as 
> information could be intercepted, corrupted, lost, destroyed, arrive late or 
> incomplete, or contain viruses.
> 
> If you have any concerns, please contact the Ohlone College IT Service Desk 
> at itserviced...@ohlone.edu   or (510) 
> 659-7333 .
> 
> 
> ___
> 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] ProofPower on Ubuntu 16.04

[Rob Arthan]

Roger,

> On 18 Jul 2016, at 22:15, Roger Bishop Jones  wrote:
> 
> I have been trying to install ProofPower on Ubuntu 16.04, without success.
> 
> The stumbling block comes early, in the prerequisites for installing 
> OpenMotif, since some of these are not available in the usual repositories.

Do you need any more than libmotif-dev?  I have a kubuntu 16.04 VM but 
unfortunately it’s not convenient for me to install all the prerequisites for 
ProofPower on it just now. However, I installed libmotif-dev and was able to 
build a simple motif programme and I can’t see any reason why xpp would need 
anything more.

> 
> If anyone figures out how to get ProofPower installed on Ubuntu 16.04 I 
> should be pleased to know how it can be done.

I’ll try a full installation on kubuntu 16.04 when I get a moment. 

Regards,

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

Re: [ProofPower] ProofPower build on OS X

[Rob Arthan]

Roger,

> On 30 Apr 2016, at 10:43, Roger Bishop Jones <r...@rbjones.com> wrote:
> 
> Rob,
> 
> Thanks for you continuing support.

Not a problem. Thank you for persisting with this bit of the
installation, because I have a bit of difficulty testing it on
Mac OS in a clean environment. I will look into improving
the way I test it.

> 
>> On 30 Apr 2016, at 10:16, Rob Arthan <r...@lemma-one.com 
>> <mailto:r...@lemma-one.com>> wrote:
>> 
>> 
> 
> ...
> 
>> Try it in in src/dev. I think it will fail. If so, try it without the 
>> obsolete options:
>> 
>>  polyc -o pp-ml pp-ml.o
>> 
> 
> Here are the results:
> 
> bash-3.2$ polyc -segprot POLY rwx rwx -o pp-ml pp-ml.o
> Only one source file name allowed
> Usage: polyc [OPTION]... [SOURCEFILE]
> bash-3.2$ polyc -o pp-ml pp-ml.o
> ld: warning: could not create compact unwind for _ffi_call_unix64: does not 
> use RBP or RSP based frame
> 
> So I need to build my own?

Hopefully not. That warning should be harmless.

I’ve just realised that it is only src/hol/hol.mkf which has this legacy way of
linking a poly executable. src/dev/dev.mkf creates slrp-ml the modern way
and will already have done that.

For the next step, I realise that you don’t need to edit thesrc/hol/hol.mkf:
to get it to call polyc correctly, run configure like this:

PPPOLYLINKFLAGS=“ “ ./configure

together with any other environment variable settings you need. I think there
is a good chance that the rest of the ML compilations will work then.

Regards,

Rob.

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

Re: [ProofPower] ProofPower build on OS X

[Rob Arthan]

Roger,

> On 29 Apr 2016, at 23:16, Roger Bishop Jones <r...@rbjones.com> wrote:
> 
> Rob,
> 
>> On 29 Apr 2016, at 20:31, Rob Arthan <r...@lemma-one.com> wrote:
>> 
>> 
>> The linker can’t find the gmp library. What version of Poly/ML are you 
>> using? Did you build
>> it yourself or download it ready-made from somewhere?
>> 
> 
> I did:
>   port install polymer
> 
> poly -v gives
> 
> Poly/ML 5.5.2 ReleaseRTS version: X86_64-5.5.1
> 
> 
OK. You may need to build your own, but let's see if we can get it working
with the MacPorts version.

>> If you go into src/dev, what happens if you run the following command 
>> interactively?
>> 
> 
> src/dev where?  Can’r find one.

In the directory OpenProofPower-3.1w7 you got when you unpacked the tarball.
> 
> But if I run it in my home directory I get:
> 
> Rogers-MacBook:~ rbj$ polyc -segprot POLY rwx rwx -o pp-ml pp-ml.o 
> Only one source file name allowed
> Usage: polyc [OPTION]... [SOURCEFILE]
> 

Try it in in src/dev. I think it will fail. If so, try it without the obsolete 
options:

polyc -o pp-ml pp-ml.o

If that works, then if you get rid of those options from the polyc command
lines in src/dev/dev.mkf and src/hol/hol.mkf, you should get a bit further.

Regards,

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

Re: [ProofPower] ProofPower build on OS X

[Rob Arthan]

Roger,

> On 29 Apr 2016, at 17:17, Roger Bishop Jones  wrote:
> 
> Rob,
> 
> OK, so now I am through to the ProofPower build, which fails pretty fast, 
> just after compiling dtd108.
> 
> Here’s the tail of the log:
> 
> rm -f hol.polydb
> Compiling dtd108.sml and imp108.sml
> { { echo "val system_version : string = \"3.1w7\"; val build_date : 
> Date.date = Date.fromTimeLocal(Time.now()); use\"dtd108.sml\"; 
> use\"imp108.sml\";" | poly ; } && { polyc -segprot POLY rwx rwx -o pp-ml 
> pp-ml.o || LD_RUN_PATH=/opt/local/lib c++ -segprot POLY rwx rwx -o pp-ml 
> pp-ml.o -L/opt/local/lib -lpolymain -lpolyml ; } && { echo "PPBuild.pp'save 
> ();" | pp-ml ; } } > dtd108.ldd0
> ld: warning: could not create compact unwind for _ffi_call_unix64: does not 
> use RBP or RSP based frame
> Undefined symbols for architecture x86_64:
>  "___gmpn_add_n", referenced from:
>  add_unsigned_long(TaskData*, SaveVecEntry*, SaveVecEntry*, int) in 
> libpolyml.a(arb.o)
>  "___gmpn_gcd", referenced from:
>  gcd_arbitrary(TaskData*, SaveVecEntry*, SaveVecEntry*) in 
> libpolyml.a(arb.o)
>  "___gmpn_gcd_1", referenced from:
>  gcd_arbitrary(TaskData*, SaveVecEntry*, SaveVecEntry*) in 
> libpolyml.a(arb.o)
>  "___gmpn_lshift", referenced from:
>  gcd_arbitrary(TaskData*, SaveVecEntry*, SaveVecEntry*) in 
> libpolyml.a(arb.o)
>  "___gmpn_mul", referenced from:
>  mult_longc(TaskData*, SaveVecEntry*, SaveVecEntry*) in libpolyml.a(arb.o)
>  "___gmpn_rshift", referenced from:
>  gcd_arbitrary(TaskData*, SaveVecEntry*, SaveVecEntry*) in 
> libpolyml.a(arb.o)
>  "___gmpn_sub_n", referenced from:
>  sub_unsigned_long(TaskData*, SaveVecEntry*, SaveVecEntry*, int) in 
> libpolyml.a(arb.o)
>  "___gmpn_tdiv_qr", referenced from:
>  quotRem(TaskData*, SaveVecEntry*, SaveVecEntry*, SaveVecEntry*&, 
> SaveVecEntry*&) in libpolyml.a(arb.o)
> ld: symbol(s) not found for architecture x86_64
> clang: error: linker command failed with exit code 1 (use -v to see 
> invocation)
> make: *** [hol.ldd] Error 1
> 
> Any idea what the problem is here?

The linker can’t find the gmp library. What version of Poly/ML are you using? 
Did you build
it yourself or download it ready-made from somewhere?

If you go into src/dev, what happens if you run the following command 
interactively?

polyc -segprot POLY rwx rwx -o pp-ml pp-ml.o 

Regards,

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

Re: [ProofPower] ProofPower on OS X

[Rob Arthan]

Roger,

> On 28 Apr 2016, at 21:32, Roger Bishop Jones <r...@rbjones.com> wrote:
> 
> 
>> On 28 Apr 2016, at 11:57, Rob Arthan <r...@lemma-one.com> wrote:
>> 
>> 
>> Can you point me at the recipe, so I can see what is likely to be
>> out of date.
> 
> http://lemma-one.com/pipermail/proofpower_lemma-one.com/2012-December/000955.html
> 
> I have managed to get Xcode installed now,

Good.

> but fail on step 2 of your prescription because the preferences in Xcode 
> doesn’t seem to have a download option.

I am not sure an analogue of this step is necessary now. If it is, then I 
believe you do it from the command line with the following command:

xcode-select --install

Regards,

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

[ProofPower] Attachments

[Rob Arthan]

Dear all,

I have had a few moderator requests recently for posts to the ProofPower list 
that were bigger than 40Kb. This was because the posts had attachments of a few 
hundred Kb. My usual practice is not to accept such posts, not because of the 
size of the attachments but because such attachments typically contain files in 
format like PDF or ProofPower documents or compressed tarballs that will be 
trashed when the post is archived. So to make your post useful in posterity, it 
is much better to include a link, e.g., to a public file or folder on Dropbox 
or to a repo on GitHub or bitbucket, rather than include the actual data. If 
this causes you any difficulty on any occasion, feel free to send me a private 
e-mail and I’ll be happy to try to help you.

Regards,

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

Re: [ProofPower] Issue in compiling OpenProofPower-3.1w5 on Xubuntu (Ubuntu) 14.04 LTS

[Rob Arthan]

Daniel,

I am taking the liberty of copying this to the ProofPower mailing list
as it may be of interest to other users. Perhaps you might like to
join the list and continue the discussion there.

Most interactive users of ProofPower need the online documentation
and they also want to create ProofPower documents as part of their
work. Hence, the build process assumes you want and have an
installation of TeX and LaTeX. If you want to build on a
minimal system without them, then that should be possible. I haven’t
got time to build a VM to test this in just now, but what I would try
is running configure (without pptex as you don’t want it) and then
editing the install script to change the line.

if  ! make -f $d.mkf inst $PPBUILDDIR/build.log 21

to read:

if  ! make -f $d.mkf bininst $PPBUILDDIR/build.log 21

then run install with -d, which stops it doing the last step that builds the
HTML index file in $PPHOME/doc.

Do let me know how you get on. It wouldn’t surprise me if at least one
of the package makefiles, hol.mkf, zed.mkf etc. does something that
depends on pptex or TeX or LaTeX, but that should be fixable.

Note xpp needs groff to build, but you could you could uninstall it
afterwards. However, groff is tiny compared with TeX and LaTeX.

If we can get it to work, I can make it something that you can select
via an environment variable when you run configure.

Regards,

Rob.

 On 5 Jun 2015, at 23:26, Daniel Moniz d...@pobox.com wrote:
 
 Hi Rob,
 
 I'm having an issue building OpenProofPower-3.1w5 on Xubuntu (Ubuntu)
 14.04 LTS (64-bit). Here are the last few lines of my build.log:
 
 [ -d   /home/dnm/pp/doc ] || mkdir /home/dnm/pp/doc
 doctex  dtd017.doc
 texdvi -b dtd017  dtd017.dvi.ldd1 /dev/null
 make: *** [dtd017.dvi] Error 1
 rm dtd017.tex
 
 This seems to happen regardless of trying some tweaks, like setting
 PPTARGETS to not include pptex (e.g. PPTARGETS=dev xpp hol zed daz),
 and/or running install post-./configure as just ./install +d; I admit
 that I'm kind of thrashing around and trying things based on the
 instructions at http://www.lemma-one.com/ProofPower/getting/README that
 don't expressly say they will help solve this issue.
 
 Ideally the tools would build without needing to generate DVI
 information at all if specifically requested not to, but that's just me.
 I guess *ideally* there wouldn't be an issue with the TeX/DVI side of
 things so wanting to not need any of the DVI files wouldn't be required.
 But it does seem that OpenProofPower really can't be built at all
 without TeX/LaTeX/DVI in the mix somewhere, which, in fairness, Section
 2 of the README does say:
 
 [...] You certainly need:
 ...
 e) the Tex and LaTeX typesetting software
 
 I'm just trying to build and run in a modestly sized VM, and thus trying
 to get away with the smallest TeX install I can since a full install
 chews up all my disk space and more. I was hoping I could build and use
 OpenProofPower without any TeX/LaTeX tools *required*, and have it spit
 out LaTeX sources, etc. that I could move/copy to typeset on my Windows
 or OS X machine (where I have plenty of disk space, and full TeX Live
 installs). As it is, I surrendered to installing texlive-latex-base
 from the Ubuntu repository (plus its dependencies), but I'm still
 getting the error above. It's also not very informative, so I'm not sure
 what is breaking such that make-ing that dvi file fails. texdvi is built
 and seems to be fine (displays usage).
 
 Any hints?
 
 Thanks in advance, thanks for making OpenProofPower, and for making it
 available.
 
 
 -- 
 Daniel Moniz d...@pobox.com [http://pobox.com/~dnm/]
 


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

Re: [ProofPower] Question about installation.

[Rob Arthan]

 On 1 Jun 2015, at 21:31, Robert White ai.robert.wangsh...@gmail.com wrote:
 
 This is what I have now. Is this a correct version?
 
 Poly/ML 5.2 ReleaseRTS version: X86_64-5.2.1

You need 5.5 or later. So you will need to build it from source.
Don’t hesitate to ask if you need any help with that.

Regards,

Rob.


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

Re: [ProofPower] building error and solution regarding the x11 path for Mac

[Rob Arthan]

Yuhui,

On 1 Apr 2015, at 23:14, YuHui Lin y@hw.ac.uk wrote:

 Hi,
 
 I’ve got two errors when I install pp, on the latest version of Mac OS 
 10.10.2. The causes of these two errors are the path of X11 which seems to be 
 different. I am thinking my experience might be helpful, so I share the 
 errors and the fixes here.
 
 The error messages I got are
'X11/Intrinsic.h' file not found
 
 and
directory not found for option '-L/usr/X11R6/lib’.

That is actually a warning and you can ignore it. However, it might be 
associated with a real error
if the right -L option isn’t there on the cc command line as well.

 
 For the first error, it can be fixed by adding a link from your local x11 
 path to the one which the install program search for. For example:
 
   ln -s /opt/X11/include/X11 /usr/local/include/X11
 
 where “/opt/X11/include/X11” is my local install of X11.

You could also have run configure like this

PPUSERCFLAGS=-I/opt/X11/include/X11 configure

to get the extra flag on the cc command lines.


 For the second error, I changed the makefile for the xpp, which is located at 
  
   xpp/xpp.mdk.
 
 The changes I made are to substitute 
/usr/X11R6
  to 
/opt/X11

Again if you need to, you can achieve this from outside:

PPUSERCFLAGS=-I/opt/X11/include/X11 PPUSERCLIBS=-L/opt/X11 configure

What I don’t understand is why it was failing. If you have used MacPorts to 
install Motif
it should have installed the MacPorts X11 files in /opt/local/include/X11.
It looks to me like you have the Apple X11 files in /opt/X11, but not the 
MacPorts X11 stuff in /opt/local.
So where do you have OpenMotif installed? Where does configure say it found 
Motif?

When I build on a Mac, what I see in build.log is this:

cc -g -DMACOSX -DGETOPTDONE=-1 -DUSE_GRANTPT -DSLOWREGEXEC -I/opt/local/include 
-Wall -I/usr/X11R6/include   -c -o help.o help.c
cc -g -DMACOSX -DGETOPTDONE=-1 -DUSE_GRANTPT -DSLOWREGEXEC -I/opt/local/include 
-Wall -I/usr/X11R6/include -o xpp cmdline.o diag.o files.o findfile.o lineno.o 
mainw.o menus.o msg.o options.o palette.o pixmaps.o pterm.o search.o 
templates.o undo.o xmisc.o xpp.o help.o -L/opt/local/lib -L/usr/X11R6/lib -lXm 
-lXext -lXp -lXt -lSM -lICE -lX11

where the extra -I and -L have been put in by configure automatically.
That works with a warning about -L/usr/X11R6/lib that can safely be ignored.

Regards,

Rob.


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

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

[Rob Arthan]

David,


On 30 Mar 2015, at 06:05, David Topham dtop...@ohlone.edu 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!
 
My pleasure! git tells me that that bit of the code will be celebrating its 
21st birthday next month.

For future reference, xpp sometimes freezes because a dialogue box asking you 
for input has got hidden behind other windows. So it’s worth sliding other 
windows out of the way to see if you can find that dialogue box before killing 
the process.

Regards,

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

Re: [ProofPower] Updated Unicode translation scheme

[Rob Arthan]

Anthony,

On 30 Mar 2015, at 17:54, Anthony Hall anth...@anthonyhall.org wrote:

 Dear Rob
  
 I have just one small query - about the minus sign problem

Thanks for your interest.

  
 I had a lot of trouble with this, as you might expect, when translating 
 between Spivey latex and standard Z, but it can be done.

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 don’t know whether translating from Proofpower is more difficult, but it 
 would be nice to get this right if possible while you are translating to 
 Unicode.

I just don’t think ISO Z got this right. 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.

 Or am I missing something?

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. Of course, perhaps 
one day, the Z Word Tools as a common front-end will also be an option.
 
  
 All the best

And to you!

Rob.

  
 Anthony
  
  
 From: Proofpower [mailto:proofpower-boun...@lemma-one.com] On Behalf Of Rob 
 Arthan
 Sent: 28 March 2015 16:03
 To: ProofPower List
 Subject: [ProofPower] Updated Unicode translation scheme
  
 Dear All,
  
 Acting on some very helpful comments from Phil Clayton, I have revised the 
 proposed scheme for translating between Unicode and the ProofPower extended 
 character set. The revised scheme is described here:
  
 http://www.lemma-one.com/ProofPower/unicode/pp-unicode.html
  
 (You can find the earlier version at 
 http://www.lemma-one.com/ProofPower/unicode/v0/pp-unicode.html)
  
 The new scheme for you to look at with your e-mail client follows below.
  
 As before, Mac OS X supports all the necessary glyphs. If you install the 
 STIX fonts on Linux (stix-fonts on Fedora, fonts-stix on Ubuntu), there is 
 now a good chance that you will have all you need.
  
 Any feedback will be much appreciated.
  
 Regards,
  
 Rob.
  
  
 0x80: %subset%: ⊆
 0x81: %rsub%: ⩥
 0x82: %bagunion%: ⨄
 0x83: %bbU%: 핌
 0x84: %Delta%: 훥
 0x85: %fcomp%: ∘
 0x86: %Phi%: 훷
 0x87: %Gamma%: 훤
 0x88: %EZ%: └
 0x89: %down%: ⋎
 0x8A: %Theta%: 훩
 0x8B: %dcat%: ⁀/
 0x8C: %Lambda%: 훬
 0x8D: %mem%: ∈
 0x8E: %notmem%: ∉
 0x8F: %bij%: ⤖
 0x90: %Pi%: 훱
 0x91: %SML%: ⓜ
 0x92: %rres%: ▷
 0x93: %Sigma%: 훴
 0x94: %:%: ⓣ
 0x95: %Upsilon%: 훶
 0x96: %boolean%: 픹
 0x97: %Omega%: 훺
 0x98: %Xi%: 훯
 0x99: %Psi%: 훹
 0x9A: %emptyset%: ∅
 0x9B: %up%: ⋏
 0x9C: %BHH%: ═
 0x9D: %SZG%: ╒
 0x9E: %finj%: ⤕
 0x9F: %ffun%: ⇻
 0xA0: %psubset%: ⊂
 0xA1: %intersect%: ∩
 0xA2: %rseq%: ⟩
 0xA3: %symdiff%: ⊖
 0xA4: %equiv%: ⇔
 0xA5: %dintersect%: ⋂
 0xA6: %def%: ≜
 0xA7: %lseq%: ⟨
 0xA8: %lrelimg%: ⦇
 0xA9: %rrelimg%: ⦈
 0xAA: %rel%: ↔
 0xAB: %overwrite%: ⊕
 0xAC: %%: ⌜
 0xAD: %fun%: →
 0xAE: %%: ⌝
 0xAF: %real%: ℝ
 0xB0: %EFT%: ■
 0xB1: %and%: ∧
 0xB2: %or%: ∨
 0xB3: %not%: ¬
 0xB4: %implies%: ⇒
 0xB5: %forall%: ∀
 0xB6: %exists%: ∃
 0xB7: %spot%: ⦁
 0xB8: %x%: ×
 0xB9: %SFT%: Ⓢ
 0xBA: %bigcolon%: ⦂
 0xBB: %rcomp%: ⨾
 0xBC: %leq%: ≤
 0xBD: %neq%: ≠
 0xBE: %geq%: ≥
 0xBF: %symbol%: 핊
 0xC0: %union%: ∪
 0xC1: %alpha%: 훼
 0xC2: %beta%: 훽
 0xC3: %refinedby%: ⊑
 0xC4: %delta%: 훿
 0xC5: %select%: 휀
 0xC6: %phi%: 휑
 0xC7: %gamma%: 훾
 0xC8: %eta%: 휂
 0xC9: %iota%: 휄
 0xCA: %theta%: 휃
 0xCB: %kappa%: 휅
 0xCC: %fn%: 휆
 0xCD: %mu%: 휇
 0xCE: %nu%: 휈
 0xCF: %psurj%: ⤀
 0xD0: %pi%: 휋
 0xD1: %chi%: 휒
 0xD2: %rho%: 휌
 0xD3: %sigma%: 휎
 0xD4: %tau%: 휏
 0xD5: %upsilon%: 휐
 0xD6: %complex%: ℂ
 0xD7: %omega%: 휔
 0xD8: %xi%: 휉
 0xD9: %psi%: 휓
 0xDA: %zeta%: 휁
 0xDB: %SX%: ⦏
 0xDC: %BV%: │
 0xDD: %EX%: ⦎
 0xDE: %dunion%: ⋃
 0xDF: %pfun%: ⇸
 0xE0: %inj%: ↣
 0xE1: %dsub%: ⩤
 0xE2: %bottom%: ⊥
 0xE3: %Leftarrow%: ⇐
 0xE4: %psupset%: ⊃
 0xE5: %supset%: ⊇
 0xE6: %fset%: 픽
 0xE7: %uptext%: ↗
 0xE8: %dntext%: ↘
 0xE9: %replacedby%: ≡
 0xEA: %cantext%: ↕
 0xEB: %cat%: ⁀
 0xEC: %extract%: ↿
 0xED: %map%: ↦
 0xEE: %nat%: ℕ
 0xEF: %surj%: ↠
 0xF0: %pset%: ℙ
 0xF1: %SZT%: ⓩ
 0xF2: %dres%: ◁
 0xF3: %rat%: ℚ
 0xF4: %thm%: ⊢
 0xF5: %ulbegin%: ⨽
 0xF6: %ulend%: ⨼
 0xF7: %BT%: ├
 0xF8: %uminus%: ﹣
 0xF9: %filter%: ↾
 0xFA: %int%: ℤ
 0xFB: %lbag%: ⟦
 0xFC: %BH%: ─
 0xFD: %rbag%: ⟧
 0xFE: %pinj%: ⤔
 0xFF: %SZS%: ┌
  
 ___
 Proofpower mailing list
 Proofpower@lemma-one.com
 http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

[ProofPower] Unicode and ProofPower

[Rob Arthan]

Dear All,

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 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)⌝

(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. Most text editors and word processors on the 
systems I have tried do support UTF-8. If anyone can advise on how to extend 
the range of Unicode glyphs available on Linux or on how to get font 
substitution working nicely with OpenMotif, I would be very grateful.

There is a prototype implementation of the translation as two free-standing 
programs pputf8 and utf8pp here:

https://github.com/RobArthan/pp-contrib

(These have been around for a while, but I have just changed them to implement 
the somewhat simplified and extended scheme described in the Web page cited 
above.)

My immediate plan is to integrate the translation into ProofPower itself, so 
that Unicode input and output are options you can select with set_flag (similar 
to the way that you can currently select ASCII output, by calling 
set_flag(“use_extended_chars”, false)). I will provide separate flags for input 
and output.

Below, as a further test of your e-mail client, you will find the ASCII 
encoding and UTF-8 encoding of the corresponding Unicode for all the characters 
in the ProofPower extended character set.

Regards,

Rob.

%rsub%: ⩥
%bagunion%: ⨄
%bbU%: 핌
%Delta%: Δ
%fcomp%: ∘
%Phi%: Φ
%Gamma%: Γ
%down%: ⋎
%Theta%: Θ
%dcat%: ⁀/
%Lambda%: Λ
%mem%: ∈
%notmem%: ∉
%bij%: ⤖
%Pi%: Π
%SML%: 
%rres%: ▷
%Sigma%: Σ
%:%: 
%Upsilon%: Υ
%boolean%: 픹
%Omega%: Ω
%Xi%: Ξ
%Psi%: Ψ
%emptyset%: ∅
%up%: ⋏
%BHH%: ═
%finj%: ⤕
%ffun%: ⇻
%psubset%: ⊂
%intersect%: ∩
%rseq%: 〉
%symdiff%: ⊖
%equiv%: ⇔
%dintersect%: ⋂
%def%: ≜
%lseq%: 〈
%lrelimg%: ⦇
%rrelimg%: ⦈
%rel%: ↔
%overwrite%: ⊕
%%: ⌜
%fun%: →
%%: ⌝
%real%: ℝ
%EFT%: █
%and%: ∧
%or%: ∨
%not%: ¬
%implies%: ⇒
%forall%: ∀
%exists%: ∃
%spot%: ⦁
%x%: ×
%SFT%: Ⓢ
%bigcolon%: ⦂
%rcomp%: ⨾
%leq%: ≤
%neq%: ≠
%geq%: ≥
%symbol%: 핊
%union%: ∪
%alpha%: α
%beta%: β
%delta%: δ
%select%: ϵ
%phi%: ϕ
%gamma%: γ
%eta%: η
%iota%: ι
%theta%: θ
%kappa%: κ
%fn%: λ
%mu%: μ
%nu%: ν
%psurj%: ⤀
%pi%: π
%chi%: χ
%rho%: ρ
%sigma%: σ
%tau%: τ
%upsilon%: υ
%complex%: ℂ
%omega%: ω
%xi%: ξ
%psi%: φ
%zeta%: ζ
%SX%: ⦏
%BV%: │
%EX%: ⦎
%dunion%: ⋃
%pfun%: ⇸
%inj%: ↣
%dsub%: ⩤
%bottom%: ⊥
%Leftarrow%: ⇐
%psupset%: ⊃
%supset%: ⊇
%fset%: 픽
%uptext%: ↗
%dntext%: ↘
%cantext%: ↕
%cat%: ⁀
%extract%: ↿
%map%: ↦
%nat%: ℕ
%surj%: ↠
%pset%: ℙ
%dres%: ◁
%rat%: ℚ
%thm%: ⊢
%ulbegin%: ₍
%ulend%: ₎
%BT%: ├
%uminus%: ﹣
%filter%: ↾
%int%: ℤ
%lbag%: ⟦
%BH%: ─
%rbag%: ⟧
%pinj%: ⤔

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

Re: [ProofPower] ProofPower PrettyPrinter

[Rob Arthan]

David,

On 22 Feb 2015, at 16:47, David Topham dtop...@ohlone.edu wrote:

 I am trying to get a proof listing (of hypothetical syllogism) for teaching 
 purposes.
 
 Thanks to help from Roger, I have the proof working, but would like to use 
 PrettyPrinter to put each step of proof on different line. I almost have it, 
 but ran into a snag with the special character Q (which means something 
 special to ProofPower).
 
 I attached the screen capture where you can see the Q has become .

There is a function translate_for_output which undoes the encoding.

Even easier in your example, there is a function diag_line which translates a
string for output and prints it on standard output followed by a newline 
character.
If you change your definition of printList

val printList = app diag_line;

it should do what you want.

Regards,

Rob.

 
 My goal is something approximating a Fitch-style proof (but I don't need the 
 lines for the subproof)
 
 I appreciate any suggestions...
 
 -Dave Topham
 prettyPrint.jpg___
 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] load proof power with PolyML

[Rob Arthan]

Yuhui,

On 22 Feb 2013, at 14:24, Yuhui Lin wrote:

 Hi,
 
 I wonder if is possible to load proof power from polyML directly, perhaps by 
 PolyML.make with the proof power source code.

I have never tried PolyML.make. There is no reason why you shouldn't compile 
the ProofPower source code by loading it in from a Poly/ML session, but I 
suspect that there are various things that might not work properly without some 
adjustment if you were to do that. 

 The fact is that we want to build a system which proof power will be in the 
 middle of the architecture, i.e some_libraries  -- proofpower -- 
 another_component_with_UI.  
 

Do you mean you want to construct one ML program that includes the source of 
some_libraries, plus the source of ProofPower, plus the source of 
another_component_with_UI. If so, then why does ProofPower need to be in the 
middle? That would only make a difference if some_libraries was providing 
replacements for functions that ProofPower uses, wouldn't it? In any case, it 
sould be a relatively simple change to make the starting point of the 
ProofPower build be Poly/ML + some_libraries.

Regards,

Rob.


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

Re: [ProofPower] proofpower

[Rob Arthan]

Sarah,

Why do you keep repeating your questions? If you do not understand the replies 
that Phil Clayton or Roger Jones provided then respond to their posts and make 
sure you copy your replies to the mailing list.

Also, you have been trying to make a post with a screenshot attached. Please do 
not do that, as I don't want to clog up the mailing list archives with large 
files. Instead describe your problems in words. If we really need to see a 
screenshot, then we will let you know.

Regards,

Rob.

On 20 Feb 2013, at 14:04, 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.
 thanks
 ___
 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] activating templates

[Rob Arthan]

Sarah,

On Feb 11, 2013, at 9:12 AM, khan khan azurc...@yahoo.com 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??? 
 

You shouldn't need to do anything special. The files in the directory 
$PPHOME/app-defaults should work as they are  (where $PPHOME stands for the 
directory where you have installed ProofPower). You may be failing to pick up 
the Xpp resource file at all. Try running xpp with the following command line 
and let us know what it tells you:

PPENVDEBUG=y xpp

Regards,

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

Re: [ProofPower] activating templates

[Rob Arthan]

Sarah,

On Feb 11, 2013, at 4:55 PM, khan khan azurc...@yahoo.com wrote:

 no i have not installed proofpower in $PPHOME...it is installed inside 
 openproofpower-2.9.1w2…

I was using $PPHOME as a symbolic name for the directory name of the ProofPower 
installation directory (chosen by you or by the configure script when you ran 
the configure script).  What output did you get when you ran the configure 
script?


 their is still a folder by name pp but its app-defaults folder is empty... 
 and i have tried this command it says no printer found, aborting ...please 
 help me …

It sounds like you are picking up another program called xpp that is used to 
configure printers on some Linux distributions. 

Regards,

Rob.

 
 thank you
 sarah
 
 --- On Mon, 11/2/13, Rob Arthan r...@lemma-one.com wrote:
 
 From: Rob Arthan r...@lemma-one.com
 Subject: Re: [ProofPower] activating templates
 To: khan khan azurc...@yahoo.com
 Cc: proofpower@lemma-one.com
 Received: Monday, 11 February, 2013, 7:29 AM
 
 Sarah,
 
 On Feb 11, 2013, at 9:12 AM, khan khan azurc...@yahoo.com 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??? 
 
 
 You shouldn't need to do anything special. The files in the directory 
 $PPHOME/app-defaults should work as they are  (where $PPHOME stands for the 
 directory where you have installed ProofPower). You may be failing to pick up 
 the Xpp resource file at all. Try running xpp with the following command line 
 and let us know what it tells you:
 
   PPENVDEBUG=y xpp
 
 Regards,
 
 Rob.


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

Re: [ProofPower] templates activation problem

[Rob Arthan]

On 15 Jan 2013, at 22:12, Phil Clayton wrote:
 
 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.

That is correct. It may also be worth knowing that the file name in a #include 
directive in a resource file is interpreted relative to the directory in which 
the resource file was found.

  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
 

N.b., the output from this does not appear on the xpp GUI, but on standard 
error, i.e., in the Terminal window where you ran the command.

 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?

I am hoping that Sarah who asked the original question that prompted this 
thread has solved her problem. In case not, here is a bit more information. 
Sarah wrote:

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

Apologies for any confusion about the XppKeyboard file. Only one of these is 
now supplied, so it is supplied as an actual file not a link (so the 
documentation quoted above is a little out of date). In the supplied example 
app-defaults directory, the Xpp file includes the line:
#include XppTemplates

and XppTemplates is a symbolic link to XppZTemplates. If the Xpp.templates 
resource that is specified in XppZTemplates is not being picked up, then this 
will result in the Templates Menu item being inactive. However, you should not 
need to change the supplied files to pick up the settings from XppZTemplates.

Most users don't need to do anything to pick up the example resource files 
supplied in the app-defaults directory in the ProofPower installation 
directory. xpp will arrange to find them there unless you have defined the 
XUSERFILESEARCHPATH (or XAPPLRESDIR) environment variables (presumably to 
specify custom resource files for other X Windows applications). As Phil says, 
running xpp with the PPENVDEBUG environment variable set as above will tell you 
whether it is using its own value for XUSERFILESEARCHPATH or yours. You may 
find that the set up for some other application has caused XUSERFILESEARCHPATH 
or XAPPLRESDIR to be defined in your shell start up files without you knowing 
about it. In any case, if xpp is using your setting, then, the simplest thing 
to do is to copy the Xpp resource files into a directory on your 
XUSERFILESEARCHPATH.

Finally, if you need to do lower level debugging of resource settings in xpp, 
then the command

xpp -c appres Xpp

will give you copious information (in the xpp journal window) about the 
resource settings that xpp is actually seeing.

Regards,

Rob.



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

[ProofPower] Fwd: Motif Released Under LGPL; Updated Version Available Now

[Rob Arthan]

See below for some good news. The dependency of xpp on OpenMotif should be much 
less problematic in the future.

Regards,

Rob.

Begin forwarded message:

 From: Natalie Adams nata...@ics.com
 Date: 24 October 2012 18:00:11 GMT+01:00
 To: r...@lemma-one.com
 Subject: Motif Released Under LGPL; Updated Version Available Now
 Reply-To: Natalie Adams nata...@ics.com
 
 Updated Version of Motif 2.3.4 Now Available on SourceForge and at the Newly 
 Updated ICS MotifZone
 Is this email not displaying correctly?
 View it in your browser.
 
 Motif Released as Open Source Software Under LGPL v2.1
 Updated Version of Motif 2.3.4 Now Available on SourceForge and at the Newly 
 Updated ICS Motif
  
 Integrated Computer Solutions (ICS) is pleased to announce that Motif 2.3.4 
 has been released under LGPL v2.1. Motif is a freely available source code 
 distribution for the Motif user interface component toolkit. Motif 2.3.4 is 
 an updated version of Open Motif 2.3 and is a major bug fix release.
  
 Source code is available on SourceForge. Binaries are also available for the 
 following operating systems on SourceForge and the ICS MotifZone:
 
 • Red Hat Enterprise Linux
 • Fedora
 • Ubuntu
  
 Motif 2.3.4 Bug Fix Release 
 This release includes performance updates and addresses numerous bug fixes 
 and application issues. A full list of modifications is available in the 
 Motif 2.3.4 Release Notes.
 
 Newly Designed ICS MotifZone
 In addition to finding the latest Version of Motif 2.3.4 on the ICS 
 MotifZone, we invite you to spend some time with our newly designed site, 
 where you will find Motif community forumsand information on Motif-related 
 products including and the latest versions of our GUI Builders and a 
 comprehensive application testing environment. The ICS MotifZone also 
 provides helpful whitepapers and training videos. In short, the ICS MotifZone 
 is home to all things Motif. 
 
 About ICS
 Integrated Computer Solutions, Inc. (ICS) of Bedford, MA, is the world's 
 leading provider of advanced visual development tools and services for 
 software professionals. ICS's BX PRO series of GUI builders has long been 
 recognized as the software of choice for visually creating mission-critical, 
 high-performance Motif applications. Additionally, ICS is the largest 
 independent supplier of professional services, and training for the Qt® 
 cross-platform UI framework. ICS primarily serves Fortune 500 clients 
 globally within the Aerospace, Government, Financial Services, Media  
 Entertainment, Health  Life Sciences, Automotive and Consumer and Industrial 
 Device industries. 
  forward to a friend 
 Copyright © 2012 Integrated Computer Solutions, Inc., All rights reserved. 
 You are receiving this email because you joined the MotifZone website at 
 http://www.motifzone.com. 
 Our mailing address is: 
 Integrated Computer Solutions, Inc.
 54 B Middlesex Turnpike
 Bedford, MA 01730
 
 Add us to your address book
  unsubscribe from this list | update subscription preferences 
 
 

___
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

[Rob Arthan]

On 14 Sep 2012, at 03:01, Jon Lockhart wrote:

 Phil,
 
 Moving them all to there own paragraph worked great. Now I am up to proving 
 the consistency of the axioms, which is where I am run into my next stumbling 
 block. Got the spec load and the consistency goal using the commands no 
 problem. This generates a sub goal which looks relatively straight forward. 
 It using the there exist symbol at the front of the goal, so my initial 
 assumption is to use the z_there exists_tac, as seen in the provided spec.

Unfortunately I can't unzip your attachment to check exactly what you are 
doing. There is minimal proof support for consistency goals in Z, since very 
few Z users have expressed much interest in proving consistency. 

 Unfortunately just giving it masterStop is not enough, and I can't feed it a 
 list of masterStop and masterReset. Next thought was there should be some 
 tactic like this that also has list in it, but I can't seem to find one.

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]);

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.

Regards,

Rob.___
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

[Rob Arthan]

Jon,

Can you post the actual input that is failing, please. (To protect it in 
transit, either gzip your .doc file and attach it to your post, or use 
conv_ascii to convert it into ASCII).

Regards,

Rob.

Regards,

Rob.

On 3 Sep 2012, at 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 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

[ProofPower] Test from lemma-one.com

[Rob Arthan]

This is a test please ignore, unless you don't receive it, in which case it 
would be helpful if you could let me know :-)

Regards,

Rob.


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

Re: [ProofPower] ProofPower Update

[Rob Arthan]

On 11 Aug 2012, at 15:07, Roger Bishop Jones wrote:

 I have now managed to build my theories on the new 
 ProofPower and MathsEgs.
 
 I had to modify 13 source files to get them through.
 
 It seems probable that the changes all resulted from the new 
 MathsEgs, and primarily were changes to names.
 These include the changes to theorems plus = additive 

Those name changes seemed like a necessary rationalisation when I was prettying 
up this stuff in preparation for my talk at the AIPA workshop at ETAPS.

 and a number of cases where identifiers which I had been 
 using are now used in MathsEgs theories which are in my 
 ancestry these include Tree TREE Pair

Were you using these names for things of your own? If so, then perhaps this 
would be solved if the underlying names of constants were prefixed with the 
theory name. What I am considering in this area is an option controlled by a 
flag (say structured_HOL_namespace), which I would turn on towards the end of 
the HOL build, whereby the HOL parser would do this for you. When you define 
constant xyz in theory abc, the underlying name would be xyz.abc and 
abc would be introduced as an alias for that. And likewise for types. This 
behaviour would be optional and language-specific (e.g., you wouldn't want it 
for Z, and you might not want it in HOL). Would that have saved you any trouble?

 (probably the most 
 disruptive) and some identifiers consisting of or starting 
 with subscripted D.
 

Really -  I can't find any identifiers that start with a subscripted character 
in the MathsEgs theories.

 There was only one broken proof (for reasons other than 
 naming), and I am guessing that the reason was a change in 
 the behaviour of R_top_anf_tac which now introduces powers 
 in place of products where possible (it doesn't look like 
 that was happening before) but I just repaired the proof and 
 didn't go into detail on what had broken it.

Sorry, I forgot to announce the change to real ANF.

 
 I have not yet considered a new way of building contribs.
 I feel that making MathsEgs build OK on the development 
 system would not be productive in the absence of a little 
 more clarity about how a contrib system would be expected to 
 work.

I had a discussion with Anthony Fox about how they do things in HOL4 and that 
has given me some more ideas on this. I think it is actually completely 
orthogonal to how the ProofPower code is organised.

In HOL4, the contents of a theory are exported to and imported from text files. 
So if you have code associated with a theory that you want to export to users 
of the theory, you put that in a separate file and let users load that file. As 
ML doesn't have separate compilation, such code has to be provided as source. 
To  make things easier for the user, HOL4 has its own make function, HOLmake, 
that automatically figures out dependencies between a set of things you want to 
bring together and loads them in the right order. Given that we don't have 
HOLmake and we don't allow export and import from files, this suggests to me 
that a contrib offering should comprise ML source to build the theory and 
provide any supporting ML functions etc.

Here is one possible set of conventions. The source of a contrib offering, XYZ, 
comprises a directory containing doc files together with a (UN*X) make file. 
The make file has a target that build a database called XYZ, that contains the 
contrib theories and associated ML and a minimal set of dependencies. Users who 
want to start from the contrib offering can just create children of the 
database. The make file also has a target that creates the ML source from the 
doc files and concatenates them into an appropriate order to give a single 
source file XYZ.ML (not XYZ.sml, since this will typically not be directly 
derived from a single .doc file). A built contrib offering would comprise the 
.doc files plus PDF of those (and/or DVI?) plus the database XYZ and the source 
file XYZ.ML.

It would also be useful to maintain a ref to a list of strings identifying the 
loaded contrib offerings. This would be managed at the head and tail of XYZ.ML 
via access functions that allow it to be interrogated and extended. At the head 
we would have code to check that all the dependencies are satisfied and to 
report on anything that is missing (or you could be cleverer and attempt to 
load the missing dependencies - so this would be a bit like a mini-HOLmake, in 
which the contrib provider has to declare the dependencies). At the tail would 
be code to add the new contrib name to the list. The contrib directories could 
be organised as a tree with an initial contrib at the top that defines the list 
of loaded offerings and includes tools for working with it.

As regards ML conventions, I would suggest that we don't mandate the rigid 
packaging of things into structures with signature constraints that ProofPower 
itself follows, but do encourage people at least to collect all the external 

Re: [ProofPower] Trying to Prove my Zed Specifications

[Rob Arthan]

On 18 Aug 2012, at 22:14, Jon Lockhart wrote:

 Rob,
 
 I got a trouble shooting question for you. Been going through the learning 
 documentation this weekend, currently still on the first tutorial wanting to 
 make sure I soak it all in before moving to HOL and Z, but I seem to be 
 running into a problem with one of the commands. Every time I try to use the 
 save_and_quit() ML command in the execution Window the whole system freezes 
 up.

Thanks to Jon for pointing this out and proviing further details. I now have a 
fix for this problem, whereby what caused a busy wait on some operating systems 
will actually stop xpp responding to the user on a recent Debian release. I 
have attached a patch which should work on any version downloaded in the last 
18 months or so.

To use the patch, copy it into /tmp say, then go to your ProofPower build 
directory (where config and install live) and do:

gunzip -c /tmp/patch-2.9.1w2.rda.120821.gz | patch -p1 -b -B orig/

then do:

PPTARGETS=xpp ./configure
./install -d

Regards,

Rob.


patch-2.9.1w2.rda.120821.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] Trying to Prove my Zed Specifications

[Rob Arthan]

Jon,

On 19 Aug 2012, at 20:51, Jon Lockhart wrote:

 Roger,
 

 Yes, the xpp interface locks. The command executes and then I can't access 
 any of the taps in the journal window, the ML command line will not close, 
 nor can I use the palette I have open either.

My first guess is that a dialogue window that has popped up but is hidden 
behind one of the other windows. Are you able to slide the windows around to 
look for such a thing? If this is the case, then please let me know what Linux 
distribution and desktop you are using and I will try to find out why the 
window manager isn't getting the stacking ordering right.

If that isn't the problem, then we need to find where xpp is hanging. To do 
this, first install gdb if you don't already have it. Then reproduce the 
problem and find out the process id for the xpp process and do:

gdb ProofPower Installation Directory/bin/xpp process id

and then when gdb gives you its prompt, type where.

Regards,

Rob.




___
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

[Rob Arthan]

Jon,

Thanks. This looks like a very strange race condition. Do you get the same 
problem if you do Kill from the Command Menu or just quit xpp from the File 
Menu rather than run the save_and_quit command? If not, then a possible 
work-around is just not to use quit or save_and_quit.

Regards,

Rob.


On 20 Aug 2012, at 20:17, Jon Lockhart wrote:

 Rob,
 
 Got it installed and this is what was reported when where was run.
 
 (gdb) where
 #0  0x7f1cfb516720 in __read_nocancel ()
 at ../sysdeps/unix/syscall-template.S:82
 #1  0x004117e3 in get_from_application (unused_p=0x0, 
 unused_source=0x168f8a8, unused_id=0x7fff12456e68) at pterm.c:829
 #2  0x7f1cfc171844 in XtAppProcessEvent ()
from /usr/lib/x86_64-linux-gnu/libXt.so.6
 #3  0x7f1cfc1661dd in XtAppMainLoop ()
from /usr/lib/x86_64-linux-gnu/libXt.so.6
 #4  0x0040c507 in main_window_go (
 file_name=0x7fff12457535 ../zed/pp/doc/usr004.doc)
 at mainw.c:2111
 #5  0x0041a3fe in main (argc=6, argv=0x7fff124570f8)
 at xpp.c:670
 
 Thanks,
 Jon
 
 
 On Mon, Aug 20, 2012 at 3:11 PM, Jon Lockhart jal...@bucknell.edu wrote:
 Rob,
 
 I have run into something interesting. None of the buttons work in the 
 window, just as File, Edit, etc, nor do the buttons for closing, maximizing 
 the window, etc., but I am able to move the window around no problem. I have 
 moved the window everywhere, there is no other window around, so that rules 
 out that. I also looked at the process id list to see if there was anything 
 besides the one xpp, and there is not, so there is just the one running.
 
 I will try and get this gdb installed on my Debian imaged and get back to you.
 
 Thanks,
 Jon
 
 
 
 On Mon, Aug 20, 2012 at 1:01 PM, Rob Arthan r...@lemma-one.com wrote:
 Jon,
 
 On 19 Aug 2012, at 20:51, Jon Lockhart wrote:
 
  Roger,
 
 
  Yes, the xpp interface locks. The command executes and then I can't access 
  any of the taps in the journal window, the ML command line will not close, 
  nor can I use the palette I have open either.
 
 My first guess is that a dialogue window that has popped up but is hidden 
 behind one of the other windows. Are you able to slide the windows around to 
 look for such a thing? If this is the case, then please let me know what 
 Linux distribution and desktop you are using and I will try to find out why 
 the window manager isn't getting the stacking ordering right.
 
 If that isn't the problem, then we need to find where xpp is hanging. To do 
 this, first install gdb if you don't already have it. Then reproduce the 
 problem and find out the process id for the xpp process and do:
 
 gdb ProofPower Installation Directory/bin/xpp process id
 
 and then when gdb gives you its prompt, type where.
 
 Regards,
 
 Rob.
 
 
 
 
 

___
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

[Rob Arthan]

Jon,


On 18 Aug 2012, at 22:14, Jon Lockhart wrote:

 Rob,
 
 I got a trouble shooting question for you. Been going through the learning 
 documentation this weekend, currently still on the first tutorial wanting to 
 make sure I soak it all in before moving to HOL and Z, but I seem to be 
 running into a problem with one of the commands. Every time I try to use the 
 save_and_quit() ML command in the execution Window the whole system freezes 
 up. There is no error being thrown, it just returns val it = (): TYPE, and 
 then locks up.
 Have to either kill all the window proc id's or restart the system to get rid 
 of them. Mostly it is restarting b/c kill sometimes will not remove them for 
 some reason. I was working on the Peanissimo theory write up. Written it 
 several times and get the lock up every time, any suggestions on trouble 
 shooting?


Are you saying that the xpp user interface locks up? If so that definitely 
shouldn't be happening. The ProofPower-ML session running in the xpp journal 
window should finish, but the xpp menus and so on should work as normal. Is 
that not what is happening?

Aside: the source of this tutorial is in usr004.doc in the doc directory, so 
you don't need to type it in yourself.

Regards,

Rob.


___
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

[Rob Arthan]

On 13 Aug 2012, at 12:05, Jon Lockhart wrote:

 Gentlemen,
 
 I apologize I should of been more specific at the tasks that I was trying to 
 accomplish and in describing where I am at so far.
 
 It seems the first point of business though from what Rob is saying is 
 actually getting the specifications into the ProofPower environment, which at 
 this point sounds like it needs to be done by hand, but I will explain it 
 more closely Rob. That way you can tell me if I got a shot of importing them 
 or if I am going to have to do a hand rewrite.
 
 So as you mentioned Rob, I am using Anthony's Z Word Tools for Word and I 
 have written all my specifications in there so far. It is a fabulous writing 
 tool, interfacing so well with Word, and providing all the structure I need 
 to write the specifications I am working on. Now, I am not sure if you are 
 aware of this, but the latest version of the Z Word Tools no longer requires 
 an export of the specification to be used with FUZZ or CZT, those checkers 
 are built right into the tool now and allow for typechecking of the 
 specification as you are writing it, using either checker

I think you will find that Z Word Tools is actually extracting the Z into a 
file and running Fuzz or CZT for you, so it feels like the typechecker is built 
in. You will find that the menu you use to do the typechecking has an item on 
it to export the Z as a file.

 Now of course, neither of these checkers run on .doc / .docx format files, 
 and there are a whole host of other files generated when you save or run a 
 check, including a LaTeX file of the specification. I was wondering if you 
 thought this LaTeX file would be possible to import into the ProofPower 
 system, or does it have to be in a special format of .tex to be of any use? 

I actually thought that the CZT unicode format might be a bit closer to what my 
prototype tools for dealing with UTF-8 can cope with. If you only have a few 
pages of Z to start with, then it will probably be quicker just to reenter it 
manually. If you have more it may be worth trying to cobble together something 
semi-automated. We should be able to do something much slicker in the slightly 
longer term.

 
 I have attached one of the specifications I was originally using to learn Z 
 Word Tools, and it has passed all the typecheckers. This is the LaTeX file 
 that is generated for the specification.
 

Thanks.  This reminds me that one of the bigger problems is that ProofPower has 
different rules for newlines than Spivey and the Standard Z. Specifically, 
ProofPower requires semicolons at the end of declarations and to separate 
stacked predicates in the predicate parts of schemas.

Regards,

Rob.


___
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

[Rob Arthan]

On 13 Aug 2012, at 10:59, Roger Bishop Jones wrote:

 On Monday 13 Aug 2012 13:12, Rob Arthan wrote:
 
 Jon is using Anthony Hall's Z Word Tools, which actually
 go quite a long way to bridging this gap. Z Word Tools
 allows you to prepare a Z specification inside a Word
 document and project out the Z in a format suitable for
 processing by other tools such as Fuzz or CZT.  Anthony
 and I have talked about adding ProofPower as a list of
 targets, but it got deferred pending some work I was
 doing on getting ProofPower to support UTF-8. I have a
 prototype converter from a UTF-8 format to the
 ProofPower formats, but it would require a bit of
 handcranking to get it to convert CZT input into
 ProofPower input. I don't know how much work would be
 involved in getting Z Word Tools to output something
 that ProofPower can eat (e.g., my UTF-8 format).
 
 That's all very interesting, and it would be good to get 
 ProofPower into a less eccentric position on document 
 formats.
 
I agree.

 I have myself recently found myself using utf8 in LaTeX 
 documents (when I wanted to get some Greek in), and may find 
 myself wanting to prepare documents which have both Greek 
 and ProofPower as a result of furthering my modelling of 
 aspects of Aristotle's Organon and Metaphysics.
 
 I see from reading a little about this in either or both of 
 emacs and PERL that the support of arbitary encodings rather 
 than specifically of one or more of the UTF variants seems to 
 be thought desirable (and is realised I think in emacs).
 From this point of view one might consider making the 
 ProofPower encoding respectable by doing whatever is 
 needed for it to be supported by such generic software.

Surely just accepting and outputting UTF-8 will achieve that, won't it?

 It might then be possible to convert between ProofPower's 
 encoding and others using some standard generic utility 
 (perhaps emacs does this).
 [On further grubbing around I think the generic facilities 
 support a fixed, if perhaps long, list of encodings.
 I haven't found anything which appears to work from a soft 
 definition of an encoding.]
 
 Somewhere in this maze I think there are ways of telling 
 that the greek alphabet does consist of alphabetic 
 characters and hence perhaps should be admitted in 
 ProofPower identifiers.

That is somewhat orthogonal to how I would plan to do the ProofPower side of 
this in the first instance.

 When you speak of my UTF8 format, presumably you are 
 talking about the mapping between the ProofPower extended 
 characters and the unicode character codes (which wouldn't 
 be specific to UTF8).

Yes.

 
 Incidentally, my hacks for making HTML from ProofPower 
 sources, though they once translated into image references, 
 were switched a while back to use unicode entities (not UTF 
 but ascii things like #;) so I do have a mapping 
 between the two (though incomplete).
 Not good enough to be of any help to you, but I would fall 
 in line with whatever mapping you have come up with if I 
 ever find myself augmenting or fixing it.

When I got some time. I will tidy up the little prototype converter I wrote and 
make it available for you to have a look at.

Regards,

Rob.


___
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

[Rob Arthan]

On 13 Aug 2012, at 13:31, Jon Lockhart wrote:

 Rob,
 
 Ok so looks like I am looking to rewrite all my specifications again in 
 ProofPower. A minor inconvenience but should not be a problem.

That is likely the quickest way to get started.

 I will just pop up my specs on one screen and bring up ProofPower's XPP up on 
 the other screen in my Linux VM, and I should be able to rewrite them with no 
 problems. The only thing I can't seem to find is the symbol library in XPP. I 
 have found where I can insert the various Zed structures, no problem, but 
 there is supposed to be an XPP keyboard that has these symbols, based on the 
 pictures in the documentation. Is this available in the editor version of XPP 
 or do I need to run the full version of XPP to have access to that?
 
The keyboard in the picture is the actual keyboard, although you may need to do 
a bit more work to set it up. There is a tool called the Palette in the Tools 
menu that lets you enter all the symbols with mouse clicks without having to do 
any more set-up and without having to learn the key combinations.

If you do want to set up the keyboard have a read of section 4.3 of the Xpp 
manual and the comments at the head of the file app-defaults/XppKeyboard in the 
first instance. 


 Once I get these in the system though, I definitely need to get some proofs 
 written for them. That is where I am having a fair bit of trouble with the 
 examples and documentation at the moment. I have a solid grasp of Z, and from 
 Rogers email and the documentation, I can just write the proofs mostly in Z, 
 which would save me some time in having to learn HOL right now, though I 
 think I will learn it anyways for the future, just at a slower pace. In any 
 case, the proof writing is not the issue, it is the writing in the ProofPower 
 environment I guess I am hung up on, along with a few other minor things.
 
 I will look over all the documentation again on the site Rob, and continuing 
 to see if I can get the examples operational so I can apply what is shown 
 there to my open specifications.


Good luck! And do keep asking if you have any more problems.

Regards,

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

[ProofPower] ProofPower Update

[Rob Arthan]

Dear All,

I plan to make a new ProofPower release shortly. In the meantime, if you want 
the state of the art, I uploaded an experimental version built from the latest 
source. You can find this here:

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

The main reason for the experimental release was because I hadn't updated the 
Mathematical Case Studies listed on the examples page 
(http://www.lemma-one.com/ProofPower/examples/examples.html) and I wanted to 
upload the latest versions of those for various people to read. So the main 
changes in ProofPower are in ProofPower-HOL. Specifically, I think higher-order 
matching is well-tested and stable now.

Regards,

Rob.

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

Re: [ProofPower] ProofPower RCS Repository

[Rob Arthan]

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 ?

Failing that, we need to compare the gcc call that caused the errors with the 
one that works when you build from the OpenProofPower distribution.

Regards,

Rob.


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

[ProofPower] ProofPower RCS Repository

[Rob Arthan]

There were some discussions last year about making the ProofPower source 
repository available online, but this didn't come to anything. The main problem 
I have is that the popular version control systems (CVS, SVN, Git, Mercurial) 
don't seem to fit very well with what I have always done once-up-a-time with 
SCCS and since then with RCS - namely have one flat repository of source files 
that different packages share. I have a symbolic link to this repository in 
directories for the various ProofPower packages and the makefiles for each 
package (which have distinctive names) get what they need out of the 
repository. Thus one source file can appear in several different packages, 
which turns out to be more useful than it sounds, given that source files here 
includes things like LaTeX style files and other stuff that isn't really source 
code, but is needed to make the package.

In order to make some progress in this direction, I have written a shell script 
that you can find here:

https://dl.dropbox.com/u/34693999/opp-developer-setup.sh

that creates a directory structure like the one I use to develop ProofPower. It 
then builds the OpenProofPower packages in that structure. Finally it builds 
the distribution (using the makefile for a pseudo-package called opp). There 
are comments at the top of the script that explain what it does and various 
environment variables that parametrize it. Unless you ask it not to, the script 
downloads a tarball of the RCS repository.

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.

Regards,

Rob.

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

Re: [ProofPower] Trouble Installing on Windows

[Rob Arthan]

On 1 Aug 2012, at 04:35, Jon Lockhart wrote:

 Phil,
 
 I ran the original yum setup you gave me. Unfortunately the polyml from the 
 yum install was not placed in the user/lib path, and I could not find it, so 
 I just built a copy of 5.4 myself and was able to get that installed no 
 problem in the /user folder. 
 
 Now I believe I am running into the issue you mentioned about Motif. I went 
 to motifzone.net and downloaded the latest version which was an rpm and I 
 grabbed the Fedora 12 version since it was the closest version to 17. The rpm 
 installed just fine, though some compatibility packages had to be downloaded 
 and installed as well. Now unfortunately the configure file for ProofPower is 
 not finding Motif installed. 

You can use the PPMOTIFHOME environment variable to tell the configure script 
where Motif is. Something like:

PPMOTIFHOME=/usr/local/ ./configure

I don't know where the rpm will have put the Motif installation, but you should 
be able to find that out with an rpm enquiry.

Does that help?

Regards,

Rob.

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

Re: [ProofPower] ProofPower in the cloud?

[Rob Arthan]

Roger,

On 22 Jul 2012, at 10:23, Roger Bishop Jones wrote:

 Has anyone tried, or even considered, running ProoPower in 
 the Amazon cloud (AWS they call it Amazon Web Services)?
 
 They offer a number of Linux images which might be used as 
 starting points.
 Presumably one could run ProofPower and xpp in the cloud and 
 access it using an X-client on cygwin on MS windows, in 
 theory.

That's an interesting idea. There are other MS Windows X-clients too, e.g., 
Xming, that don't have such a big footprint as Cygwin.
 
 (I had a poke around but didn't spend enough time to get 
 anywhere).

What is the AWS pricing model?

Regards,

Rob.

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

Re: [ProofPower] Trouble Installing on Windows

[Rob Arthan]

John,

On 21 Jul 2012, at 17:56, Jon Lockhart wrote:

 Dear Rob,
 
 Thank you for returning my email and the advice you have given.
 
 After getting more into the installation I realized that Motiff was not 
 available for Cygwin and I was going to have no interface to work with. I 
 thought maybe there was some terminal commands I could use to run ProofPower, 
 but there as well there was no dice.
 

You can run it from a terminal and you can set a flag so that the output is all 
in ASCII, but the ASCII format was mainly designed for interchange and I 
wouldn't recommend it for interactive use.


 I have moved on to looking at installing a VM. I am familiar and have used 
 VM's plenty over my albeit short career, but I have never personally 
 installed one. I was actually looking at Virtual Box, and was a little 
 concerned b/c just like you I am using an XP laptop for my work since I 
 travel to and from the lab and my apartment. I am glad to see I can get away 
 with just using 10 to 15 GB. Since this is a much older laptop, do you think 
 I will have an issue with only have 1 GB of RAM. If so I can use my desktop 
 since I have plenty of performance there.
 

 Rather than Ubuntu, do you think a Fedora distro would be sufficient for the 
 task?

Fedora and 1GB of RAM should work fine.

Regards,

Rob.



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

Re: [ProofPower] Trouble Installing on Windows

[Rob Arthan]

Jon,

On 19 Jul 2012, at 21:57, Jon Lockhart wrote:

 Dear PP Community,
 
 I was wondering if anyone had any help or suggestions for trying to install 
 ProofPower on a Windows machine?
 
 I am currently running Windows XP Professional, Service Pack 3, 32-bit.
 
 I have downloaded all the necessary components that were necessary. I have 
 tried installing PP using Cygwin, but I can't get to any of my Windows 
 directories from it.

Cygwin sets up a directory /cygdrive whose subdirectories are the mounted file 
systems on Windows. Your Windows directories will be there under /cygdrive/c (= 
C:) or /cygdrive/d (= D:) or wherever. Once you have found My Documents etc. 
you can put links to them in your Cygwin home directory.

 I have also tried installing it from GIT Bash, but when I run the config file 
 I get an error returned saying I have no ML installed, though I do have Poly 
 ML installed, as the page instructions say to do. I have added Poly ML to my 
 path variable but that does not seem to fix the problem either.

I am afraid I have no experience of GIT Bash and don't know what kind of UN*X 
look-alike environment it gives you. 

On MS Windows, ProofPower will only build out of the box using Cygwin. With 
some modifications a build can be got to work with MinGW, but I have not proved 
that route myself. ProofPower was ported to Cygwin to meet the needs of a 
particular group of users who have their own front-end that uses ProofPower to 
provide proof services running as a server on Windows. But they are experts who 
have their own custom build, now using MinGW, that is not currently available 
in the OpenSource distribution.

However, Cygwin doesn't support Motif currently, so, even if your persever with 
Cygwin, you won't have any kind of usable interactive user interface. So I 
don't recommend this route for ordinary users. If you want to run ProofPower on 
MS Windows at the moment, your best option is to install a virtualization 
package, e.g., VirtualBox, build one of the standard Linux distributions as a 
guest operating system and then install ProofPower in that. If you are not 
familiar with VirtualBox or similar, then I can assure you that this is a great 
deal easier than its sounds and the footprint on your Windows systems is 
quite small: you can do a lot in 10 or 15GB. I often have to travel with an XP 
laptop, and this approach using VirtualBox and Ubuntu works very well indeed 
when I want to do ProofPower work while I am on the train.

The good news is that the licencing restrictions that prevent OpenMotif being 
used on Cygwin look likely to be relaxed soon. This will give me some incentive 
to get the whole system to build reliably on Cygwin and maybe making a canned 
binary build for Windows.

Regards,

Rob.



___
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

[Rob Arthan]

On 15 Apr 2012, at 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.

Alas, I am fairly confident that Phil's reading was Spivey's intention. Fuzz 
allows monsters like:

A == 1 .. 10

S ^= [A : A x A | (_+_)A  10]

 
I endorse your view that this is a bad thing and that the ProofPower way is 
better. 
 ...
 Another consideration is the effect of the scope rules on 
 proof.
 

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.

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.

Regards,

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

[ProofPower] Fwd: ABZ2012

[Rob Arthan]

Begin forwarded message:

 From: ABZ2012 abz2...@easychair.org
 Date: 9 January 2012 08:53:58 GMT
 To: Rob Arthan r...@lemma-one.com
 Subject: ABZ2012
 
 Dear Rob,
 
 after several requests, the ABZ deadline has been extended to Jan. 22.
 The conference web page will be updated soon.
 Please, advertise this extension (especially for the track chairs) to those 
 can be interested in submitting a paper.
 
 Best regards,
 Elvinia

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

[ProofPower] Fwd: ABZ2012 remind deadline

[Rob Arthan]

Begin forwarded message:

 From: ABZ2012 abz2...@easychair.org
 Date: 22 December 2011 09:25:34 GMT
 To: Rob Arthan r...@lemma-one.com
 Subject: ABZ2012 remind deadline
 
 Dear Rob,
 
 I would like to recall you the ABZ submission deadline of Jan. 14th.  
 I also kindly ask you, especially the track chars, to advertise this deadline 
 to any mailing list members or researchers you believe could be interested in 
 the event.
 
 I take the opportunity to wish you
 Marry Christmas and Happy New Year!

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

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

[Rob Arthan]

Dear All,

I have just completed a new experimental release of OpenProofPower. You can 
find it here:

http://www.lemma-one.com/ProofPower/getting/experimental/OpenProofPower-2.9.1w2.rda.110814.tgz

The idea is that an experimental release is a step toward the next stable 
version (2.9.2 in this case). There may be additional working versions 2.9.1wN 
to fix problems, but the interfaces in the working versions will be stable 
within one release. The experimental release directory also contains changed 
versions of other items, e.g., the mathematical case studies, if those need to 
be updated for the experimental release.

See the CHANGES file for details of the changes relative to 2.9.1w2, but some 
noteworthy changes relative to 2.9.1w2.rda.110727 are:

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.

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.

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.

My thanks to everyone who has helped with this release and my apologies to 
anyone who contributed requests for features that haven't been implemented yet. 
Your requests are much appreciated and are on the to-do list.

Regards,

Rob.___
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

[Rob Arthan]

Oops1

On 14 Aug 2011, at 16:18, Rob Arthan wrote:

 ...
 b) In xpp, you can now switch dynamically between the horizontal and vertical 
 layout using a new item in the window geometry.

I meant new item in the Window Menu.

Regards,

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

Re: [ProofPower] How do you arrange Xpp?

[Rob Arthan]

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 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] Experimental OpenProofPower release 2.9.1w2.rda.110727

[Rob Arthan]

Dear All,

It has taken a little bit longer than I would have hoped but I have just 
completed a new experimental release of OpenProofPower. You can find it here:

http://www.lemma-one.com/ProofPower/getting/experimental/OpenProofPower-2.9.1w2.rda.110727.tgz

The idea is that an experimental release is a step toward the next stable 
version (2.9.2 in this case). There may be additional working versions 2.9.1wN 
to fix problems, but the interfaces in the working versions will be stable 
within one release. The experimental release directory also contains changed 
versions of other items, e.g., the mathematical case studies, if those need to 
be updated for the experimental release.

See the CHANGES file for details of the changes relative to 2.9.1w2, but some 
noteworthy changes relative to 2.9.1w2.rda.110226 are:

a) Rewriting with higher-order matching is now supported in HOL. It is enabled 
using the component proof context 'sho_rw
(short for: simple higher-order rewriting). As an example, higher-order 
rewriting with the theorem prenex_clauses will put a formula in prenex normal 
form. See if the following turns you into an intuitionist:

merge_pcs_rule1 [predicates, 'sho_rw] rewrite_rule[prenex_clauses] 
induction_thm;

b) Thanks to Phil Clayton, ProofPower-Z now supports empty declaration parts in 
paragraphs (as well as in expressions
which were already supported, also thanks to Phil, in 2.9.1w2.rda.110226).

c) The guillemet brackets that are used in Spivey Z and ISO Standard Z around 
the domains of the constructors in a free type definition are now supported in 
ProofPower-Z. These brackets are entered as %% and %% and are typeset as in 
the Z Reference Manual or the ISO Standard LaTeX mark-up. The brackets are 
defined as an outfix operator in the toolkit with defining property %% x %% 
= x. So you can use them as a general purpose form of brackets that are not 
eliminated automatically by the parser.

d) You can now use == as an alternative to %def% in abbreviation definitions 
and binding displays in ProofPower-Z.

e) There are new underlining bracket characters in the font. These appear on 
screen as underlined brackets and cause the text they enclose to be underlined 
when typeset.

f) A new operator is defined in ProofPower-Z whose name is _ %ulbegin% _ 
%ulend% _ (where %ulbegin% and %ulend% are the ASCII names for the underlining 
bracket characters - so this typesets as three underscores with the middle one 
underlined). It is defined so that x %ulbegin% R %ulend% y holds iff (x, y) 
is a member of the relation R. This effectively generalises the feature in 
Spivey Z whereby underlined identifiers act as infix relation symbols. In 
ProofPower-Z you can now use any expression as an infix relation by underlining 
it.

My thanks to everyone who has helped with this release and my apologies to 
anyone who contributed requests for features that haven't been implemented yet. 
Your requests are much appreciated and are on the to-do list.

Regards,

Rob.___
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

[Rob Arthan]

Phil,

On 15 Jul 2011, at 15:29, Phil Clayton wrote:

 I was going to leave this issue for now but I bumped into it again today, so 
 I've had a look into it.  (It's not something that is holding me up, just 
 forcing me to put in parentheses where I don't want to!)
 
 This issue was 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.

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.

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

 
 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.

See above - this is just an omission from USR005.

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 variables while x and y appear free in pred2. pred1 is the 
false assertion that the function mapping an integer x to the set of bindings 
(y == y) where y  x is empty. pred2 is equivalent to the potentially true 
assertion that y is greater than x. ISO Z appears to allow all the brackets to 
be omitted from pred1 and pred2, which is a little unfortunate.

On the 

Re: [ProofPower] Schema in a predicate stub

[Rob Arthan]

Phil,

On 6 Jul 2011, at 16:15, Phil Clayton wrote:

 On 21/06/11 16:58, Phil Clayton wrote:
 Is there any reason why a schema argument in a predicate stub (_?) isn't
 implicitly converted to a predicate?
 
 A Z specification taking a Standard-compatible approach to booleans may
 have:
 
 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.

The parser and type checker are doing what the ProofPower-Z language 
description says and no more: it talks about the stubs _? and _! in terms of 
the syntactic context in which operands are parsed and says nothing about what 
happens after that. And, in fact, they currently have no effect on 
type-checking. You will find that the following actually works:

if True %and% False then X else Y

This is because the parser knows that the conjunction must be predicate 
conjunction and passes that information on to the type-checker, which then does 
the right thing and converts the operands of the conjunction into predicates. I 
agree with you that it would be much better to have the type checker treat 
contexts corresponding to _? stubs as contexts in which schema expressions are 
converted into booleans.

 
 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.

Yes. I agree it would be better if the type inference aspects of %Pi% came from 
a general rule about predicate stubs. (%Pi% would still be treated specially, 
in that it is removed from the final type-checked term).

 
 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?

No. It is just a historical accident that things are as they are.

 
 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 would put it slightly differently: I can't imagine any useful definition of 
op2 in which it would have a context stub for its operand and be capable of 
delivering a truth value when its operand is a number. So I agree with your 
suggestion that context stubs be type-checked as predicates in predicate 
contexts. A little bit of experimentation with conditionals also supports this. 
E.g., try the following:

(1) [|if 1 = 2 then True else True]

(2) [|if 1 = 2 then True %and% False else (False %and% True)]

(3) [|if 1 = 2 then True %and% False else True]

(1) and (2) work, but if you pick the terms apart you will find that the 
conversion from schema to predicate has happened as late as possible in (1) and 
as early as possible in (2). (3) fails because the else part is type-checked as 
a schema and its type doesn't unify with the type %bbB% of the then part.  If 
the predicate context was passed into the type-checking all (3) would work and 
the conversion of schemas to predicates would be treated uniformly.

I will look into implementing something along these lines.

Regards,

Rob.


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

Re: [ProofPower] Printing of \not\in

[Rob Arthan]

Roger,

I had put this on my list of things to fix by changing \not\in in the style 
file to \notin, but I get exactly the opposite problem: \not\in work but \notin 
fails. Are you still having this problem? I am suspecting that you are using a 
style file that redefines both \not and \notin to something different from what 
LaTeX gives you out of the box. Note that \notin is not in the standard list of 
mathematical symbols in the LaTeX User's Guide.

Regards,

Rob.


On 31 Mar 2011, at 14:26, Roger Bishop Jones wrote:

 On Tuesday 29 Mar 2011 16:48, Rob Arthan wrote:
 
 It works fine for me. What goes wrong?
 
 The failing occurrences are either in index brackets or in 
 theory listings (probably also in index brackets).
 
 The actual error message is:
 
 ! Undefined control sequence.
 \not #1-\let \@@not 
 =\not \let \@@n =\n \let \not =\relax 
 \let \n =\relax \...
 l.849 ...M{} \$\PrNL{}\PrIO{}\PrIJ{m}\PrIJ{p}\PrNN
  {}: S 
 \PrKN{} S \PrKN{} PR...
 
 Unfortunately I don't know how to read these things and 
 hence don't know exactly what it is complaining about,
 but the odds are it is the double at signs.
 
 Also I should say that I am using hyperref and makeindex 
 rather than the standard indexing arrangements, which I 
 would be inclined to blame if the failure was in the index, 
 but I don't see how it (makeindex) affects these occurrences.
 
 Roger
 
 
 
 
 ___
 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

[Rob Arthan]

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_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___
 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] Characteristic function construction?

[Rob Arthan]

Phil,

On 5 Jun 2011, at 22:53, Phil Clayton wrote:

 I've noticed that the ProofPower-Z grammar accepts lambda expressions without 
 a spot, e.g.
 
  (%lambda% x : X)
 
 because it uses the same grammar rules as for mu expressions.  Such 
 expressions always produce the error message
 
 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?

No. Just one of those things.

  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.

Thanks.

Regards,

Rob.

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

Re: [ProofPower] Broken theory indexes

[Rob Arthan]

On 10 Aug 2010, at 17:08, Roger Bishop Jones wrote:
 ...
 \typeout{$Id: rbj.sty,v 1.2 2010-08-08 15:50:44 rbj Exp $}
 \NeedsTeXFormat{LaTeX2e}
 \ProvidesPackage{rbj}
 \RequirePackage{ProofPower}
 \RequirePackage{mathabx}
 \def\Zdef{\MMM{\corresponds}}
 \def\holindexon{\def\holin...@aux##1{%
   \suppr...@quotechars
   \MMM{\def\${\noexpand\$}
   \edef\Temp{##1}\index{!\Temp 
 
 I then invoked package rbj instead of ProoFPower in my 
 ProofPower .doc file.
 
 For what TeX calls macros and LaTeX calls commands, the
 TeX \def or \let will override and existing definition
 while in LaTeX you have to use \renewcommand rather than
 \newcommand. For LaTeX environments, you use
 \renewenvironment. Do bear in that both TeX and LaTeX
 are block-structured, but LaTeX has something called

Oops! That last LaTeX should read TeX.

 \gdef which lets you make top-level definitions from
 within a block.
 
 Unfortunately the distinction between tex and Latex 
 environments is one which I have not grasped, so I don't 
 know which I am in.

When I wrote environment I was using it as the LaTeX technical term for the 
things like tabular in

\begin{tabular}

\end{tabular}

of which LaTeX predefines many and which you can define for yourself using 
\newenvironment. LaTeX is just a macro package as far as TeX is concerned and 
there isn't any sense in which you are in one or the other: when you run 
latex or pdflatex they are both there, cheerfully providing too many different 
ways of doing the same thing.

Regards,

Rob.

  However, since ProofPower uses \def I 
 guess it must be in a tex environment, and so I would 
 suppose that my change is also.
 
See above. In fact the ProofPower style files use a mixture of TeX's \def 
(rather than LaTeX's \newcommand) and LaTeX's \newenvironment (which has no 
equivalent in TeX).

 Possibly my problem is that my redefinition comes later than 
 the crucial invocation of HOLindexOn.
 I see that it is invoked immediately, so perhaps I should 
 reinvoke after my redefinition.
 

Yes, indeed. What the macro you are redefining does does is redefine another 
macro, so nothing much will happen if you don't invoke it.

Regards,

Rob.

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

Re: [ProofPower] Using sqsubset symbol

[Rob Arthan]

On 6 Jul 2010, at 10:29, Roger Bishop Jones wrote:

 I find myself in puzzlement when trying to use the square 
 subset symbol.
 
 When I use it I get an Unknown extended character error.
 If I try to add it (as if it were one of the unallocated 
 codes) using add_new_symbols it complains that the 
 sqsubset keyword is duplicated,
 
 If I use sqsubset2 instead, it works, and it prints OK,
 but I am left wondering whether something somewhere is
 going to misbehave because I added it with the wrong 
 keyword. 

This is the result of a historical oversight. This one symbol should be defined 
as an extended character with two keyword forms %sqsubset% (to match the 
LaTeX manual) and %refinedby% (which is what it is called in the Compliance 
Notation, i.e., DAZ), unfortunately it hasn't been done like that and DAZ does 
exactly what you do and defines a separate extended character. Nothing will 
misbehave given what you have done except that you have two extended characters 
that are logically distinct but will print identically. I thought I had fixed 
this, but it doesn't seem to have got into the release, so I will add it to my 
list of things to do.

 
 Should I have enabled the symbol some other way?
 

No, the build should have done it properly for you! See above.

Regards,

Rob.


___
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

[Rob Arthan]

On 14/04/2010 17:03, Roger Bishop Jones wrote:

On Wednesday 14 Apr 2010 16:07, Rob Arthan wrote:

   

Can you test texpdf on wrk066 from maths_egs? makeindex
  produces some garbled entries resulting in LaTeX erros
  when I try running it by hand.
 

No, doesn't work.

! Extra }, or forgotten $.
argument  ...\mathgroup \symAMSb \relax R\egroup
   {}\kern
.06em\vbox {\hrule...
l.3447}

?
! Emergency stop.
argument  ...\mathgroup \symAMSb \relax R\egroup
   {}\kern
.06em\vbox {\hrule...
l.3447}

!  ==  Fatal error occurred, no output PDF file produced!

My tex isn't good enough to know what's up there.

   
makeindex is having several problems: it is rejecting some index entries 
and garbling others. This LaTeX error is caused by it deleting 
everything up to the bgroup in something beginning ... 
\m...@bgroup.  Some combination of your sed commands and your index 
style file (rbjpp.ist), probably the former, need to be changed to 
protect special characters like ! and multiple occurrences of @.  I 
have attached a small file which shows all the problems. Note that you 
get error messages from makeindex the first time you run texpdf but not 
on subsequent runs (even though the errors persist). I don't fully 
understand your sed commands (why do you change @@ into @?), so you 
are perhaps better placed to look into this.


Do you need hierarchic indexes? If not, then it might be better to write 
a shell function in texpdf (and texdvi) to gather multiple entries for 
the same name rather than use makeindex.


Regards,

Rob.



  Do you use printindex to
  include the index in your documents?
 

Yes

RBJ

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

   




forrbj.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] help

[Rob Arthan]

Igor,

You would need to use an old version (4.2) of Poly/ML for version 2.7.8 of 
ProofPower. Do you have a special reason for not using the latest version 
(2.8.1) of ProofPower? 

Regards,

Rob.

On 16 Nov 2009, at 19:44, Igorj V wrote:

 when using polyML still some error; missing ML_dbase (tryed find -name 
 '*ML_dbase*')
 
 ig...@igorj-laptop:~/Desktop/OpenProofPower-2.7.8$ ./configure 
 Using /opt/pp as the installation target directory
 Using Poly/ML
 ERROR: The file /usr/lib/poly/ML_dbase does not exist
 
 
 2009/11/16 Rob Arthan r...@lemma-one.com
 Igor,
 
 PS: the mailing list rejects posts with big attachments. If you need to send 
 a log file bigger than 30kb or so it is probably better to post an extract 
 first. In this case, the extract was all I needed to see.
 
 Regards,
 
 Rob.
 
 On 15 Nov 2009, at 18:32, Igorj V wrote:
 
 thanx you are right;
 futher how to understand what is missing ?!
 
 file imp116.err contains (from programming languages am studing java ;)
 
 instream:1.278825 Error: overloaded variable not defined at type
   symbol: *
   type: INTEGER
 instream:1.278813 Error: overloaded variable not defined at type
   symbol: *
   type: INTEGER
 instream:1.279323 Error: overloaded variable not defined at type
   symbol: *
   type: INTEGER
 instream:1.279328 Error: overloaded variable not defined at type
   symbol: +
   type: INTEGER
 instream:1.279246 Error: overloaded variable not defined at type
   symbol: *
   type: INTEGER
 instream:1.280628 Error: overloaded variable not defined at type
   symbol: +
   type: INTEGER
 instream:1.280592 Error: overloaded variable not defined at type
   symbol: +
   type: INTEGER
 instream:1.280771 Error: overloaded variable not defined at type
   symbol: +
   type: INTEGER
 Exception+ (Exception: Error: Error) abandoning file imp116.sml at line 5682
 *** (Exception: Stop: Stop) ***
 
 
 2009/11/15 Rob Arthan r...@lemma-one.com
 
 On 14 Nov 2009, at 11:01, Igorj V wrote:
 
  trying t install OpenProofPower-2.7.8
  appears some error
 
  how to read build.log file?!
 
 It is telling you that it failed while compiling file imp116.sml. The output 
 from the compilation will be in the file src/imp116.err. Have a look at that.
 
 Regards,
 
 Rob.
 
  build.log___
  Proofpower mailing list
  Proofpower@lemma-one.com
  http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
 
 
 imp116.err
 
 
 ___
 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] ProofPower on Ubuntu 9.04

[Rob Arthan]

On Tuesday 13 Oct 2009 1:15 pm, Roger Bishop Jones wrote:
 I have tried to build ProofPower on Ubuntu 9.04,
 but it failed so I was wondering whether anyone
 else has succeeded and if they have any helpful
 hints.

 I used the lastest p2 sources, which build OK
 for me on openSUSE 10.3.

 On Ubuntu the build fails pretty quickly in
 makehelp.sh with the message:

 troff: fatal error: can't find macro file s

The nroff/groff/troff suite is missing the -ms macro library (which due to 
the bad joke that is the naming scheme for troff macros lives is referred to 
without the inital m in this error message). You probably have a minimalist 
installation of the suite that is only good for displaying the manual pages. 
So I imagine you need to install the rest of groff by doing something like:

sudo aptitudeinstall groff

or using your favourite package management GUI.

Phil Clayton found that the following aptitude command got everything that was 
needed on Ubuntu 9.04.

sudo aptitude install \
  groff \
  libmotif-dev \
  libxt-dev \
  libxp-dev \
  libxmu-dev \
  texlive-latex-base texlive-generic-recommended


 Any ideas what the problem might be?

 I have built the PolyML 5.2.1 without problems,
 but am uncertain about whether I have an adequate motif
 installation.
 Some motif client stuff has been installed from debian packages.
 Since it didn't look like it would be enough I downloaded
 the source from OpenMotif but it would not build in my
 environment (perhaps not enough X11 development stuff available).

 However, it doesn't look on the face of it as if
 the problem I am hitting has anything to do with Motif.

So far it is nothing to do with Motif. Let's see how you get on.

Regards,

Rob.


 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

[ProofPower] Forthcoming Poly/ML 5.3

[Rob Arthan]

Dear All,

Poly/ML 5.3 is likely to be released very soon. I have just posted a patch on 
the ProofPower website that fixes a performance problem you will experience 
if you compile using the latest development version of Poly/ML or with 5.3 
when it is released.

As most people have fairly fast Internet connections these days, in future, I 
will now make the web page:

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

lead to a recommended version of the ProofPower source with all the patches 
that I recommend for all users applied (so you can just download the lot 
rather than apply the patches yourself). Earlier versions of the ProofPower 
source will still be available via the link at the end of the paragraph about 
DownLoading OpenProofPower.

Regards,

Rob.



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

[ProofPower] OpenProofPower 2.8.1

[Rob Arthan]

Dear All,

I am happy to announce that OpenProofPower version 2.8.1 is now available from 
the ProofPower web site:

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

Many thanks to all who helped with the new version and particularly Phil 
Clayton of QinetiQ.

Regards,

Rob.

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

Re: [ProofPower] Clashing definitions

[Rob Arthan]

Roger,

On 9 Jun 2009, at 07:23, Roger Bishop Jones wrote:


On Monday 08 June 2009 22:59:01 Rob Arthan wrote:


The name clash should definitely cause an error. Perhaps you are
catching the error somehow?


I don't think so.

Re-instating the error, I end up in a context in which
rbjmisc is an ancestor:

:) get_ancestors -;
val it =
  [pre_func, catfun, nfu_f, cache'rbjhold, \250, dyadic,  
\175,

 analysis, equiv_rel, fincomb, cache'maths_egs, groups,
 group_egs, bin_rel, fun_rel, seq, fin_set, topology,
 rbjmisc, orders, set_thms, ordered_sets, U_orders,  
one,
 combin, sum, min, log, init, misc, pair, \238,  
list,
 char, basic_hol, sets, hol, tc, wf_relp, fixp,  
metapi]

: string list

but in which Set is not a constant:

:) get_spec ¬Set®;
Exception Fail * ¬Set® is not a constant, or a constant applied to  
some

arguments


That is only telling you that the parser doesn't think Set is the  
name of a constant (which isn't a guaranteed test of const-ness: it  
can happen even when the name is that of a constant in scope if you've  
used undeclare_alias).





The theory listing corroborates this obliquely:

:) print_theory rbjmisc;
=== The theory rbjmisc ===

--- Constants ---

CombC   ('a – 'b – 'c) – 'b – 'a – 'c
PDisj   'a SET SET – BOOL
FunImage('a – 'b) – 'a SET – 'b SET
Œmk_const(Set, ‰'a NESET – 'a SET®)®
'a NESET – 'a SET
NeSet   'a SET – 'a NESET
$Ÿ≈L'a – 'a LIST – BOOL

Set is listed as a constant, but printed as if it were not in scope.


What do map dest_const(get_conststbjmisc) and map dest_const  
(get_constsnfu_f) come up with?



Similarly, in theory nfu_f:

:) print_theory nfu_f;
=== The theory nfu_f ===
--- Constants ---

$Ÿ≈nf   SET≈nf – SET≈nf – BOOL
˚   SET≈nf
Œmk_const(Set, ‰SET≈nf – BOOL®)®
SET≈nf – BOOL
Ur  SET≈nf – BOOL

So both definitions are out of scope.

Tracing back to the point at which the clash should have happened
there is no sign of this in the log.

val FuncCatCon_def = ... : THM
val it = () : unit
val it = () : unit
val it = () : unit

The first unit is force_new_theory, the second is  
`new_parentnfu_f;'

and the clash should have been seen then.

Is this what would have happened if I had caught an exception?

No. if new_parent failed, then it shouldn't have made the theory a  
parent. All I meant was that you might have failed to make the theory  
a parent without noticing, but that doesn't seem to be the problem.


Is it possible to supply a version of your source (ideally cut down to  
a minimum) that I can have a look at?


Regards,

Rob.


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

Re: [ProofPower] Extended character support

[Rob Arthan]

On 5 Jun 2009, at 08:35, Roger Bishop Jones wrote:


I quite often find that I want to use a new character in
ProofPower HOL.

However, ProofPower seems to be quite fussy about what
characters you use.

For example, there are three spares at the moment,
which would be useful for me. They wouldn't look right
in xpp but I could get them to print nicely.


Yes - you can add entries for additional symbols in the sievekeyword  
files so that doctex understands them.




However, ProofPower rejects the use of these characters.

Also, some of the characters which are not spare and
are in the palette are rejected altogether, e.g. the
equivalence symbol (three horizontal bars).


Aside: you can customise the palette, e.g., to add in the three  
spares. Have a look at app-defaults/Xpp.




Would there be any problem in extending the set of
of characters which are accepted in HOL terms?


No. You can do it yourself:

val _ =
let open  ReaderWriterSupport.PrettyNames;
in  add_new_symbols [ ([identeq], Value \233, Simple) ]
end;

After that you can use the three-barred gate or equivalently %identeq%  
in HOL types and terms.


You can use the character from the xpp  palette instead of \233 in the  
above if you like.


Even when you run out of extended characters, you can use Nil to add  
new symbols that only have the %XXX% form.


Regards,


Rob.



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

Re: [ProofPower] Subgoal limits

[Rob Arthan]

On 18 May 2009, at 23:27, Artur Oliveira Gomes wrote:



Rob,

Can you tell me how can I increase the default subgoal limit when
stripping a goal?

In that proof I sent you an example, or me, the complete version
of the proof creates over 34 subgoals, then, ProofPower give me
a warning telling that the proof reached the limit, and asking
me if I want to continue, entering y.


set_int_control(tactic_subgoal_warning, 35);

or 40 or whatever you want. However, don't set the limit much bigger  
than the number of subgoals yo are prepared to deal with. If you set  
the limit high and a tactic produces 100s or 1000s of subgoals, the  
subgoal package could waste a lot of your time  processing those  
subgoals and you won't know that there are an intractable number of  
subgoals  until it has finished.


I think it would be better if the subgoal package just told you there  
were lots of subgoals and then carried on trying to process them  
rather than output the warning - you can always interrupt it if you  
don't want to wait. Does anyone else have any views on this?


Regards,

Rob

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

Re: [ProofPower] Instantiation of free variables according to some matching.

[Rob Arthan]

Frank,

On 7 Apr 2009, at 14:39, Frank Zeyda wrote:


Dear Roger,

Many thanks for the reply.

 The additional feature of better error handling is easily supported  
with another line of code handling possible exceptions.


The idea behind the caller parameter in many of these internal  
functions was to make the reporting of the function that was the real  
detector of the error more precise. In this case, apply_matches_rule  
isn't doing anything very subtle so you are right that the calling  
function could do it with a simple handler.


Maybe apply_matches_rule could be a nice function to have in the  
general interface, what about exposing it?


In many instances in the original development of ProofPower, there  
were instances of general purpose functions like this  that were  
nearly general enough and useful enough to productise but not quite  
(e.g., because of the effort involved in getting the error handling  
completely general or in documenting exactly what the function does,  
or even just thinking up the right name for the function). I will  
certainly consider  exposing apply_matches_rule - finding a good name  
for it seems the hardest problem just now :-)





 A second case is when y occurs free in both thm and term,
 is not substituted but nonetheless introduced through the  
substitution.

 I presume this is okay
 as long as the types of y are identical in thm and term.

 Its still OK if the types are not the same, they will be
 logically distinct variables and its a confusing situation
 you shold seek to avoid.

This sounds a little bit curious, is there a document that explains  
more about this situation?


There are at least two accounts of the semantics of HOL and they agree  
on this point as do the classical references on type theory and on  
many-sorted first-order logic. For HOL, I have in mind the account by  
Andy Pitts in the Cambridge HOL documentation and my account in HOL in  
spc00{1,2,3,4}.doc supplied with ProofPower. It isn't really curious  
if you think about it the other way round: how could the semantics  
possibly consider two variables with different types to be the same?  
In Church's simple type theory and its polymorphic variant HOL, the  
types are disjoint.


So although the variables have the same name they are actually  
treated as logical distinct by the fact that they have different  
types? So instantiation would have be sensitive to variable types  
(not just names) and might result in one variables n to be  
substitution, while another n is left unaffected e.g. if it has a  
different type?





For example, assume we have a theorem thm

n = 1 |- n = {1}

Then (asm_inst_term_rule [(2, n)] thm) would yield

2 = 1 |- n = {1}  ?




Absolutely! Instantiation works just like that (it even has to rename  
bound variables if the instantiation would cause a capture problem).  
But this is a tiny price to pay: the alternative approaches are very  
unattractive: e.g., the abstract data type of terms could ban terms  
that used the same variable name with different types but that would  
impose a big runtime overhead on the constructors for applications and  
lambda-abstraction.


Thanks for pointing this out, it clarified one or two behaviours of  
ProofPower for me which I could not explain before.


 I think the main problem you will have is in matching against terms
 containing bound variables.

I haven't given considerations to this, but as far as I can see such  
a situation may not arise in the particular application. Thanks for  
pointing this out!


Cheers once more,
Frank

PS: What about a function that supports backward-chaining with Z  
theorems, something like z_bc_tac and z_bc_thm_tac? I suppose this  
could be quite useful too. Is there anything more that needs to be  
done other than rewriting the Z universal quantifier into a HOL one,  
and using the HOL backward-chaining tactics?




Yes. I have been meaning to get round to this for a long time. It  
isn't quite as simple as you might think because the Z tactics are  
designed to keep in Z, but  the back-chaining tactics often need to  
produce an existentially quantified goal and that would need to be  
converted from HOL back into Z.


PPS: A final comment. To implement some custom error handling I  
noticed that there was no functions that could be used to infer the  
id of an error message (of type MESSAGE). Since the MESSAGE datatype  
is not exposed, we cannot take the message apart; the only solution  
seems to be to dissect the string of the error message. If I'm  
overlooking something please let me know, otherwise it would be  
beneficial to have some function get_id in the general interface of  
BasicError to extract the id of an error message ;-).


You aren't overlooking anything. I have thought that a function like  
you get_id would be useful in some circumstances. I think I will add a  
function that will just let you take the MESSAGE type apart, but with  
a warning 

Re: [ProofPower] Real Numbers - Proofs

[Rob Arthan]

Artur,

You may like to know that there is a so-called component proof context called 
'z_reals which will make evaluation of real arithmetic expressions happen 
automatically when you rewrite.


Try:


set_merge_pcs['z_reals, z_library];
set_goal([], %SZT% real 30 %mem% real 20 ..%down%R real 40 %%);
a(rewrite_tac[z_%bbR%_dot_dot_def]);

Regards,

Rob.

Artur Oliveira Gomes wrote:

Hi there

Now I know how to prove it: using z_R_=_conv.

Thanks anyway,

Artur

2009/3/25 Artur Oliveira Gomes artur.o.go...@gmail.com 
mailto:artur.o.go...@gmail.com


Hi there,

How could I prove that given two real numbers, 20 and 30, that 20 =40?
Moreover, given three real numbers, 20, 30 and 40,
how could I prove that 30 in 20..40.

Regards,

-- 
Artur Oliveira Gomes





--
Artur Oliveira Gomes




___
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] Error when installing Proofpower 2.8

[Rob Arthan]

On 27 Jan 2009, at 21:54, Artur Oliveira Gomes wrote:


Rob,

I'll try to install this release on Ubuntu.

You mentioned Mac OS X. Do you have a tutorial, anything to help me  
in order to install ProofPower on a Mac?




It is just like installing on Linux. You need to have installed the  
Darwin developer tools, also known as Xcode tools, so that you have a  
gcc-based C development environment - this is all supplied with Mac  
OS X but doesn't get installed by default. Then you can install Poly/ 
ML and Motif and then ProofPower on top.


Regards,

Rob.


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