JetBrains / JetBrains/Arend

NPE in typechecking

Open
#296 2 comments 0 reactions 0 assignees View on GitHub
bug
Dominant language
Java
Stars
756
Forks
31
PR merge metrics
No merged PRs in 30d

Description

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).

Contributor guide

No contributing guide indexed for this repository

Research direction

Start with org.arend.core.definition.DataDefinition.getTypeWithParams at DataDefinition.java:217, then follow the listed typechecking calls through CheckTypeVisitor and DefinitionTypechecker. Reproduce the failure by rerunning typechecking after the proof state loses its goals, using the reported Arend 1.6.0.3 environment if possible. Done means the exception no longer occurs and an unfinished hole is not shown as proven.

Written by the indexing model from the issue text.

Assessment

Tech stack
java
Domain
compilers
Issue type
Bug
Difficulty
4/5
Estimated time
3-5 days
Activity status
Stale
Clarity
Needs clarification
Newbie friendliness
32/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.