Email Gateway (Apr 04 2024 at 12:10): Email Gateway (Apr 04 2024 at 12:10):From: Lars Hupel <lars@hupel.info>
Dear list,
I noticed that new flags are now required to compile generated Scala code.
For example, when exporting something involving equality on lists, the
"equal_list" function breaks unfortunately as follows:
def equal_listA : equal : Boolean = (x0,
x1) match<linebreak>
{
Due to Scala 3's new indentation-sensitive syntax, this is now a compile
error:
[error] -- [E040] Syntax Error: export1.scala:494:2
[error] 494 | {
[error] | ^
[error] | 'case' expected, but '{' found
The workaround is quite simple, in our case we had to supply the
following additional compiler flags:
-source 3.3 -old-syntax
When using "checking Scala" in Isabelle, these are automatically
supplied, as is "-no-indent" (which was not required in our application).
The example above can be reproduced with:
definition cmp_list :: ‹'a::_ list ⇒ _ ⇒ bool› where
‹cmp_list xs ys ⟷ xs = ys›
code_identifier
code_module HOL ⇀ (Scala) Test
| code_module Scratch ⇀ (Scala) Test
| code_module List ⇀ (Scala) Test
export_code cmp_list
in Scala
There is probably no immediate need to act for the Isabelle2024 release,
but I found this to be surprising. The NEWS entry about Scala 3.3 only
refers to Isabelle/Scala itself, not the generated code.
A future challenge might arise should the Scala team decide to drop
"-old-syntax" as a flag.
Cheers
Lars
Email Gateway (Apr 05 2024 at 09:36):From: Makarius <makarius@sketis.net>
On 04/04/2024 14:04, Lars Hupel wrote:
I noticed that new flags are now required to compile generated Scala code.
For example, when exporting something involving equality on lists, the
"equal_list" function breaks unfortunately as follows:def equal_listA : equal : Boolean = (x0, x1)
match<linebreak>
{
The workaround is quite simple, in our case we had to supply the following
additional compiler flags:-source 3.3 -old-syntax
Thank you for testing Isabelle2024-RC1 now, where there is still time to
refine things for the release.
I have briefly tried your example with Isabelle2022, Isabelle2023, and
Isabelle2024-RC1, but did not see a difference.
The full options for scalac are provided via ISABELLE_SCALAC_OPTIONS and used
from there in the regular codegen setup. The key options are now "-source 3.3
-old-syntax" or before "-source 3.1 -old-syntax".
The example above can be reproduced with:
definition cmp_list :: ‹'a::_ list ⇒ _ ⇒ bool› where
‹cmp_list xs ys ⟷ xs = ys›code_identifier
code_module HOL ⇀ (Scala) Test
| code_module Scratch ⇀ (Scala) Test
| code_module List ⇀ (Scala) Testexport_code cmp_list
in Scala
This works for me with "scalac -old-syntax" in all 3 Isabelle versions. The
options "-source 3.1" or "-source 3.3" don't make a difference.
A future challenge might arise should the Scala team decide to drop
"-old-syntax" as a flag.
That would mean to change a few things in Scala code generation, and to
automatically rewrite all Isabelle/Scala sources (quite a lot of material).
It would be indeed an inconvenient, annoying, and ultimately pointless move,
but no big challenge.
Makarius
Email Gateway (Apr 05 2024 at 10:07):From: Lars Hupel <lars@hupel.info>
I have briefly tried your example with Isabelle2022, Isabelle2023, and
Isabelle2024-RC1, but did not see a difference.
There is a subtle difference. In older Isabelle versions, this is
printed as follows:
def equal_list[A : equal](x0: List[A], x1: List[A]): Boolean = (x0, x1)
match {<linebreak>
Notice the fewer spaces. This was introduced here:
changeset: 78594:1cce41dc0c41
user: wenzelm
date: Tue Aug 29 15:23:06 2023 +0200
summary: clarified generated Scala, for the sake of "scalac -source
3.3";
... presumably to work around some other incompatibility between Scala
3.1 and 3.3.
Code generated from Isabelle2023 could be compiled with Scala 3.1
without any flags (at least in our application). Now, we need flags.
(Another example is "divmod_nat", where the extra spaces also lead to a
difference in line breaking.)
Presumably because ISABELLE_SCALAC_OPTIONS are always set this subtle
incompatibility never surfaced in testing (i.e. when using "checking
Scala").
This works for me with "scalac -old-syntax" in all 3 Isabelle versions.
The options "-source 3.1" or "-source 3.3" don't make a difference.
You're right, "-old-syntax" is sufficient.
For our application I will just set this flag and hope that it keeps
working in the future.
Email Gateway (Apr 05 2024 at 15:58):From: Makarius <makarius@sketis.net>
On 05/04/2024 12:06, Lars Hupel wrote:
Code generated from Isabelle2023 could be compiled with Scala 3.1 without
any flags (at least in our application). Now, we need flags. (Another
example is "divmod_nat", where the extra spaces also lead to a difference in
line breaking.)Presumably because ISABELLE_SCALAC_OPTIONS are always set this subtle
incompatibility never surfaced in testing (i.e. when using "checking Scala").
OK, I now understand the situation: the generated Scala code worked by
accident both with -new-syntax and -old-syntax, although I only had one
variant in mind: the one of Isabelle/Scala modules.
I think we can make this accidental flexibility official: a suitable change
for Isabelle2024-RC2 (next week) is in the pipeline. That works, because 'if'
statements are normally not used in generated Scala.
You're right, "-old-syntax" is sufficient.
For our application I will just set this flag and hope that it keeps working
in the future.
As long as the Scala version (and basic options) are those of the underlying
Isabelle version, it will always work, regardless of future changes of Scala.
That is a consequence of the "static closure" on all contributing components
(Java, Scala, whatever).
Makarius
Last updated: May 05 2024 at 04:19 UTC