Я работаю с Stainless , программным верификатором для программ Scala.Я хотел бы отладить процесс проверки примера программы на Intellij Idea.В предыдущем посте я решил эту проблему интеграции для интерактивного средства доказательства теорем .Но теперь я столкнулся с двумя проблемами:
Очевидно, что программное обеспечение для проверки запускается во время компиляции.То есть я вхожу в консоль sbt и запускаю команду компиляции, а затем процесс проверки, похоже, завершен.Вы можете попробовать это с этим проверенным примером .Эта ситуация является новой для меня, так как я использовался для отладки программы во время выполнения.
Все настройки в файлах sbt приведенного выше примера (см., Например, этот файл), похоже, относится к онлайн-контенту, хотя я хочу убедиться, что я работаю с моей локальной копией, разветвленной из исходного хранилища верификатора.
Ни одна из конфигураций, которые я пробовал, не работала.Можете ли вы помочь мне решить эту проблему?
Подробности
Этот является текущей страницей конфигурации из нержавеющей стали.