Email Gateway (Aug 22 2022 at 14:24): Email Gateway (Aug 22 2022 at 14:24):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Isabelle developers,
The code generator seems to print literal strings (String.literal) differently in
Isabelle2016-1-RC1 than it did in Isabelle2016, at least for the target language Scala.
Here's a minimal example:
definition "newline = STR [Char Nibble0 NibbleB]" (* Isabelle2016 *)
definition "newline = STR ''⏎''" (* Isabelle2016-1-RC1 *)
export_code newline in Scala
In Isabelle2016, the newline constant is printed as
def newline: String = "\12"
in octal notation. In Isabelle2016-1-RC1, it is printed as
def newline: String = "\u0012"
which uses hexadecimal notation, but the numbers are still the same, so this is actually
the character at codepoint 18. The same problem occurs for other characters that are
output in \uNNNN notation.
In Haskell, OCaml, and SML, a newline gets pretty-printed as "\n". Why can't we just use
this also for Scala?
Andreas
Email Gateway (Aug 22 2022 at 14:33):From: Makarius <makarius@sketis.net>
On 01/11/16 16:44, Andreas Lochbihler wrote:
definition "newline = STR ''⏎''" (* Isabelle2016-1-RC1 *)
export_code newline in Scala
In Isabelle2016-1-RC1, it is printed as
def newline: String = "\u0012"
which uses hexadecimal notation, but the numbers are still the same, so
this is actually the character at codepoint 18. The same problem occurs
for other characters that are output in \uNNNN notation.
Interestingly, the deprecation of Scala's octal \NNN in favour of
hexadecimal \uNNNN was motivated by avoidance of such mistakes
concerning the base of numerals.
I have now changed that here
https://bitbucket.org/isabelle_project/isabelle-release/commits/bed02fca80b
It shows that there can be errors in formally verified and generated
programs, but that should not be surprising to users who understand how
things work.
In Haskell, OCaml, and SML, a newline gets pretty-printed as "\n". Why
can't we just use this also for Scala?
That uniform, but awkward use of \u actually exposed the mistake in the
first place.
Florian Haftmann, who is presently on vacation, is free to refine that
further in post-release development.
Makarius
Last updated: Apr 23 2024 at 16:19 UTC