[isabelle-dev] Odd name space problem in quickcheck or codegen (due to change in typedef)
traytel at inf.ethz.ch
Sat Feb 27 21:57:55 CET 2016
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.
> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev