Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Closed
bishabosha opened this issue May 23, 2023 · 8 comments
Closed

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

bishabosha opened this issue May 23, 2023 · 8 comments
Labels
area:pattern-matching itype:bug itype:crash regression This worked in a previous version but doesn't anymore stat:needs minimization Needs a self contained minimization stat:needs triage Every issue needs to have an "area" and "itype" label

Comments

@bishabosha
Copy link
Member

bishabosha commented May 23, 2023 •
edited
Loading

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

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
@bishabosha bishabosha added itype:bug itype:crash stat:needs triage Every issue needs to have an "area" and "itype" label labels May 23, 2023
@szymon-rd szymon-rd added area:pattern-matching regression This worked in a previous version but doesn't anymore stat:needs minimization Needs a self contained minimization stat:needs bisection Need to use nightly builds and git bisect to find out the commit where this issue was introduced and removed stat:needs triage Every issue needs to have an "area" and "itype" label labels May 23, 2023
@WojciechMazur
Copy link
Contributor

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)

@WojciechMazur WojciechMazur removed the stat:needs bisection Need to use nightly builds and git bisect to find out the commit where this issue was introduced label Jul 18, 2023
@WojciechMazur WojciechMazur mentioned this issue Jul 18, 2023
Merged
@dwijnand
Copy link
Member

@WojciechMazur after your fix, does this still fail?

@WojciechMazur
Copy link
Contributor

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
Copy link
Member

dwijnand commented Jul 19, 2023 •
edited
Loading

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
Copy link
Contributor

@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

@dwijnand
Copy link
Member

I assume that if we get to reporting bisect information it means that it's still broken using latest. But I guess I shouldn't assume that. The bisect points to #16621. Does it still break after #16827, which was fixed 2 weeks after that previous PR and 5 months ago from today?

@dwijnand dwijnand added the stat:needs triage Every issue needs to have an "area" and "itype" label label Jul 20, 2023
@WojciechMazur
Copy link
Contributor

Seems like SpaceEngine issue is still present in the main of lisa project. Here's the build logs of latest build: https://github.com/VirtusLab/community-build3/actions/runs/5626149769/job/15246428654

@Decel
Copy link
Contributor

Decel commented Dec 18, 2023

It's fixed via #19216

@Decel Decel closed this as completed Dec 18, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
area:pattern-matching itype:bug itype:crash regression This worked in a previous version but doesn't anymore stat:needs minimization Needs a self contained minimization stat:needs triage Every issue needs to have an "area" and "itype" label
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
5 participants
@dwijnand @szymon-rd @Decel @bishabosha @WojciechMazur