问题描述
我正在使用
- 打开sbt shell工具窗口
- 点击左侧的附加调试器到sbt shell按钮
- 设置代码中的断点
- 运行任务
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:
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.
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.
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:
- open the sbt shell toolwindow
- click the "attach debugger to sbt shell" button on the left
- set breakpoints in your code
- run the task
这篇关于在Intellij Idea上调试用sbt编写的软件验证程序的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！