Failure of AFP/Go_Test_Slow

[Florian Haftmann]

See now 
https://foss.heptapod.net/isa-afp/afp-devel/-/commit/b1295207946a90e2c347c43f08518f4e222ac7d3

After so many years of unnoticed accumulation of various ambitious code 
generation extensions over the AFP, some rearrangement of elementary 
material in the distribution raise this now to the surface.

Cheers,
	Florian

Am 31.01.25 um 18:59 schrieb Makarius:
> 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0xA707172232CFA4E9.asc
Type: application/pgp-keys
Size: 22777 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250131/06344bae/attachment-0001.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250131/06344bae/attachment-0001.sig>