GRPC message size limit error on verify

[bugarela]

On apalache server

13:59:45.204 [main] INFO at.forsyte.apalache.tla.tooling.opt.ServerCmd -- Loading configuration
# Usage statistics is OFF. We care about your privacy.
# If you want to help our project, consider enabling statistics with config --enable-stats=true.

Output directory: /home/gabriela/_apalache-out/server/2024-03-01T13-59-45_14890697073968654447
# APALACHE version: 0.44.2 | build: 3360796                       I@13:59:45.422
Starting server on port 8822...                                   I@13:59:45.427
The Apalache server is running on port 8822. Press Ctrl-C to stop.
Mar 01, 2024 1:59:50 PM io.grpc.netty.NettyServerStream$TransportState deframeFailed
WARNING: Exception processing message
io.grpc.StatusRuntimeException: RESOURCE_EXHAUSTED: gRPC message exceeds maximum size 8388608: 10284721
	at io.grpc.Status.asRuntimeException(Status.java:529)
	at io.grpc.internal.MessageDeframer.processHeader(MessageDeframer.java:392)
	at io.grpc.internal.MessageDeframer.deliver(MessageDeframer.java:272)
	at io.grpc.internal.MessageDeframer.request(MessageDeframer.java:162)
	at io.grpc.internal.AbstractStream$TransportState$1RequestRunnable.run(AbstractStream.java:233)
	at io.grpc.netty.NettyServerStream$TransportState$1.run(NettyServerStream.java:188)
	at io.netty.util.concurrent.AbstractEventExecutor.runTask(AbstractEventExecutor.java:174)
	at io.netty.util.concurrent.AbstractEventExecutor.safeExecute(AbstractEventExecutor.java:167)
	at io.netty.util.concurrent.SingleThreadEventExecutor.runAllTasks(SingleThreadEventExecutor.java:470)
	at io.netty.channel.nio.NioEventLoop.run(NioEventLoop.java:569)
	at io.netty.util.concurrent.SingleThreadEventExecutor$4.run(SingleThreadEventExecutor.java:997)
	at io.netty.util.internal.ThreadExecutorMap$2.run(ThreadExecutorMap.java:74)
	at io.netty.util.concurrent.FastThreadLocalRunnable.run(FastThreadLocalRunnable.java:30)
	at java.base/java.lang.Thread.run(Thread.java:1589)

on my quint command:

Error: 1 CANCELLED: Call cancelled
    at callErrorFromStatus (/home/gabriela/projects/quint/quint/node_modules/@grpc/grpc-js/build/src/call.js:31:19)
    at Object.onReceiveStatus (/home/gabriela/projects/quint/quint/node_modules/@grpc/grpc-js/build/src/client.js:192:76)
    at Object.onReceiveStatus (/home/gabriela/projects/quint/quint/node_modules/@grpc/grpc-js/build/src/client-interceptors.js:360:141)
    at Object.onReceiveStatus (/home/gabriela/projects/quint/quint/node_modules/@grpc/grpc-js/build/src/client-interceptors.js:323:181)
    at /home/gabriela/projects/quint/quint/node_modules/@grpc/grpc-js/build/src/resolving-call.js:99:78
    at process.processTicksAndRejections (node:internal/process/task_queues:77:11)
for call at
    at ServiceClientImpl.makeUnaryRequest (/home/gabriela/projects/quint/quint/node_modules/@grpc/grpc-js/build/src/client.js:160:32)
    at ServiceClientImpl.run (/home/gabriela/projects/quint/quint/node_modules/@grpc/grpc-js/build/src/make-client.js:105:19)
    at Object.<anonymous> (/home/gabriela/projects/quint/quint/dist/src/quintVerifier.js:182:55)
    at node:internal/util:375:7
    at new Promise (<anonymous>)
    at Object.run (node:internal/util:361:12)
    at Object.check (/home/gabriela/projects/quint/quint/dist/src/quintVerifier.js:95:44)
    at /home/gabriela/projects/quint/quint/dist/src/quintVerifier.js:344:53
    at EitherConstructor.asyncChain (/home/gabriela/projects/quint/quint/node_modules/@sweet-monads/either/cjs/index.js:125:16)
    at verify (/home/gabriela/projects/quint/quint/dist/src/quintVerifier.js:344:29) {
  code: 1,
  details: 'Call cancelled',
  metadata: Metadata { internalRepr: Map(0) {}, options: {} }
}

[thpani]

I encountered this before, I think you just need to bump the number Apalache-side.
See apalache-mc/apalache#2622

[bugarela]

@thpani Ah, thanks a lot! Both me and Shon were sure there was an issue for this already, but we didn't find it because it was already closed - amazing! I had no recollection of that being fixed.