on line 20:
r ! nroff -ms help.txt
Presumably it's the '-ms' in this line, but I don't know. Any ideas
anyone?
Mark.
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
y today in Hanoi of the Viet Flyspeck workers.
It seems 7 out of 8 use 'xpp' in preference to 'emacs'. That's better than
the cat food adverts!
Regards,
Mark.
on 6/7/10 7:40 PM, Rob Arthan wrote:
>
> On 6 Jul 2010, at 10:29, Roger Bishop Jones wrote:
>
>>
OpenMotif 2.3.2 works as well.
on 7/7/10 6:56 PM, Phil Clayton wrote:
> This has been the subject of much discussion in the past... The
> solution should be as simple as using OpenMotif 2.3.1.
>
> If you're a Fedora user see my previous post:
>
>
http://lemma-one.com/pipermail/proofpower_lemma-
In fact, Roger, could you confirm that you are using OpenMotif 2.3.0?
Mark.
on 8/7/10 10:12 AM, m...@proof-technologies.com wrote:
> OpenMotif 2.3.2 works as well.
>
> on 7/7/10 6:56 PM, Phil Clayton wrote:
>
>> This has been the subject of much discussion in the past..
stions for improving the clarity or scope of
this file please contact me.
Mark.
on 10/7/10 10:06 PM, Roger Bishop Jones wrote:
> On Thursday 08 Jul 2010 11:21, m...@proof-technologies.com
> wrote:
>> In fact, Roger, could you confirm that you are using
>> OpenMotif 2.3.0?
&g
Note that instruction 4 for the ProofPower install instructions I just
posted is only for OCaml, and this will not feature in any general README
instructions.
Mark.
on 11/7/10 10:35 AM, m...@proof-technologies.com wrote:
> I'm preparing some revised instructions (attached) for install
t 'libxp6-dev') for installing ProofPower 'xpp'.
Thanks very much Roger, that was very valuable. Any more problems anyone,
please let me know.
Mark.
on 12/7/10 6:53 AM, Roger Bishop Jones wrote:
> On Sunday 11 Jul 2010 10:34, m...@proof-technologies.com
> wrote:
&g
I should have said that it should be 'libxp6' for all versions of Ubuntu,
not just Ubuntu 9.04.
Mark.
on 12/7/10 9:21 AM, m...@proof-technologies.com wrote:
> Ok - it seems it should be 'libxp6' not 'libxp'. That is, the instruction
> for ancestor package
d return:
/usr/local/bin
If it is, then you can probably get things working by doing
POLYHOME=/usr/local ./configure
Hope this helps.
Mark
on 14/3/11 12:33 PM, Marcel Oliveira wrote:
> Hi Rob,
>
> Yes, I have. I am currently trying to solve the issue with Arthur who has
bove incorporated into a normal
PP build, so that the user doesn't have to type it in? I seem to remember
there was a good reason, but I can't put my finger on it...
Mark.
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
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 wrote:
> I nearly always use Xpp with the following settings in
> $HOME/app-de
That's because ProofPower overwrites PolyML's ML structure List with its
own, for holding theory about HOL lists. I'm not sure if anything can be
done about this without alterning the ProofPower build process (and, say,
creating a copy of PolyML's List with a name not used b
e: <=>
universal quantification: !
existential quantification: ?
unique existential quantification: ?!
Mark.
On 11/03/2016 08:53, David Topham wrote:
> I am trying to do a forward proof using hypothetical syllogism
> (V_cancel_Rule)
> of this form: ~q v r, q |- r
> but get
, "subgoal package", "meson"), and to make it
an HTML file or PDF.
Many thanks to Rob and Roger for helping me with many parts of this
glossary.
Mark Adams
Proof Technologies Ltd
___
Proofpower mailing list
Proofpower@lemma-one.co
ailed
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
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
Cheers,
Mark.
On 15/06/2017 02:27, Phil Clayton wrote:
Hi Mar
oes the
log file for imp002 say?
Which log file?
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
n
(PolyML.install_pp) (PPCompiler.make_pp ["BasicError", ...]
error_pp)
end)
*** Fail: Fail "Static Errors" ***
Chers,
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 in
Hello Rob, I'm still here!
Mark.
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,
19 matches
Mail list logo
