epfl-lara / inox

Solver for higher-order functional programs, used by Stainless
Apache License 2.0
88 stars 20 forks source link

Bump to 3.3.3 (does not compile) #209

Closed samuelchassot closed 5 months ago

samuelchassot commented 6 months ago

This PR is to discuss about the bump to Scala 3.3.3.

Bumping to this version makes the solver hierarchy for NativeZ3Opt not valid anymore, with this error message:

[error] -- Error: /Users/samuel/EPFL/inox/src/main/scala/inox/solvers/SolverFactory.scala:207:14 
[error] 207 |        class NativeZ3OptImpl(override val program: p.type)
[error]     |              ^
[error]     |parent trait NativeZ3Optimizer has a super call which binds to the value inox.solvers.unrolling.AbstractUnrollingSolver.targetProgram. Super calls can only target methods.
[error] one error found
[error] (Compile / compileIncremental) Compilation failed

For now, I found this commit which introduces this check https://github.com/scala/scala3/commit/a53b1855f793d59b0e43925697eb769ebbacba4c.

This was introduced in release 3.3.1.

samuelchassot commented 6 months ago

this was in response to this issue: https://github.com/scala/scala3/issues/16704

samuelchassot commented 6 months ago

I'll continue to look into it, but for now I don't know how to solve this.