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



Hi Florian,

thanks for your answers. 

>> - The most tedious update task was changing all the occurrences of “def”
>>   into “define”. 
> 
> This coincides with my personal experience; but maybe it appears less
> tedious when writing new proofs instead of migrating existing ones.

That might be the case. 

>> - 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)?

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

>> - 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”?

> For the longer story, maybe we could have a phone chat on that issue?

That would be nice, but first I also want to discuss this issue here in Innsbruck
to get a clear idea on possible actions and consequences. And this discussion won’t
happen this week. 

Cheers,
René


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