Dear all,
shortly after I started to use PolyML (outside of Isabelle), I created
the attached bash script for compilation of executables and custom
top-levels (also there is some special treatment to reuse Isabelle's
library, which you may safely ignore). Maybe it is of use to somebody.
cheers
chris
On 04/02/2013 10:36 PM, David Matthews wrote:
On 02/04/2013 13:25, René Neumann wrote:
Am 02.04.2013 14:02, schrieb David Matthews:
This would definitly be a great help for people new to Poly/ML. When I
had to produce a standalone executable from an ML-file it took me quite
some time before figuring out how it works.
Actually it's probably not much more than
polyml --use myprogram.ML --use export.ML
Where export.ML is
PolyML.export("polyml.o", main);
OS.Process.exit OS.Process.success: unit;
Make the name of the resulting obj file a parameter and it's fine, I
think. Could look like (shell script):
polyml --use myprogram.ML <<EOF
PolyML.export("${output}", main);
EOF
Yes, of course. Having the object file name as a parameter, perhaps
defaulting to the name of the source file with ".o" on the end, was my
"much more than".
Perhaps one can also pour in the gcc-compile phase already, so it's one
step from ML-file to executable.
I don't know how that works so perhaps that's for later.
So, in summary, it should look like:
-c option: Compile a source file which must contain a function main of
type unit -> unit (or string list => unit or string list -> int ???) and
export the object file.
-o option: Used with -c to override the default object file name.
-i option: Force interactive mode. The default is interactive only if
stdin is a terminal. This controls whether to print a prompt.
--skip-first-line option: Skip the first line of the input stream. Used
with scripts with #! at the start.
Does that seem reasonable? I don't think there's much there that is
very complicated. Should some of these imply the -q option?
David
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
#!/bin/bash
POLY=poly
OPTS=`getopt -o ihto:m: --long isabelle,help,top-level,ouptut:,main: -n 'polyc'
-- "$@"`
if [ $? != 0 ] ; then echo "error when parsing command line options ..." >&2 ;
exit 1 ; fi
eval set -- "$OPTS"
usage () {
echo "usage: `basename $0` <file>"
echo " where <file> is the SML file to be used."
echo "OPTIONS"
echo "-h --help print this message"
echo "-i --isabelle set up isabelle environment"
echo "-m --main m use the ML function 'm' as main-function"
echo "-o --output b set the name of the generated binary to 'b'"
echo "-t --top-level build custom top-level"
}
while true
do
case "$1" in
-h|--help)
usage
exit 0
;;
-i|--isabelle)
export ML_SYSTEM="polyml-5.5.0" ML_PLATFORM="x86_64-linux"
shift 1
;;
-o|--output)
PROG="$2"
shift 2
;;
-m|--main)
MAIN="$2"
shift 2
;;
-t|--top-level)
TOP=1
shift 1
;;
--)
shift
break
;;
*)
echo "Internal error!"
exit 1
;;
esac
done
if [[ $# != 1 ]]
then
usage >&2;
exit 1
fi
FILE=$1
NAME=${FILE%%.*}
if [[ $PROG == "" ]]; then PROG=$NAME; fi
if [[ $MAIN == "" ]]; then MAIN="main"; fi
if [[ $TOP ]]
then
echo "PolyML.export(\"${PROG}\", PolyML.rootFunction);" | \
${POLY} --use ${FILE} && cc -o ${PROG} ${PROG}.o -lpolymain -lpolyml
else
echo "PolyML.export(\"${NAME}\", ${MAIN});" | \
${POLY} --use ${FILE} && cc -o ${PROG} ${NAME}.o -lpolymain -lpolyml
fi
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
