LS-Lab / KeYmaeraX-release

KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems (release)
http://keymaeraX.org/
GNU General Public License v2.0
75 stars 37 forks source link

Scala 2.13/dotty compatibility #68

Open zstone1 opened 4 years ago

zstone1 commented 4 years ago

Hello,

I'm having a problem with scala versions. I'm trying to use KeymaeraX as a library (I want the parser, printer, expression subsitution, ect. All stuff from core). But I'm using it in a newer scala project. There seems to be a backwards incompatibility between scala 2.13 and scala 2.12 where the standard library broke some methods. Compiling works fine, but at runtime I get the error

[error] (run-main-0) java.lang.NoSuchMethodError: scala.collection.immutable.Seq$.apply(Lscala/collection/Seq;)Lscala/collection/GenTraversable;
[error] java.lang.NoSuchMethodError: scala.collection.immutable.Seq$.apply(Lscala/collection/Seq;)Lscala/collection/GenTraversable;
[error]         at edu.cmu.cs.ls.keymaerax.core.package$.<init>(package.scala:204)
[error]         at edu.cmu.cs.ls.keymaerax.core.package$.<clinit>(package.scala)
[error]         at edu.cmu.cs.ls.keymaerax.core.NamedSymbol.insistNamingConvention(Expression.scala:155)
[error]         at edu.cmu.cs.ls.keymaerax.core.NamedSymbol.insistNamingConvention$(Expression.scala:154)
[error]         at edu.cmu.cs.ls.keymaerax.core.BaseVariable.insistNamingConvention(Expression.scala:256)
[error]         at edu.cmu.cs.ls.keymaerax.core.BaseVariable.<init>(Expression.scala:257)
[error]         at edu.cmu.cs.ls.keymaerax.core.Variable$.apply(Expression.scala:252)
... a bunch of stuff from my code ...
[error]         at java.lang.reflect.Method.invoke(Method.java:498)

Looks like keymaera is using some deprecated methods.

Long story short, is there a plan to upgrade to a newer version of Scala? How hard would it be to fix these issues?

I'd try to post pull request myself, except that I don't reasonable access to mathematica on my dev machine. So the build fails catastrophically.

rbohrer commented 4 years ago

Hi,

I recently looked into upgrading Scala versions. Unfortunately, we depend on a number of libraries which have not released their own 2.13 versions. It is unclear when that would happen, because some of them (including a few surprisingly prominent packages) have maintainers who have not had much time for maintenance :'(

I'm not sure about the error message so I will leave that for others to chime in.

zstone1 commented 4 years ago

Ah, that is not surprising. I guess everyone is waiting for scala 3 to do any real maintenance. Well, with no obvious path forward, I'll see about downgrading the other stuff. Thanks for the info.

aplatzer commented 3 years ago

There is not much we can do about this until Scala itself is compatible. While there is a fair amount of flexibility, a set of compatible scala, sbt etc versions for compiling is listed in the Building section of the README.md

aplatzer commented 3 years ago

Applied wontfix label until Scala and libraries get more compatible

EnguerrandPrebet commented 2 months ago

The latest KeYmaera X release now works with Scala 2.13.