search

epfl-lara / lisa

Proof assistant based on first-order logic and set theory
Apache License 2.0
33 stars 18 forks source link

Fix compilation errors in util.parsing.Printer #171

Closed WojciechMazur closed 1 year ago

WojciechMazur commented 1 year ago

Seems, like some typos slipped through to the main branch. This PR fixes these typos allowing to compile the project

WojciechMazur commented 1 year ago

May I ask how you found this?

Sure! I was trying to bisect one of the long standing regressions found in the compiler discovered in this project https://github.com/lampepfl/dotty/issues/17562 To make sure that we would not get this regression again I've added it to Scala 3 Open Community Build https://github.com/VirtusLab/community-build3/pull/197/commits/ee7a9f0e80d3288974e7d0f86cfe9613c6fc372d this way we would build it weakly with nightly compilers. However, I've seen that main branch is not compiling. To prevent false positives I've fixed it on my fork, and filled a PR to backport it to upstream. When it's merge we would again test against epfl-lara/lisa main branch in nightly builds.

WojciechMazur commented 1 year ago

What we have here 

case class SCValidProof(proof: String, val usesSorry: Boolean = false)
val x = SCValidProof("")
x match { case SCValidProof(_) => ???}

should not compile with any version of Scala. I have no idea, how it could have compiled, unless there would be some bug, allowing to skip extracting default arguments (but I have never witnessed any) or if there would be some alternative unapply method (but there isn't)

sankalpgambhir commented 1 year ago

What we have here 

case class SCValidProof(proof: String, val usesSorry: Boolean = false)
val x = SCValidProof("")
x match { case SCValidProof(_) => ???}

should not compile with any version of Scala. I have no idea, how it could have compiled, unless there would be some bug, allowing to skip extracting default arguments (but I have never witnessed any) or if there would be some alternative unapply method (but there isn't)

I had the same concern after seeing your PR, and my hypothesis was that given the _, it was probably translated to an _.isInstanceOf[SCValidProof], throwing away the parameter list. But, I'm not in a position to immediately verify this.

In any case, thanks a lot for your fix. I'll merge it into main. I'll try to check why it does compile on 3.2.2 later.