Objective Caml - Пятница, 29 марта 2013

Objective Caml

ocaml@conference.jabber.ru

Пятница, 29 марта 2013< ^ >

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

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

GMT+4
[00:01:01] Typhon вышел(а) из комнаты
[00:29:47] UncleVasya вышел(а) из комнаты
[01:07:57] f[x] вошёл(а) в комнату
[01:34:51] f[x] вышел(а) из комнаты
[01:37:16] Kakadu вышел(а) из комнаты
[02:12:57] ftrvxmtrx вошёл(а) в комнату
[02:23:11] f[x] вошёл(а) в комнату
[02:29:49] f[x] вышел(а) из комнаты
[02:39:56] strobegen вышел(а) из комнаты
[02:40:33] tilarids вошёл(а) в комнату
[03:34:31] tilarids вышел(а) из комнаты: Computer went to sleep
[04:50:14] tilarids вошёл(а) в комнату
[05:11:21] ftrvxmtrx вышел(а) из комнаты
[05:16:17] ftrvxmtrx вошёл(а) в комнату
[07:39:39] tilarids вышел(а) из комнаты: Computer went to sleep
[08:12:39] zinid вошёл(а) в комнату
[08:15:44] tilarids вошёл(а) в комнату
[08:21:45] <zinid> Kakadu: а нефиг всякие плазмы юзать :)
[08:22:09] <zinid> у меня в xmonad никаких багов ;)
[08:55:39] strobegen вошёл(а) в комнату
[10:11:55] komar вошёл(а) в комнату
[10:12:02] tilarids вышел(а) из комнаты: Computer went to sleep
[10:35:10] akovbovich вышел(а) из комнаты
[10:43:47] akovbovich вошёл(а) в комнату
[11:03:59] ermine вошёл(а) в комнату
[11:14:35] komar вышел(а) из комнаты: Logged out
[11:36:11] Typhon вошёл(а) в комнату
[11:36:48] f[x] вошёл(а) в комнату
[11:55:41] Kakadu вошёл(а) в комнату
[11:56:45] <Kakadu> zinid: во-первых это плазма тут нипричем. Во-вторых, оказалось это не баг, а отключаемая фича.
[11:56:55] Kakadu вышел(а) из комнаты
[11:57:04] Kakadu вошёл(а) в комнату
[12:00:15] <zinid> Kakadu: хорошо, только не бей меня
[12:03:58] <ermine> а куда делся сайт киселева?
[12:06:01] <f[x]> ermine: на месте
[12:06:59] <ermine> f[x]: а как открываешь?
[12:07:23] <ermine> у меня не открывается
[12:07:29] <f[x]> okmij.org
[12:08:21] <ermine> хм, а теперь открылся
[12:10:52] Typhon вышел(а) из комнаты: Replaced by new connection
[12:11:02] Typhon вошёл(а) в комнату
[12:44:42] komar вошёл(а) в комнату
[14:13:03] komar вышел(а) из комнаты
[14:13:06] komar вошёл(а) в комнату
[14:49:22] ftrvxmtrx вышел(а) из комнаты
[14:52:21] <ermine> gds: таки да, sf по coq еще более нежная штука чем у адама, как раз для белокурых девочек
[15:14:17] <gds> ermine: ой, только не прикидывайся блондинкой.
[15:24:28] ermine скрипит ржавой извилиной над доказыванием примитивных теорем
[15:42:48] Zbroyar вошёл(а) в комнату
[15:43:19] ftrvxmtrx вошёл(а) в комнату
[16:29:36] Zbroyar вышел(а) из комнаты
[16:48:48] Typhon вышел(а) из комнаты: Replaced by new connection
[16:48:58] Typhon вошёл(а) в комнату
[16:55:48] komar вышел(а) из комнаты: Logged out
[16:56:52] <Kakadu> вы представляете как фиксить такое http://paste.in.ua/8150/raw ?
[16:59:30] <f[x]> покораптил хип
[16:59:32] <f[x]> теперь страдай
[16:59:34] <aleksey> сишные биндинги есть?
[16:59:46] <f[x]> там один сплошной биндинг :)
[16:59:54] <aleksey> о, вот тама бага
[17:00:07] <f[x]> понатый Gc.compact и принеси в жертву одного хаскельщиа - должно помочь
[17:00:12] <f[x]> * понатыкай
[17:04:23] <ermine> пасту удалили, ааа, не дали посмотреть на чей-то позор
[17:04:55] <aleksey> ermine: http://paste.in.ua/8150/
[17:05:41] <Kakadu> хмммм
[17:06:33] <Kakadu> А что, правда сишный new может выдать указатель на память зарезервированную камлом?
[17:08:20] <Kakadu> О, после первого compact всё упало
[17:10:01] ftrvxmtrx вышел(а) из комнаты
[17:12:22] <f[x]> нет, не может
[17:12:33] <aleksey> скорее где-то на хватает CAMLlocal и ему подобного
[17:19:33] <ermine> aleksey: баго в последней строчке!
[17:21:08] <gds> Kakadu:
> А что, правда сишный new может выдать указатель на память зарезервированную камлом?
может быть интереснее: ты сделаешь delete (кстати, new -- не сишный), указатель будет где-то висеть и ждать мусорщика, сишечька отдаст память, камло загребёт память, и вуаля -- теперь указатель указывает на хип.
[17:23:29] komar вошёл(а) в комнату
[17:24:45] <Kakadu> какая хренотень
[17:25:49] komar вышел(а) из комнаты
[17:25:56] komar вошёл(а) в комнату
[17:25:59] komar вышел(а) из комнаты
[17:26:24] komar вошёл(а) в комнату
[17:29:00] <ermine> не надо тогда писать на цэ или прибивать чужой биндинг, а переписывать на пюре камло
[17:29:21] <ermine> волосы чище будут
[17:30:45] <gds> не обязательно, можно вполне грамотно работать с указателями.  Например, custom block, туда повешать финализацию в виде free/delete, либо, в зависимости от ресурса, наоборот, делать free/delete в сишном коде, при этом ставя указатель в NULL после освобождения памяти.
[17:32:12] komar вышел(а) из комнаты: Logged out
[17:33:05] <gds> f[x]: дяденька, я всё правильно им сказал?
[17:33:56] <f[x]> сишка деткам не игрушка
[17:38:47] <ermine> в говядине есть указатели, но нет арифметики с ними, и это прально
[17:41:41] <ermine> арифметику вообще надо запретить как вредное рационализаторское изобретение
[17:44:45] <gds> только Таблицы Квадратных Уравнений!
[17:46:21] <ermine> а что они уравнивают?
[17:46:41] <Kakadu> квадратные трехчлены с нулем
[17:47:30] <gds> это таблицы, по которым из коэффициентов квадратного уравнения можно найти его корни с пригодной для практики точностью.  И никакой б-дской топологии!
[17:47:43] <ermine> (xyz)^2=0?
[17:48:08] <gds> ax^2+bx+c=0.  По таблицам ищешь строки с нужными a, b, c, получаешь корни.
[17:49:17] <ermine> вот если б так цены в магазинах рассчитывать
[17:50:46] ermine вчера почитала одну бумажку про хаскиль, в которой вместо нормальных букв в выражениях хаскиля употреблялись греческие буквы, и поняла, что это сделано для демотивации чтения
[17:51:06] <gds> нет.  Для приближения к илитности.
[17:53:08] <Kakadu> А если я дергаю камло из с++ной фукции-члена, мне надо CAMLparam0/CAMLreturn* ?
[17:57:12] <ermine> они ставятся в функцию, которая дергается из камла
[17:57:41] <ermine> если переменные камловские в том числе
[18:01:14] <Kakadu> Это то я знаю
[18:01:24] <Kakadu> Но может их надо пихать ещё куда-то куда я не знаю
[18:01:55] tilarids вошёл(а) в комнату
[18:02:02] <ermine> gds: а можно вгрузить в coqtop некомпиленный файл?
[18:02:45] <ermine> Kakadu: ну посмотри в доке, там был пример функции вызываемой в камло
[18:02:48] <gds> ermine: а зачем тебе вообще coqtop?
А так -- вроде нет.
[18:03:17] <ermine> gds: удобно rlwrap coqtop юзать
[18:03:29] <gds> coqide получше.
[18:03:34] <aleksey> ermine: proofgeneral в emacs или хотя бы coqide
[18:04:08] <ermine> aleksey: пробовали, правали, плевали
[18:04:17] <ermine> там курсор неустойчивый
[18:04:40] <Kakadu> ermine: был я в доке. Судя по ней не надо ничего такого
[18:04:48] <ermine> а чем rlwrap coqtop не то?
[18:05:20] <aleksey> неудобно туда-сюда по доказательствам бродить
[18:05:58] <gds> и неудобно, когда гипотезы и цель занимают много.  Скроллить замучаешься.
[18:06:15] <ermine> Kakadu: а чего бродить? доказывай только и qedай и забивай :)
[18:06:30] <ermine> пока до бродилки видимо не дошло
[18:07:27] <ermine> а вообще я просто уже не помню на какие кнопки давить, чтобы coq в емаксе появился
[18:07:55] <ermine> в статусе светится coq, и чо?
[18:08:22] <gds> бродить -- ну, попробовать один вариант, не проканало, откатываемся назад, пробуем дальше.  Всякие Undo есть, но как-то извратно.
[18:09:09] <ermine> gds: Restart и пробуешь!
[18:09:57] <gds> ermine: у тебя там под рукой, случаем, нет гамака и противогаза?  А то вспомнил одно интересное занятие, может тебе понравится.
[18:11:15] <ermine> gds: в противогазе?
[18:13:16] <ermine> run-coq-...
[18:27:20] <ermine> у меня coq.inria.fr не открывается
[18:27:46] <ermine> и выпить в доме нечего в вечер тяпницы
[19:04:24] Typhon вышел(а) из комнаты
[19:29:18] <ermine> gds: наверное книжка sf все же устарела, не компилится тамошний хак
[19:29:24] <ermine> для ltac
[19:29:26] komar вошёл(а) в комнату
[19:33:37] tilarids вышел(а) из комнаты: Computer went to sleep
[19:33:46] zinid вышел(а) из комнаты
[19:44:53] <ermine> gds:
Ltac move_to_top x :=
  match reverse goal with
  | H : _ * _ => try move x after H
  end.
