Namdak Tonpa (maxim) wrote,
Namdak Tonpa
maxim

Групоид Инфинити открывает свой репозиторий Coq пакетов

С коком такая тема, что не все пакеты обновляются часто, никому не нужны FTC, Category Theory, CoInduction свойтва на последних коках. Последний — 8.6 — вышел в декабре 2016, а у всех пакетов в OPAM стоит жестко меньше 8.6. Они там язык тактик поменяли, и улучшлили тайпчек вселенных.

Демонстрировать кому-то всю силу кока приходится на своем компе, и простых инструкций взять и склонировать что-то для известных теорем нет. Более того, не все теоремы есть в OPAM, много просто валяются на ftp серверах унивеситетов.

Поэтому в соответствии с парадигмой "Грабь и Воруй" я принял решение сделать свой репозиторий пакетов под игидой Групоид Инфинити. Делаю я это для того, чтобы крамсать код пакетов в (само)-образовательных целях и публикации статей по основаниями математики с примерами кок-термов. Следите за сайтом Групоид Инфинити, а также языком Infinity Language.

Итак, встречайте, кодовое название проекта "Вери Мас Сач Вау" https://github.com/verimath Логотип тупо ноль — обозначает начальный уровень Кунг-фу в Зависимой теории :-)



Хочу сделать максимальный smooth экспириенс для математиков и академии, чтобы студенты могли очень просто начать разрабатывать на коке. Смешно, но даже матерые коко-писатели из НАН не знают как накатить HoTT патчи и чекнуть гомотопические теоремы.

Хочу, чтобы простая последовательность действий всегда позволяла запустить любой наш репо на последнем коке. У чуваков культуры оформления вообще никакой, какие-то перл скрипты, беш скрипты — представьте, что вы говорите математику на виндовсе поставить перл и беш, чтобы у вас работали теоремы. Вообщем, я это все повыбрасывал и оставил только coq_makefile. В репозиториях ничего кроме коковских файлов нет и все собирается простой последовательностью команд:

$ brew install opam
$ opam install coq
$ git clone http://github.com/verimath/topology && cd topology
$ coq_makefile -f Make -o Makefile
$ make

Начал я с таких тем-репозиториев — все рабочие (только ftc wip):

1. topology — общая топология + лемма Цорна
2. co — первый коиндуктивный репл-шелл на коке
3. real — действительные числа, как коиндуктивные стримы цифр
4. termination — терминальная категорная семантика коиндуктивных стримов
5. set — теория множеств Тарского-Гротендика
6. interpreter — интерпретатор гомотопической теории
7. ftc — основная теорема анализа по предложению риалити хакера
8. lambda — нетипизированное лямбда исчисление как инициальный объект категории экспоненциальных монад

Пакеты можно будет добавлять так:

$ opam repo add coq-released https://groupoid.space/opam

Делаем зависимые лямбда термы ближе к народу!
Tags: coq, cs, groupoid infinity
  • Post a new comment

    Error

    default userpic

    Your IP address will be recorded 

  • 27 comments