Skip to content

Cross-compilation support for Scala 3 (WIP)

Viktor Kuncak requested to merge dotty-compat into master

Created by: gsps

This is a WIP branch to track the progress on making inox cross-compile on Scala 2 and Scala 3. So far, we can compile and manually run inox on test cases using the CLI and Z3.

The remaining tasks roughly comprise:

  • Fix the sbt build to support cross-compilation out of the box (currently fixed to dotc).
  • Reactivate TipDebugger and the core methods of TimeoutSolver (blocked by dotc bug around abstract override).
  • Reactivate Variable#copy (blocked by dotc bug that raises denotation merge error). The synthetic copy method is still there, but doesn't preserve positions now.
  • Reactivate BagEncoder and SetEncoder (blocked by dotc bug on vararg applications). As a result we can also fix up CVC4 and reactivate its code.
  • Fix up Princess.
  • Ideally, make some of the test suite work on dotc (scalatest is currently unavailable, since it relies on macros).
  • Reactivate @inlines, dotc's inliner just causes too much trouble at the moment.

This PR includes workarounds for several other dotc issues and also some fixes for things that are presumably (non-serious) bugs in inox.

We track the related dotc issues here:

Merge request reports