1. I wish to install Poly/ML 4.1.3 on Linux. Since we don't usually install from RPMs, I first downloaded and unpacked the tar file of the binary release. With the files in a single directory, ./polyml worked fine:
$ ls -l total 4152 -rwxr-xr-x 1 john staff 3653632 Sep 30 15:48 DB413Release lrwxrwxrwx 1 john staff 12 Sep 30 15:48 ML_dbase -> DB413Release -rwxr-xr-x 1 john staff 586235 Sep 30 2002 poly $ ./poly Poly/ML RTS version I386-4.1.3 (13:57:33 Sep 30 2002) Copyright (c) 2002 CUTS and contributors. Running with heap parameters (h=10240K,ib=2048K,ip=100%,mb=6144K,mp=20%) Mapping ./ML_dbase Poly/ML 4.1.3 Release
but when I tried placing the DB413Release database file (and its symbolic link ML_dbase) in a) /usr/local/lib/poly and b) /usr/lib/poly. (Experiment shows me that the search path is: .:/usr/local/lib/poly:/usr/lib/poly - it would be good if the web page http://www.polyml.org/download.html mentioned this under "Tar-ed archives".) I found that DB413Release had to be writeable (nothing to do with where I put it, of course, just the file permissions I used):
$ ./poly Poly/ML RTS version I386-4.1.3 (13:57:33 Sep 30 2002) Copyright (c) 2002 CUTS and contributors. Running with heap parameters (h=10240K,ib=2048K,ip=100%,mb=6144K,mp=20%) WARNING:/usr/local/lib/poly/ML_dbase: Write permission denied. WARNING:/usr/local/lib/poly/ML_dbase: Opened for reading only. Mapping /usr/local/lib/poly/ML_dbase Poly/ML 4.1.3 Release
Does this matter? If so, if the database must be generally writeable, I think that this is rather unfortunate.
2. I'd really like to be able to put the database somewhere else. (We have the convention of placing installations of application software in version-specific sub-directories of /usr/local/pkg - e.g. PKG= /usr/local/pkg/polyml-$VERSION/, and any library files in ./lib.) In order to do this, I recompiled from source. One aspect of this wasn't immediately obvious to me.
Perhaps the web page http://www.polyml.org/download.html should say "You may alter the DEFAULT_POLYPATH assignment in driver/configure to indicate where you will place the DB413Release file and the link ML_dbase." before "To build the poly binary download the driver, unpack it and then type: cd driver; ./configure; make
Then, after "Then run poly ML_dbase < mlsource/BuildAll.sml", add:
"Finally, copy DB413Release into the directory you have specified in the driver/configure file and link DB413Release to ML_dbase. The poly(1) command should locate it. There is no need to copy anything else from the source." (If the last is true!)
3. There are no Unix manual pages for Poly/ML, either for the command or for the library routines. I'd write some, but I think the developers will know best what to write. The Linux manual page man(7) explains the format best, I've found.
John A. Murdie Department of Computer Science University of York
John,
Hello again! I can help a little with 1 and 3.
On Tuesday, September 30, 2003, at 05:36 pm, John Murdie wrote:
- I wish to install Poly/ML 4.1.3 on Linux. Since we don't usually
install from RPMs, I first downloaded and unpacked the tar file of the binary release. With the files in a single directory, ./polyml worked fine: ... $ ./poly Poly/ML RTS version I386-4.1.3 (13:57:33 Sep 30 2002) Copyright (c) 2002 CUTS and contributors. Running with heap parameters (h=10240K,ib=2048K,ip=100%,mb=6144K,mp=20%) WARNING:/usr/local/lib/poly/ML_dbase: Write permission denied. WARNING:/usr/local/lib/poly/ML_dbase: Opened for reading only. Mapping /usr/local/lib/poly/ML_dbase Poly/ML 4.1.3 Release
Does this matter?
No. In fact, so far, it hasn't reported an error, but it will when it reads end-of-file.
If so, if the database must be generally writeable, I think that this is rather unfortunate.
The master database does not need to be writable. It looks like an error when you run poly on a read-only database and terminate the session with an end-of-file, but it isn't. You will find when you use Poly/ML to build ProofPower that our mods to the read-eval-print loop bypass the automatic attempt to save the state in the database that is causing the apparent error.
- There are no Unix manual pages for Poly/ML, either for the command
or for the library routines. I'd write some, but I think the developers will know best what to write. The Linux manual page man(7) explains the format best, I've found.
As a workaround, poly -? will tell you about most of the options (I think some recent options to do with minimum and maximum database sizes aren't in there yet).
Over to David for the real facts ...
Regards,
Rob.
-
john＠cs.york.ac.uk -
rda＠lemma-one.com