Re: [isabelle] A short report on updating IsaFoR to Isabelle 2018 RC0
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and