Re: [isabelle] Profiling time?



On 27/05/2021 14:50, Florian Haftmann wrote:
> I am still somehow lost on how to actually apply profiling
> 
> I have defined a dedicated session »profile« that I want to profile.
> 
> But after a
> 
> 	isabelle build -o profiling=allocations profile
> 
> neither
> 
> 	isabelle profiling_report
> 
> nor the slightly more explicit
> 
> 	isabelle profiling_report heaps/polyml-5.8.2_x86_64_32-linux/log/profile.gz
> 
> emit anything.

This actually does not quite work in Isabelle2021, due to the change of the
build process to use a PIDE session: messages end up elsewhere.

For the next release, I have reworked the overall setup, see
https://isabelle-dev.sketis.net/phame/post/view/39/reactivated_ml_profiling

	Makarius





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