polycスクリプト

Isabelleの ./conrib/polyml-5.6-1/x86-windows/polyc を手直しして ~/bin/polyc32 とした。動くようになったが、色々とまだ不便。

#!/bin/sh
IsabelleHome=/c/Installed/Isabelle2016/
PolymlVer=5.6-1
Missing=missing
PolySuffix=poly

prefix=${IsabelleHome}/contrib/polyml-${PolymlVer}
exec_prefix=${prefix}
BINDIR=${exec_prefix}/x86-windows
LINK=g++
LIBDIR=${exec_prefix}/x86-windows
LIBS="-lpthread  -lgmp-10 -lgdi32 -lws2_32 -lstdc++ -lgcc_s -lgcc  "
CFLAGS="-O3 -mthreads -I../libffi/include time.o"


DEFAULT_COMPILER="${BINDIR}/poly"
COMPILER=${DEFAULT_COMPILER}

EXTRALDFLAGS="-Wl,-u,_WinMain@16 -Wl,--large-address-aware "

#EXTRALDFLAGS+="-mwindows"
EXTRALDFLAGS+="-mconsole"

SUFFIX="obj"

# Msys passes the Windows TEMP in temp (lower case)
# On other systems allow TMPDIR to override /tmp.
TEMPORARYDIR=${temp:-/tmp}

TMPOBJFILE=${TEMPORARYDIR}/polyobj.$$.$SUFFIX
trap 'rm -f "$TMPOBJFILE"' 0

compile()
{
    echo "use (List.nth(CommandLine.arguments(), 2)); 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}
    else
        ${LINK} ${EXTRALDFLAGS} ${CFLAGS} "$1" -o "$2" \
                -L${LIBDIR} -Wl,-rpath,${LIBDIR} -lpolymain -lpolyml ${LIBS}
    fi
}

printhelp()
{
    echo "Usage: polyc [OPTION]... [SOURCEFILE]"
    echo Compile and link a Standard ML source file with Poly/ML.
    echo
    echo "   -b poly      Use 'poly' as compiler instead of ${DEFAULT_COMPILER}"
    echo "   -c           Compile but do not link.  The object file is written to the source file with .$SUFFIX extension."
    echo "   -o output    Write the executable file to 'output'"
    echo "   --help       Write this text and exit"
    exit
}

usage()
{
    echo "$1"
    echo "Usage: polyc [OPTION]... [SOURCEFILE]"
    exit 1
}

checkml()
{
    extension="${1##*.}"
    case "$extension" in
        sml|ML)
             return 0 ;;
        o|obj)
             return 1;;
        *)
             test -r "$1" && file -b "$1" | grep -q text ;;
    esac
}

sourcefile=""
outputfile=""
compileonly="no"

while [ $# -gt 0 ]
do
    case "$1" in
        --help)
            printhelp ;;
        -b)
            shift
            [ $# -eq 0 ] && usage "Expected file name after -b"
            COMPILER="$1";;
        -c) compileonly="yes";;
        -o)
            shift
            [ $# -eq 0 ] && usage "Expected file name after -o"
            outputfile="$1";;
        *)
            [ X"$sourcefile" = "X" ] || usage "Only one source file name allowed"
            sourcefile="$1";;
    esac
    shift
done

[ X"$sourcefile" = "X" ] && usage "No input files"
[ -r "$sourcefile" ] || usage "Error: $sourcefile: No such file"

case "$compileonly" in
     yes)
         if [ "x$outputfile" = "x" ]; then
             basename=${sourcefile##*/}
             outputfile=${basename%.*}.${PolySuffix}
         fi
         compile "$sourcefile" "$outputfile"
         ;;
     no)
         if checkml "$sourcefile"
         then
             compile "$sourcefile" "$TMPOBJFILE" && link "$TMPOBJFILE" "$outputfile"
         else
             link "$sourcefile" "$outputfile"
         fi
         ;;
esac

time.o は次のソースをgccでコンパイルしたもの。

#define _wassert ___wassert
#include <windows.h>
#include <wchar.h>
#include <signal.h>
#undef _wassert
#include <stdio.h>
#include <time.h>

void __cdecl _wassert(const wchar_t *message,
                      const wchar_t *file,
                      unsigned line)
{
    wchar_t *msgbuf = (wchar_t *)malloc(8192*sizeof(wchar_t));

    if (!file || file[0] == 0) {
        file = L"<unknown>";
    }
    if (!message || message[0] == 0) {
        message = L"?";
    }
    _snwprintf(msgbuf, 8191,
               L"Assertion failed!\n\nFile: %ws, Line %u\n\nExpression: %ws",
               file,line, message);
    OutputDebugStringW(msgbuf);
    free(msgbuf);
    abort();
}

time_t _time32(time_t *timer) {
    return time(timer);
}

struct tm * _localtime32(const time_t *timr ) {
    return localtime(timr);
}

struct tm * _gmtime32(const time_t *timer) {
    return gmtime(timer);
}

time.c と _wassert.c に分けて、.aファイルにしたほうがいいだろう。