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
