Re: [isabelle] Death by tracing



I should probably add that this is not a regression. Isabelle2015 and
Isabelle2016 show the exact same behaviour.

On 06/12/16 12:32, Manuel Eberl wrote:
> Hallo,
> 
> I just noticed some odd behaviour and tracked it down to the following
> minimal example:
> 
> This expression evaluates in Isabelle/ML almost immediately:
> 
> ML â
>   map (fn _ => tracing "Foo") (1 upto 1000)
> â
> 
> This one apparently take forever:
> 
> ML â
>   map (fn _ => tracing "Foo") (1 upto 1001)
> â
> 
> Cheers,
> 
> Manuel
> 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.