Re: [ProofPower] Test
Received! (By both my email addresses - it seems I am doubly subscribed!) Phil On 06/11/2023 00:54, Rob Arthan wrote: This is an attempt to investigate what happened to the ProofPower mailing list and to see if I can bring it back to life. If you get this message please reply. Best regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] HOLCONST
The problem is that ⌜n + 1⌝ can't be matched with a numeric literal. It may be possible to add such a matching capability but this is easily worked around by converting the operand first. For a numeric literal, as in your example, plus1_conv can be used. With this, you can build up a conversion evaluate your summ function. I've included my steps below to build up such a conversion. Hopefully you can see what's going on at each step. Phil (* Use plus1_conv to get the operand in the right form *) plus1_conv ⌜3⌝; (* * val it = ⊢ 3 = 2 + 1: THM *) (* Convert the argument if non-zero then rewrite *) (RAND_C (TRY_C plus1_conv) THEN_C pure_once_rewrite_conv [get_spec ⌜summ⌝]) ⌜summ 0⌝; (RAND_C (TRY_C plus1_conv) THEN_C pure_once_rewrite_conv [get_spec ⌜summ⌝]) ⌜summ 3⌝; (* * val it = ⊢ summ 0 = 0: THM * val it = ⊢ summ 3 = summ 2 + 2 + 1: THM *) (* Give this conversion a name and define a conversion that * recursively applies it to the left operand of the resulting * '+' term until is fails *) val summ_step_conv = RAND_C (TRY_C plus1_conv) THEN_C pure_once_rewrite_conv [get_spec ⌜summ⌝]; fun summ_conv t = (summ_step_conv THEN_TRY_C LEFT_C summ_conv) t; summ_conv ⌜summ 0⌝; summ_conv ⌜summ 3⌝; (* * val it = ⊢ summ 0 = 0: THM * val it = ⊢ summ 3 = ((0 + 0 + 1) + 1 + 1) + 2 + 1: THM *) (* Add up the resulting '+' tree *) (summ_conv THEN_C MAP_C plus_conv) ⌜summ 3⌝; (* * val it = ⊢ summ 3 = 6: THM *) (* We want summ_conv to reduce the '+' terms so sum as we go. * Redefine the above. *) val summ_step_conv = RAND_C (TRY_C plus1_conv) THEN_C pure_once_rewrite_conv [get_spec ⌜summ⌝] THEN_C TRY_C (RIGHT_C plus_conv); summ_step_conv ⌜summ 0⌝; summ_step_conv ⌜summ 3⌝; (* * val it = ⊢ summ 0 = 0: THM * val it = ⊢ summ 3 = summ 2 + 3: THM *) fun summ_conv t = (summ_step_conv THEN_TRY_C (LEFT_C summ_conv THEN_C plus_conv)) t; summ_conv ⌜summ 0⌝; summ_conv ⌜summ 3⌝; (* * val it = ⊢ summ 0 = 0: THM * val it = ⊢ summ 3 = 6: THM *) map summ_conv (map (fn n => mk_app (⌜summ⌝, mk_ℕ (integer_of_int n))) (interval 0 50)); (* * val it = *[⊢ summ 0 = 0, ⊢ summ 1 = 1, ⊢ summ 2 = 3, ⊢ summ 3 = 6, * ⊢ summ 4 = 10, ⊢ summ 5 = 15, ⊢ summ 6 = 21, ⊢ summ 7 = 28, * ⊢ summ 8 = 36, ⊢ summ 9 = 45, ⊢ summ 10 = 55, * ⊢ summ 11 = 66, ⊢ summ 12 = 78, ⊢ summ 13 = 91, * ⊢ summ 14 = 105, ⊢ summ 15 = 120, ⊢ summ 16 = 136, * ⊢ summ 17 = 153, ⊢ summ 18 = 171, ⊢ summ 19 = 190, * ⊢ summ 20 = 210, ⊢ summ 21 = 231, ⊢ summ 22 = 253, * ⊢ summ 23 = 276, ⊢ summ 24 = 300, ⊢ summ 25 = 325, * ⊢ summ 26 = 351, ⊢ summ 27 = 378, ⊢ summ 28 = 406, * ⊢ summ 29 = 435, ⊢ summ 30 = 465, ⊢ summ 31 = 496, * ⊢ summ 32 = 528, ⊢ summ 33 = 561, ⊢ summ 34 = 595, * ⊢ summ 35 = 630, ⊢ summ 36 = 666, ⊢ summ 37 = 703, * ⊢ summ 38 = 741, ⊢ summ 39 = 780, ⊢ summ 40 = 820, * ⊢ summ 41 = 861, ⊢ summ 42 = 903, ⊢ summ 43 = 946, * ⊢ summ 44 = 990, ⊢ summ 45 = 1035, ⊢ summ 46 = 1081, * ⊢ summ 47 = 1128, ⊢ summ 48 = 1176, ⊢ summ 49 = 1225, * ⊢ summ 50 = 1275]: THM list *) On 31/03/20 17:09, David Topham wrote: I have been able to get the length sample for HOLCONST from user013 to work, but when I try my own function, I get an error. Can anyone see what my problem is? I suspect it may be setting the correct proof context since I needed to add set_pc "hol2" to get the length function to work. I have tried several contexts such as "lin_arith", "R", "misc", but I have not seen how to find the correct one (if that is even the problem). This one OK: :) force_delete_theory "cs113" handle Fail _ => (); val it = (): unit :) open_theory "hol"; new_theory "cs113"; val it = (): unit val it = (): unit :) set_pc "hol2"; val it = (): unit :) ⓈHOLCONST :# │ length:'a LIST→ℕ :# ├── :# │ length [] = 0 :# │ ∧ ∀ h t⦁ length (Cons h t) = length t + 1 :# │ :# ■ val it = ⊢ length [] = 0 ∧ (∀ h t⦁ length (Cons h t) = length t + 1): THM :) get_spec⌜length⌝; val it = ⊢ length [] = 0 ∧ (∀ h t⦁ length (Cons h t) = length t + 1): THM :) rewrite_conv[get_spec⌜length⌝] ⌜length [1;2;3;4]⌝; val it = ⊢ length [1; 2; 3; 4] = 4: THM But not this one: :) ⓈHOLCONST :# │ summ:ℕ→ℕ :# ├── :# │ summ 0 = 0 :# │ ∧ ∀n⦁ summ (n + 1) = (summ n) + (n + 1) :# │ :# ■ val it = ⊢ summ 0 = 0 ∧ (∀ n⦁ summ (n + 1) = summ n + n + 1): THM :# get_spec⌜summ⌝; val it = ⊢ summ 0 = 0 ∧ (∀ n⦁ summ (n + 1) = summ n + n + 1): THM :) rewrite_conv[get_spec⌜summ⌝] ⌜summ 2⌝; Exception Fail * no rewriting occurred [rewrite_conv.26001] * raised ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] PP 3.1w7 installation problems with Fedora 24
(I replied from the wrong email address which silently fails, trying again...) Forwarded Message Subject: Re: [ProofPower] PP 3.1w7 installation problems with Fedora 24 Date: Thu, 15 Jun 2017 16:31:29 +0100 From: Phil Clayton <phil.clay...@lineone.net> To: proofpower@lemma-one.com Hi Mark, On 15/06/17 10:29, Mark Adams wrote: Hi Phil, On 15/06/2017 10:24, Phil Clayton wrote: ... Can you try the following to make sure you have the required packages installed: dnf install \ gcc-c++ \ texlive-latex texlive-epsf \ ed \ motif motif-devel \ libXp-devel.x86_64 \ libXext-devel.x86_64 \ libXmu-devel.x86_64 \ libXt-devel.x86_64 \ xorg-x11-fonts-misc and see how it goes with 3.1w7. It all works now. I was missing texlive-epsf. I wonder whether/where it is documented anywhere that this is needed.. I think the system requirements just say that TeX/LaTeX is required and suggest Tex-Live or teTeX installations. The issue here is that TeX-Live is provided by several Fedora packages, presumably because it is so large, that are not all installed by default. If every Tex-Live package was installed, this wouldn't be an issue. There should have been an error message saying "can't find espf.sty" or similar in the log file for dtd017. Incidentally, if I try building ProofPower 3.1w6 with Poly/ML 5.6, I get further still in processing dev.mkf, but it fails this time with: Compiling (code) imp002.sml dev.mkf:349: recipe for target 'imp002.ldd' failed make: *** [imp002.ldd] Error 1 I don't know why 3.1w6 doesn't build with Poly/ML 5.6. What does the log file for imp002 say? Which log file? The one with the output from processing imp002.doc, which will probably be called imp002.ldd (as this is the target mentioned in the Make error above) but could be called imp002.err. It should be the last modified file in the list given by ls -ltr src/*/* | tail Phil Cheers, Mark. On 15/06/2017 02:27, Phil Clayton wrote: Hi Mark, You probably need to do yum install openmotif-devel to ensure that the Motif C header files are also installed. ProofPower 3.1w7 doesn't build with Poly/ML 5.7 due to a change in the integer types described here: http://lemma-one.com/pipermail/proofpower_lemma-one.com/2017-May/001178.html You would need to apply the patch in that message. Poly/ML 5.6 should work though. Poly/ML 5.5 is quite old and doesn't have polyc so I can't see how ProofPower 3.1w7 can build with that version, even though the website say that it does. There are also versions 5.5.1 and 5.5.2 which do provide polyc. Poly/ML release dates are as follows: 5.7 2017-05-12 5.6 2016-01-25 5.5.2 2014-05-13 5.5.1 2013-11-18 5.5 2012-09-14 See https://sourceforge.net/projects/polyml/files/polyml/ Phil On 15/06/17 00:39, Mark Adams wrote: Hi, I'm getting problems installing ProofPower 3.1w7 on Fedora 24 with Poly/ML 5.7. The first thing that looks wrong is that, even though I have OpenMotif installed, running ./configure complains that it can't find it. yum install openmotif ... Package motif-2.3.4-11.fc24.x86_64 is already installed, skipping. Dependencies resolved. Nothing to do. Complete! ./distclean PPHOME=`pwd` PPPOLYHOME=/usr/programs/polyml/polyml-5.7 ./configure Using /usr/programs/pp/pp-3.1w7 as the installation target directory Using Poly/ML from /usr/programs/polyml/polyml-5.7 Using dynamic linking for Motif WARNING: Motif installation not found Using 50 for the size of the labelled product cache Generating code to install the following packages: pptex dev xpp hol zed daz If you are happy with these settings, now run ./install to install ProofPower. But ./install seems to fail for another reason: ./install OpenProofPower installation begins [Wed Jun 14 21:41:19 2017] ... Moving to build directory /usr/programs/pp/pp-3.1w7/src Building pptex dev xpp hol zed daz See /usr/programs/pp/pp-3.1w7/build.log for messages install: installation failed; see /usr/programs/pp/pp-3.1w7/build.log for more details Last few lines of build.log: echo "use\"polyml-build.sml\";" | poly > slrp-bin.log 2>&1 polyc -o slrp-bin slrp-bin.o Error: slrp-bin.o: No such file Usage: polyc [OPTION]... [SOURCEFILE] dev.mkf:174: recipe for target 'slrp-bin' failed make: *** [slrp-bin] Error 1 I get the same problem if I use Poly/ML 5.5. Regards, Mark. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] PP 3.1w7 installation problems with Fedora 24
Hi Mark, On 15/06/17 07:05, Mark Adams wrote: Thanks very much for that Phil. This definitely helps but I still get failure for Poly/ML 5.6.. Installing openmotif-devel clears up the Motif problem. Regarding Poly/ML, yes when I look closer, the failure recorded in build.log is indeed different for Poly/ML 5.5: echo "use\"polyml-build.sml\";" | poly > slrp-bin.log 2>&1 polyc -o slrp-bin slrp-bin.o make: polyc: Command not found dev.mkf:174: recipe for target 'slrp-bin' failed make: *** [slrp-bin] Error 127 So for 5.5 it's Error 127, but for 5.7 it's Error 1. So Poly/ML 5.5 fails as expected: polyc not found. That error code is probably from the shell. For Poly/ML 5.7, polyc can't find the file slrp-bin.o specified as a argument. That error code is probably from polyc. There error codes aren't particularly useful. There is usually an error message in the log file for the failing source file that gives more details about what went wrong. This is usually the last file written, which you can find with ls -ltr src/*/* | tail Anyway, Poly/ML 5.6 gets further in processing dev.mkf but still fails, this time with: doctex dtd017.doc texdvi -b dtd017 > dtd017.dvi.ldd1 I haven't yet applied the patch for ProofPower 3.1.w7 (which shouldn't be necessary because I'm using Poly/ML 5.6). Correct, Poly/ML 5.6 should work fine. It looks like 5.6 is failing whilst building the documentation. Can you try the following to make sure you have the required packages installed: dnf install \ gcc-c++ \ texlive-latex texlive-epsf \ ed \ motif motif-devel \ libXp-devel.x86_64 \ libXext-devel.x86_64 \ libXmu-devel.x86_64 \ libXt-devel.x86_64 \ xorg-x11-fonts-misc and see how it goes with 3.1w7. Incidentally, if I try building ProofPower 3.1w6 with Poly/ML 5.6, I get further still in processing dev.mkf, but it fails this time with: Compiling (code) imp002.sml dev.mkf:349: recipe for target 'imp002.ldd' failed make: *** [imp002.ldd] Error 1 I don't know why 3.1w6 doesn't build with Poly/ML 5.6. What does the log file for imp002 say? Phil Cheers, Mark. On 15/06/2017 02:27, Phil Clayton wrote: Hi Mark, You probably need to do yum install openmotif-devel to ensure that the Motif C header files are also installed. ProofPower 3.1w7 doesn't build with Poly/ML 5.7 due to a change in the integer types described here: http://lemma-one.com/pipermail/proofpower_lemma-one.com/2017-May/001178.html You would need to apply the patch in that message. Poly/ML 5.6 should work though. Poly/ML 5.5 is quite old and doesn't have polyc so I can't see how ProofPower 3.1w7 can build with that version, even though the website say that it does. There are also versions 5.5.1 and 5.5.2 which do provide polyc. Poly/ML release dates are as follows: 5.7 2017-05-12 5.6 2016-01-25 5.5.2 2014-05-13 5.5.1 2013-11-18 5.5 2012-09-14 See https://sourceforge.net/projects/polyml/files/polyml/ Phil On 15/06/17 00:39, Mark Adams wrote: Hi, I'm getting problems installing ProofPower 3.1w7 on Fedora 24 with Poly/ML 5.7. The first thing that looks wrong is that, even though I have OpenMotif installed, running ./configure complains that it can't find it. yum install openmotif ... Package motif-2.3.4-11.fc24.x86_64 is already installed, skipping. Dependencies resolved. Nothing to do. Complete! ./distclean PPHOME=`pwd` PPPOLYHOME=/usr/programs/polyml/polyml-5.7 ./configure Using /usr/programs/pp/pp-3.1w7 as the installation target directory Using Poly/ML from /usr/programs/polyml/polyml-5.7 Using dynamic linking for Motif WARNING: Motif installation not found Using 50 for the size of the labelled product cache Generating code to install the following packages: pptex dev xpp hol zed daz If you are happy with these settings, now run ./install to install ProofPower. But ./install seems to fail for another reason: ./install OpenProofPower installation begins [Wed Jun 14 21:41:19 2017] ... Moving to build directory /usr/programs/pp/pp-3.1w7/src Building pptex dev xpp hol zed daz See /usr/programs/pp/pp-3.1w7/build.log for messages install: installation failed; see /usr/programs/pp/pp-3.1w7/build.log for more details Last few lines of build.log: echo "use\"polyml-build.sml\";" | poly > slrp-bin.log 2>&1 polyc -o slrp-bin slrp-bin.o Error: slrp-bin.o: No such file Usage: polyc [OPTION]... [SOURCEFILE] dev.mkf:174: recipe for target 'slrp-bin' failed make: *** [slrp-bin] Error 1 I get the same problem if I use Poly/ML 5.5. Regards, Mark. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com
Re: [ProofPower] Setting up on macosx Sierra fails...
I have successfully built ProofPower with SML/NJ 110.81 which was recently released. (That was on Fedora but any SML type errors should be the same on different platforms.) I haven't tried earlier versions. In the ProofPower source directory, did you run ./distclean before rebuilding? Phil On 13/05/17 04:44, Hugh Anderson wrote: Hi - I just tried using SMLNJ instead of polyML, but I got the same error at the same place... Cheers Hugh On Sat, 13 May 2017, Hugh Anderson wrote: Hi - I am trying to install ProofPower-Z using my new mac/Sierra machine, using polyml, installed from brew: Poly/ML 5.7 Release RTS version: X86_64-5.6 ... Hugh Anderson E-mail: h...@comp.nus.edu.sg SoC, National University of Singapore http://www.comp.nus.edu.sg/~hugh ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] z_app_thm
In z_app_thm, which states ∀ a : 핌; f : 핌; x : 핌 ⦁ (∀ f_a : 핌 | (a, f_a) ∈ f ⦁ f_a = x) ∧ (a, x) ∈ f ⇒ f a = x I notice that the antecedent (a, x) ∈ f does not actually need to map a to x because that is already captured in the first antecedent. It only needs to say that a is in the domain of f, so the theorem could state ∀ a : 핌; f : 핌; x, y : 핌 ⦁ (∀ f_a : 핌 | (a, f_a) ∈ f ⦁ f_a = x) ∧ (a, y) ∈ f ⇒ f a = x As it stands, I suspect there could be some unnecessary proof overhead for users (and perhaps in the PP implementation) because it may be necessary to forward chain with the left antecedent, once established, and eliminate a variable to get the form required by z_app_thm. I think other proof operations like z_app_eq_tac and z_app_λ_rule would naturally become simpler: - z_app_eq_tac could return a goal containing ... ∧ (∃ v : 핌 ⦁ (a, v) ∈ f) so we can choose any v, instead of ... ∧ (a, v) ∈ f - z_app_λ_rule would not include the predicate V' = x in the antecedents. Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] error msg when instantiating quantifier in asm
Hi Yuhui, I asked a similar question some years ago here: http://lemma-one.com/pipermail/proofpower_lemma-one.com/2004-September/000235.html See the replies for an explanation of the issue, in particular Roger's emails. In your case, you need to specialize the theorem z_id_%bij%_thm before adding/stripping into the assumtions, e.g. a (strip_asm_tac (z_%forall%_elim %SZT% y %% z_id_%bij%_thm)); Phil 28/05/15 17:18, YuHui Lin wrote: Dear all, I get the following error when I tried to instantiated a forall quantifier in an assumption which I inserted using asm_tac. Exception Fail * Trying to instantiate type variable 'a, which occurs in assumption list [z_∀_elim.6006] * raised The following dummy example can replay this error set_goal ([], %SZT% %forall% x : %int%; y : %pset% %int% %=% x %mem% y %or% x %notmem% y %%); a (strip_tac);a (strip_tac);a (strip_tac); a (asm_tac z_id_%bij%_thm); a (z_spec_nth_asm_tac 1 %SZT% y %%); What does this error mean ? Where did I do wrong here ? Thanks in advance. best, Yuhui - We invite research leaders and ambitious early career researchers to join us in leading and driving research in key inter-disciplinary themes. Please see www.hw.ac.uk/researchleaders for further information and how to apply. Heriot-Watt University is a Scottish charity registered under charity number SC000278. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] OpenProofPower 3.1w5
Rob, I have build 3.1w5 and am seeing Z characters in the terminal which is great! I find that I need to set LD_LIBRARY_PATH for the Poly/ML libraries when running. I suspect that this is because the polyc command in HOLSTARTCMD in hol.mkf does does not include LD_RUN_PATH=$(LD_RUN_PATH) (Similarly for SLRPSTARTCMD in dev.mkf) Is there any reason for that? Regards, Phil On 18/04/15 14:08, Rob Arthan wrote: Dear All, I am happy to announce that OpenProofPower version 3.1w5 is now available. You can read about it and download it from: http://www.lemma-one.com/ProofPower/getting/getting.html The main change since version 3.1w4 is support for Unicode and UTF-8. Setting the flag output_in_utf8 true in a ProofPower session, causes output to use UTF-8 rather than the ProofPower extended character set. Likewise setting the input_in_utf8 true makes the session expect subsequent input to be UTF-8 encodings. The UTF-8 support is currently mainly targeted at people who are programming their own GUIs and need to interface to GUI toolkits using UTF-8. The document preparation system and xpp do not yet support UTF-8. Note that this version does not work with Standard ML of New Jersey, due to a bug in that compiler’s handling of hexadecimal character constants. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Unicode and ProofPower
Rob, 28/03/15 16:03, Rob Arthan wrote: On 27 Mar 2015, at 14:41, Phil Clayton phil.clay...@lineone.net mailto:phil.clay...@lineone.net wrote: You currently have 208D SUBSCRIPT LEFT PARENTHESIS for %ulbegin% 208E SUBSCRIPT RIGHT PARENTHESISfor %ulend% but these parentheses don't have underscores like the ProofPower glyphs. One option is 298B LEFT SQUARE BRACKET WITH UNDERBAR 298C RIGHT SQUARE BRACKET WITH UNDERBAR They appear as ⦋ (298B) and ⦌ (298C) but I think they're too close to refinement symbols. I think this could be a case where you probably want to combine another glyph with the existing parenthesis using the combining diacritics. I think the best options are 0331 COMBINING MACRON BELOW which gives ̱( ̱) These work in my email client and terminal. Alternatively 0332 COMBINING LOW LINE which gives (̲ )̲ These don't overlay correctly in my email client or terminal but are a single wide character. I am chary about using the COMBINING characters as it seems likely to increase the chances that any given text-processing system will go wrong in some way. The use of underlined brackets in the ProofPower font was a bit of an arbitrary choice. So I have changed to the following which look like the beginning and end of underlining. 2A3D RIGHTHAND INTERIOR PRODUCT: ⨽ 2A3C INTERIOR PRODUCT: ⨼ I agree that it could be too soon to depend on combining characters. The less common ones aren't quite working on my 3-4 year old Linux installation. These new characters don't sit quite as low as one would like, to emphasize underlining, but I can't suggest anything better without combining characters. For epsilon, I can see why 03F5 GREEK LUNATE EPSILON SYMBOL has been used instead of 03B5 GREEK SMALL LETTER EPSILON - it is the correct shape for the equivalent LaTeX character. I don’t know why we used \varepsilon in LaTeX rather than \epsilon for this. (I think there is slight tendency to use the lunate epsilon for the Hilbert choice operator in the literature, but the ordinary is often used too and seems to be more common these days, and in Z you expect it just to be the ordinary greek letter.) l I was finding that the lunate epsilon is very similar to the membership operator. The lower case LaTeX mathematical greek letters appear italicized so I wonder whether the standard should have used e.g. 휃 (1D703) instead of θ (03B8) 휆 (1D706) instead of λ (03BB) 휇 (1D707) instead of μ (03BC) so you would have chosen 휖 (1D716) instead of ϵ (03F5) That would have meant also that any Greek authors of Z don't find themselves deprived of certain letters. As things stand, I agree with your choice. I think it is an excellent idea to use the mathematical greek letters. I have done that, fixing a mistake with 휓 in passing and treating epsilon the same as all the others now. I wasn't sure about the uppercase greek letters because the LaTeX counterparts are not italicized. On reflection, I agree with your decision. My main concern was that the following letters, now in italics, would look wrong for n-ary product and sum: 훱 (1D6F1) 훴 (1D6F4) Of course, such operators should actually use the dedicated characters as follows: ∏ (220F N-ARY PRODUCT) ∑ (2211 N-ARY SUMMATION) There are some multi-character operators that could be translated to a single character operator that would result in Unicode documents more in line with ISO Z. \%down%s--- ⧹ (29F9) for schema hiding %filter%%down%s --- ⨡ (2A21) for schema projection %rcomp%%down%s --- ⨟ (2A1F) for schema composition This would require ProofPower-Z to be updated to add the new symbols. I mention it now because the transition to Unicode could be used as an opportunity to eliminate the non-ISO forms from Unicode documents, if you wished to transition to the ISO symbol. Either way, you probably want to add schema projection and composition to the ML function utf8_to_pp_replacement_data. I don’t think you had updated your clone of the pputf8 contrib. utf8_to_pp_replacement_data was a half-hearted attempt to introduce a bit more compatibility with ISO Z that I decided to abandon. A proper translation between ProofPower-Z and ISO Z needs to be on parse trees rather than on streams of lexical tokens. Yes, sorry, I hadn't updated my clone. I notice in pp-contrib/src/pputf8 you have files a.txt t.tgz Did you mean to commit those? I agree that it would be good to start accepting keywords with single-character Unicode equivalents for the Z operators as variant syntax for the forms with subscripts. There is also schema piping. I assume that the existing operator '' can be dropped in favour of ⨠ (2A20 Z NOTATION SCHEMA PIPING) because, with only parser support existing, nobody would be using it to date. The following are not well supported on my system: 01F13C SQUARED LATIN CAPITAL LETTER Mfor %SML% 01F143 SQUARED LATIN CAPITAL LETTER Tfor %:% 01F149 SQUARED LATIN CAPITAL LETTER Zfor %SZT% What do
Re: [ProofPower] Unicode and ProofPower
Rob, 12/03/15 12:31, Rob Arthan wrote: I am currently working on support for input and output using Unicode into ProofPower. I would appreciate any feedback on the translation scheme I am proposing to use, which is described here: http://www.lemma-one.com/ProofPower/unicode/pp-unicode.html I doubt %xNN% occurs in any existing scripts, so I think that's fine. Your Unicode values for %lseq% and %rseq% have not taken into account the correction to the Z Standard in Technical Corrigendum 1: Page 24, in 6.4.6.5 In line 3, replace “ 3008 LEFT ANGLE BRACKET” by “ 27E8 MATHEMATICAL LEFT ANGLE BRACKET”. In line 4, replace “ 3009 RIGHT ANGLE BRACKET” by “ 27E9 MATHEMATICAL RIGHT ANGLE BRACKET”. So - 3008 should be 27E8 - 3009 should be 27E9 You currently have 2588 FULL BLOCK for %EFT%. This renders quite large. I'm guessing that the description 'full block' means that the intention is for the glyph to be entirely black. This is larger that the square we're used to and it may not even be square. I think 25A0 BLACK SQUARE could be more suitable (and would be square!) To compare in your email client: █ (2588) and ■ (25A0) What do you think? You currently have 208D SUBSCRIPT LEFT PARENTHESIS for %ulbegin% 208E SUBSCRIPT RIGHT PARENTHESISfor %ulend% but these parentheses don't have underscores like the ProofPower glyphs. One option is 298B LEFT SQUARE BRACKET WITH UNDERBAR 298C RIGHT SQUARE BRACKET WITH UNDERBAR They appear as ⦋ (298B) and ⦌ (298C) but I think they're too close to refinement symbols. I think this could be a case where you probably want to combine another glyph with the existing parenthesis using the combining diacritics. I think the best options are 0331 COMBINING MACRON BELOW which gives ̱( ̱) These work in my email client and terminal. Alternatively 0332 COMBINING LOW LINE which gives (̲ )̲ These don't overlay correctly in my email client or terminal but are a single wide character. For epsilon, I can see why 03F5 GREEK LUNATE EPSILON SYMBOL has been used instead of 03B5 GREEK SMALL LETTER EPSILON - it is the correct shape for the equivalent LaTeX character. I was finding that the lunate epsilon is very similar to the membership operator. The lower case LaTeX mathematical greek letters appear italicized so I wonder whether the standard should have used e.g. 휃 (1D703) instead of θ (03B8) 휆 (1D706) instead of λ (03BB) 휇 (1D707) instead of μ (03BC) so you would have chosen 휖 (1D716) instead of ϵ (03F5) That would have meant also that any Greek authors of Z don't find themselves deprived of certain letters. As things stand, I agree with your choice. There are some multi-character operators that could be translated to a single character operator that would result in Unicode documents more in line with ISO Z. \%down%s--- ⧹ (29F9) for schema hiding %filter%%down%s --- ⨡ (2A21) for schema projection %rcomp%%down%s --- ⨟ (2A1F) for schema composition This would require ProofPower-Z to be updated to add the new symbols. I mention it now because the transition to Unicode could be used as an opportunity to eliminate the non-ISO forms from Unicode documents, if you wished to transition to the ISO symbol. Either way, you probably want to add schema projection and composition to the ML function utf8_to_pp_replacement_data. The situation with hyphen minus is unfortunate. I presume the issue is that you can't identify which instances of ASCII hyphen-minus are Z subtraction operators. The following are not well supported on my system: 01F13C SQUARED LATIN CAPITAL LETTER Mfor %SML% 01F143 SQUARED LATIN CAPITAL LETTER Tfor %:% 01F149 SQUARED LATIN CAPITAL LETTER Zfor %SZT% What do you consider converting them to the expanded form, e.g. %SZT% --- ⌜↘Z↕ ? I think a single character is preferable and ideally it would be somehow based on the opening corner '⌜'. I wonder if there is a combining trick possible here. I am particularly interested to know how good the coverage for the Unicode characters needed is on different systems and on different applications. You can see how good your web browser is just by looking at the above Web page, which includes GIFs that show how LaTeX renders the ProofPower symbols alongside the Unicode translation as rendered by your browser. To see how good your mail client is, the following should look something like the HOL definition of distributed union: ⌜∀ x a⦁ x ∈ ⋃ a ⇔ (∃ s⦁ x ∈ s ∧ s ∈ a)⌝ This is readable on my system - all glyphs are available. The sizes are a little odd but that could be due to font substitution. (There is a complete list of the symbols used at the end of this e-mail.) Current indications are that Mac OS can do everything that is required, but that recent Linux systems and MS Windows tend to miss one or two glyphs: the squared upper case letters I am using for some of the quotation symbols seem to be poorly supported, for example.
Re: [ProofPower] templates activation problem
On 15/01/13 21:39, Roger Bishop Jones wrote: On Tuesday 15 Jan 2013 09:27:06 Roger Bishop Jones wrote: On Tuesday 15 Jan 2013 07:43:30 Phil Clayton wrote: When you select Tools-Templates, do you see the templates dialog box (with very small buttons) or does nothing happen? (The first is a known issue that is easily worked around.) I havn't used the templates for a long time, but I see now that I don't have them either (in 2.9.1w5). I have unhashed the template include line in Xpp but the Tools menu in Xpp still has Templates greyed out. On further investigation I do get the templates if I use an Xpp file in which the include for the templates is omitted (hashed), but if I use an include even with a full pathname it doesn't seem to pick up the template file. This applies also to the XppKeyboard file as well, I can't get the include to work, but if the include is omitted the behaviour corresponds to the issued XppKeyboard file (so far as I can see). In an X/Motif resource file, I believe '!' starts a comment and include is a macro so must have a '#' before it, as in the Xpp file distributed with ProofPower. Roger - do you still get the issue with #include ? To find out what is disabling the Templates menu item, it is worth trying PPENVDEBUG=1 xpp and checking that the paths reported in the terminal look sensible. In particular, what is given for XUSERFILESEARCHPATH ? Also, if %N is replaced by XppTemplates does any element of the path refer to a file on the file system? Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] templates activation problem
Hi Sarah, When you select Tools-Templates, do you see the templates dialog box (with very small buttons) or does nothing happen? (The first is a known issue that is easily worked around.) Phil On 15/01/13 05:33, khan khan wrote: Hi i have a problem in activating templates in the tools menu PPXpp-2.9.1w2 that i have installed it...the templates in the tools menu is not active...could you please tell me that how to activate it...how to customize xpp resource file (application defaults file) ??? The example resource file uses #include directives to include two files XppKeyboard and XppTemplates in my case it is XppZTemplates which define the keyboard layoiut and the behaviour of the Templates Tool. XppKeyboard and XppTemplates are set up as symbolic links to other resource files in the same directory. now the problem is that i do not understand that how to include XppKeyboard and XppZTemplates in the resource file for xpp so that the templates get activated??? Thank you Regards Sarah ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Initialisation convention
On 22/09/12 10:45, Roger Bishop Jones wrote: I see that Potter Sinclair and Till An Introduction to Formal Specification Using Z 1991 use the primed version of the convention, and offer the following rationale (p43): Here we use Vocab' as the variable to suggest that initialisation is like an operation which produces after objects which are acceptable as starting values for the persistent objects of the system. Admittedly in this very simple case this seems a complicated way of saying that the system must start with an empty vocabulary. (but note that they did not actually use an operation, the initial state is defined as a bare after-state). Possibly the priming of initial state began here. By making initialization an operation without a before state, the initialization can be used with schema operators such as composition and pre, e.g. Init ⨟ Op pre Init the latter being another way to write the following: ∃ Init ∙ true ∃ State' ∙ Init Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Trying to Prove my Zed Specifications
Jon,
On 20/09/12 17:59, Jon Lockhart wrote:
So based on what you have
said does that mean then that pushed = {} should be changed to pushed' =
{} since it would be a consequence of the Init operation running at
start up?
I had a quick read yesterday but no time to reply. My initial reaction
was you meant pushed' = {}.
However, for initialization, you don't have an initial state, so your
schema should just have
State'
where you currently have
Δ State
I strongly recommend reading chapter 12 of Using Z, available at
http://www.usingz.com/
If this change is necessary, and of course I will apply it to the other
two init operations, would the pre operator then be more useful in being
applied to this operation?
pre Init is certainly worth establishing: it is useful to know whether
the Init operation can be achieved. Note that with the above change to
use State', pre Init is either true or false as there are no unprimed
variables. You want to know that it is not false. As there is no
initial state, pre Init may be written
∃ State' ∙ Init
However, I see you're calculating
pre Button_State
pre Elevator_State
pre Floor_State
which is pointless. These schemas are not operations: they have no
concept of before state and after state. You'll see that none have
primed variables. Not surprisingly, you're finding
pre X_State = X_State
I also recommend chapter 14 of Using Z. The whole book is worth a read,
in fact!
Phil
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Trying to Prove my Zed Specifications
On 14/09/12 15:50, Rob Arthan wrote: When you set up the consistency goal for a Z axiomatic description, what you see is a mixture of HOL and Z and the existential quantifier is an HOL quantifier not a Z one. So you would need to use %exists%_tac rather than z_%exists%_tac. If the axiomatic description defines several global variables, the witness you need would be provided as a HOL tuple. As the witnesses for the individual variables are likely to be Z terms, you are already into some not entirely trivial mixed language working. I just tried a Z axiomatic description declaring three integers x, y, and z with defining property x y z 0. Here is the tactic that proves the consistency: a(%exists%_tac %%(%SZT%3%%, %SZT%2%%, %SZT%1%%)%% THEN PC_T1 z_library rewrite_tac[z'decl_def, z'dec_def]); This has really confused me! I get a Z existential quantifier for the initial goal. Even when there are generic parameters, I still get a Z existential quantifier, it's just that the witness must be a HOL function. Are you sure you used z_push_consistency goal rather than push_consistency_goal? Perhaps there is a ProofPower issue on some platforms or am I just missing something? A while ago, I had an issue with z_push_consistency_goal where it failed to produce the expected Z statement - I can't remember exactly what went wrong. This issue was that the initial proof step it performs was sensitive to the environment - the proof context, I think. However, I can't reproduce the issue. Phil Even when you translate that back into the extended character set (e.g., by pasting the bit between %% and %% into ProofPower), it is not very nice. So on the whole I don't think doing consistency proofs is not a good place to start learning proof in Z, because it will expose too much HOL to you. If you have a strong interest in doing consistency proofs later on, it would actually be quite easy to provide some tools to protect you from the HOL. Finally, there isn't a list flavour of %exists%_tac or z_%exists%_tac. It would be a minor convenience in HOL (where existentials with a list of bound variables are obtained by iterating existential quantifier over a single variable), but MAP_EVERY %exists%_tac does what you want. It is rarely what you want in Z, where you use a binding display as the witness for an existential quantifier that binds several variables and where iterated existential quantification is fairly rare. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Trying to Prove my Zed Specifications
On 14/09/12 18:48, Roger Bishop Jones wrote: (I attach a revised version of your document with the proof fixed). In order for z_get_spec to drop the consistency hypothesis, it is necessary to use save_consistency_thm on the resulting theorem. So after the proof you need a line like: save_consistency_thm %SZT%masterStop%% (pop_thm ()); I tend to write such proofs with the following form, for some global variable C: save_consistency_thm %SZT%C%% ( z_push_consistency_thm %SZT%C%%; (* proof steps here *) pop_thm () ); Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Best platform for ProofPower?
On 12/09/12 21:05, Roger Bishop Jones wrote: I'm having bad luck lately getting suitable environments for running ProofPower. My laptop is on Ubuntu 10.4, and that is fine for ProofPower, but is now so out of date that I can't upgrade it, I would have to install a more recent version of Ubuntu from scratch. So I revived an old server to try out a more up-to-date context for running ProofPower. (my efforts in the amazon cloud ran into the buffers some time ago). So far I'm not having much success on Ubuntu 12.04 (the PolyML build doesn't seem to work for me). What error message do you get? I ask because David Matthews is about to release 5.5 so it would be worth resolving any issue there. I'm interested to know what people are actually running ProofPower on these days? I'm using Fedora 16. Generally I've had no issue installing on the Fedora series of Linux provided that all the prerequisite packages are installed - achieved with the following yum/rpm commands: yum install \ gcc-c++ \ polyml \ texlive-latex \ libXp-devel \ libXext-devel \ libXmu-devel \ libXt-devel \ xorg-x11-fonts-misc rpm -ivh \ http://motif.ics.com/sites/default/files/openmotif-2.3.3-1.fc12.x86_64.rpm \ http://motif.ics.com/sites/default/files/openmotif-devel-2.3.3-1.fc12.x86_64.rpm The key bindings 'just work' with AltGr and Left Window as the modifiers. However, many new distributions use Gnome 3 which causes screen redraw problems for Xpp (and Motif applications generally). One simple work-around for Gnome 3 is to run in 'fallback mode' which avoids hardware acceleration. That's what I do. (There appear to be various discussions out there about this issue so it may be resolved now.) Phil P.S. Also, I have an issue when using X in Depth30 mode, i.e. 10 bits per colour. Unless Xpp is run as root, it fails to start. Probably not an Xpp-specific issue. I haven't bothered reporting that yet. For now I just use Depth24, which is what most people without fancy displays are using. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Trying to Prove my Zed Specifications
On 13/09/12 23:48, Jon Lockhart wrote: I see now, I did not know that. You can lump them together in the Word document when I am using those tools but that is b/c when it is parsed each is separated into its own paragraph on the back end. I will be sure to correct that and see where I can get from there. Thanks for the help. You're welcome. By the way, I don't think any dialect of Z allows multiple horizontal definitions in one paragraph. As for the zipped file I used the gzip command, which is short for gunzip. Was the first couple I sent you corrupted? No, all the other GZ attachments have been fine - it must have been corrupted somewhere. Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Trying to Prove my Zed Specifications
Jon,
On 13/09/12 00:24, Jon Lockhart wrote:
Unfortunately the two extra sets I want to
declare and add to the spec are causing parser errors in ProofPower. The
sets I am trying to declare are TIMER == 0..5 and BOOLEAN == {0, 1}
which is allowed in the normal standard and has been syntactically
cleared by FUZZ and CZT through Anthony's Z Word Tools. Unfortunately
ProofPower doesn't allow me to do such a thing and I am wondering what
would be the proper protocol for adding such sets to a specification in
ProofPower.
These work in the version I have, 2.9.1w2.rda.120805, the latest patch
which fixes the recent Xpp issue. (Generally it would be useful to see
the error message you get.) ProofPower used to require ≜ (hat-equals)
for an abbreviation definition but a recent patch allows the standard ==
to be used. If you are using the 'current release' 2.9.1w2, == is not
supported. Can you check the version of ProofPower in the banner that
is shown when it starts?
My second question derives from this where right after the
sets I list some axioms which are used to hold globals which I use in
operations throughout the rest of my specification. They rely on the
boolean set I just created or are just parameters for the sets in
general. How would one go about proofing these or is it even necessary?
I'm not sure I understand the question. The axiomatic description
involving masterStop and masterReset is referring to the global variable
BOOLEAN that was defined to be 0 .. 5 earlier. The constraint holds
throughout the theory and is obtained as a theorem by
z_get_spec %SZT%masterStop%%
Phil
P.S. A better way to define booleans in Z is as follows:
BOOLEAN == ℙ []
True == [ | true]
False == [ | false]
This is standard Z. I don't know whether FuZZ accepts empty schemas.
The main advantage is that the usual logical connectives can be used
with such boolean expressions and the implicit conversion of schemas as
predicates allows such a boolean expressions to be used where a
predicate is required, and giving the expected predicate value. The
specification is more readable as a result. For example, your expression
if (elevatorRightHeading? = 1 ∧ elevatorGoingToFloor? = 1) then ...
could just be
if elevatorRightHeading? ∧ elevatorGoingToFloor? then ...
To negate a value one can write
¬ elevatorRightHeading?
rather than encouraging numerical tricks like
(1 - elevatorRightHeading?)
Note also that [] is a maximal set, so ℙ [] is too. Consequently type
checking ensures that such boolean values can take no other values.
Using BOOLEAN == {0, 1}, the constraint is a semantic one: type checking
will not reject e.g.
elevatorRightHeading? = 2
which, presumably, would be a mistake.
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Trying to Prove my Zed Specifications
On 13/09/12 02:47, Phil Clayton wrote:
BOOLEAN that was defined to be 0 .. 5
I meant to say {0, 1}, of course!
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Trying to Prove my Zed Specifications
Hi John, On 02/09/12 23:59, Jon Lockhart wrote: The problem I am having is this. I am trying to use the union operator in my specification. More specifically I am trying to and a individual item to a set in the predicate of a specification paragraph in z, which is allowed by the rules of the language. The PP system comes back with expection 62000 of the Z-Parser, saying that the union symbol from the palette is a free variable and those are not permitted in Z paragraphs. If ProofPower says that ∪ is a variable then the Z toolkit theory z_sets that defines the Z global variable (_ ∪ _) is not in scope, i.e. z_sets is not an ancestor theory of your current theory. Generally, Z specifications should always have the theory z_library as an ancestor, which brings all Z toolkit theories into scope. Typically your theory would start open_theory z_library; new_theory some_new_theory; ... If you need other theories in scope, add them as parents e.g. new_parent z_reals; Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Trying to Prove my Zed Specifications
Hi John, That sounds strange. It's probably easiest if you can cut your example down to a short script that produces the error, say containing just a single paragraph, and send a zipped version of that to the list. Phil On 03/09/12 01:47, Jon Lockhart wrote: Phil, Thanks for the reply. I have set it so up like that where the parent theory is z_library and my new theory is named something else. Just ran the print status again and that is what it says as well. Could it be one more minor thing is not loaded? Regards, Jon On Sep 2, 2012 8:43 PM, Phil Clayton phil.clay...@lineone.net mailto:phil.clay...@lineone.net wrote: Hi John, On 02/09/12 23:59, Jon Lockhart wrote: The problem I am having is this. I am trying to use the union operator in my specification. More specifically I am trying to and a individual item to a set in the predicate of a specification paragraph in z, which is allowed by the rules of the language. The PP system comes back with expection 62000 of the Z-Parser, saying that the union symbol from the palette is a free variable and those are not permitted in Z paragraphs. If ProofPower says that ∪ is a variable then the Z toolkit theory z_sets that defines the Z global variable (_ ∪ _) is not in scope, i.e. z_sets is not an ancestor theory of your current theory. Generally, Z specifications should always have the theory z_library as an ancestor, which brings all Z toolkit theories into scope. Typically your theory would start open_theory z_library; new_theory some_new_theory; ... If you need other theories in scope, add them as parents e.g. new_parent z_reals; Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] ProofPower RCS Repository
On 17/08/12 15:12, Phil Clayton wrote: Also, I encountered some confusing behaviour in that if PPRCSDIR is relative, it must be relative to PPDEVHOME, not the current directory, so I updated the comment. I failed to read the notes below where that was documented. But I think it's relative to $PPDEVHOME rather than $PPDEVHOME/pp . Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Trouble Installing on Windows
On 01/08/12 06:40, Jon Lockhart wrote: I will try the rpm inquiry and see what i come up with. I remember seeing that in the README. Guess it will be necessary to set those config variables. I have never found it necessary to set the PPMOTIFHOME environment variable. I believe I am currently using openmotif-2.3.3-1.fc12.x86_64.rpm openmotif-devel-2.3.3-1.fc12.x86_64.rpm as obtained from http://www.motifzone.org/files/public_downloads/openmotif/2.3/2.3.3/openmotif-2.3.3-1.fc12.x86_64.rpm http://www.motifzone.org/files/public_downloads/openmotif/2.3/2.3.3/openmotif-devel-2.3.3-1.fc12.x86_64.rpm Note that you need the devel package which provides the C header files required for building Motif applications. (I suspect it certain header files that configure is looking for.) Regards, Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Trouble Installing in cloud
Roger, From the reported package name openmotif-2.3.3-4.6.amzn1.x86_64 I can see that you're not using the packages from motifzone.net. Can you provide the output of rpm -ql openmotif-devel It could be that the Amazon 'amzn1' packages for OpenMotif have the same issue as the RPM Fusion OpenMotif packages that I describe here: http://lemma-one.com/pipermail/proofpower_lemma-one.com/2010-January/000592.html In that message, I see that I also noted I think there could be an issue beyond the configure script because PPMOTIFHOME doesn't seem to be used anywhere, namely in any include paths for compilation or linking. So I don't even know whether setting PPMOTIFHOME does anything! Phil On 01/08/12 13:10, Roger Bishop Jones wrote: I seem to have the same problem as John in a different place. i.e. in a linux image in the amazon cloud. I followed Phil's Yum list to get me started, which worked apart from failing to find polyml. I successfully built polyml from the sources. Then I checked with yum and found that the openmotif in the amazon repositories seemed to be the right one, and installed openmotif. However, the ProofPower configure script can't find it. Here's is what rpm says about it: [ec2-user@domU-12-31-39-05-56-E9 ~]$ rpm -q openmotif openmotif-2.3.3-4.6.amzn1.x86_64 [ec2-user@domU-12-31-39-05-56-E9 ~]$ rpm -ql openmotif /etc/X11/mwm/system.mwmrc /etc/X11/xinit/xinitrc.d/xmbind.sh /usr/bin/mwm /usr/bin/xmbind /usr/include/X11/bitmaps/xm_error /usr/include/X11/bitmaps/xm_hour16 /usr/include/X11/bitmaps/xm_hour16m /usr/include/X11/bitmaps/xm_hour32 /usr/include/X11/bitmaps/xm_hour32m /usr/include/X11/bitmaps/xm_information /usr/include/X11/bitmaps/xm_noenter16 /usr/include/X11/bitmaps/xm_noenter16m /usr/include/X11/bitmaps/xm_noenter32 /usr/include/X11/bitmaps/xm_noenter32m /usr/include/X11/bitmaps/xm_question /usr/include/X11/bitmaps/xm_warning /usr/include/X11/bitmaps/xm_working /usr/lib64/libMrm.so.4 /usr/lib64/libMrm.so.4.0.3 /usr/lib64/libUil.so.4 /usr/lib64/libUil.so.4.0.3 /usr/lib64/libXm.so.4 /usr/lib64/libXm.so.4.0.3 /usr/share/X11/bindings /usr/share/X11/bindings/acorn /usr/share/X11/bindings/apollo /usr/share/X11/bindings/dec /usr/share/X11/bindings/dg_AViiON /usr/share/X11/bindings/doubleclick /usr/share/X11/bindings/hal /usr/share/X11/bindings/hitachi /usr/share/X11/bindings/hp /usr/share/X11/bindings/ibm /usr/share/X11/bindings/intergraph /usr/share/X11/bindings/intergraph17 /usr/share/X11/bindings/megatek /usr/share/X11/bindings/motorola /usr/share/X11/bindings/ncr_at /usr/share/X11/bindings/ncr_vt /usr/share/X11/bindings/pc /usr/share/X11/bindings/sgi /usr/share/X11/bindings/siemens_9733 /usr/share/X11/bindings/siemens_wx200 /usr/share/X11/bindings/sni /usr/share/X11/bindings/sni_97801 /usr/share/X11/bindings/sony /usr/share/X11/bindings/sun /usr/share/X11/bindings/sun_at /usr/share/X11/bindings/tek /usr/share/X11/bindings/xmbind.alias /usr/share/doc/openmotif-2.3.3 /usr/share/doc/openmotif-2.3.3/COPYRIGHT.MOTIF /usr/share/doc/openmotif-2.3.3/README /usr/share/doc/openmotif-2.3.3/RELEASE /usr/share/doc/openmotif-2.3.3/RELNOTES /usr/share/man/man1/mwm.1.gz /usr/share/man/man1/xmbind.1.gz /usr/share/man/man4/mwmrc.4.gz Should I be setting OPENMOTIFHOME? If so, to what, surely ProofPower looks in /usr/bin Roger Jones ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Trouble Installing on Windows
Jon, On 01/08/12 22:43, Jon Lockhart wrote: I forgot to grab the devel rpm when I was on the download site. I had olbly grabbed the OpenMotif rpm. That did the trick on the configuration file. devel packages are easily overlooked! Usually, when you have source code with a build dependency on X, you need X's devel package. Now I am running into the issue on the install. I have attached the build log for your convienece. The install is failing b/c the file Print.h is not available in the X11 folder, and I have tried reinstalling with yum several times. Is there another package from yum that I have possibly missed downloading? The missing file is /usr/include/X11/extensions/Print.h On my machine, the command rpm -q --whatprovides /usr/include/X11/extensions/Print.h indicates that the package libXp-devel provides this file. This should have been installed by the yum command I quoted previously, which included libXp-devel. Can you double check that you entered the command exactly, omitting only the line containing polyml? (I checked the fc17 package, and it does appear to provide this file.) I just want to take the time now to thank you and Rob for all the help you been providing me on getting PP up and running. It has been a long time since I used a Linux system, and having to relearn all this material I go is frustrating, along with trying to get a tool installed that I really want to try and use with my formal specification writing. I appreciate everything I have been provided. Glad to help. With Linux distributions these days, package management support takes most of the pain out of fetching/installing prerequisites. But you still need to know which packages to install... It's a pity that 90% of the installation effort is just to get Xpp working. I'm working on a GTK-based replacement to Xpp but it's not quite ready yet. Regards, Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Trouble Installing in cloud
On 01/08/12 14:35, Roger Bishop Jones wrote: The real challenge (for me at least) is to get xpp and/or emacs to run in the cloud with a display here on earth, I don't have much clue how to do that. I've been thinking about this. To me, it seems conceptually wrong to be running Xpp remotely. Would it not make more sense to run a local (earth-based) Xpp whose journal window contains a remote ProofPower shell (up in the cloud) via e.g. ssh? Initially I tried testing xpp -c ssh -Y user@host but is seems that the capabilities of Xpp's pseudo terminal aren't up to ssh login interaction. However, if you can automatically log in then all is fine. I used the instructions here: http://docs.fedoraproject.org/en-US/Fedora/17/html/System_Administrators_Guide/s2-ssh-configuration-keypairs.html to create .ssh/authorized_keys on the remote account to allow automatic log in. However, xpp -c ssh -Y user@host pp -d zed fails to find pp when attempting to run on the remote host, even though the remote account adds the ProofPower home directory to the path in .bash_profile. The issue is that the remote shell is not an interactive shell, so .bash_profile does not get run. Many options here: 1. Specify full remote path, e.g. xpp -c ssh -Y user@host \ $REMOTEPPHOME/bin/pp -d $REMOTEPPHOME/db/zed where REMOTEPPHOME is the ProofPower home directory in the cloud. 2. Source the required environment as part of the command, e.g. xpp -c ssh -Y user@host source .bash_profile; pp -d zed 3. Add the ProofPower home directory to the path in an rc file (e.g. .bashrc) instead of in a profile file (such as .bash_profile), then just use xpp -c ssh -Y user@host pp -d zed For a cloud service, option 3 looks like the best set up. Regards, Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Trouble Installing on Windows
Jon, On 01/08/12 23:44, Jon Lockhart wrote: I did run the yum install commands as you mentioned, but it is possible I spelled it wrong. I will look into and get back to you. You can copy and paste the required lines of the yum command from the email directly into a terminal. A trailing backslash on a line means that the command is continued on the next line. There is no problem copying and pasting the command in several pieces. Note that in Linux, you can copy and paste just by selecting text to copy and middle-clicking where you want to paste. (If middle-clicking in a terminal window, text is inserted at the cursor.) Apologies if you're aware of these Linux basics. Thought this may help to avoid spelling errors. Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Trouble Installing on Windows
Jon, I have been running ProofPower under Fedora for many years now. A long time ago, Rob and I established that the following yum command gave us the prerequisites needed for ProofPower (apart from OpenMotif itself, which is not properly open source) after a standard Fedora install: yum install \ gcc-c++ \ polyml \ texlive-latex \ libXp-devel \ libXext-devel \ libXmu-devel \ libXt-devel \ xorg-x11-fonts-misc It would be useful to know if anything is missing after entering this command, which you need to run as root. (I believe the package gcc-c++ will give you g++.) There are a couple of things Fedora users need to know though. 1. OpenMotif is available via yum from the RPM Fusion repository. If you add the RPM Fusion repository to your system, you mustn't use the version of OpenMotif that it supplies - see my previous message here for details: http://lemma-one.com/pipermail/proofpower_lemma-one.com/2010-January/000592.html If you don't use RPM Fusion, don't worry about this! 2. With Fedora 16 and later, the GNOME 3 shell is the default and this breaks the Motif Text widget, making Xpp very cumbersome to use. (At least on x86-64 platforms.) The solution is to use fallback mode: in 'System Settings' - 'System Info' - 'Graphics', set 'Forced Fallback Mode' to 'On'. This issue has now been officially noted as an OpenMotif bug here: http://bugs.motifzone.net/long_list.cgi?buglist=1551 Regards, Phil On 31/07/12 21:35, Jon Lockhart wrote: Hey Rob, Thanks for the link to motifzone, that worked immediately and I was able to get the latest binary for open motif installed on my Fedora 17 image. I am now currently having trouble with getting polyml to install. After running the config file I try to run the make file and it says that command g++ is not found. I did a yum install of gcc and gpp to make sure I had a c and c++ compiler installed on my fedora and it appeared to have installed both packages fine. Any thoughts on this? Sorry for asking for all the help, my linux is pretty rusty. Thanks, Jon Lockhart On Mon, Jul 30, 2012 at 2:58 AM, Jon Lockhart jal...@bucknell.edu mailto:jal...@bucknell.edu wrote: Rob, Thank you very much for the site. I will give it a try as soon as i can. Regards, Jon On Jul 30, 2012 2:48 AM, r...@lemma-one.com mailto:r...@lemma-one.com wrote: Jon, Rob, I was wondering, you know of any problems with the download site for OpenMotif? I got Virtual Box and Fedora 17 working on my desktop, my laptop did not have enough RAM to run it, and I got ProofPower and ML downloaded no problems, but seems you get a blank page when getting OpenMotif 2.3.3. I contacted there list but have not heard back all week. Any ideas? Try motifzone.net http://motifzone.net rather than www.openmotif.org http://www.openmotif.org Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Trouble Installing on Windows
On 01/08/12 00:07, Phil Clayton wrote: yum install \ gcc-c++ \ polyml \ Of course, you can leave the package polyml out if you're building it yourself. I believe the Fedora 17 repo supplies 5.4.1. If you always want to manage your own versions of Poly/ML, you can ensure that yum never installs the package polyml from any repo by adding polyml to the line starting exclude= in /etc/yum.conf , e.g. exclude=polyml In my case, I have exclude=openmotif*,lesstif*,polyml,mlton,ocaml* Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Scope of variables in Z declaration
On 20/04/12 18:48, Phil Clayton wrote: On 20/04/12 11:19, Rob Arthan wrote: ... A == 1 .. 10 S ^= [A : A x A | (_+_)A 10] ... And as so often, language decisions that are bad for proof are often bad for pedagogical and other reasons too. In this case, it stops the language being closed under certain desirable transformations. In particular, the standard account of how to normalise a schema fails. If you try to normalise S, you get the ill-typed schema [A : Z x Z | A in A x A /\ (_+_) A 10]. In this example, you can expand the definition of A, but if A were loosely specified, I don't see any clean way of describing the normalised version. Whilst horizontal schemas are not closed under normalization, we can write [A' : A × A | (_ + _) A' 10][A / A'] Oops, that should have been [A' : ℤ × ℤ | A' ∈ A × A ∧ (_ + _) A' 10][A / A'] so at least schemas are closed. For practical purposes, that seems sufficient. GIven its provenance in academia, it amazes me how many design decisions in Z make it harder to teach, typically, as here, by making useful rules of thumb fail to work in edge cases. Yes, another headache for teachers and students. Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Theorem QA
On 24/03/12 09:32, Rob Arthan wrote: The scripts for the ProofPower mathematical case studies have a little tool called check_thms which does a quality assurance check on the the theorems in a theory. It checks against: a) Theorems with free variables. Typically this means you forgot an outer universal quantifier. Later on you will be puzzled when tools like the rewriting tools think you don't want the free variables to be instantiated. b) Theorems with variables bound by logical quantifiers (universal, existential and unique existential) that are not used in the body of the abstraction. This happens for various reasons (often hand in hand with (a)). It is misleading for the reader and can be confusing when you try to use the theorem. It outputs a little report on any problems it finds. I am considering putting a bug-fixed and documented version of check_thms in the next working release of ProofPower. Any comments or suggestions for other things to check for would be welcome. I am wondering about a stronger version of check b for individual conjuncts of a theorem. In the past, I have found that e.g. rewriting can be awkward when an equational conjunct of a theorem does not mention a universally quantified variable (that is mentioned by other conjuncts). I think the issue was when the unmentioned variable was quantified over a non-maximal set, so this is probably most relevant to Z. For example, given │ _ ^ _ : ℤ × ℕ → ℤ ├── │ ∀ i : ℤ; j : ℕ ⦁ i ^ 0 = 1 ∧ i ^ (j + 1) = i * i ^ j I think rewriting with the base case requires manual intervention to provide a value for j, so the following would be preferable: ├── │ ∀ i : ℤ ⦁ i ^ 0 = 1 ∧ (∀ j : ℕ ⦁ i ^ (j + 1) = i * i ^ j) I expect that this sort of check would be dependent on the current proof context (perhaps making use of canonicalization support) so may not be desirable as part of the same utility. This is currently just for HOL, but I could do something similar for Z too. Certainly this would be a useful facility for HOL users but I could only make use of a Z version. Regards, Phil P.S. The above formal text is UTF8 encoded! Hopefully that is not a problem these days. It would be useful to know if any mail systems aren't displaying it properly. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] Fixes for building with SML/NJ
Currently ProofPower doesn't build with SML/NJ. A patch is attached to fix this. Although working with Poly/ML is recommended, any (less-trusting) users building on theories of others may wish to check, by running with both compilers, that the supplied proof scripts do not exploit compiler-specific loopholes to circumvent proof. Anyone following the Isabelle mailing list recently will note that this provides little additional assurance when operating in a zero-trust environment: running with both compilers only helps with item 2d on Mark's list: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-January/msg00085.html Still, every little helps... Phil patch-2.9.1w2.rda.110814.pbc.120131.gz Description: GNU Zip compressed data ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Writing Z schema predicates with decorations
On 27/09/11 13:25, Roger Bishop Jones wrote: On Sunday 25 Sep 2011 16:20, Phil Clayton wrote: Although the Z'SchemaPred semantic constant enables renaming to be avoided, Z'SchemaPred HOL terms are not Z when the schema components are decorated inconsistently. So perhaps renaming is useful? I'm sure it is. But I doubt that it is sensible in the mapping of a decorated schema reference. In this case the same decoration is applied to all components. As to the merits of the design of z_schema_pred, it seems to me that the mapping is not only simpler but works more as one would expect if a decorated schema reference uses the decoration parameter as intended. In that case, simply rewriting with the definition of Z'SchemaPred (which is just membership) yields the statement that the binding with decorated variable names (but undecorated component names) is a member of the schema (undecorated). This is as close as you get to asserting that the decorated theta term is a member of the schema (which might possibly have been even better in some ways, though less efficient). My guess is that it probably was done that way in the prototype embedding of Z into the prototype ICL HOL (I did the specifications and explained them to Geoff Scullard who implemented them), but that when this was all re-implemented for the product version, the implementation fell out without using it (I don't think either Geoff or myself had much involvement at that stage, so the reason for using it got lost). I wondered whether the original design intended to map decoration differently for predicates and expressions? Then the user could determine the mapping of e.g. S' as either mk_z_schema_pred (S, ') mk_z_schema_pred (mk_z_decor%down%s (S, '), ) by controlling predicate/expression parsing modes as usual. (As Rob points out, the second is always used currently.) A better answer as to why Z'SchemaPred needs to support decoration is to allow e.g. predicate S' to match with S, for e.g. forward chaining, with such an S' being a valid Z term. (Currently, when a schema predicate is stripped in the subgoal package with the proof context 'z_schemas, any top-level Z'Decor is converted to decoration on the Z'SchemaPred binding variables.) My suggestion regarding renaming was not about the mapping of Z into HOL but about what Z proof operations could do to avoid not Z HOL terms. That is actually a separate issue/discussion. Sorry for the confusion. Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Writing Z schema predicates with decorations
On 28/09/11 13:40, Phil Clayton wrote: On 27/09/11 13:25, Roger Bishop Jones wrote: On Sunday 25 Sep 2011 16:20, Phil Clayton wrote: Although the Z'SchemaPred semantic constant enables renaming to be avoided, Z'SchemaPred HOL terms are not Z when the schema components are decorated inconsistently. So perhaps renaming is useful? I'm sure it is. But I doubt that it is sensible in the mapping of a decorated schema reference. In this case the same decoration is applied to all components. As to the merits of the design of z_schema_pred, it seems to me that the mapping is not only simpler but works more as one would expect if a decorated schema reference uses the decoration parameter as intended. In that case, simply rewriting with the definition of Z'SchemaPred (which is just membership) yields the statement that the binding with decorated variable names (but undecorated component names) is a member of the schema (undecorated). This is as close as you get to asserting that the decorated theta term is a member of the schema (which might possibly have been even better in some ways, though less efficient). My guess is that it probably was done that way in the prototype embedding of Z into the prototype ICL HOL (I did the specifications and explained them to Geoff Scullard who implemented them), but that when this was all re-implemented for the product version, the implementation fell out without using it (I don't think either Geoff or myself had much involvement at that stage, so the reason for using it got lost). I wondered whether the original design intended to map decoration differently for predicates and expressions? Then the user could determine the mapping of e.g. S' as either mk_z_schema_pred (S, ') mk_z_schema_pred (mk_z_decor%down%s (S, '), ) by controlling predicate/expression parsing modes as usual. (As Rob points out, the second is always used currently.) To answer my own question: from what Roger is saying, this must have been the intention as Z'SchemaPred can only occur in a predicate and Z'Decor only in an expression. Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Writing Z schema predicates with decorations
My guess would be that a non-empty decoration is possible for Z'SchemaPred to allow for variable decoration during proof operations: if all variables in the characteristic binding are consistently decorated, the resulting term is still Z. However, not all Z proof operations consistently decorate the variables in the characteristic binding, so the semantic constant Z'SchemaPred is exposed fairly often. (This could be avoided with schema renaming as already done recently.) Phil On 24/09/11 13:09, Rob Arthan wrote: Phil, On 17 Sep 2011, at 15:06, Phil Clayton wrote: Using the subgoal package, I have just been trying to quote an assumption (as a term quotation) but couldn't. On the assumption term, dest_z_term returns the form ZSchemaPred (..., ') Given, e.g. (* S : P [a, b : Z] *) val S = %SZT% S %bigcolon% %bbP% [a, b : %bbZ%] %%; is there a way to write a Z term quotation equal to tm1 as follows: val tm1 = mk_z_schema_pred (S, '); ? (I can do so in HOL using Z'SchemaPred directly.) The quick answer is no - the term generator (imp063.doc) never calls mk_z_schema_pred with non-empty decoration. I need to remind myself exactly what the decoration in mk_z_schema_pred is for (I know what the semantics is intended to be but I can't recall why we have it). Perhaps Roger can cast his mind back to this. This reminds me that I always meant to make the Z specifications of the Z to HOL mapping available. As a quick fix, I have put the documents here: http://dl.dropbox.com/u/34693999/zed002.pdf http://dl.dropbox.com/u/34693999/zed003.pdf http://dl.dropbox.com/u/34693999/zed005.pdf I will make sure they typecheck presently and include them in the doc directory in future builds. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Writing Z schema predicates with decorations
On 25/09/11 10:04, Roger Bishop Jones wrote: On Saturday 24 Sep 2011 22:53, Roger Bishop Jones wrote: On Saturday 24 Sep 2011 13:09, Rob Arthan wrote: The quick answer is no - the term generator (imp063.doc) never calls mk_z_schema_pred with non-empty decoration. I need to remind myself exactly what the decoration in mk_z_schema_pred is for (I know what the semantics is intended to be but I can't recall why we have it). Perhaps Roger can cast his mind back to this. My memory is pretty bad on the history. I expect that I started out with the syntax in Spivey's The Z Notation (It was the only game in town at the time). But then you might expect to see gen actuals and renaming! there. A better answer is as follows. We were making the Spivey syntax more orthogonal by allowing schema expressions in places where only schemas were previously allowed, and in that context there was no benefit in putting actual parameters or renamings into the predication operation, since they could be implemented using the normal schema expression operations. However, decoration is another matter. Decoration during schema-predication requires only that the free variables in the covert theta term be decorated. Decorating the schema(expression) is a more horrible operation and is unnecessary. So the parameter would enable a more efficient mapping of the Z into HOL, if it had actually been used! Presumably the implementation (of z_schema_pred) does just decorate the theta term not the schema expression. I have just found section 4.3.7 in ZED003 and it appears to say that. Although the Z'SchemaPred semantic constant enables renaming to be avoided, Z'SchemaPred HOL terms are not Z when the schema components are decorated inconsistently. So perhaps renaming is useful? Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] Writing Z schema predicates with decorations
Using the subgoal package, I have just been trying to quote an assumption (as a term quotation) but couldn't. On the assumption term, dest_z_term returns the form ZSchemaPred (..., ') Given, e.g. (* S : P [a, b : Z] *) val S = %SZT% S %bigcolon% %bbP% [a, b : %bbZ%] %%; is there a way to write a Z term quotation equal to tm1 as follows: val tm1 = mk_z_schema_pred (S, '); ? (I can do so in HOL using Z'SchemaPred directly.) All my attempts result in a term equal to tm2 as follows: val tm2 = mk_z_schema_pred (mk_z_decor%down%s (S, '), ); tm1 and tm2 are equivalent so this is hardly an issue for writing Z specifications but can make quoting terms awkward. In the end, I just referred to the assumption by index. Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Experimental OpenProofPower release 2.9.1w2.rda.110814
Rob, On 04/09/11 11:49, Rob Arthan wrote: Phil, On 3 Sep 2011, at 20:01, Phil Clayton wrote: Rob, Thanks for the latest release. I have been using this for a while now and have a few comments. On 14/08/11 16:18, Rob Arthan wrote: a) For visual compatibility with the ISO standard, a symbol for unary minus in Z has been added to the font and defined as a synonym of the unary minus written as a tilde in the theory z_numbers. The symbol displays and typesets as short minus sign. %cat%/ (i.e., a frown followed by a backslash) is now defined as an alias for distributed concatenation written %dcat% in the theory z_sequences. The new minus sign appears to be missing from the palette. (Am I going blind?) It should be at row 6 column 3, just right of greater-than-or-equals. My fault. For some reason I failed to merge that line of the new Xpp file into the one in my home directory. (Normally I merge in the opposite direction to avoid this happening.) b) In xpp, you can now switch dynamically between the horizontal and vertical layout using a new item in the window geometry. N.b., this is accompanied by a change in the way you specify the initial layout and geometry in app-defaults/Xpp. See the CHANGES file for more details. The switching is useful. A few observations: 1. When there is no journal window, Show Geometry causes a crash: xpp: fatal error: signal 11: memory fault: ... (It may not crash the first time.) Also, Ctrl+T causes a crash, even though there is no menu item Toggle Geometry without a journal window. I have attached a patch that fixes these two (which were intermittent/system dependent). Thanks, that fixes it. 2. I have an issue with the design when using horizontal mode. My app-defaults/Xpp sets column widths assuming there will be a journal window. However, I am often opening file just to view/edit, i.e. no journal window, and always have to resize the window which is far too wide. But you far too wide may be another user's very nice (see below). If there are users who want as much width as possible, then I suppose so. I would have a similar issue the other way around. Is it possible for the width of the editor window to be the same whether or not Xpp is started with a journal window? That is exactly the old behaviour which is bad for people who like to use the horizontal layout even on smallish screens. The only way to keep everybody happy is to have separate resources for the width and height of an edit-only session. The extra configuration would be appreciated by me but, while I'm the only one, perhaps it is not worth doing. For vertical mode, the current behaviour seems preferable. I think different behaviour for the different orientations makes sense because of the asymmetric nature of documents: bounded width, unbounded height. That's not really a valid assumption: you may worry about keeping your source files within a fixed width. but many people don't. When entering text, it is quite common to use carriage-returns only to separate paragraphs or sentences and this logical arrangement is convenient for many reasons, e.g., when searching for phrases. Likewise, in code, many people prefer long lines to artificially inserted line breaks with no logical significance. (A line-wrapping mode for formal text in ProofPower documents is on my wish-list). There are pros and cons. I find it useful to make the text fit e.g. 80 columns not just for general readability but to get a decent view of two source files on the screen at once. This especially helps comparing/merging side by side and working with a journal window (which has sizeable output). (Even with a line wrapping mode for formal text, I would stick to N columns because other tools, e.g. visual diff programs, would not have such a line wrapping mode.) 3. Given the above observation about document shape, should toggling attempt to maintain width by resizing the Xpp window? I have had various ideas along these lines. Have you thought about that? Aside from my reservations above, it is generally considered to be bad practice for X applications to resize or move top-level windows programmatically once they are created unless there is some really compelling reason in the application logic for doing this. The results of trying to do so are dependent on the window manager and many window managers will just ignore resize requests from the program. Yes, I wondered if it was bad practice for the window to resize itself. Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] How do you arrange Xpp?
I meant to add that I always use horizontal mode, so that would have got my vote as Mark predicted! A dynamic toggle would be very useful, I think. Phil On 27/07/11 13:37, Rob Arthan wrote: Thanks to Mark and Artur for their feedback. We have one vote each way, so for the time being I won't change this. People like Mark with smallish screens should be aware that the window menu now has a Show/Hide Journal item as well as Show/Hide Script. Even when I using a big screen, I use these a lot when I am doing proofs (I set PPLINELENGTH so that ProofPower formats things to use the full width of the journal window when the script window is hidden). What I may do in a forthcoming version is add a toggle geometry item to the window menu so that the horizontal/vertical distinction can be made dynamically. Regards, Rob. On 22 Jul 2011, at 16:03, Mark wrote: I use Xpp in 1-window mode for general text editing, and I also 2-window mode for developing scripts. I want to develop my text with 80-character width, which is the industry standard. Like many, I only have a 1280x800 screen, and so horizontal mode means that the journal window is very squashed up if the script window stays at 80. So I prefer vertical. I bet Phil is now going to show off about his new, super-hidef screen laptop and suggest horizontal mode... :) Mark. on 22/7/11 3:10 PM, Rob Arthan r...@lemma-one.com mailto:r...@lemma-one.com wrote: I nearly always use Xpp with the following settings in $HOME/app-defaults/Xpp Xpp*script.rows: 32 Xpp*script.columns: 60 Xpp*script.background: white Xpp*script.foreground: black Xpp*journal.rows: 32 Xpp*journal.columns: 60 Xpp*namestring.columns: 24 Xpp*journal.background: light blue Xpp*journal.foreground: black Xpp*journal.editable: true Xpp*mainpanes.orientation: HORIZONTAL This differs from the out of the box default in laying out the windows side-by-side and letting you bring up the command dialogue by trying to type into the journal window. I am tempted to change the default settings to the above - it looks a bit less like a standard Motif application, but it makes much better use of modern screens (or at least modern screens that have a landscape aspect ratio). It would be nice to know what other people do before I commit to this change. So please let me know your preferences. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com mailto:Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Schema in a predicate stub
Rob, On 11/07/11 13:37, Rob Arthan wrote: Further to my earlier reply to Phil's suggestion (outlined below), I have looked into implementing it and it all looks good to me. That's good - I was poised to have a go myself! There is only one consequence that I can see that looks a little strange at first, but makes sense when you think about it. This is the treatment of conditionals in quotations. If you enter: %SZT% if 1 = 2 then 3 else 4 %% it will fail, because the top level of a Z quotation is a predicate context (but not an operand of a stub, so non-predicates are allowed). To get this to work you have to force an expression context: %SZT% (if 1 = 2 then 3 else 4) %bigcolon% %bbU %% Arguably we should have a separate quotation symbol to introduce a Z expression. The justification for the quotation to default to predicate is easy to see when you think about entering ordinary logical expressions: it would be very painful if they defaulted to being treated as schema expressions. I think the above slight complication (which is specific to conditionals or user-defined things like them) is worth the improved uniformity of the new approach. I agree with your view. Although it may be necessary to force an expression for such terms, overall I think the behaviour is clearer because it's more uniform. Whether to have a separate expression quotations is an interesting question. The need to force an expression is not that common so %bigcolon% %bbU% seems all right. It just takes getting used to. Expression quotations would be clearer and more intuitive though. Phil Regards, Rob. On 11 Jul 2011, at 09:45, Rob Arthan wrote: Phil, On 6 Jul 2011, at 16:15, Phil Clayton wrote: On 21/06/11 16:58, Phil Clayton wrote: Is there any reason why a schema argument in a predicate stub (_?) isn't implicitly converted to a predicate? ... There is also the question of whether context stubs (_!) should be checked as predicates when the context is a predicate. Given function (op2 _!) would we expect %SZT% [ | op2 2] %% to fail because 2 is not a predicate? (Irrespective of any definition op2 may have.) I think I would. (This looks more effort to implement.) I will look into implementing something along these lines. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com mailto:Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Xpp on Fedora 14 and later
On 08/07/11 01:00, Phil Clayton wrote: On Fedora 15, building Xpp works but it seg faults when I run it - see attached xpp_output.log. On further investigation, I may have unfairly attributed this to using Fedora 15. The cause of the issue appears to be having a long path to the xpp executable, i.e. a long string in argv[0], at run-time. On my machine, when argv[0] (incl. null terminator) is more than 78 characters, xpp crashes. I can reproduce it simply by copying my existing pp installation to a new directory as follows: cp -a /opt/pp/pp-2.9.1w2.rda.110226 /tmp/ppxxx Then argv is /tmp/ppxxx/bin/xpp which is 79 characters (incl. null terminator) and this makes xpp crash. Unfortunately all my builds since moving to Fedora 15 were temporary builds to test patches which were located somewhere deep in the directory hierarchy. Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Xpp on Fedora 14 and later
Rob, Thanks - using jpegs solves the issue. Phil On 09/07/11 15:28, Rob Arthan wrote: Phil, The OpenMotif bug report suggests that if you use jpeg versions of the template images, then things will work. You can find a tarball containing the jpegs you need here: http://dl.dropbox.com/u/34693999/ProofPower/template-jpegs.tgz If you copy these into the bitmaps directory in the ProofPower installation directory (or your own bitmaps directory if you have one) and change all the .bmp file extensions in app-defaults/Xpp to .jpg, that should give you a workaround. Please let me know how you get on. Regards, Rob. On 8 Jul 2011, at 01:00, Phil Clayton wrote: On Fedora 14 and later, Xpp always produces a warning dialog on start up saying it can't find the bitmap images for the templates. (And the images don't appear in the templates window.) This appears to be due to the following: http://bugs.openmotif.org/long_list.cgi?buglist=1539 I haven't looked into any work-around. On Fedora 15, building Xpp works but it seg faults when I run it - see attached xpp_output.log. I can run a version built elsewhere but it has serious issues not updating the text windows when scrolling under certain circumstances, which may be related to Gnome 3 - I don't know. Anyone unfortunate enough to be using Gnome 3 as well will find that the left window key (Super_L) is now used by Gnome. There is a simple work-around apart from the obvious using another modifier key. For Shift+Super_L make sure you press Shift first Super_L press X; press Super_L; release X where X is any benign key. I use Shift (as I'm already in the habit of pressing Shift+Super_L). Phil - wishing I had stuck with Fedora 13 for now... 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 ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] Xpp on Fedora 14 and later
On Fedora 14 and later, Xpp always produces a warning dialog on start up saying it can't find the bitmap images for the templates. (And the images don't appear in the templates window.) This appears to be due to the following: http://bugs.openmotif.org/long_list.cgi?buglist=1539 I haven't looked into any work-around. On Fedora 15, building Xpp works but it seg faults when I run it - see attached xpp_output.log. I can run a version built elsewhere but it has serious issues not updating the text windows when scrolling under certain circumstances, which may be related to Gnome 3 - I don't know. Anyone unfortunate enough to be using Gnome 3 as well will find that the left window key (Super_L) is now used by Gnome. There is a simple work-around apart from the obvious using another modifier key. For Shift+Super_L make sure you press Shift first Super_Lpress X; press Super_L; release X where X is any benign key. I use Shift (as I'm already in the habit of pressing Shift+Super_L). Phil - wishing I had stuck with Fedora 13 for now... xpp_output.log.gz Description: GNU Zip compressed data ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] Schema in a predicate stub
Is there any reason why a schema argument in a predicate stub (_?) isn't implicitly converted to a predicate? A Z specification taking a Standard-compatible approach to booleans may have: BOOL == P [] True == [| true] False == [| false] if True then X else Y However, this produces a type error: we must explicitly say that True is to be taken as a predicate, i.e. if %Pi% True then X else Y which seems unnecessary. Above example attached. Phil schema_in_pred_stub.sml.gz Description: GNU Zip compressed data ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] Type inference issue with characteristic tuples
(Examples also included in attached file char_tuple_issue.sml)
After defining e.g.
[T]
S %def% [X : T]
the type inference issue with characteristic tuples can be seen when the
term
{S; S'}
occurs as a subterm. For example, the following terms fail when they
are being constructed, due to an internal type mismatch:
{{S; S'}}
{S; S'} = A
The type of {S; S'} should be the same as for {S; (S)'}, i.e.
[X : T] %rel% [X : T]
However, type inference incorrectly computes the type of {S; S'} as
[X : T] %rel% [X' : T]
- the type of the different term {S; (S ')}. When terms are constructed
after type inference, construction of the characteristic tuple has the
correct type. However, incorrect type annotations can be present
elsewhere in the term from type inference, causing the type mismatch
when building terms.
The problem is that type inference generates the characteristic tuple
for the schema text, e.g. S; S', before type checking the schema text.
Consequently S' has not been converted from a local variable to a
decorated global variable when the characteristic tuple is generated, so
the characteristic tuple (effectively) contains
%theta% (S ')
rather than
%theta% S '
I think this is fairly simple to fix - see attached patch. Note that
there is no problem with
{S; (S)'}
because there is no local variable S' to cause the problem. (This can
be used as a work-around.)
I suppose this is a good opportunity to raise item 219, i.e.
1. Should the Spivey-Z schema decoration S' be supported in
ProofPower-Z? I believe Standard-Z requires one of
(S)'
S '
to decorate a schema reference S. This avoids the question of what
happens when both S and S' are global variable names.
2. Should ProofPower-Z allow S ' to be interpreted as the name S', i.e.
ignoring space between the two tokens and taking them as one token? I
would never expect e.g. abc def to be taken as the name abcdef. Note
that when both S and S' are global variable names, S ' is a reference to
S' in ProofPower-Z, not the schema decoration of S. Not only is this
surprising, it is different to Standard-Z. (Section 7.3 in Z Standard.)
Phil
char_tuple_issue.sml.gz
Description: GNU Zip compressed data
imp062.doc.patch.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] xpp Segmentation fault
Hi Shu, We will need some more information about this... 1. Does pp -d database work? (Note pp not xpp.) This should give you the ProofPower session directly in the terminal. 2. What version of ProofPower are you using? If pp -d database worked above: The version printed by ProofPower. Otherwise: The ProofPower version is contained in the file $PPHOME/VERSION where PPHOME is such that which xpp returns $PPHOME/bin/xpp. Also, in this case, the Poly/ML version will be useful. What does ldd `which pp-ml` say for libpolyml and what version is Poly/ML in that directory. 3. What OS (incl. version) are you using? What does uname -a report? 4. Are you running xpp (or pp) on the machine that it was built on? If not: What does file `which xpp` report? If you can, what does uname -a give for the machine that built it? 5. Does PPENVDEBUG=1 xpp produce any more output? That's probably enough to start with! Phil Shu Cheng wrote: Hello everyone, I am a fresher here. When I try to use xpp -d database to open an xpp session in X11, I get an error message -- Segmentation fault. Is anyone have any idea for this? Thanks a lot! Shu Cheng ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] xpp Segmentation fault
Rob Arthan wrote: b) Try running it under the gnu debugger, gdb. To do this run the command: gdb /usr/local/pp/bin/pp I'm guessing Rob meant /usr/local/pp/bin/xpp [Aside to Phil: when xpp runs in the background, gdb won't follow xpp through the fork unless you do clever things that have never worked for me: it will just say that the process exited normally. As it is fairly rare that running in the background makes any difference, I usually try debugging with -b first. You don't need to single step with gdb if the failure you are expecting is a signal like a segmentation fault, gdb will trap the signal and prompt for commands.] Thanks, that's useful to know. Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Experimental OpenProofPower release 2.9.1w2.rda.110226.tgz
Rob Arthan wrote: a) Alongside the functions set_pc, set_merge_pcs, PC_T, MERGE_PCS_T, etc. there are now functions set_extend_pc, set_extend_pcs, EXTEND_PC_T, EXTEND_PCS_T etc., that extend the current proof context rather than overwrite it. This facilitates proof contexts that just change the behaviour of particular proof procedures like forward chaining. I've noticed some change to the proof context output of print_status (as supplied by get_current_pc): 1. The output of print_status now includes the all proof contexts implicitly included by the specified proof context. For example, for set_pc z_library print_status produces Current proof context name(s): ['z_predicates, 'z_decl, z_predicates, 'z_%mem%_set_lang, 'z_bindings, 'z_schemas, 'z_tuples, z_language, 'z_normal, 'z_%mem%_set_lib, 'z_sets_alg, z_sets_alg, 'z_rel_alg, 'z_fun_alg, 'z_numbers, z_library]; 2. If a proof context is requested more than once, explicitly or implicitly, it appears more than once in the list printed by print_status. For example, for set_merge_pcs [z_library, z_predicates]; print_status produces Current proof context name(s): ['z_predicates, 'z_decl, z_predicates, 'z_%mem%_set_lang, 'z_bindings, 'z_schemas, 'z_tuples, z_language, 'z_normal, 'z_%mem%_set_lib, 'z_sets_alg, z_sets_alg, 'z_rel_alg, 'z_fun_alg, 'z_numbers, z_library, 'z_predicates, 'z_decl, z_predicates]; I suspect 1 and 2 are really the same thing. I presume this is unintended as it does not fit the behaviour described for get_current_pc in the manual. I actually found it quite useful to see the component parts of the proof context without having to refer to the manual, though I think the old behaviour should still be present for print_status, i.e. telling the user what they specified. Regarding this new capability, given a current proof context e.g. [z_library, 'z_reals], is it more efficient to do e.g. set_extend_pcs [a, b]; than set_merge_pcs [z_library, 'z_reals, a, b] ? It looks like it is from reading the source code but I didn't fully digest everything. Also I noticed imp051.doc, line 1594: fun Ûset_extend_pcsÝ ([]: string list): unit = fail set_merge_pcs 51020 [] should probably not say set_merge_pcs. b) A variable capture problem in %implies%_match_mp_rule1 that made forward chaining fail has been addressed in a new rule %implies%_match_mp_rule2. The new behaviour has been adopted as the default, but this can make some existing proofs break. Component proof contexts 'mmp1 and 'mmp2 are provided that let you switch between the new and old behaviour. Using, set_extend_pc'mmp1 or EXTEND_PC_T 'mmp1 will revert to the old behaviour and gives a quick way of fixing any broken proof scripts. Glad to see that has been fixed. I have stumbled on that one every so often for years but never got around to looking into it. Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
