apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint
https://apalache-mc.org/
Apache License 2.0
440 stars 40 forks source link

Print JVM args in Apalache #1505

Open thpani opened 2 years ago

thpani commented 2 years ago

Blocked by #1624

We currently print JVM arguments in the apalache-mc runscript:

$ apalache-mc version --debug
# Tool home: ...
# Package:   ...
# JVM args:  -Xmx4096m
#
...

To make sure that the JVM actually picks them up, we should print them in Apalache instead.

shonfeder commented 2 years ago

I'm in favor of this!

thpani commented 2 years ago

This has to wait. We cannot check the --debug flag on version with our current cmdline parser backuity.clist (returns None)

To print the JVM args:

  val bean = ManagementFactory.getRuntimeMXBean
  Console.println("# JVM args: " + bean.getInputArguments.mkString(" "))
  Console.println("#")