Email Gateway (Mar 26 2024 at 21:17): Email Gateway (Mar 26 2024 at 21:17):From: Makarius <makarius@sketis.net>
* System *
Example:
isabelle go_setup
isabelle go env
isabelle go
This refers to Isabelle/ce9b649ee2dd. It is analogous to "isabelle dotnet_setup".
The motivation is to support AFP/Go from AFP/aafd2b24370d, and maybe to see
some tests within the session using 'compile_generated_files' (e.g. see
AFP/Buchi_Complementation), guarded by [condition = ISABELLE_GOEXE] in the
ROOT file.
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).
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Mar 27 2024 at 22:02):From: Makarius <makarius@sketis.net>
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-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Mar 27 2024 at 22:46):From: Makarius <makarius@sketis.net>
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-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Mar 27 2024 at 22:48):From: Makarius <makarius@sketis.net>
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-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Mar 28 2024 at 08:40):From: Fabian Huch <huch@in.tum.de>
Side note: there is a stop (and start) button if you log in to the
Jenkins using your TUM credentials.
Fabian
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Mar 28 2024 at 09:56):From: Makarius <makarius@sketis.net>
Thanks, I managed to sign-in.
I did not stop anything, because it now looks OK: tests still running, but
"isabelle go_setup" appears to have worked properly.
Side note: I was not fully aware that the "continuous-integration" has
degraded into a "nightly-build". It is high time to roll out new hardware and
use the distributed build setup --- we have a few weeks left to do the final
polishing until Isabelle2024-RC2/RC3.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Apr 27 2024 at 20:14 UTC