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

Hi Rene,

> Ah, I see. I figured out that the import of > "HOL-Cardinals.Wellorder_Extension” was the reason: > > In Isabelle
2017, this transitively imports>   HOL-Cardinals.Order_Union ->
HOL.Order_Relation ->* Lattice_Syntax> > whereas in Isabelle 2018 we
have>   HOL-Cardinals.Order_Union -> Main

I currently wonder how a corresponding generic, instructive and
searchable (!) NEWS entry should look like.

>>> - The most visible impact from our side is the deletion of Code_Char.
>> 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).
> Short remark on this: we also some input files which used 8-bit characters,
> e.g., XML-files with comments having the name “René” in it.
> On these files, the current Haskell binary just crashes with a non-informative
> "Non-exhaustive patterns in function ord” error. Perhaps one can define
> ord in a way that leads to a more informative error message.
>> The short answer is: if you want to have target language string
>> literals, use type String.literal.
> Okay, this is a possible alternative, but it will become tedious for us: 
> - adjust all error messages within IsaFoR
> - adjust the XML-Parser
> - change the Show-AFP-entry and the show-class from “string” to “String.literal”?

well, if the story is about *parsing*, String.literal might not be the
ultimate solution.

Is the application tailored towards Haskell?  Then a more specific
solution could be established by mapping Isabelle/HOL's char to a really
specific Haskell type.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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