Email Gateway (Oct 15 2022 at 10:36): Email Gateway (Oct 15 2022 at 10:36):From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hi,
when installing Isabelle2022-RC3 in, e.g., "c:\temp\with spaces" (or,
more reasonably but a little harder because of permissions: "c:\Program
Files"), I cannot run "scala isabelle" in the Cygwin Terminal. I get:
Error: Could not find or load main class
spaces.Isabelle2022-RC3.contrib.scala-3.2.0
Caused by: java.lang.ClassNotFoundException:
spaces.Isabelle2022-RC3.contrib.scala-3.2.0
I would guess that this is due to a missing quoting in some script
somewhere, where the part of the scala-directory after the space is
interpreted as an additional command line argument.
This also affects the normal execution of theory files, for example
HOL-Library.Finite_Sets which contains some scala codegeneration.
I experience the problem on Windows 11. I have not tested it on other OSs.
Isabelle2021-1 does not have this problem.
Best wishes,
Dominique.
Email Gateway (Oct 15 2022 at 10:38):From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Minor correction:
"This also affects the normal execution of theory files, for example
HOL-Library.Finite_Map which contains some scala codegeneration."
Email Gateway (Oct 17 2022 at 12:08):From: Makarius <makarius@sketis.net>
On 15/10/2022 12:34, Dominique Unruh (via cl-isabelle-users Mailing List) wrote:
when installing Isabelle2022-RC3 in, e.g., "c:\temp\with spaces" (or, more
reasonably but a little harder because of permissions: "c:\Program Files"), I
cannot run "scala isabelle" in the Cygwin Terminal. I get:Error: Could not find or load main class
spaces.Isabelle2022-RC3.contrib.scala-3.2.0
Caused by: java.lang.ClassNotFoundException:
spaces.Isabelle2022-RC3.contrib.scala-3.2.0I would guess that this is due to a missing quoting in some script somewhere,
where the part of the scala-directory after the space is interpreted as an
additional command line argument.
Thank you for testing Isabelle2022-RC thoroughly.
This problem has been newly introduced in Scala 3: the shell scripts appear to
be written without any clue about the white space problem. There is not just
one bad spot, but many places that need to be done differently.
This resembles the early years of Scala 2, but in Scala 3 the scripts have
become even more complex. By rewriting everything from scratch in Scala 3, old
problems of Scala 2 have returned (and become worse).
This also affects the normal execution of theory files, for example
HOL-Library.Finite_Sets which contains some scala codegeneration.
I don't see this theory. Can you point to a proper counter-example?
I experience the problem on Windows 11. I have not tested it on other OSs.
It happens an all platforms.
On Windows, one could try odd tricks with "cygpath -d", but I am unsure if
this is a good idea.
Makarius
Email Gateway (Oct 17 2022 at 12:20):From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Sorry, it was HOL-Library.Finite_Maps. And the offending fragment is
export_code
fBall fmrel fmran fmran' fmdom fmdom' fmpred pred_fmap fmsubset
fmupd fmrel_on_fset
fmdrop fmdrop_set fmdrop_fset fmrestrict_set fmrestrict_fset
fmimage fmlookup fmempty
fmfilter fmadd fmmap fmmap_keys fmcomp
checking SML Scala Haskell? OCaml?
Best wishes,
Dominique.
Email Gateway (Oct 17 2022 at 18:42):From: Makarius <makarius@sketis.net>
After staring at the Scala shell scripts long enough, it turns out that there
are many bad spots, but semantically only one is actually wrong. There is even
already a change for the coming scala-3.2.1 release:
https://github.com/lampepfl/dotty/commit/390505893ab
So we are lucky in a messy situation: only a small patch is required, and we
are one step closer to the final Isabelle2022 release.
Makarius
Email Gateway (Oct 18 2022 at 08:16):From: Makarius <makarius@sketis.net>
Yes, beyond plain space it is getting difficult.
A shell script alone can hardly cover all odd cases. The Isabelle functions
Bash.string (in ML or Scala) do it differently, e.g. see
https://isabelle.sketis.net/repos/isabelle-release/file/Isabelle2022-RC3/src/Pure/System/bash.scala
--- but this only covers processes started from within Isabelle/ML/Scala.
The bootstrap of Java/Scala itself is subject to further side-conditions that
I don't fully understand (e.g. default Locale). E.g. on Windows, "Test a"
usually works, but "Test ä" fails.
Likewise there can be differences with Simplified Chinese vs. Traditional
Chinese; I sometimes try "Test 中国". After experimenting with the Windows
machine of a Chinise student approx. 10 years ago, I am still unsure how well
it works for far Eastern users.
I guess that the Cyrillic world is fine (e.g. Russian or Serbian Locales).
Makarius
Email Gateway (Oct 18 2022 at 08:48):From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Looking at the diff you linked, I would think that even with the patch this still is sensitive to quotes, dollar signs, and more in path names... I agree that this is not well written code... But at least whitespaces, the most common culprit, should be covered... (Especially on Windows, where white spaces are common in directory names, this seems important.)
Best wishes,
Dominique.
After staring at the Scala shell scripts long enough, it turns out that there
are many bad spots, but semantically only one is actually wrong. There is even
already a change for the coming scala-3.2.1 release:
https://github.com/lampepfl/dotty/commit/390505893ab
So we are lucky in a messy situation: only a small patch is required, and we
are one step closer to the final Isabelle2022 release.
Makarius
Last updated: Apr 27 2024 at 01:05 UTC