[isabelle-dev] NEWS: isabelle go_setup

[Makarius]

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