runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
452 stars 150 forks source link

Port all Scala code to Java #4030

Open Scott-Guest opened 9 months ago

Scott-Guest commented 9 months ago

While Scala is a nice language, the consensus of the frontend team is that maintaining a mixture of Scala and Java causes more friction than it is worth:

As a result, we have decided that

The largest blocker will be the matching library in the LLVM backend, which makes heavy usage of pattern matching and likely can't be ported until we update to Java 21 (#3499).

However, searching the frontend, there are only 47 Scala files, and many of them can be straightforwardly ported even without pattern matching support in Java.

A high level roadmap:

Scott-Guest commented 9 months ago

Another option might be to extend @Baltoli's pattern matching library then port matching to C++.

This would be more work in the short term, but would also make the LLVM backend more cohesive and get rid of the reverse dependency on K.

ehildenb commented 9 months ago

Love the idea of removing the reverse dependency! LLVM backend being self-contained seems worth the effort. That matching code is just used for LLVM codegen right?

Baltoli commented 9 months ago

Yep, that's the only place it's used. I think we'd want to first build a C++ implementation that generates the same YAML as the scala code does, test equivalence of the outputs, then eliminate the intermediate YAML. It would be a reasonably big rewrite but Dwight's documentation is really good, and we have a strong way of testing any new implementation!