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). >> * 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 see further references to the install dir in: pkgconfig/polyml.pc libpolymain.la libpolyml.la Are these relevant for polyc? Makarius
From a8a6536a6a308565f1a056969104dadfba653586 Mon Sep 17 00:00:00 2001 From: Makarius <makar...@sketis.net> Date: Fri, 15 Dec 2017 19:24:06 +0100 Subject: More robust shell script: allow spaces in directory names. diff --git a/polyc.in b/polyc.in index adaa586..e460305 100755 --- a/polyc.in +++ b/polyc.in @@ -1,14 +1,14 @@ #! /bin/sh -prefix=@prefix@ -exec_prefix=@exec_prefix@ -BINDIR=@bindir@ -LINK=@CXX@ -LIBDIR=@libdir@ +prefix="@prefix@" +exec_prefix="@exec_prefix@" +BINDIR="@bindir@" +LINK="@CXX@" +LIBDIR="@libdir@" LIBS="@dependentlibs@" CFLAGS="@polyc_CFLAGS@" DEFAULT_COMPILER="${BINDIR}/poly" -COMPILER=${DEFAULT_COMPILER} +COMPILER="${DEFAULT_COMPILER}" # Extra options for Windows. config.status sets these conditionals to either "" or "#". @@ -25,27 +25,27 @@ COMPILER=${DEFAULT_COMPILER} # Msys passes the Windows TEMP in temp (lower case) # On other systems allow TMPDIR to override /tmp. -@NATIVE_WINDOWS_TRUE@TEMPORARYDIR=${temp:-/tmp} -@NATIVE_WINDOWS_FALSE@TEMPORARYDIR=${TMPDIR:-/tmp} +@NATIVE_WINDOWS_TRUE@TEMPORARYDIR="${temp:-/tmp}" +@NATIVE_WINDOWS_FALSE@TEMPORARYDIR="${TMPDIR:-/tmp}" # Extra options for Mac OS X @MACOSLDOPTS_TRUE@EXTRALDFLAGS="-Wl,-no_pie" -TMPOBJFILE=${TEMPORARYDIR}/polyobj.$$.$SUFFIX +TMPOBJFILE="${TEMPORARYDIR}/polyobj.$$.$SUFFIX" trap 'rm -f "$TMPOBJFILE"' 0 compile() { - echo "val () = use (List.nth(CommandLine.arguments(), 2)); val () = PolyML.export(List.nth(CommandLine.arguments(), 3), main);" | ${COMPILER} -q --error-exit "$1" "$2" + echo "val () = use (List.nth(CommandLine.arguments(), 2)); val () = PolyML.export(List.nth(CommandLine.arguments(), 3), main);" | "${COMPILER}" -q --error-exit "$1" "$2" } link() { if [ X"$2" = "X" ] then - ${LINK} ${EXTRALDFLAGS} ${CFLAGS} "$1" -L${LIBDIR} -Wl,-rpath,${LIBDIR} -lpolymain -lpolyml ${LIBS} + "${LINK}" ${EXTRALDFLAGS} ${CFLAGS} "$1" "-L${LIBDIR}" "-Wl,-rpath,${LIBDIR}" -lpolymain -lpolyml ${LIBS} else - ${LINK} ${EXTRALDFLAGS} ${CFLAGS} "$1" -o "$2" -L${LIBDIR} -Wl,-rpath,${LIBDIR} -lpolymain -lpolyml ${LIBS} + "${LINK}" ${EXTRALDFLAGS} ${CFLAGS} "$1" -o "$2" "-L${LIBDIR}" "-Wl,-rpath,${LIBDIR}" -lpolymain -lpolyml ${LIBS} fi } @@ -112,8 +112,8 @@ done case "$compileonly" in yes) if [ "x$outputfile" = "x" ]; then - basename=${sourcefile##*/} - outputfile=${basename%.*}.o + basename="${sourcefile##*/}" + outputfile="${basename%.*}.o" fi compile "$sourcefile" "$outputfile" ;;
_______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml