Configuration.sanitizedPathSegments breaks execution on Windows

[bk-jb]

Since Configuration.sanitizedPathSegments was indtroduced a few months ago, keymaerax-core is broken for Windows.

Exception in thread "main" java.lang.ExceptionInInitializerError
        at edu.cmu.cs.ls.keymaerax.hydra.SQLite$.ProdDB$lzycompute(SQLite.scala:46)
        at edu.cmu.cs.ls.keymaerax.hydra.SQLite$.ProdDB(SQLite.scala:46)
        at edu.cmu.cs.ls.keymaerax.launcher.Main$.exitIfDeprecated(Main.scala:190)
        at edu.cmu.cs.ls.keymaerax.launcher.Main$.main(Main.scala:88)
        at edu.cmu.cs.ls.keymaerax.launcher.Main.main(Main.scala)
Caused by: java.util.regex.PatternSyntaxException: Unexpected internal error near index 1
\

This is because of home.split(File.separator) and sub.split(File.separator). They fail because String.split takes a regex as argument, and the Windows File.separator is "\", and therefore not a valid regex. I think the solution would be to just escape it using Pattern.quote, like

val hf = home.split(Pattern.quote(File.separator))
val sf = sub.split(Pattern.quote(File.separator))

[bk-jb]

I have created a pull request for the suggested solution, https://github.com/LS-Lab/KeYmaeraX-release/pull/111

[bk-jb]

@smitsch Hi, since this really blocks launching the keymaerax server on Windows, and since this is a rather small change, I'd be grateful if you would consider merging my PR :) (I have tested it and was able to launch the server on Windows again with my patch.)

[mrdarok]

I second this issue. See error log, running from Windows 11 terminal:

Rolling back to 5.0.1 allows me to launch successfully.

[nrfulton]

The fix looks reasonable and doesn't break anything for me on linux/mac.

[EnguerrandPrebet]

Thanks for pointing that out, in the meantime, this issue is now fixed in the current release.