Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] export_code ... checking


view this post on Zulip Email Gateway (Aug 19 2022 at 16:48):

From: Christian Sternagel <c.sternagel@gmail.com>
Dear code export experts,

do I assume correctly that

export_code f1 ... fN checking

can be used to "check" whether code generation "works" (at least to some
extend) for constants f1 ... fN. If so, is it an unofficial feature that
shouldn't be used in production code?

cheers

chris

view this post on Zulip Email Gateway (Aug 19 2022 at 16:50):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Christian,

it is fine to use. It does juts check whether the generated code
compiles. Recently Andreas has devised other mechanisms to really check
what the code does.

Cheers,
Florian
signature.asc


Last updated: Apr 30 2024 at 01:06 UTC