Spec rejected due to being outside ReTLA throws stack trace instead of exiting cleanly
Kukovec opened this issue · 1 comments
Kukovec commented
The spec:
---------------------------- MODULE test --------------------------
EXTENDS Integers, Apalache
\* @type: Set(Int);
GEN == Gen(1)
Init == 0 \in GEN
Next == TRUE
Inv == TRUE
=================================================================
The command: transpile test.tla
Expected: EXITCODE: ERROR (75)
Actual:
java.lang.NoSuchMethodError: 'upickle.core.Types$TupleNWriter upickle.default$.Tuple2Writer(upickle.core.Types$Writer, upickle.core.Types$Writer)'
at at.forsyte.apalache.tla.passes.pp.PreproPassPartial.postLanguageCheck(PreproPassPartial.scala:75)
at at.forsyte.apalache.tla.passes.pp.PreproPassPartial.executeWithParams(PreproPassPartial.scala:87)
at at.forsyte.apalache.tla.passes.pp.ReTLAPreproPassImpl.execute(ReTLAPreproPassImpl.scala:48)
at at.forsyte.apalache.infra.passes.PassChainExecutor$.exec(PassChainExecutor.scala:64)
at at.forsyte.apalache.infra.passes.PassChainExecutor$.$anonfun$runPassOnModule$3(PassChainExecutor.scala:53)
at scala.util.Either.flatMap(Either.scala:352)
at at.forsyte.apalache.infra.passes.PassChainExecutor$.$anonfun$runPassOnModule$1(PassChainExecutor.scala:51)
at scala.collection.LinearSeqOps.foldLeft(LinearSeq.scala:183)
at scala.collection.LinearSeqOps.foldLeft$(LinearSeq.scala:179)
at scala.collection.immutable.List.foldLeft(List.scala:79)
at at.forsyte.apalache.infra.passes.PassChainExecutor$.runOnPasses(PassChainExecutor.scala:44)
at at.forsyte.apalache.infra.passes.PassChainExecutor$.run(PassChainExecutor.scala:34)
at at.forsyte.apalache.tla.tooling.opt.TranspileCmd.run(TranspileCmd.scala:25)
at at.forsyte.apalache.tla.Tool$.runCommand(Tool.scala:138)
at at.forsyte.apalache.tla.Tool$.run(Tool.scala:118)
at at.forsyte.apalache.tla.Tool$.main(Tool.scala:40)
at at.forsyte.apalache.tla.Tool.main(Tool.scala)
It took me 0 days 0 hours 0 min 1 sec I@17:14:04.605
Total time: 1.801 sec I@17:14:04.605
EXITCODE: ERROR (255)
Please report an issue at [https://github.com/informalsystems/apalache/issues]: java.lang.NoSuchMethodError: 'upickle.core.Types$TupleNWriter upickle.default$.Tuple2Writer(upickle.core.Types$Writer, upickle.core.Types$Writer)'
Kukovec commented
Looks like this was a local problem with dependencies, and CI can't reproduce this, so I'm closing the issue.