[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