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
Subscribe
  • Post a new comment

    Error

    default userpic

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 0 comments