Ошибки OCaml во время использования Why3

Я пытаюсь скомпилировать why3ide (why3-0.81) с krakatoa & jessie (why-2.33) для Windows (Cygwin). Все прошло хорошо, за исключением того, что я не могу сделать правое нижнее текстовое поле для отображения обозначений (оно всегда пустое), более того, я получаю сообщение об ошибке (выделено на рисунке) каждый раз, когда пытаюсь выбрать элемент для проверки.

Why3ide на WindowsИзображение: https://dl.dropboxusercontent.com/u/39984835/why3ide/error_capture.jpg

Вот эта ошибка:

Apply transformation introduce_premises
Why3ide callback raised an exception:
anomaly: End_of_file

Backtrace:
Raised at file "format.ml", line 197, characters 41-52
Called from file "format.ml", line 425, characters 8-33
Called from file "format.ml", line 440, characters 6-24

Как я могу отладить эту ошибку? (Я новичок в OCaml)

файл format.ml находится здесь:
Cygwin / Библиотека / OCaml / format.ml

Файлы, которые ссылаются на преобразование ввести_premises, находятся здесь:
why3-0.81 / драйверы / gappa.drv
why3-0.81 / SRC / язь / gmain.ml
why3-0.81 / SRC / преобразования / introduction.ml
why3-0.81 / драйверы / mathematica.drv

PS Я пытался добавить теги Why3 & Why3ide для этого поста, но моей репутации пока недостаточно.

0 ответов

Другие вопросы по тегам