stackoverflow in space engine with epfl-lara/lisa and 3.3.0-RC6

[bishabosha]

There is a stack overflow in the space engine compiling one of the source files in lisa-utils submodule

• no debug information was available in the original error

Compiler version

3.3.0-RC6

Minimized code

• checkout epfl-lara/lisa@5e6f10e
• in build.sbt set scala3 = 3.3.0-RC6

val scala3 = "3.3.0-RC6"

• sbt lisa-examples/compile

Output (click arrow to expand)

sbt:lisa> lisa-examples/compile
[info] compiling 13 Scala sources to /Users/jamie/workspace/lisa/lisa-kernel/target/scala-2.13/classes ...
[info] compiling 27 Scala sources to /Users/jamie/workspace/lisa/lisa-utils/target/scala-3.3.0-RC6/classes ...
java.lang.StackOverflowError while running MegaPhase{crossVersionChecks, protectedAccessors, extmethods, uncacheGivenAliases, elimByName, hoistSuperArgs, forwardDepChecks, specializeApplyMethods, tryCatchPatterns, patternMatcher} on /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
java.lang.StackOverflowError while compiling /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/prooflib/BasicMain.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/prooflib/Exports.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/prooflib/Library.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/prooflib/OutputManager.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/prooflib/ProofTacticLib.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/prooflib/SimpleDeducedSteps.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/prooflib/TheoriesHelpers.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/utils/LisaException.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/utils/ProofsShrink.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/utils/SecondOrderMatcher.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/utils/package.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/utils/parsing/Parser.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/utils/parsing/ParsingUtils.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/utils/parsing/Printer.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/utils/parsing/ProofPrinter.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/utils/parsing/SynonymInfo.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/utils/tptp/Example.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/utils/tptp/KernelParser.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/utils/tptp/ProblemGatherer.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/utils/tptp/package.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/utils/unification/FirstOrderUnifier.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/utils/unification/SecondOrderUnifier.scala, /Users/jamie/workspace/lisa/lisa-utils/src/main/scala/lisa/utils/unification/UnificationUtils.scala
[error] ## Exception when compiling 27 sources to /Users/jamie/workspace/lisa/lisa-utils/target/scala-3.3.0-RC6/classes
[error] java.lang.StackOverflowError
[error] dotty.tools.dotc.core.Types$TypeMap.mapOver(Types.scala:5671)
[error] dotty.tools.dotc.core.Types$AvoidWildcardsMap.apply(Types.scala:6098)
[error] dotty.tools.dotc.core.OrderingConstraint.init(OrderingConstraint.scala:525)
[error] dotty.tools.dotc.core.OrderingConstraint.add(OrderingConstraint.scala:511)
[error] dotty.tools.dotc.core.OrderingConstraint.add(OrderingConstraint.scala:504)
[error] dotty.tools.dotc.core.ConstraintHandling.addToConstraint(ConstraintHandling.scala:760)
[error] dotty.tools.dotc.core.ConstraintHandling.addToConstraint$(ConstraintHandling.scala:29)
[error] dotty.tools.dotc.core.TypeComparer.addToConstraint(TypeComparer.scala:30)
[error] dotty.tools.dotc.core.TypeComparer$.addToConstraint(TypeComparer.scala:3011)
[error] dotty.tools.dotc.typer.ProtoTypes$.constrained(ProtoTypes.scala:716)
[error] dotty.tools.dotc.typer.ProtoTypes$.newTypeVar(ProtoTypes.scala:749)
[error] dotty.tools.dotc.core.TypeOps$InferPrefixMap$1.apply(TypeOps.scala:886)
[error] dotty.tools.dotc.core.Types$TypeMap.op$proxy18$1(Types.scala:5657)
[error] dotty.tools.dotc.core.Types$TypeMap.mapOver(Types.scala:5657)
[error] dotty.tools.dotc.core.TypeOps$InferPrefixMap$1.apply(TypeOps.scala:889)
[error] dotty.tools.dotc.core.TypeOps$.instantiateToSubType(TypeOps.scala:895)
[error] dotty.tools.dotc.core.TypeOps$.refineUsingParent(TypeOps.scala:757)
[error] dotty.tools.dotc.transform.patmat.SpaceEngine.$anonfun$13(Space.scala:682)
[error] scala.collection.immutable.List.map(List.scala:246)
[error] dotty.tools.dotc.transform.patmat.SpaceEngine.rec$1(Space.scala:696)
[error] dotty.tools.dotc.transform.patmat.SpaceEngine.rec$1(Space.scala:666)
...
[error] dotty.tools.dotc.transform.patmat.SpaceEngine.rec$1(Space.scala:666)
[error] dotty.tools.dotc.transform.patmat.SpaceEngine.rec$1(Space.scala:666)
[error] dotty.tools.dotc.transform.patmat.SpaceEngine.decompose(Space.scala:703)
[error] dotty.tools.dotc.transform.patmat.SpaceLogic.tryDecompose1$3(Space.scala:239)
[error] dotty.tools.dotc.transform.patmat.SpaceLogic.minus(Space.scala:247)
[error] dotty.tools.dotc.transform.patmat.SpaceLogic.minus$(Space.scala:78)
[error] dotty.tools.dotc.transform.patmat.SpaceEngine.minus(Space.scala:349)
[error] dotty.tools.dotc.transform.patmat.SpaceLogic.minus$$anonfun$2(Space.scala:259)
...
[error] scala.collection.immutable.List.map(List.scala:246)
[error] scala.collection.immutable.List.map(List.scala:79)
[error] dotty.tools.dotc.transform.patmat.SpaceLogic.minus(Space.scala:259)
[error] dotty.tools.dotc.transform.patmat.SpaceLogic.minus$(Space.scala:78)
[error] dotty.tools.dotc.transform.patmat.SpaceEngine.minus(Space.scala:349)
[error] dotty.tools.dotc.transform.patmat.SpaceLogic.tryDecompose1$3(Space.scala:239)
[error] dotty.tools.dotc.transform.patmat.SpaceLogic.minus(Space.scala:247)
[error] dotty.tools.dotc.transform.patmat.SpaceLogic.minus$(Space.scala:78)
[error] dotty.tools.dotc.transform.patmat.SpaceEngine.minus(Space.scala:349)
[error] dotty.tools.dotc.transform.patmat.SpaceLogic.minus$$anonfun$2(Space.scala:259)
[error] scala.collection.immutable.List.map(List.scala:246)
[error] scala.collection.immutable.List.map(List.scala:79)
[error] dotty.tools.dotc.transform.patmat.SpaceLogic.minus(Space.scala:259)
[error]            
[error] stack trace is suppressed; run last lisa-utils / Compile / compileIncremental for the full output
[error] (lisa-utils / Compile / compileIncremental) java.lang.StackOverflowError
[error] Total time: 25 s, completed 23 May 2023, 14:55:18

