Re: [isabelle] Ctrl-Click on abbreviation from locale in image jumps to begin of context



On Thu, 5 Dec 2013, Makarius wrote:

where the script SML/build.sh looks as follows (it creates a test driver for the exported code, compiles it with polyml and cc to produce a stand-alone executable, such that the run function can then execute it.

#! /bin/bash
POLYHOME=~/.isabelle/contrib/polyml-5.5.0-3/x86_64-linux/
POLYLIB=${POLYHOME}

The script makes many assumptions about the particular operating system environment. I did not manage to run it myself yet.

After some more tinkering with the script, it somehow works for me with polyml-5.5.0-3, using the following in $ISABELLE_HOME_USER/etc/settings:

ML_PLATFORM=x86_64-linux
ML_HOME="$HOME/.isabelle/contrib/polyml-5.5.0-3/$ML_PLATFORM"
ML_SYSTEM=polyml-5.5.0
ML_OPTIONS="-H 1000 --gcthreads 4"
ML_SOURCES="$ML_HOME/../src"

I've run the build.sh either via "isabelle env ..." in the shell or via
ML {* Isabelle_System.bash ...*}, which should provide the same process environment in both situations.


Note that David Matthews changed the ways of Poly/ML batch compilation in Poly/ML 5.5.1, which is bundled with Isabelle2013-1 and Isabelle2013-2 (uniformly for all release candidates). The new polyc script might actually help to make this more robust.

For now, I merely need a confirmation that the issues is just one of local settings, not due to any change in the long chain of release candidates.


	Makarius

Attachment: build.sh
Description: Bourne shell script



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.