[isabelle-dev] Admin/components/README.md
Isabelle/36e33d227bf0 now provides Admin/components/README.md as merged and updated version of former PLATFORMS + README in that directory. Using Markdown makes it look more fancy, but that is also difficult to do properly, because there are too many Markdown standards. This version is meant to work for VSCode and Phabricator, e.g. see the bottom of https://isabelle-dev.sketis.net/source/isabelle/browse/default/Admin/components/;36e33d227bf0 Concerning the text, the main addition is: """ ### Repeatable component builds ### Historically, Isabelle components have often been assembled manually, packaged as `.tar.gz` and uploaded to the administrative directory. This model no longer fits the typical complexity of multi-platform tools. The current quality standard demands a separate tool in Isabelle/Scala, to build a component in a repeatable manner: e.g. see `isabelle component_jdk` or `isabelle component_e` with sources in `src/Pure/Admin`. Such tools often require a Unix platform (Linux or macOS), or the specific platform for which the target is built. In the latter case, the component build tool is run manually in each operating-system context, using the base-line versions specified above (e.g. via Docker); all results are assembled into one big `.tar.gz` archive. Multi-platform tools also require thorough testing on all platforms: base-line and latest versions. It "works for me on my system" is not sufficient for the general public. """ Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Towards Isabelle2024-RC1
Dear Isabelle contributors, we have approx. 10 days left until Isabelle2024-RC1. That is the first public release candidate, and there is usually time until RC2/RC3 to finalize everything. See also https://isabelle-dev.sketis.net/phame/post/view/76/release_candidates_for_isabelle2024 Now is a good point to update CONTRIBUTORS and NEWS: the headline says "Isabelle NEWS -- history of user-relevant changes", or seen from a different angle: a change that is not user-relevant is hardly relevant at all. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Timing for AFP/CakeML_Codegen
On 25/03/2024 13:08, Makarius wrote: On 25/03/2024 11:48, Tobias Nipkow wrote: 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. I did not see any changeset ids in that private threads. Looking more closely, here they are: AFP/fccdd28b5d84 which says "adapted to Isabelle/84a7a0029c82". You had to look more closely, i.e. follow the link I posted. Tobias Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Timing for AFP/CakeML_Codegen
On 25/03/2024 11:48, Tobias Nipkow wrote: 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. I did not see any changeset ids in that private threads. Looking more closely, here they are: AFP/fccdd28b5d84 which says "adapted to Isabelle/84a7a0029c82". Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Timing for AFP/CakeML_Codegen
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-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Timing for AFP/CakeML_Codegen
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. 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-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
