Re: [isabelle] A short report on updating IsaFoR to Isabelle 2018 RC0



Hi Rene,

thanks for your feedback.

> - The most tedious update task was changing all the occurrences of “def” >   into “define”. In particular, the duplication of the name was
annoying,>   e.g., changing < def \<sigma> == some_exp > into < define
\<sigma> where "\<sigma> == some_exp” >.>   If possible, it would be
nice to have a short form available in Isabelle 2018 like>   it is
possible with “definition”: < define "\<sigma> = some_exp” > would be nice.

This coincides with my personal experience; but maybe it appears less
tedious when writing new proofs instead of migrating existing ones.

> - I would have expected a statement in the NEWS file >   on the necessary import of "HOL-Library.Lattice_Syntax”.

Well, this import has always been necessary. The only difference that
might have slipped in is that an existing session used to import
Lattice_Syntax and now no longer does; do you have more detail at hand
(or maybe point to a commit in IsaFoR where this had to be introduced)?

> - The most difficult update was the change of the “rewrites” and “defines” >   conditions in locale interpretations where it now does not seem
possible>   anymore, to define “rewrite"-rules that depend on newly
defined constants>   from the “defines” part. >   (I wrote a separate
e-mail to Clemens B. on this issue)

Admittedly when observing that refinement I didn't realize that the
changed syntax would have that consequence.

> - The most visible impact from our side is the deletion of Code_Char.>   The result is that our generated code became>   - 3x larger: from
2575550 bytes to 7848600 bytes>   - much less readable: compare the
previous string >          “ is symbol …” >     in the generated code
which now became>          [Char False False False False False True
False False,>           Char True False False True False True True
False,>           Char True True False False True True True False,>
     Char False False False False False True False False,>
Char True True False False True True True False, …]>     where every
character is expanded into a whole line>   - 1.5x slower on average,
when running on it on an 2359 examples (30 min before, now 45 min)

What the NEWS file announces unspectacularly as »Clarified relationship
of characters, strings and code generation« is indeed the elimination of
an inconsistency in code generation (8-bit characters in Isabelle/HOL
vs. a lot of different notions about characters in target languages).
The short answer is: if you want to have target language string
literals, use type String.literal. For the longer story, maybe we could
have a phone chat on that issue?

Cheers,
	Florian

-- 

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

Attachment: signature.asc
Description: OpenPGP digital signature



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