c.sternagel at gmail.com
Tue Aug 6 09:38:17 CEST 2013
(Almost) everything back. I merely stumbled across a known issue (which
in hindsight I vaguely remember, but I did not find the corresponding
First I had to increase unify_search_bound (otherwise I obtained an
error as described in my previous email). What I did *not* notice
however, was the following message at the end of a very long trace (in
Tracing paused. Stop, or continue with next 100, 1000, 10000 messages?
So, actually jEdit was just waiting for my input and not computing for
hours (as I thought; I should have observed that from the missing scream
of my laptops fan).
By setting "unify_trace_bound" to the same value for which
"unify_search_bound" succeeded, everything was fine again.
Sorry for the false alarm.
On 08/06/2013 02:40 PM, Christian Sternagel wrote:
> Dear all,
> I'm currently checking IsaFoR  against the repository versions of
> Isabelle (8d8cb75ab20a) and the AFP (05436df687d1). Doing so, I stumbled
> across a "partial_function" definition that worked with Isabelle2013 but
> aborts now with a "Unification bound exceeded".
> Is anybody aware of changes in "partial_function" or unification (or
> somewhere I didn't think of) that could explain this?
> The general shape of the function (which is employed to parse XML into
> an internal datatype) is:
> partial_function (parse_result)
> "parser x y = xml1element ''tag name'' (xml_options [
> (''tag name 1'', parser_1),
> (''tag name 2'', parser_2,
> (''tag name N'', parser_N)
> ]) ..."
> where some of the "parser_i" use "parser" recursively. Currently we have
> around 20 parsers in the above list and the error disappears if I reduce
> that to 14 (with "unify_search_bound = 90").
> If anybody has the energy to look at the real code ;) see , theory
> CPF_Parser.thy, partial function "xml2dp_termination_proof". You will
> also have to apply a patch from my local patch queue (which is
> attached), since the "official" repository is for Isabelle2013.
>  http://cl-informatik.uibk.ac.at/software/ceta/
>  http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR
More information about the isabelle-dev