scala - 调试用 Scala 编写的作为 sbt 插件的软件验证程序

Question

我正在与 Stainless 一起工作, Scala 程序的软件验证程序。我想调试一个示例程序的验证过程。在上一篇文章中，我为 interactive theorem prover 解决了这个集成问题。 .但是现在，我面临两个问题:

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

或者，我发现它 was possible (2013) 在 Intellij Idea 中调试插件，released 可能就是这种情况。 (参见 sbt 部分)在 Sbt 上使用不锈钢的插件。

所以澄清一下，我正在寻找一个完整的设置，它允许我从终端/使用某些特定软件调试验证过程，以便我可以遵循不锈钢和我自己的项目的控制流/变量等.

详情

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

This我的问题是关于如何在 Intellij Idea 上解决这个问题(我猜更具挑战性)

管道

如果它有助于我离开这里发布的工具的管道(从文档中获取):



其他观察

在 Intellij Idea 中有一个 Unresolved 问题支持。

我必须尝试的另一种方法是 Scala REPL。

Answer 1

我也在寻找这个工具，但我没有找到任何好处。我尝试记录器，对我来说很好。

scala-logger: Simple Scala friendly logging interface.

Logback Project for backend