Re: [isabelle] Recommended use of try and try0
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and