~omrigan/lalambda-env

3b221ec26828106de836a15e5466578320a0fc64 — Oleg Vasilev 7 months ago e2dcf98
fix readme
1 files changed, 9 insertions(+), 7 deletions(-)

M readme.md
M readme.md => readme.md +9 -7
@@ 4,21 4,23 @@
Установите https://github.com/coq/platform/

### Редакторы
Дима советует: заведите VSCode + VSCoq.
Антон советует: пользуйте Emacs + Proof General.
Олег бурчит: если ничего не работает, сработает CoqIDE.
 - Дима советует: заведите VSCode + VSCoq.
 - Антон советует: пользуйте Emacs + Proof General.
 - Олег бурчит: если ничего не работает, сработает CoqIDE.

## TLA
Установите https://adoptopenjdk.net/ java16 должны работать
Установите Java
 - Java 16 с https://adoptopenjdk.net/ должна работать

### Редакторы
Дима говорит: рекомендуется VSCode. Сгодится TLA+ Toolbox.
 - Дима говорит: рекомендуется VSCode. 
 - Сгодится TLA+ Toolbox.

## Haskell
Установите stack

# Сдача контеста
 - Верифицируйте лемму из coq/hello.v. Посмотрите в выводе через какую лемму была доказана наша лемма
 - Верифицируйте лемму из coq/hello.v. Посмотрите в выводе какую лемма использовал `auto` для доказательства
 - Сделайте model checking у модели из tla. Посмотрите в выводе сколько всего состояний было использовано
 - Запустите stack run в папке haskell. Введите полученные на предыдущих шагах значения. Выведенное число и есть ваш ответ на контест
 - Запустите stack run в папке haskell. Введите полученные на предыдущих шагах значения. Выведенное число и есть ваш ответ. Его нужно отправить в форму подтверждения участия