Инструкция по установке и настройке Rodin » History » Version 6
Ilya Shchepetkov, 06/30/2021 11:09 AM
| 1 | 1 | Ilya Shchepetkov | h1. Инструкция по установке и настройке Rodin |
|---|---|---|---|
| 2 | |||
| 3 | Для установки Rodin выполните следующие действия: |
||
| 4 | |||
| 5 | 6 | Ilya Shchepetkov | # Установить @Java Runtime Environment (JRE) 11@ . |
| 6 | # Скачать архив с Rodin нужной версии и для нужной ОС, выложенный в данном проекте на вкладке @Files@: https://forge.ispras.ru/projects/spmodeler/files |
||
| 7 | # Распаковать архив в любом месте на жестком диске и запустить исполняемый файл @rodin@. |
||
| 8 | 1 | Ilya Shchepetkov | |
| 9 | 6 | Ilya Shchepetkov | Перед использованием Rodin необходимо установить два плагина: |
| 10 | * @SMT Solvers@, позволяет использовать SMT-решатели для автоматического доказательства. |
||
| 11 | * @Atelier B Provers@, набор дополнительных инструментов автоматического доказательства. |
||
| 12 | 1 | Ilya Shchepetkov | |
| 13 | 6 | Ilya Shchepetkov | Для установки плагина @SMT Solvers@ нужно выполнить следующие действия: |
| 14 | # Скачать файл с плагином со вкладки @Files@ данного проекта. Например, подойдет следующая версия: https://forge.ispras.ru/attachments/8943. |
||
| 15 | # Запустить Rodin, перейти в раздел @Help > Install New Software@ и нажать @Add@. |
||
| 16 | # В открывшемся окне нужно ввести имя (например, @SMT Solvers ISP RAS@), нажать на кнопку @Archive...@, найти на диске архив с плагином, и затем закрыть окно нажав кнопку @Add@. |
||
| 17 | # Убедиться, что в поле @Work with@ выбран путь до архива с плагином. |
||
| 18 | # После этого необходимо убрать галочку напротив опции @Group items by category@, выбрать для установки плагин @SMT Solvers@ (поставить галочку), и нажать @Next@. |
||
| 19 | # Проверить, что все верно, и нажать @Next@. |
||
| 20 | # Принять условия лицензионного соглашения и нажать @Finish@. |
||
| 21 | # Появится предупреждение о том, что содержимое устанавливаемого плагина не подписано. Нажать @OK@. |
||
| 22 | # Установка может занять некоторое время. По окончанию нажать на @Restart Now@. |
||
| 23 | 3 | Ilya Shchepetkov | |
| 24 | 6 | Ilya Shchepetkov | Для установки плагина @Atelier B Provers@ нужно выполнить следующие действия: |
| 25 | # Запустить Rodin, перейти в раздел @Help > Install New Software@. |
||
| 26 | # В выпадающем меню @Work with@ выбрать @Atelier B Provers@. |
||
| 27 | # Поставить галочку рядом с @Atelier B Provers@ и нажать @Next@. |
||
| 28 | # Принять условия лицензионного соглашения и нажать @Finish@. |
||
| 29 | # Появится предупреждение о том, что содержимое устанавливаемого плагина не подписано. Нажать @OK@. |
||
| 30 | # Установка может занять некоторое время. По окончанию нажать на @Restart Now@. |
||
| 31 | 2 | Ilya Shchepetkov | |
| 32 | 6 | Ilya Shchepetkov | После установки плагинов их нужно настроить. Для этого нужно: |
| 33 | # Открыть окно настроек Rodin (пункт @Window > Preferences@ в меню, или @Rodin Platform > Preferences@ на macOS). |
||
| 34 | # В выпадающем списке меню перейти в @Event-B > Sequent Prover > Auto/Post Tactic@. |
||
| 35 | # В разделе @Auto-Tactics@ в выпадающем списке @Tactic profile to be used for auto-tactics@ выбрать @Default Auto Tactic with SMT@. |
||
| 36 | # В разделе @Interactive-Tactics@ в выпадающем списке @Tactic profile to be used for interactive-tactics@ выбрать @Default Interactive Tactic with SMT@. |
||
| 37 | # В разделе @Post-Tactics@ убрать галочку напротив @Enable post-tactic for proving@. |