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
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe
Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: [email protected]
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
