Rob, I am really enjoying learning about ProofPower and so impressed at the
amount of documentation and extra facilities that I didn't even know were
part of this program.  e.g. I have long been interested in "literate
programming" and find your approach using =SML and =TEX to be very
efficient. I read in the usr001.pdf that it is possible to add other
languages such as =C but don't quite see what I have to do to make that
work.  I tried just putting =C followed by the some C code, but got errors
from docsml that say =C is not defined.
The example is from page 56 in the section about sieve so I imagine the
info is there somewhere, but I find that section a bit difficult for me at
this early stage of learning about ProofPower. I found I can use =DUMP to
get a similar effect, however in the document =C would certainly be more
descriptive.
-Dave
p.s. I am cc'ing the literate programming group to this discussion because
I think there may be others that do not know about ProofPower
<http://www.lemma-one.com/ProofPower/index/> and its support for literate
programming.

On Fri, Dec 19, 2014 at 2:50 PM, David Topham <dtop...@gmail.com> wrote:

> Rob, Fantastic!  That was the key!  I reinstalled PolyML just to be sure
> and checked that poly and polyc worked OK, but still got same error
> building ProofPower. But I made the changes to the mkf (just xpp and hol,
> not zed) as you suggested and now it completed successfully. I had to
> install the standard Linux utilities to override BusyBox to get nroff, ed,
> and nl which are needed too. Anyway, now I can (finally) concentrate on
> learning ProofPower by looking at the tutorials on your site. If all goes
> well, I intend on using it as a supplement to teaching Discrete Math. I am
> excited to see some references to zed since I am also trying to learn to
> use Z for specifications. I appreciate your help getting me over these
> first hurdles. I use this less common distribution of Linux (TinyCore)
> since it is small enough to run within a virtual machine (I use Qemu) so
> can be carried around on a USB flash drive and run from within any
> computer! Makes it easier for students that can't install software on their
> own machines or school machines.
> -Dave
>
> On Thu, Dec 18, 2014 at 8:04 AM, Rob Arthan <r...@lemma-one.com> wrote:
>>
>> David,
>>
>> > On 17 Dec 2014, at 00:19, David Topham <dtop...@gmail.com> wrote:
>> >
>> > Maybe another non-Posix issue?  Attached is latest build attempt. This
>> time it fails
>> > trying to build processes.cpp because pthread functions are undefined...
>> > (setting OS=linux made progress, then I had to install mkfontdir
>> utility and load the Xp libraries as well before getting to the current
>> error)
>> >
>>
>> What has actually happened is that it is failing to link the slrp-ml
>> executable,
>> almost certainly because the c++ command line it is using to do this does
>> not
>> identify the location of the pthreads and various XWindows libraries that
>> are
>> used by the Poly/ML runtime library. The error message talk about
>> processes.cpp
>> and xwindows.cpp because these are the Poly/ML source files that depend on
>> these libraries. You can now use a script polyc that is supplied with
>> Poly/ML to
>> link standalone executables created with Poly/ML and it should take care
>> of locating all the libraries that are needed. If you change src/dev.mkf
>> to
>> use polyc as shown in the following diff output, then it may work.
>>
>> --- dev.mkf-    2013-08-04 15:22:21.000000000 +0100
>> +++ dev.mkf     2014-12-18 15:49:48.000000000 +0000
>> @@ -65,9 +65,7 @@
>>         PPBuild.pp'save ();
>>  SLRPSTARTCMD= \
>>         {       { echo "$(SLRPSTARTMLCMD)" | poly ; } && \
>> -               LD_RUN_PATH=$(LD_RUN_PATH) \
>> -                       c++ $(POLYLINKFLAGS) -o slrp-ml pp-ml.o \
>> -                               -L$(POLYLIBDIR) -lpolymain -lpolyml && \
>> +                       polyc -o slrp-ml pp-ml.o && \
>>                 { echo "$(SLRPMAKEDBCMD)" | slrp-ml ; } }
>>
>>
>> If that does work, then you will either need to make the same changes
>> to src/hol.mkf and src/zed.mkf, or you may just be better off downloading
>> the latest development version of ProofPower (which will become the
>> next stable release very shortly). You can find this here:
>>
>>
>> http://www.lemma-one.com/ProofPower/getting/snapshots/OpenProofPower-3.1w2.tgz
>>
>> If it does not work, then we need to look into how you managed to build
>> Poly/ML
>> since the compiler managed to link itself and it will have the same
>> library
>> dependencies.
>>
>> Regards,
>>
>> Rob.
>>
>>
>> > On Tue, Dec 16, 2014 at 1:19 PM, Rob Arthan <r...@lemma-one.com> wrote:
>> > David,
>> >
>> > On 16 Dec 2014, at 16:25, David Topham <dtop...@gmail.com> wrote:
>> >
>> >> Thanks for helping Rob,  TinyCore does have uname, and that command
>> returns "Linux".
>> >>
>> >> It uses BusyBox for shell commands and a subset of dd is supported
>> which does not have the lcase option!
>> >>
>> >
>> > Ah! I try to make the ProofPower build process only use POSIX features
>> > of the usual UN*X utilities. BusyBox’s dd is not POSIX-compliant if it
>> doesn’t
>> > support conv=lcase.
>> >
>> > xpp.mkf is the only ProofPower make file that needs this trick, so if
>> you just edit it to say
>> >
>> > OS=linux
>> >
>> > you should be able to make more progress. I will be interested to hear
>> how you get on.
>> >
>> > Regards,
>> >
>> > Rob.
>> >
>> >> (see attached)
>> >>
>> >> -Dave
>> >>
>> >> On Tue, Dec 16, 2014 at 2:02 AM, Rob Arthan <r...@lemma-one.com> wrote:
>> >> David,
>> >>
>> >> > On 15 Dec 2014, at 23:43, David Topham <dtop...@gmail.com> wrote:
>> >> >
>> >> > It is version 2.9.1w8... and here is the latest attempt (attached).
>> >> >
>> >> >
>> >> > I notice that SOLARIS is on the compile line which is not
>> true..should be LINUX perhaps?
>> >> > but how do I influence that?
>> >>
>> >> The relevant makefile (src/xpp.mkf) uses the following command to
>> determine the OS:
>> >>
>> >> uname -s | dd conv=lcase 2>/dev/null
>> >>
>> >> Is your TinyLinux installation missing uname or dd?
>> >>
>> >> By the way, at the point that this has failed, it hasn’t started
>> trying to compile any ML.
>> >>
>> >> Regards,
>> >>
>> >> Rob.
>> >>
>> >>
>> >> >
>> >> > On Mon, Dec 15, 2014 at 2:40 PM, Rob Arthan <r...@lemma-one.com>
>> wrote:
>> >> > David,
>> >> >
>> >> >
>> >> >> On 15 Dec 2014, at 22:24, David Topham <dtop...@gmail.com> wrote:
>> >> >>
>> >> >> Rob, Yes I was following the instructions in the README file and
>> did ./configure, then ./install but it failed on the line in the Makefile
>> that invoked PolyML.commit();
>> >> >>
>> >> >> I replaced that in the Makefile with:
>> >> >> PolyML.export("mypoly",PolyML.rootFunction);
>> >> >>
>> >> >> ...and it ran further, but still I have been unable to compile it
>> successfully all the way with other errors I haven't tracked down yet.  If
>> you have time, I could keep trying, and report to you what I can't figure
>> out on my own.
>> >> >
>> >> > I have copied this over to the ProofPower mailing list where we
>> should be able to answer it for you. What version have you downloaded? In
>> version 2.9.1w8, there is a spurious occurrence of PolyML.commit in
>> src/dev.mkf, but it is in a variable that is no longer used and shouldn’t
>> stop anything building.
>> >> >
>> >> > Regards,
>> >> >
>> >> > Rob.
>> >> > <build.log>
>> >>
>> >> <busybox.PNG>_______________________________________________
>> >> Proofpower mailing list
>> >> Proofpower@lemma-one.com
>> >> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
>> >
>> > <build.log>_______________________________________________
>> > 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

Reply via email to