[WojciechMazur]

Bisect job logs: https://github.com/VirtusLab/community-build3/actions/runs/5586559456/jobs/10210742890
Last good release: 3.3.0-RC1-bin-20230118-9337bd6-NIGHTLY
First bad release: 3.3.0-RC1-bin-20230119-13b8d7d-NIGHTLY

Becouse of specific build (using remote sbt projects) the commit-based bisect has failed, however luckily range of commits it quite narrow:

1. 13b8d7d (Handle sealed prefixes in exh checking #16621)
2. 0dae27d (see above)
3. ad8d3bb (the community-build timouts change)

[dwijnand]

@WojciechMazur after your fix, does this still fail?

[WojciechMazur]

The linked fix is not related to the reported issue. The fix targeted main to allow for inclusion of project in open community build. The reported error was existing is some other branch

[dwijnand]

Which branch? Because the issue points to a commit on main and says to change the scala 3 version to 3.3.0. In the open community build you'll also be changing the version to a nightly of 3.3.0. So if it works in the open community build then it's not broken any more, no?

[WojciechMazur]

@dwijnand you're correct, the referenced commit sits on main (currently HEAD^4), and seems like some of the follow up changes allowed to mitigate to SpaceEngine issues. However, it's worth to remeber that the underlying problem would still be present in the compiler, even though the project would manage to compile it's current source code.

@bishabosha do have some more context about this issue. I guess that right now it's not a blocker for lisa project