[isabelle-dev] Odd name space problem in quickcheck or codegen (due to change in typedef)

[Dmitriy Traytel]

Maybe a guess in the blue, but here is what grep tells me:

~$ grep base_name ~/isabelle/src/HOL/Tools/ -r | grep Quick
/Users/traytel/isabelle/src/HOL/Tools//Quickcheck/abstract_generators.ML:    val name = Long_Name.base_name tyco

I have not investigated further.

Dmitriy

> On 27 Feb 2016, at 19:36, Makarius <makarius at sketis.net> wrote:
> 
> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev