Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] A short report on updating IsaFoR to Isabelle ...


view this post on Zulip Email Gateway (Aug 22 2022 at 17:33):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear all,

here is a short report on my experience after updating all of IsaFoR from
Isabelle 2017 to Isabelle 2018 RC0.

Cheers,
René

view this post on Zulip Email Gateway (Aug 22 2022 at 17:33):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Rene,

thanks for your feedback.

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

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

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

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
signature.asc

view this post on Zulip Email Gateway (Aug 22 2022 at 17:33):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Hi Florian,

thanks for your answers.

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.

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

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:

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é

view this post on Zulip Email Gateway (Aug 22 2022 at 17:34):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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.

Cheers,
Florian
signature.asc


Last updated: Mar 29 2024 at 08:18 UTC