Objective Caml - Воскресенье, 24 марта 2013

Objective Caml

ocaml@conference.jabber.ru

Воскресенье, 24 марта 2013< ^ >

Конфигурация комнаты

Участники комнаты

GMT+4
[00:18:37] Kakadu вышел(а) из комнаты
[00:25:12] gds вышел(а) из комнаты
[00:36:59] f[x] вошёл(а) в комнату
[00:49:48] f[x] вышел(а) из комнаты
[01:11:36] tilarids вышел(а) из комнаты
[01:14:07] ftrvxmtrx вошёл(а) в комнату
[01:57:56] cirno вошёл(а) в комнату
[02:15:51] gds вошёл(а) в комнату
[02:17:56] ftrvxmtrx вошёл(а) в комнату
[02:22:47] ftrvxmtrx вышел(а) из комнаты
[02:34:26] Sun][ вышел(а) из комнаты
[03:06:58] cirno изменил(а) имя на tensai
[04:39:55] strobegen вышел(а) из комнаты
[05:05:23] tensai вышел(а) из комнаты
[08:18:58] strobegen вошёл(а) в комнату
[10:02:58] f[x] вошёл(а) в комнату
[11:00:56] Kakadu вошёл(а) в комнату
[11:15:50] ermine вошёл(а) в комнату
[11:28:18] Sun][ вошёл(а) в комнату
[11:35:04] f[x] вышел(а) из комнаты
[12:28:43] f[x] вошёл(а) в комнату
[12:38:51] <f[x]> Kakadu: unix_close определён в libunix.a - ты с ним линкуешься?
[12:39:17] <f[x]> в unix.a есть камлевый код - то что генерит ocamlopt
[12:39:29] <f[x]> в libunix.a - код сишных биндингов
[12:40:18] <f[x]> g++ -L$QT5_ROOT/qtbase/lib -lQt5Core -lQt5Qml -lQt5Quick -lQt5Gui \
        ../_build/stubs.o `ocamlc -where`/unix.a camlcode.o DataItem_c.o moc_DataItem_c.o MainModel_c.o moc_MainModel_c.o MiniModel_c.o moc_MiniModel_c.o main.o -L"`ocamlc -where`" -lm  -ldl -lasmrun \
        -o main
[12:40:25] <f[x]> ты же ликуешь unix.a
[12:40:29] <f[x]> вместо libunix.a
[12:41:11] <f[x]> а вообще мораль в том что лучше избегать напрямую вызовов g++ или gcc - а компитить всё через камлевые компиляторы
[12:41:42] <f[x]> а в том коде что ты кинул в caml-list там на финальном шаге написано -lunix - странно
[12:41:48] <Kakadu> да
[12:41:57] <Kakadu> я пробовал и так, и так --- одна фигня
[12:42:35] <f[x]> проверь что в libunix.a у тебя есть эти функции
[12:42:46] <f[x]> nm $(ocamlc -where)/libunix.a | grep unix_close
[12:42:59] <f[x]> ещё там с порядком надо не налажать
[12:43:42] <f[x]> переставь -lunux в конец строки
[12:44:13] <Kakadu> да, в libunix.a оно есть
[12:45:25] <Kakadu> f[x]: Да ты телепат!
[12:46:27] <f[x]> так что именно помогло?
[12:46:36] <Kakadu> в конец помогло
[12:46:50] <f[x]> и -lunix должно быть не -ccopt а -cclib
[12:47:04] <f[x]> тогда елси линковать через ocamlopt оно само будет в правильное место ставить\
[12:49:19] <Kakadu> А почему когда я генерю из камла файл .о я не могу делать тот же трюк с -cclib -lunix ?
[12:49:44] <f[x]> потому что в .o некуда это вписывать
[12:49:55] <f[x]> эти опции вписываются в cma/cmxa
[12:50:22] <f[x]> если ты делаешь только .o файл - то информация о том что надо слинковать чтобы этот .o удовлетворить - внешняя
[12:50:32] <f[x]> т.е. в readme там или через libastral передаётся
[12:52:39] Typhon вошёл(а) в комнату
[12:52:47] <Kakadu> угу
[12:58:20] <Kakadu> f[x]: большое спасибо!
[12:59:02] <f[x]> "спасибо" не булькает!
[12:59:04] <f[x]> :)
[13:00:05] <ermine> и на хлеб не намазать!
[13:00:17] <f[x]> ermine шарит
[13:01:07] ermine -shared
[13:03:21] <f[x]> -lol
[13:06:34] ermine читает очередной кусок книжки по coq - чем дальше, тем всё затяжнее и менее понятно...
[13:07:20] <ermine> "вон эта штука не сработала, давайте попробуем вот так, а вот тут проблема есть! давайте попробуем этак..."
[13:07:50] <ermine> gds - гений, если сумел это прожевать
[13:21:53] <Kakadu> ты про ту книжку на  http://adam.chlipala.net ?
[13:24:58] <ermine> ага
[13:25:13] <ermine> вроде больше нечего читать про coq или есть попроще? :)
[13:25:55] <f[x]> coq for dummies
[13:27:23] <ermine> чота такого в гугле не видно!
[13:27:35] <ermine> хоть coq for girls
[13:29:16] <aleksey> ermine: с самим coq идёт tutorial
[13:31:39] <ermine> aleksey: а что там? максимум forall n, m : nat, m = n?
[13:34:39] <aleksey> только азы
[13:35:00] <aleksey> а если надо посложнее, не жалуйся что сложное :)
[13:49:18] Sun][ вышел(а) из комнаты
[13:50:00] Sun][ вошёл(а) в комнату
[14:31:49] f[x] вышел(а) из комнаты
[14:38:48] f[x] вошёл(а) в комнату
[14:45:52] strobegen вышел(а) из комнаты
[14:56:19] f[x] вышел(а) из комнаты
[15:00:53] strobegen вошёл(а) в комнату
[15:03:47] strobegen вышел(а) из комнаты: Replaced by new connection
[15:03:48] strobegen вошёл(а) в комнату
[15:29:17] zinid вошёл(а) в комнату
[16:17:42] <gds> ermine: "вон эта штука не сработала" -- он как раз и объясняет, почему не сработала.  То есть, объясняет внутренности на конкретных примерах.
Впрочем, судя по #coq irc, существует народ, которому CPDT сложно, а "software foundations" в самый раз.  Попробуй, вдруг.
[16:21:39] <ermine> gds: про что они? другая книжка? coq art?
[16:22:08] <gds> другая книжка.  не coq'art.
[16:22:12] ermine пошла на страничку coq искать
[16:22:51] <gds> coq "software foundations" лучше поищи.  Автор -- Пирс.
[16:23:05] <ermine> да, есть там такая хрень
[16:23:33] <gds> говорят, там нежнее.
[16:26:03] <ermine> хмтыль и там, что ценно, надо попробовать
[16:27:04] <gds> так вроде cpdt в pdf отдаётся в том числе.
[16:29:50] <gds> Kakadu: если не лень, отпиши в рассылку, что именно помогло в линковке.  Профиты: 1. будет доступный для поиска ответ, 2. людишки не будут ломать голову зря.  Но смотри сам.
[16:33:41] <ermine> gds: ну я больше надеюсь что наличие альтернативного изложения таки поможет мне осилить механизм уговаривания coq
[16:34:30] <ermine> gds: у адама я засыпала на том, когда он объяснял какие гипотезы и когда и почему надо применять в доказательствах типа apply H0
[16:34:42] <gds> так тут всё проще: давай примеры, в чём надо coq уговорить, а я тебе расскажу "интуицию", которая применима тут.
[16:34:53] <ermine> я не пойму как гипотезами можно доказывать
[16:35:07] <ermine> гипотезы сами нуждаются в доказательстве, так учили в школе
[16:36:51] <ermine> гипотезы, леммы и теоремы
[16:36:55] <gds> допустим, Lemma q : forall n, n + n = 0 -> n = 0.  Вот тут, если сделаем "intros", гипотезами будут n : nat и n + n = 0 : Prop, а целью доказательства -- n = 0.
[16:37:11] <ermine> в coq между ними разница большая, поболее чем можно себе представить
[16:38:31] <gds> то есть, если надо доказать утверждение "forall A, B", мы можем его преобразовать так: "допустим, есть какое-то любое A, вынесем его отдельно, обзовём гипотезой.  Тогда, допуская эту гипотезу, докажем B.".  Что действительно эквивалентно исходному "для любого A имеем B".
[16:39:11] <gds> просто вот это "для любого A" не мешается в цели доказательства, а вынесено в гипотезы, это удобно для работы с этим A.
[16:40:14] <gds> но можно и наоборот делать: если есть гипотеза A и цель B, то через "revert A" (обратное от intro A) можно превратить цель в forall A, B.  (или, если B не зависит от A, то в A -> B.)
[16:42:27] <ermine> gds: я уже примерно поняла как делаются гипотезы - да, часто в них выносят варианты прохода по ветвям индукции, но вообще у адама больше сбивает с толку, что у него типа художественное определение терминов
[16:43:44] <gds> в общем, тут главное понять, что гипотезы -- то же, что forall-квантификаторы, только отдельно.  Это понимаешь?
[16:44:26] <gds> про адама -- ну хз, слишком абсракционизма не заметил.  А художественное часто в тему.
[16:47:22] <ermine> ладно
[16:47:31] <ermine> женские мозги значит у меня
[16:47:56] <ermine> gds: а снег у вас не сыплется?
[16:48:08] <ermine> хотя наверное у вас не европа
[16:49:52] <gds> был пипизодически вчера, таял быстро, аж неинтересно.  ну и температура не обычные +15..+20 для сезона, а -5..0.
[16:51:40] <ermine> ужасный дубак наверное для солнечной индии
[16:53:10] <gds> не, просто весна медленно идёт, а так -- бывают и весьма серьёзные зимы в нашей индии.
[16:57:26] <gds> ermine: а нащот coq -- возьми какой-нибудь мелкий проектик и вперёд.  Если там будет с серьёзными сайдэффектами -- поделюсь "мировой манаткой".  Если попроще сайдэффекты -- есть наколенные state/error трансформеры (соответственно, и манатки).
Можем и тут его поковырять, но если задолбаем сочятников, то я и в приватном порядке умею.
[16:58:45] <gds> (ну и всякие reader/writer манатки пишутся несложно, если нужны.  Кстати, у меня не только сам код манаток/трансформеров, но и доказательства выполнения всех их законов.)
[17:00:42] <gds> а если брать "мировую манатку" (которая грязный хак, но полезный аццки), то я даже бд из coq дёргаю нормально, всё работает.
[17:02:07] <ermine> gds: была мысля поиграться со своей либлой treap
[17:02:30] <gds> которая со случайными числами в узлах дерева?
[17:02:37] <ermine> там может и не быт сайд эффекта, если трахаться как в хаскеле
[17:03:04] <ermine> ну с двойной сортировкой, да
[17:03:37] <ermine> сбалансированное дерево но со приоритетами
[17:04:22] <gds> если делать чисто-функциональную структуру -- можно вполне.  Если мутабельную -- ну, профита от coq будет мало.
[17:05:43] <ermine> gds: а я не помню как у меня там, мутабельно или нет :)
[17:06:34] <gds> да и так, как бы, особо мало профита, разве что подоказывать что-то типа "оно таки сбалансировано", "добавление/удаление соблюдают семантику".  Лучше что-нибудь практически-полезное возьми.
[17:06:53] <gds> (я подразумеваю, что окамловская реализация у тебя вполне отлажена и хорошо работает.)
[17:07:49] ermine глянула одним глазом в начало файла teap,ml и увидела нечто похожее на копипасту из set.ml
[17:09:24] <ermine> еще не дочитала как в coq делается функтор хотя бы для функции сравнения
[17:09:49] <gds> а вот если бы взялась за finger tree, было бы хорошо.  Структура данных сама по себе хороша.  Но там аццки.  Тем более, вроде как, оно для хорошей производительности требует ленивость (забыл это дело -- поправьте, кто помнит), а как в coq с ленивостью -- мне неизвестно.  (можно, конечно, ввести внешние аксиомы типа
Axiom lazy : Type -> Type.
Axiom mklazy : (unit -> A) -> lazy A.
Axiom force : lazy A -> A.
Axiom lazy_prop : forall f, (force (mklazy f)) = f tt.
)
[17:12:13] <ermine> gds: для treap? в treap беда - часто выкидываешь корень, на его место встает другой элемент с наивысшим приоритетом
[17:12:15] <gds> ermine: функторы -- как в окамле.  А сравнения -- похитрее: http://coq.inria.fr/library/Coq.Structures.OrderedType.html (тем хитрее, что надо бы ещё доказать свойства того, что это именно сравнение.)
[17:13:01] <ermine> да, сравнения зачотные
[17:14:28] <gds> Kakadu: уважаю.
[17:18:44] Sun][ вышел(а) из комнаты
[17:50:59] f[x] вошёл(а) в комнату
[18:49:06] zinid вышел(а) из комнаты
[19:09:02] komar вошёл(а) в комнату
[19:35:01] <ermine> gds: туториал по coq еще более нежная штучка, теперь всё понятнее и понятнее становится!!!
[19:41:33] f[x] вышел(а) из комнаты
[19:44:13] Sun][ вошёл(а) в комнату
[20:01:19] f[x] вошёл(а) в комнату
[20:16:04] <gds> ermine: какой именно?
[20:17:23] f[x] вышел(а) из комнаты
[20:19:29] <ermine> gds: http://coq.inria.fr/V8.1/tutorial.html какой ж еще :)
[20:21:38] <gds> полезное чтиво.  Годно как для "доказывать матан", так и для "писать программы".
[20:23:04] <ermine> gds: ну это вторичное, только вот у адама я так и не поняла зачем нужна например команда intro или assumption
[20:23:29] <ermine> тут - просто другими словами показали чо к чему
[20:23:36] <gds> а теперь про эти команды понятно?
[20:24:05] <gds> (кстати, а меня спросить было лень?)
[20:24:08] <ermine> ну намного стало понятнее
[20:25:12] <ermine> я у тебя спросила как-то про intros
[20:25:20] <ermine> ты объяснял
[20:25:29] <ermine> не помню даже сути объяснения
[20:25:46] <ermine> тут intros тоже в двух словах тупо показали что к чему
[20:26:43] f[x] вошёл(а) в комнату
[20:27:34] <f[x]> intros даже я умею
[20:27:47] <f[x]> intros. apply. qed.
[20:28:36] <ermine> auto еще короче будет
[20:33:29] ermine выучила Inspect (про которую у адама еще не видела)
[20:55:02] pepyakaer вошёл(а) в комнату
[20:55:20] <pepyakaer> а в чём профит от написания софта на coq?
[20:56:24] <f[x]> пацаны на раёне уважают!
[20:56:25] <ermine> говорят, безглючный
[20:56:54] <pepyakaer> то есть, это язык программирования «с гарантиями»?
[20:57:44] <ermine> без гарантии
[20:58:06] <ermine> никто не мешает 2 умножить на 5 вместо поделить
[20:59:02] <pepyakaer> но чем-то он помогает?
[20:59:05] <ermine> просто coq может помочь в сертификации/валидации кода похлеще чем тест-юниты
[20:59:24] <pepyakaer> может доказать, что код работает?
[20:59:40] <ermine> используя всю скуку и унылость математических теорий
[21:00:13] <pepyakaer> унылость — веб-девелопмент; матан ок :)
[21:00:18] pepyakaer вышел(а) из комнаты
[21:00:46] <ermine> испугался
[21:04:12] pepyakaer вошёл(а) в комнату
[21:09:24] <pepyakaer> с чего бы, я логи читаю :)
[21:09:34] pepyakaer вышел(а) из комнаты
[21:12:13] <gds> про код можно доказать кое-какие вещи.  Но насколько оно надо -- зависит от задачи.
А ещё можно работать с "высокоуровневыми типами", тоже где-то рядом.  А типы эти могут содержать какие-то доказательства/инварианты про структуры данных.
Я очень кратко описал.
[21:13:46] <gds> если особых гарантий не нужно -- тут гораздо лучше окамл и лёгкие извращения на типах.  Как только извращения становятся тяжёлыми -- лучше подумать, может coq будет более уместен.
[21:14:30] f[x] вышел(а) из комнаты
[21:20:15] <ermine> gds: теперь всех желающих поизучать coq отговаривай от пустой траты времени :)
[21:27:18] pepyakaer вошёл(а) в комнату
[21:27:37] <pepyakaer> gds: как соотносятся coq и agda2?
[21:29:09] <pepyakaer> извините за дурацкие вопросы :)
[21:29:49] komar вышел(а) из комнаты: Logged out
[21:31:16] <ermine> соотносятся крутизной зависимых типов
[21:32:57] <gds> pepyakaer: 1. coq умеет кодогенерить в окамл/х-ь/схему, а агда -- в х-ь только, 2. в coq есть тактики и автоматизация доказательств с их помощью, а в агде -- только аналог coq'овского "auto" и какой-то режим для емакса, где слабое подобие тактик, 3. эстетам не нравится то, что Prop в coq является impredicative.  Из этого ничего для практики не следует, но.. эстеты!
А я, как "эстет с другой стороны", сообщу, что мне не нравится слишком много юникода в агде.
ermine говорит про разницу в зависимых типах, но вроде её нет, в обоих случаях в целом одно и то же.
[21:36:08] <ermine> gds: я ж сказала соотносятся, а не различаются :P
[21:38:56] <pepyakaer> тогда да, coq интереснее
[21:39:42] <pepyakaer> юникод — в смысле матан?
[21:39:53] <gds> юникод -- это юникод.
[21:40:06] <pepyakaer> ну математические символы
[21:40:40] <pepyakaer> не ascii-заменители, а полноценные сымволы?
[21:41:11] <gds> там и математические, и около.
в общем, поищи примеры кода на агде, поймёшь.
[21:42:12] <pepyakaer> ну мне такое тоже не очень нравится
[21:45:31] <gds> да поищи, сам увидишь.
[21:45:36] gds afk 30..60min
[21:47:03] <ermine> все языки надо запретить, кроме русского, тогда юникод будет не нужен
[21:48:53] <pepyakaer> так я поискал, посмотрел, вспомнил, как запретил юникод вместо ASCII в исходниках на хацкеле :)
[21:51:14] pepyakaer вышел(а) из комнаты
[21:51:30] <ermine> цикл (деньги больше 100) делать
деньги делить 2
конец
[21:51:45] <ermine> вот так надо писать!
[21:52:16] <ermine> а не переменные/имена только в юникоде, а все остальное на собачьем иностранном
[21:52:38] ermine жалеет, что русский кобол не выжил
[22:05:28] Sun][ вышел(а) из комнаты
[22:08:37] Sun][ вошёл(а) в комнату
[22:22:15] Typhon вышел(а) из комнаты: Replaced by new connection
[22:22:25] Typhon вошёл(а) в комнату
[22:31:55] komar вошёл(а) в комнату
[22:38:07] ermine вышел(а) из комнаты
[22:48:35] f[x] вошёл(а) в комнату
[23:02:13] Typhon вышел(а) из комнаты
[23:16:16] f[x] вышел(а) из комнаты
[23:32:31] Typhon вошёл(а) в комнату
[23:53:16] Typhon вышел(а) из комнаты