Re: [isabelle] Recommended use of try and try0



Hi Gottfried,

> What is this "global timing"?
> 
> I know how to use "min" to check the timing of metis proofs, and I now see that try0 and try give some timing information. But how do I check the timing of proofs in general?
> 
> I found this in the mailing list archives:
> 
>    ML_command "Toplevel.timing := true"

I think that's what it is. I'm still using Proof General, and there it's activated by going to "Isabelle > Settings > Global Timing".

> When I put that in, the Isar commands have an orange line under them. If I hover over them, some give timing information, and some don't. If I change "by" to "apply", then I get timing information, but "by" by itself doesn't give any timing information.

I don't know what the feature looks like in jEdit.

> This helps a lot. Is there something special I'm supposed to be doing to use it?

I don't know. I use it if I want a background theory to load faster, to find out whether "blast" or "simp" is best.

Cheers,

Jasmin





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