Objective Caml - Четверг, 25 февраля 2010

Objective Caml

ocaml@conference.jabber.ru

Четверг, 25 февраля 2010< ^ >

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

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

GMT+3
[00:12:53] Typhon вышел(а) из комнаты
[00:15:55] ermine вышел(а) из комнаты
[00:21:24] Typhon вошёл(а) в комнату
[00:21:35] Typhon вышел(а) из комнаты
[00:35:54] digital_curse вышел(а) из комнаты
[01:02:38] <ygrek> ох ты ж. читаю http://lionet.livejournal.com/53209.html?thread=1295577#t1302745, замечаю знакомую фамилию - lindig - праавтор ocaml-mysql
[01:12:43] ygrek вышел(а) из комнаты
[01:23:58] gds вышел(а) из комнаты
[03:38:24] Sergey Plaksin вошёл(а) в комнату
[03:58:51] daapp вошёл(а) в комнату
[04:15:58] Sergey Plaksin вышел(а) из комнаты
[06:37:11] digital_curse вошёл(а) в комнату
[07:49:42] iNode вошёл(а) в комнату
[09:01:28] gds вошёл(а) в комнату
[09:49:50] Typhon вошёл(а) в комнату
[10:19:54] ygrek вошёл(а) в комнату
[10:37:44] Sergey Plaksin вошёл(а) в комнату
[11:19:58] f[x] вошёл(а) в комнату
[11:30:12] ermine вошёл(а) в комнату
[12:26:37] Sergey Plaksin вышел(а) из комнаты
[12:55:56] Yakov Zaytsev вошёл(а) в комнату
[12:55:56] Yakov Zaytsev вышел(а) из комнаты
[13:50:58] Yakov Zaytsev вошёл(а) в комнату
[13:52:24] <Yakov Zaytsev> када уже будет 3.12-то!
[13:52:49] <Yakov Zaytsev> опять у меня проблемы. с окамлом из цвс надо править camlp5
[13:53:09] <Yakov Zaytsev> кстати, я собрал окамл из цвс под N900 ;-)
[13:55:26] <gds> под N900 -- крут.
camlp5 -- мелочи, переходной период, после релиза его подправят (а то и сейчас уже готовы исправления, есть вероятность).
[13:55:53] <Yakov Zaytsev> я блин все никак не найду их секретный репо
[13:55:59] <Yakov Zaytsev> для камлп5-то
[13:56:12] <Yakov Zaytsev> то бы давно уже оттуда его брал. глядиш проще б вышло.
[13:56:21] <Yakov Zaytsev> мне-то оно надо чтоб Кок на Н900 собрать.
[13:57:24] <f[x]> даёшь кок на iphone. слоган - "доказательство одним пальцем"
[13:57:40] <gds> автору camlp5 писать надо, чтобы репку дал и заодно рассказал, как там дела с 3.12.
[13:58:00] <Yakov Zaytsev> там кстати фигня в камлп5.. оно под 3.12-то есть и все в порядке. но когда у тебя из цвс версия то камл грит что он не просто "3.12" а еще и девХ-че-то-там.. отсюда по ходу дела валится сборка в lib из camlp5
[13:58:35] <gds> а, если такая фигня, то можно и самостоятельно поправить.
[13:58:47] <Yakov Zaytsev> то есть сам-то camlp5 собирается в байткод. а потом в папке lib фатал еррор...
[13:59:01] <Yakov Zaytsev> угу угу угу угу
[13:59:11] <Yakov Zaytsev> вот че за ерунда тут - угу
- Error sending message 'угу': too long message
[13:59:40] <gds> а ваще да, скомпилировать coq под iphone -- идея хорошая.  глядишь, он наконец-то станет модным.
[14:00:51] <Yakov Zaytsev> главное в coqide оставить только одну такую кнопку жирную Auto
[14:01:15] <Yakov Zaytsev> gds: а ты что делаеш с кок? :-)
[14:01:53] <gds> если ты про "у меня есть кок и интернет", то, пожалуй, как все.
[14:03:37] <gds> а так -- всякую мелочь доказывал, пробовал program extraction (неинтересно, так как только риальни сложные алгоритмы так разумно кодить), пробовал кое-что из категорий моделировать, но весьма тупо, и заткнулся на сложностях доказательства.
[14:04:36] <gds> вот хочу новую штуку попробовать, ща найду урло.
[14:04:57] <gds> http://antilamer.livejournal.com/312540.html
[14:05:07] <Yakov Zaytsev> я б кстати всегда пользовал extraction если б так же быстро писал док-ва как программы.. даже разучил окамл :-) ну, почти разучил.
[14:05:53] <Yakov Zaytsev> хочу в одну простенькую in-house gui тулу на ocaml вставить certified кусочек.
[14:06:44] <Yakov Zaytsev> Матью все никак не доделает я так понимаю.
[14:07:27] <gds> а в кусочке хитрая логика?  какого рода, если не секрет?
[14:07:40] <Yakov Zaytsev> этот ламер слишком восторжено пишет
[14:08:30] <Yakov Zaytsev> бугага, там смотрю все экшперты набежали как обычно в жжешечке..
[14:08:51] <Yakov Zaytsev> каждый назвал свою ассоциацию на слова автоматическое док-во теорем
[14:09:07] <Yakov Zaytsev> gds: ну, ты ведь мог раньше взять refine+auto
[14:09:23] <Yakov Zaytsev> всякие auto это поиск.
[14:09:40] <Yakov Zaytsev> с помощью них можно сводить только элементарные связки
[14:09:58] <Yakov Zaytsev> мало-мальски неочевидное надо в ручную доказывать, а то авто может выдать не лучший алгоритм.
[14:10:08] <Yakov Zaytsev> textbook material.
[14:11:00] <Yakov Zaytsev> кстати книжка Zhao про кок хорошая книжка, чтобы разобраться почему все так сделано, типа зачем нам отдельно Проп и Сет и тп..
[14:14:24] <Yakov Zaytsev> а так мы с коллегой из итмо пишем диссер на коке.
[14:14:38] <Yakov Zaytsev> если интересно - джойн. там чето много работы выходит :-)
[14:15:57] daapp вышел(а) из комнаты
[14:19:45] <gds> про жжшных экспертов -- товарищ, связанный с "mps", точно "экшперт".
refine+auto -- оно есть, и даже можно тактики добавлять, но в конце концов мне ход доказательства стал очевиден, и я забил.  А так -- пусть себе выдал бы не лучший алгоритм доказательства, мне не жалко.
про диссер -- лично у меня сейчас мало времени на компы вообще, даже на тупой кодинг рука редко поднимается, поэтому лично я пас в ближайшие полгода так-эдак.
[14:22:17] <Yakov Zaytsev> gds: а чем ты занимаешься, если не секрет?
[14:24:44] <gds> сейчас -- не слишком интеллектуальная работа (большая опердень) на полный рабочий день и внезапно появившаяся семья с кучей всего, что нужно сделать, на остальное время.  ну и отдых, само собой -- пепси-пейджер-эмтиви.
[16:23:25] f[x] вошёл(а) в комнату
[16:28:36] Yakov Zaytsev вошёл(а) в комнату
[17:02:36] ermine вошёл(а) в комнату
[17:21:35] olegfink вошёл(а) в комнату
[17:34:06] Yakov Zaytsev вошёл(а) в комнату
[17:48:34] Yakov Zaytsev вышел(а) из комнаты
[18:20:34] gds вошёл(а) в комнату
[18:21:46] ygrek вошёл(а) в комнату
[19:27:31] f[x] вошёл(а) в комнату
[20:28:00] Typhon вошёл(а) в комнату
[20:28:47] <Typhon> к fprog#4-шуму подготовились? :)
[20:31:03] akon32 вошёл(а) в комнату
[20:32:29] akon32 вышел(а) из комнаты
[20:44:25] sceptic вошёл(а) в комнату
[20:44:30] sceptic вышел(а) из комнаты
[21:29:05] iNode вошёл(а) в комнату
[21:36:45] <ygrek> что-то я его читаю медленней чем новые номера выходят
[21:40:10] <Typhon> по свежему: первую статью можно пропустить, вторая (первая половина прочитана) похожа на маркетинговый булшит "use clojure!1!!!" :)
[21:41:05] <Typhon> ygrek, до работы не на общественном транспорте едешь? формат как раз для него: серьезное не что-то не почитаешь, а художественное не хочется :)
[21:42:05] <ygrek> да, это вариант, если не в подвешенном состоянии
[21:42:52] <Typhon> мне то вообще хорошо: в ридер закинул и читай :)
[21:51:34] <Typhon> жив mlton, мол, жив, а на сайте трусами торгуют: mlton.org
[21:54:25] cgfbna3h_s вошёл(а) в комнату
[21:54:26] cgfbna3h_s вышел(а) из комнаты
[22:11:18] sceptic вошёл(а) в комнату
[22:17:42] gds вышел(а) из комнаты
[23:07:52] gds вошёл(а) в комнату
[23:44:35] gds вышел(а) из комнаты
[23:59:48] ermine вышел(а) из комнаты