Является ли библиотека mach.int частью по умолчанию для Why3?

Question

Я пытаюсь использовать 32-разрядные целые числа в спецификации Why3 модели Simulink для Why3, и я нашел библиотеку mach.int, которая, по крайней мере, в одном месте, описана как часть стандартной библиотеки. Однако, когда я пытаюсь использовать его со следующей командой импорта:

  use import mach.int.Int32

Я получаю сообщение:

Library file not found: mach.int

Это моя первая библиотека с "." в этом, поэтому я не уверен, что мой синтаксис неправильный, или эта библиотека на самом деле не является частью стандартной библиотеки, или я делаю что-то другое неправильно.

Как правильно использовать mach.int.Int32 модуль?

Дополнительные детали

мой why3 версия 0.87.3:

▶ why3 --version
Why3 platform, version 0.87.3

Я посмотрел в своем файле ~/.why3.conf и нашел следующие строки:

[main]
loadpath = "/opt/gps/share/why3/theories"
loadpath = "/opt/gps/share/why3/modules"
loadpath = "/opt/gps/share/spark/theories"

Я заглянул в /opt/gps/share/why3/modules (а также /opt/gps/share/why3/theories а также /opt/gps/share/spark/theories) и не нашел mach.int.*Итак, я создал mach.int.mlw файл в /opt/gps/share/why3/modulesи убедился, что why3 было в порядке с этим:

▶ why3 prove -P z3 mach.int.mlw        
mach.int.mlw Int WP_parameter infix / : Valid (0.01s)
mach.int.mlw Int WP_parameter infix % : Valid (0.01s)
mach.int.mlw Refint63 WP_parameter incr : Valid (0.02s)
mach.int.mlw Refint63 WP_parameter decr : Valid (0.02s)
mach.int.mlw Refint63 WP_parameter infix += : Valid (0.02s)
mach.int.mlw Refint63 WP_parameter infix -= : Valid (0.02s)
mach.int.mlw Refint63 WP_parameter infix *= : Valid (0.02s)
mach.int.mlw MinMax63 WP_parameter min : Valid (0.01s)
mach.int.mlw MinMax63 WP_parameter max : Valid (0.02s)

Результат тот же.

Answer 1

Оказывается, почему3 искал mach.int.Int32 в модуле int.mlw в mach подкаталог.

Ввод mach.int библиотека в /opt/gps/share/why3/modules/mach/ каталог решает проблему с библиотекой, не найденной (где /opt/gps/share/why3/modules определяется как часть loadpath в моем ~/.why3.conf файл).