search

JetBrains / Arend

The Arend Proof Assistant
https://arend-lang.github.io/
Apache License 2.0
694 stars 33 forks source link

NPE in typechecking #296

Open marat-rkh opened 3 years ago

marat-rkh commented 3 years ago

I was writing a proof, and at some point plugin stoped showing goals although I had a hole:

Screen Shot 2021-05-02 at 2 34 40 PM

As you can see <-trans is shown as proven, but this is not true. The log have the following NPE:

2021-05-02 14:34:10,472 [68609791]   INFO - .deployment.AsyncDevicesGetter - adb not found 
2021-05-02 14:34:10,602 [68609921]  ERROR - pechecking.TypeCheckingService - null 
java.lang.NullPointerException
    at org.arend.core.definition.DataDefinition.getTypeWithParams(DataDefinition.java:217)
    at org.arend.typechecking.result.DefCallResult.makeTResult(DefCallResult.java:40)
    at org.arend.typechecking.visitor.CheckTypeVisitor.typeCheckDefCall(CheckTypeVisitor.java:1495)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitReference(CheckTypeVisitor.java:1532)
    at org.arend.typechecking.implicitargs.StdImplicitArgsInference.infer(StdImplicitArgsInference.java:274)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitApp(CheckTypeVisitor.java:2631)
    at org.arend.typechecking.visitor.CheckTypeVisitor.visitApp(CheckTypeVisitor.java:93)
    at org.arend.term.concrete.Concrete$AppExpression.accept(Concrete.java:392)
    at org.arend.typechecking.visitor.CheckTypeVisitor.checkType(CheckTypeVisitor.java:835)
    at org.arend.typechecking.visitor.CheckTypeVisitor.finalCheckType(CheckTypeVisitor.java:873)
    at org.arend.typechecking.visitor.DefinitionTypechecker.typecheckParameters(DefinitionTypechecker.java:484)
    at org.arend.typechecking.visitor.DefinitionTypechecker.typecheckConstructor(DefinitionTypechecker.java:1799)
    at org.arend.typechecking.visitor.DefinitionTypechecker.typecheckDataBody(DefinitionTypechecker.java:1510)
    at org.arend.typechecking.visitor.DefinitionTypechecker.visitData(DefinitionTypechecker.java:180)
    at org.arend.typechecking.visitor.DefinitionTypechecker.visitData(DefinitionTypechecker.java:66)
    at org.arend.term.concrete.Concrete$DataDefinition.accept(Concrete.java:2226)
    at org.arend.typechecking.order.listener.TypecheckingOrderingListener.unitFound(TypecheckingOrderingListener.java:221)
    at org.arend.typechecking.order.listener.CollectingOrderingListener$MyUnit.feedTo(CollectingOrderingListener.java:49)
    at org.arend.typechecking.order.listener.CollectingOrderingListener.feed(CollectingOrderingListener.java:142)
    at org.arend.typechecking.order.listener.TypecheckingOrderingListener.lambda$typecheckCollected$4(TypecheckingOrderingListener.java:126)
    at org.arend.typechecking.computation.ComputationRunner.run(ComputationRunner.java:37)
    at org.arend.typechecking.computation.BooleanComputationRunner.run(BooleanComputationRunner.java:8)
    at org.arend.typechecking.order.listener.TypecheckingOrderingListener.typecheckCollected(TypecheckingOrderingListener.java:125)
    at org.arend.typechecking.execution.TypeCheckProcessHandler$startNotify$1.run(TypeCheckProcessHandler.kt:185)
    at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
    at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
    at java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1$1.run(Executors.java:668)
    at java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1$1.run(Executors.java:665)
    at java.base/java.security.AccessController.doPrivileged(Native Method)
    at java.base/java.util.concurrent.Executors$PrivilegedThreadFactory$1.run(Executors.java:665)
    at java.base/java.lang.Thread.run(Thread.java:834)
2021-05-02 14:34:10,602 [68609921]  ERROR - pechecking.TypeCheckingService - IntelliJ IDEA 2021.1  Build #IC-211.6693.111 
2021-05-02 14:34:10,603 [68609922]  ERROR - pechecking.TypeCheckingService - JDK: 11.0.10; VM: Dynamic Code Evolution 64-Bit Server VM; Vendor: JetBrains s.r.o. 
2021-05-02 14:34:10,603 [68609922]  ERROR - pechecking.TypeCheckingService - OS: Mac OS X 
2021-05-02 14:34:10,603 [68609922]  ERROR - pechecking.TypeCheckingService - Plugin to blame: Arend version: 1.6.0.3

When I try to rerun the Typecheck, this exception appears again. The only way to fix this is to reopen the project.

I have seen this a number of times. Sometimes this bug can be very confusing as it looks like the proof is accepted, but I am not sure why (before I realize it is a bug).

marat-rkh commented 3 years ago

Not sure if it clarifies anything, but it seems like the bug happens after I use actions like "Replace with constructor" or "Fill goal".

valis commented 3 years ago

I saw it too, but I cannot reproduce it stably.