apalache-mc/apalache

Spec rejected due to being outside ReTLA throws stack trace instead of exiting cleanly

Kukovec opened this issue · 1 comments

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

Looks like this was a local problem with dependencies, and CI can't reproduce this, so I'm closing the issue.