search

JetBrains / Arend

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

ISE in `ExpressionSerialization` #253

Open ice1000 opened 4 years ago

ice1000 commented 4 years ago 
4:09 AM [ERROR] An exception happened during persisting of module: Order.LinearOrder
                java.lang.IllegalStateException
                at org.arend.module.serialization.ExpressionSerialization.writeLevel(ExpressionSerialization.java:80)
                at org.arend.module.serialization.ExpressionSerialization.visitFieldCall(ExpressionSerialization.java:557)
                at org.arend.module.serialization.ExpressionSerialization.visitFieldCall(ExpressionSerialization.java:32)
                at org.arend.core.expr.FieldCallExpression.accept(FieldCallExpression.java:69)
                at org.arend.module.serialization.ExpressionSerialization.visitApp(ExpressionSerialization.java:269)
                at org.arend.module.serialization.ExpressionSerialization.visitApp(ExpressionSerialization.java:32)
                at org.arend.core.expr.AppExpression.accept(AppExpression.java:72)
                at org.arend.module.serialization.ExpressionSerialization.visitApp(ExpressionSerialization.java:269)
                at org.arend.module.serialization.ExpressionSerialization.visitApp(ExpressionSerialization.java:32)
                at org.arend.core.expr.AppExpression.accept(AppExpression.java:72)

Full stacktrace:

java.lang.IllegalStateException
 at org.arend.module.serialization.ExpressionSerialization.writeLevel(ExpressionSerialization.java:80)
 at org.arend.module.serialization.ExpressionSerialization.visitFieldCall(ExpressionSerialization.java:557)
 at org.arend.module.serialization.ExpressionSerialization.visitFieldCall(ExpressionSerialization.java:32)
 at org.arend.core.expr.FieldCallExpression.accept(FieldCallExpression.java:69)
 at org.arend.module.serialization.ExpressionSerialization.visitApp(ExpressionSerialization.java:269)
 at org.arend.module.serialization.ExpressionSerialization.visitApp(ExpressionSerialization.java:32)
 at org.arend.core.expr.AppExpression.accept(AppExpression.java:72)
 at org.arend.module.serialization.ExpressionSerialization.visitApp(ExpressionSerialization.java:269)
 at org.arend.module.serialization.ExpressionSerialization.visitApp(ExpressionSerialization.java:32)
 at org.arend.core.expr.AppExpression.accept(AppExpression.java:72)
 at org.arend.module.serialization.ExpressionSerialization.visitApp(ExpressionSerialization.java:270)
 at org.arend.module.serialization.ExpressionSerialization.visitApp(ExpressionSerialization.java:32)
 at org.arend.core.expr.AppExpression.accept(AppExpression.java:72)
 at org.arend.module.serialization.ExpressionSerialization.visitApp(ExpressionSerialization.java:269)
 at org.arend.module.serialization.ExpressionSerialization.visitApp(ExpressionSerialization.java:32)
 at org.arend.core.expr.AppExpression.accept(AppExpression.java:72)
 at org.arend.module.serialization.ExpressionSerialization.writeFunCall(ExpressionSerialization.java:281)
 at org.arend.module.serialization.ExpressionSerialization.visitFunCall(ExpressionSerialization.java:288)
 at org.arend.module.serialization.ExpressionSerialization.visitFunCall(ExpressionSerialization.java:32)
 at org.arend.core.expr.FunCallExpression.accept(FunCallExpression.java:70)
 at org.arend.module.serialization.ExpressionSerialization.writeExpr(ExpressionSerialization.java:162)
 at org.arend.module.serialization.ExpressionSerialization.writeElimClause(ExpressionSerialization.java:198)
 at org.arend.module.serialization.ExpressionSerialization.writeElimBody(ExpressionSerialization.java:260)
 at org.arend.module.serialization.ExpressionSerialization.visitCase(ExpressionSerialization.java:523)
 at org.arend.module.serialization.ExpressionSerialization.visitCase(ExpressionSerialization.java:32)
 at org.arend.core.expr.CaseExpression.accept(CaseExpression.java:80)
 at org.arend.module.serialization.ExpressionSerialization.writeExpr(ExpressionSerialization.java:162)
 at org.arend.module.serialization.DefinitionSerialization.writeBody(DefinitionSerialization.java:366)
 at org.arend.module.serialization.DefinitionSerialization.writeFunctionDefinition(DefinitionSerialization.java:309)
 at org.arend.module.serialization.DefinitionSerialization.writeDefinition(DefinitionSerialization.java:50)
 at org.arend.module.serialization.ModuleSerialization.writeGroup(ModuleSerialization.java:90)
 at org.arend.module.serialization.ModuleSerialization.writeGroup(ModuleSerialization.java:102)
 at org.arend.module.serialization.ModuleSerialization.writeGroup(ModuleSerialization.java:102)
 at org.arend.module.serialization.ModuleSerialization.writeModule(ModuleSerialization.java:38)
 at org.arend.source.StreamBinarySource.persist(StreamBinarySource.java:168)
 at org.arend.library.SourceLibrary.persistModule(SourceLibrary.java:360)
 at org.arend.typechecking.BinaryFileSaver$saveFile$$inlined$runReadAction$1.compute(actions.kt:58)
 at com.intellij.openapi.application.impl.ApplicationImpl.runReadAction(ApplicationImpl.java:855)
 at org.arend.typechecking.BinaryFileSaver.saveFile(BinaryFileSaver.kt:75)
 at org.arend.typechecking.BinaryFileSaver.saveAll(BinaryFileSaver.kt:69)
 at org.arend.typechecking.execution.TypeCheckProcessHandler$startNotify$1.run(TypeCheckProcessHandler.kt:190)
 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)
valis commented 4 years ago

Can you reproduce it?

ice1000 commented 4 years ago

No successful attempts so far