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/ 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

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_OPTIONS="-H 1000 --gcthreads 4"

I've run the 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.


Description: Bourne shell script

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