update for Isabelle2024

Dockerfile

@@ -1,18 +1,13 @@
-FROM docker.io/makarius/isabelle:Isabelle2023
-
-USER root
-RUN apt-get -y update && \
-  apt-get install -y golang && \
-  apt-get clean && \
-  rm -rf /var/lib/apt/lists/*
-USER isabelle
+FROM docker.io/makarius/isabelle:Isabelle2024
 
 COPY --chown=isabelle:users ROOT *.ML *.thy go-code-gen/
 COPY --chown=isabelle:users document go-code-gen/document/
 COPY --chown=isabelle:users test go-code-gen/test/
 
-ENV ISABELLE_GO=/usr/bin/go
+ENV PATH "$PATH:/home/isabelle/Isabelle/bin"
+
+RUN isabelle go_setup
 
-ENTRYPOINT Isabelle/bin/isabelle build -v -e -D go-code-gen && \
+ENTRYPOINT isabelle build -v -e -D go-code-gen && \
   cd ./go-code-gen/test/quick/go && \
-  go test  -v ./Interface
+  isabelle go test -v ./Interface

README.md

@@ -4,7 +4,7 @@
 [![arXiv](https://img.shields.io/badge/arXiv-2310.02704-b31b1b.svg)](https://arxiv.org/abs/2310.02704)
 
 This repository contains a standalone code generation target for the Go
-programming language for use with Isabelle2023.
+programming language for use with Isabelle2024.
 
 To use it, simply import the `Go` session defined herein into your own development,
 and import the `Go_Setup` theory. Code can then be exported in the usual way with
@@ -18,7 +18,7 @@ which produces code that can be used from Go.
 ## Trying it out (the quick version)
 
 This repository contains a test session `Go_Test_Quick`. If you have
-Isabelle2023 installed, just run the following command:
+Isabelle2024 installed, just run the following command:
 
 ~~~shell
 isabelle build -v -e -d . Go_Test_Quick
@@ -76,6 +76,28 @@ isabelle build -v -e -D .
 If run this for the first time, it may take quite a while to complete (half an
 hour on a slow machine).
 
+## Bundled Go version
+
+Since Isabelle2024, the Isabelle distribution ships with a script to
+automatically install Go. If you prefer to only manually install Isabelle, but
+not Go, this is how you can get started:
+
+~~~shell
+isabelle go_setup
+~~~
+
+Afterwards, you can run the bundled Go version as follows:
+
+~~~shell
+isabelle go
+~~~
+
+The latter command behaves exactly like a direct invocation of `go`.
+
+The Docker image contained in this repository (see below) uses this bundled
+version. Due to Go's backwards compatibility, any version of Go including or
+after 1.18 should work.
+
 ## Using Docker/Podman
 
 If you do not want to install Isabelle or Go, you can also run the test

ROOT

@@ -11,7 +11,7 @@ session Go_Test_Quick in "test/quick" = Go +
   options [timeout = 300]
   sessions
     "HOL-Data_Structures"
-  theories [document = false, condition = "ISABELLE_GO"]
+  theories [document = false, condition = ISABELLE_GOEXE]
     RBT_Test
   export_files [3]
     "*:code/export1/**"
@@ -24,7 +24,7 @@ session Go_Test_Slow in "test/slow" = "HOL-Library" +
     "HOL-Number_Theory"
     "HOL-Data_Structures"
     "HOL-Examples"
-  theories [document = false, condition = "ISABELLE_GO"]
+  theories [document = false, condition = ISABELLE_GOEXE]
     Candidates
     Generate
-    Generate_Binary_Nat
+    Generate_Binary_Nat