(Almost) everything back. I merely stumbled across a known issue (which
in hindsight I vaguely remember, but I did not find the corresponding
thread).
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
jEdit):
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.
cheers
chris
On 08/06/2013 02:40 PM, Christian Sternagel wrote:
Dear all,
I'm currently checking IsaFoR [1] 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)
...
where
"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 [2], 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.
cheers
chris
[1] http://cl-informatik.uibk.ac.at/software/ceta/
[2] http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
