Dear all,
I use Isabelle to generate ML code from my formalisation in Isabelle. When I try to load the output ML file in Poly/ML 5.4, I get the following exception:
Exception- InternalError: jump too large raised while compiling
Exception- Fail "Exception- InternalError: jump too large raised while compiling" raised
It occurs when Poly/ML processes a structure with a large function definition (2750 lines of ML code). The same error occurs with Poly/ML 5.3.
What could I do to avoid this error? Are there any options to Poly/ML that allow larger jumps? Changing the code itself is difficult as it is automatically generated. If it helps, I can provide the ML file.
Regards, Andreas
On 18/02/2011 08:54, Andreas Lochbihler wrote:
Dear all,
I use Isabelle to generate ML code from my formalisation in Isabelle. When I try to load the output ML file in Poly/ML 5.4, I get the following exception:
Exception- InternalError: jump too large raised while compiling
Exception- Fail "Exception- InternalError: jump too large raised while compiling" raised
It occurs when Poly/ML processes a structure with a large function definition (2750 lines of ML code). The same error occurs with Poly/ML 5.3.
What could I do to avoid this error? Are there any options to Poly/ML that allow larger jumps? Changing the code itself is difficult as it is automatically generated. If it helps, I can provide the ML file.
This looks like a bug. Could you send me the file. I assume this is X86. Is it 32-bit or 64-bit?
David
-
andreas.lochbihler＠kit.edu -
David.Matthews＠prolingua.co.uk