[isabelle-dev] NEWS: isabelle go_setup

Makarius makarius at sketis.net
Wed Mar 27 23:47:48 CET 2024


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



More information about the isabelle-dev mailing list