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 <[email protected]> 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 <[email protected]> wrote: >> >> David, >> >> > On 17 Dec 2014, at 00:19, David Topham <[email protected]> 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 <[email protected]> wrote: >> > David, >> > >> > On 16 Dec 2014, at 16:25, David Topham <[email protected]> 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 <[email protected]> wrote: >> >> David, >> >> >> >> > On 15 Dec 2014, at 23:43, David Topham <[email protected]> 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 <[email protected]> >> wrote: >> >> > David, >> >> > >> >> > >> >> >> On 15 Dec 2014, at 22:24, David Topham <[email protected]> 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 >> >> [email protected] >> >> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com >> > >> > <build.log>_______________________________________________ >> > Proofpower mailing list >> > [email protected] >> > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com >> >>
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
