Failure of AFP/Go_Test_Slow

Makarius makarius at sketis.net
Fri Jan 31 18:59:50 CET 2025


After running "isabelle go_setup" it is possible to run test with 
"condition=ISABELLE_GOEXE" manually. This produces the following failure:

Go_Test_Slow FAILED (see also "isabelle build_log -H Error Go_Test_Slow")
*** Unknown statement name: "Code_Numeral.Neg"
*** At command "export_code" (line 12 of 
"$AFP/Go/test/slow/Generate_Binary_Nat.thy")
*** Unknown statement name: "Code_Numeral.Neg"
*** At command "export_code" (line 19 of "$AFP/Go/test/slow/Generate.thy")

Any clues?

This is Isabelle/9601f5582f33 + AFP/26bfca109e32.


	Makarius


More information about the isabelle-dev mailing list