[19:45:07] <ermine> gds: _ * _ ему не нравится
[19:53:11] ermine подобрала другие символы без понимания смысла, скомпилилось, так, посмотрим, много ли смысл значит...
[20:03:29] Kakadu вышел(а) из комнаты
[20:17:25] bobry вошёл(а) в комнату
[20:24:52] bobry вышел(а) из комнаты
[20:37:21] f[x] вышел(а) из комнаты
[20:48:59] <gds> ermine: не нужно гипотезы move it move it.  Бесполезное занятие.
А так -- должно быть
| H : _ |- _ => try move x after H
[20:52:22] <ermine> gds: там была бирюлька, которая вешает строчный заголовок над целью, а этот ltac видимо следил за тем чтобы бирюлька висела на самом верху
[20:52:46] <ermine> gds: я заменила ту ветку на [H: _ |- _] и оно согласилось скомпилиться
[20:53:36] <gds> да, оно даже и работает.
[20:54:06] <ermine> работает :))
[20:55:51] <ermine> вместо мозгов пригодились гугль и паттерн матчинг в виде встроенной в глаз матрицы
[21:03:17] <ermine> gds: вообще это хорошо, что в книжке sf есть упражнения
[21:04:14] <gds> только многие там туповатые.  "докажите то, что в реальной жизни доказывается одним auto/omega".
[21:06:35] <ermine> gds: а другое и не надо, программинг - это не искусство, а ремесло, надо только набить руку, а искусство будешь разводить в своем емаксе
[21:07:49] <ermine> вот если я прочту, как надо доказывать код парсера - точно делать нечего будет долгими зимними вечерами
[21:07:53] <gds> лучше набивать руку на автоматизации доказательств.
[21:08:34] <gds> как надо -- не прочтёшь, разве что погугли, кто-то доказывал.
[21:09:32] <ermine> ну я сюда ссылку на пдф давала, там уже доказали что можно одновременно парсить и претти-принтить по одному описанию
[21:09:49] <gds> конечно можно, и что?
[21:11:07] <ermine> gds: а что, надо доказывать что не всё так хорошо? :)
[21:12:08] <gds> не понял.  В общем, суть: берёшь то, что нужно сделать, и делаешь.
[21:13:23] <ermine> если бы еще знать как это делать. Рука не набита...
[21:14:26] <gds> а что нужно сделать?
[21:15:30] <gds> вообще, не парься по поводу доказательств, лучше вникай в хитрые типы, а доказательства подтянутся.
[21:17:00] <ermine> да доказательства в этой книжке уже не напрягают
[21:18:54] Kakadu вошёл(а) в комнату
[21:29:21] <ermine> gds: вот щас набила руку на команде rewrite гипотезами!
[21:36:08] <gds> ermine: это хорошо, но учитывай, что, если будешь переписывать равенством A терм B, то потом, как ни откидывай, при Eval compute in B будешь иметь громадный терм, содержащий следы A и всякие eq_ind.  Конечно, это если тебе важно получать адекватное при Eval compute.  Мне -- важно, так как использую coqide для работы с неким edsl.
[21:40:05] <gds> более того, чтобы получать адекватные результаты в Eval compute, я нафигачил сотни строк, содержащих доказательства простых арифметических вещей, в основном про сложение и меньше-равно.  А разгадка тому -- безблагодатность Qed'а, который запрещает разворачивать термы при вычислениях.
[21:40:33] <ermine> если уж кто-то наступал на грабли и не убрал их - то наступлю и я...
[21:41:19] <gds> но тебе Eval не очень нужно, если цель или просто подоказывать, или поэкстрактить.
[21:46:10] komar вышел(а) из комнаты
[22:10:40] ermine и без Eval таки забрела в такие дебри с помощью rewrite & induction, что просто ужас-ужас
[22:12:35] <gds> ermine: давай полный пример, разберёмся.
[22:18:25] <ermine> gds: чо, n+m=m+n :))
[22:19:25] <ermine> на третьем бранче блуждаю
[22:44:13] <gds> ermine: если не включать моск, то так: http://paste.in.ua/8153/
[22:44:25] <gds> специально самые тупые и предсказуемые способы брал.
[22:46:06] komar вошёл(а) в комнату
[22:51:42] ermine не смогла включить свой моск и сама не решила
[22:52:37] <gds> ermine: так прогуляйся по доказательству, посмотри, чо там творится.  Всё очень просто.
[22:52:41] ermine поленилась делать as, видимо зря
[22:53:05] <gds> да, as полезен для наглядства.  Без него мозги плавятся порой.
[23:04:16] <ermine> gds: я еще не проходила f_equal, так что оно отвергается
[23:04:47] <gds> ну докажи вспомогательную лемму, что n = m -> S n = S m, и далее apply её.
[23:05:11] <gds> а доказывается аж через rewrite; reflexivity.
[23:09:43] <ermine> тогда бяда
[23:51:03] aleksey рекомендует auto with arith :)
[23:53:15] <ermine> auto там тоже еще не проходился!
[23:53:42] <ermine> можно только с помощью вспомогательной леммы, если уж совсем никак индукцией и симлификацией
[23:56:40] <ermine> короче пока не решила эту задачку
[23:56:54] <ermine> пойду положу моск на подушку