Email Gateway (Aug 22 2022 at 17:33): 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.
In total, the transition went quite smooth by using the information
that was provided in the NEWS file.
It took only 12 hours to update the 213k lines of theory files,
including IsaFoR-compilation times.
The tools “isabelle update_op”, Rafal Kolanski’s “goto_error” macro, and
the indication of error-free theories via bold-boxes in the Theories-panel
were all very helpful.
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.
I would have expected a statement in the NEWS file
on the necessary import of "HOL-Library.Lattice_Syntax”.
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)
The most visible impact from our side is the deletion of Code_Char.
The result is that our generated code became
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)
Cheers,
René
Email Gateway (Aug 22 2022 at 17:33):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc
Email Gateway (Aug 22 2022 at 17:33):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
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:
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é
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: Nov 21 2024 at 12:39 UTC