David,
On 21 Dec 2014, at 19:25, David Topham <dtop...@gmail.com> wrote:
> 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.
You have to put entries in what we call “view file” to tell the tools how to
process text after =C. See Section 6.1.9 of usr001.pdf.
> 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 and its support
> for literate programming.
Thanks for that.
Regards,
Rob.
>
> 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
