Re: [isabelle] code del and code drop



Hi Peter,

see the attached preview for a slightly polished version.

Cheers,
	Florian

Am 07.05.2018 um 10:16 schrieb Peter Lammich:
> 
> 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: ]]
> 
> --
>   Peter
> 
> 
> 
> 
> On So, 2018-05-06 at 17:12 +0200, Florian Haftmann wrote:
>>>
>>>>
>>>> From the NEWS file for 2017:
>>> * Deleting the last code equations for a particular function using
>>> [code del] results in function with no equations (runtime abort)
>>> rather
>>> than an unimplemented function (generation time abort). Use
>>> explicit
>>> [[code drop:]] to enforce the latter. Minor INCOMPATIBILITY.
>>>
>>>
>>> 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.
>> What are you referring to exactly?  The tutorial on code generation
>> from
>> Isabelle2017 does not contain any »code del«.
>>
>> 	Florian
>>
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: preview.pdf
Description: Adobe PDF document

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.