On 15/12/2017 18:41, Makarius wrote:
On 15/12/17 17:46, David Matthews wrote:
On 15/12/2017 16:15, Makarius wrote:
* The polyc script cannot handle directory names with spaces, e.g. the
main "prefix".
I guess it would need some extra quotation. Do you want to propose a fix?
See the included change: my very first commit produced with git (with
VSCode and gitk).
Thanks. I'll have a look at that.
* Instead of insisting in hardwired directory locations it should be
possible to refer to the relative location of the polyc itself. In GNU
bash I am using THIS="$(cd "$(dirname "$0")"; pwd)" -- it is unclear to
me how to do it in /bin/sh.
The paths are set from the installation directories in configure i.e.
where the binaries and libraries are to be installed. It's possible to
set the library and binary directories independently so there's no
necessary relationship between them.
The above change might already be sufficient for that: isabelle
build_polyml merely needs to change /bin/sh into bash and make the
prefix relative. This will allow users of Isabelle to use the bundled
Poly/ML polyc, even though it is not directly relevant for Isabelle --
see also
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-February/msg00144.html
I don't think you can give configure anything but absolute paths but
when I'm testing I usually set --libdir, --bindir and --mandir to the
same directory so everything ends up in the same place. The only case
where I've had a problem is with shared libraries in Msys/Mingw where
libtool insists on putting the DLL in "libdir/../bin".
I see further references to the install dir in:
pkgconfig/polyml.pc
libpolymain.la
libpolyml.la
Are these relevant for polyc?
No. polyml.pc is only used if you have pkg_config. The other two are
only used by libtool as far as I'm aware.
David
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
