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