Email Gateway (Aug 22 2022 at 17:12): Email Gateway (Aug 22 2022 at 17:12):From: Peter Lammich <lammich@in.tum.de>
From the NEWS file for 2017:
Can please someone update the code generator tutorial Sec 2.5 (pg 12).
I spent almost half an hour being puzzled why
definition [code del]: "foo == ..."
still admitted code generation for foo.
Email Gateway (Aug 22 2022 at 17:13):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
What are you referring to exactly? The tutorial on code generation from
Isabelle2017 does not contain any »code del«.
Florian
signature.asc
Email Gateway (Aug 22 2022 at 17:13):From: Peter Lammich <lammich@in.tum.de>
I referred to pg 12 of the codegen tutorial (Isabelle2017 version):
"Normally, if constants without any code equations occur in a program,
the
code generator complains (since in most cases this is indeed an error).
[...] In order to categorise a constant into that category explicitly,
use the code
attribute with abort:"
However, if there are no code equations, the new behaviour is to handle
the constant as code-abort, and the behaviour mentioned in the first
sentence that I cited has to be forced with [[code drop: ]]
Email Gateway (Aug 22 2022 at 17:20):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,
see the attached preview for a slightly polished version.
Cheers,
Florian
preview.pdf
signature.asc
Last updated: Apr 24 2024 at 12:33 UTC