Debugging a software verifier written in sbt on In

问题:

I'm working with Stainless, a software verifier for Scala programs. I would like to debug the verification process of a sample programme on Intellij Idea. On a previous post, I solved this integration problem for an interactive theorem prover. But now, I'm facing two problems:

1. Apparently, the verification software runs at compile time. That is, I enter in the sbt console and run the compile command and then the verification process seems to be done. You may try this with this verified example. This situation is new to me, since I was used to debug the program while executing.

2. All the setup in the sbt files of the example above (see for instance this file) seem to refer to online content, while I want to make sure that I work with my local copy forked from the original repository of the verifier.

None of the configurations I tried worked. Can you help me out of this problem?

Details

This is the current configuration page of stainless.

回答1:

If the verification runs within the sbt process, you can debug it by attaching the debugger to sbt. IntelliJ makes this easy with the embedded sbt shell:

1. open the sbt shell toolwindow
2. click the "attach debugger to sbt shell" button on the left
3. set breakpoints in your code
4. run the task