[isabelle-dev] Odd name space problem in quickcheck or codegen (due to change in typedef)
Makarius
makarius at sketis.net
Sat Feb 27 19:36:34 CET 2016
On Sat, 27 Feb 2016, Florian Haftmann wrote:
> Are you still close enough to obtain an ML traceback? It will take some
> time for me to analyze this.
The exception trace (produced with polyml-5.3.0) points to
src/HOL/Tools/Quickcheck/random_generators.ML: compile_generator_expr_raw
/ iterate_and_collect. It think it is coming from "compile" defined as
Code_Runtime.dynamic_value_strict.
It is very difficult to figure out where it really happens, due to all
these indirections of Random_Engine.run etc.
Makarius
More information about the isabelle-dev
mailing list