[isabelle-dev] Timing for AFP/CakeML_Codegen

Tobias Nipkow nipkow at in.tum.de
Mon Mar 25 11:48:56 CET 2024



On 25/03/2024 11:38, Makarius wrote:
> Dear colleagues,
> 
> there have been private questions about recent timing information of 
> AFP/CakeML_Codegen. I am answering this publicly on the regular isabelle-dev 
> channel.
> 
> 
> The official build status results for Isabelle + AFP are available here: 
> https://isatest.sketis.net/devel/build_status/index.html
> 
> Looking briefly at CakeML_Codegen, I don't see anything suspicious for the past 
> 30 days. I've also queried the underlying database for 120 days: nothing to be 
> seen --- at least not for threads=1 that is used here.

As I pointed out in that private thread, the problem started 10 months ago with 
a partiular changeset. Since then the running times have been stable.

Tobias

> Side-remark: Just yesterday, I had to shutdown the AFP test machine (from LRZ), 
> see Isabelle/1fd5f96e1da3. I hope to find another test setup in the coming days, 
> so we will be "flying blind" briefly.
> 
> Afterwards, the nightly build will dig into old history and provide more and 
> more data points to recover the charts.
> 
> 
>      Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4950 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20240325/60f8f99e/attachment.bin>


More information about the isabelle-dev mailing list