scala - 在 Intellij Idea 上调试用 sbt 编写的软件验证器

Question

我正在使用不锈钢，一个 Scala 程序的软件验证器。我想在 Intellij Idea 上调试一个示例程序的验证过程。在上一篇文章中，我为交互式定理证明器解决了这个集成问题。但是现在，我面临两个问题：

1. 显然，验证软件在编译时运行。也就是说，我进入 sbt 控制台并运行编译命令，然后验证过程似乎完成了。你可以试试这个经过验证的例子。这种情况对我来说是新的，因为我习惯于在执行时调试程序。

2. 上面示例的 sbt 文件中的所有设置（例如，参见这个文件）似乎都引用了在线内容，而我想确保我使用从验证器的原始存储库分叉的本地副本。

我尝试过的所有配置都不起作用。你能帮我解决这个问题吗？

细节

这是不锈钢的当前配置页面。

标签： scaladebuggingintellij-ideasbtformal-verification

Answer 1

如果验证在 sbt 进程中运行，您可以通过将调试器附加到 sbt 来对其进行调试。IntelliJ 使用嵌入式 sbt shell 使这变得简单：

1. 打开 sbt shell 工具窗口
2. 单击左侧的“将调试器附加到 sbt shell”按钮
3. 在代码中设置断点
4. 运行任务