Re: [isabelle-dev] NEWS: isabelle go_setup
On 27/03/2024 23:01, Makarius wrote: This shows that proper multi-platform support is not optional. Side-remark: Windows appears to work properly (Isabelle/308ccc1ef982 + AFP/1699d5f4b11d), but this was only a quick manual test: $ isabelle build -d '$AFP' -c Go_Test_Quick Finished Go_Test_Quick (0:00:27 elapsed time) diff -r 1699d5f4b11d thys/Go/test/quick/RBT_Test.thy --- a/thys/Go/test/quick/RBT_Test.thy Wed Mar 27 22:19:56 2024 +0100 +++ b/thys/Go/test/quick/RBT_Test.thy Wed Mar 27 23:45:18 2024 +0100 @@ -21,6 +21,6 @@ module_name RbtTest -export_code delete_list tree_from_list join invc trees_equal t1 checking Go? +export_code delete_list tree_from_list join invc trees_equal t1 checking Go end Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: isabelle go_setup
On 27/03/2024 23:01, Makarius wrote: This shows that proper multi-platform support is not optional. Side-remark: Windows appears to work properly (Isabelle/308ccc1ef982 + AFP/1699d5f4b11d), but this was only a quick manual test: diff -r 1699d5f4b11d thys/Go/test/quick/RBT_Test.thy --- a/thys/Go/test/quick/RBT_Test.thy Wed Mar 27 22:19:56 2024 +0100 +++ b/thys/Go/test/quick/RBT_Test.thy Wed Mar 27 23:45:18 2024 +0100 @@ -21,6 +21,6 @@ module_name RbtTest -export_code delete_list tree_from_list join invc trees_equal t1 checking Go? +export_code delete_list tree_from_list join invc trees_equal t1 checking Go end Finished Go_Test_Slow (0:03:10 elapsed time) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: isabelle go_setup
On 26/03/2024 22:16, Makarius wrote: Another motivation is to get rid of the unfinished experiment from https://isabelle-dev.sketis.net/rISABELLE8347ffa1f92c (the log should explain the purpose, but apparently there is none). I've now found out that Jenkins would have needed the Admin/components/go setup, but it is already gone: see Isabelle/38bbc2ff3c24 and Isabelle/a2d15ad6877a. (I did ask about that before, see the old thread "Status of Isabelle "go" component" from 25-Aug-2023.) So while Jenkins is running (How many hours? Without stop button?) -- here are my attempts to get it back into proper shape: Isabelle/a0210a24b547 -- dummy Admin/components/go to avoid crash of Jenkins Isabelle/da323d3d7570 -- proper "isabelle go_setup" for Jenkins AFP/1699d5f4b11d -- proper Go setup, following Isabelle/da323d3d7570 There appears to be some Jenkins "shadow configuration" that uses Admin/components/go. Or did I overlook that in the regular Isabelle/Admin setup? I would like to revert Isabelle/a0210a24b547 again. From the above AFP change, I also learned that the "Go" session does have some tests of the compiler, but if that is absent the test succeeds without any feedback! Please consider getting this right, i.e. with theory options condition = ISABELLE_GOEXE and a strict test inside the theory. The HOL-Codegenerator_Test may also serve as successful example --- after some years of tinkering --- but it has its own custom-commands with extra complexity. Note that in Isabelle/308ccc1ef982 the regular AFP nightly build now has ISABELLE_GO_SETUP=true to test that properly. The test machine happens to be on macOS right now, because the Linux LRZ nodes are no longer available. This shows that proper multi-platform support is not optional. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Admin/components/README.md
On 25/03/2024 20:03, Makarius wrote: Isabelle/36e33d227bf0 now provides Admin/components/README.md as merged and updated version of former PLATFORMS + README in that directory. Here is an updated version: https://isabelle-dev.sketis.net/source/isabelle/browse/default/Admin/components/;ebd988ee1d57 In particular: """ ### Dynamic setup of large components ### An alternative approach, especially for components that are very large and/or rarely used, is to provide an Isabelle setup tool that interested users may run for themselves. This works particularly well for software products that have their own "store" of downloadable artifacts. For example, see `isabelle dotnet_setup` as defined in `src/Pure/Tools/dotnet_setup.scala`. """ Isabelle component management has become and art and an industry. There is more to say, especially for automated build setup (e.g. Setup_Tool service classes), but the text is already rather long. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
