Objective Caml - Воскресенье, 21 февраля 2010

Objective Caml

ocaml@conference.jabber.ru

Воскресенье, 21 февраля 2010< ^ >

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

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

GMT+3
[00:00:23] sceptic вышел(а) из комнаты
[00:15:59] sceptic вошёл(а) в комнату
[00:21:38] ermine вышел(а) из комнаты
[00:22:36] gds вышел(а) из комнаты: Replaced by new connection
[00:22:37] gds вошёл(а) в комнату
[00:24:34] <gds> ygrek: в автоматически-применяемые тактики можно записать (auto и/или auto with xxx), либо в самой ide есть такая шняга ("выполнять какие-то команды после каждой применённой тактики").
но тактики -- фигня, давай доказывай через лямбды (refine и всё такое), это труЪ :)
[00:27:31] <ygrek> я до тактик ещё не дошёл :)
[00:27:43] <ygrek> руками всё выписываю
[00:33:57] <gds> руками -- refl, intro, auto и подобное, и каждая команда изменяет доказываемые утверждения? это и есть доказательство через тактики. (однако охотно верю, что ты не пользовался user-defined тактиками.)
[00:38:30] <ygrek> угу. я просто про то что reflexivity писать приходится часто - а слово длинное, я удивлён что нет какой-то клавиатурной комбинации
[00:41:41] <gds> пиши auto, быстрее будет, заодно не только reflexivity там. Хотя это слегка отдаёт читерством.
[00:43:20] <ygrek> auto в предпоследней главе - наверное автор замыслил не вести меня этим путём сначала.
[00:44:28] <ygrek> я идиот. только что сократил 40 строк бреда в 5. coq не отменяет применения мозга :)
[00:49:04] gds вышел(а) из комнаты
[01:35:51] ygrek вышел(а) из комнаты
[10:23:02] ygrek вошёл(а) в комнату
[10:57:14] gds вошёл(а) в комнату
[11:11:36] ermine вошёл(а) в комнату
[12:56:28] Typhon вошёл(а) в комнату
[12:58:19] <Typhon> http://github.com/jacknyfe/ocaml-erlang-port видели?
[12:59:23] Typhon вышел(а) из комнаты
[14:43:33] Typhon вошёл(а) в комнату
[16:24:01] gds вышел(а) из комнаты: Replaced by new connection
[16:24:02] gds вошёл(а) в комнату
[16:59:11] gds вышел(а) из комнаты: Replaced by new connection
[16:59:13] gds вошёл(а) в комнату
[17:40:50] gds вышел(а) из комнаты: Replaced by new connection
[17:40:51] gds вошёл(а) в комнату
[18:18:19] <ygrek> ocamlnet это конечно хорошо, но я вот недавно докатился - навелосипедил http сервер, ибо fastcgi синхронный и без мультиплексирования - это плохо, nethttpd слишком сложный, а eliom слишком радикальный
[18:21:55] <ygrek> http/1.0 конечно, но всё равно наружу nginx торчит, который к бэкендам 1.1 даже не умеет
[18:29:28] <Typhon> ygrek, покажешь?
[18:31:58] Typhon вышел(а) из комнаты
[18:44:12] <ygrek> ок, но там ничего интересного
[18:51:30] ygrek вышел(а) из комнаты
[18:54:15] Sergey Plaksin вошёл(а) в комнату
[18:55:12] Sergey Plaksin вышел(а) из комнаты
[18:55:23] ygrek вошёл(а) в комнату
[18:56:34] ygrek вышел(а) из комнаты: Replaced by new connection
[18:56:35] ygrek вошёл(а) в комнату
[18:57:12] ygrek вышел(а) из комнаты
[19:08:59] sceptic вышел(а) из комнаты
[19:54:56] sceptic вошёл(а) в комнату
[20:21:54] ygrek вошёл(а) в комнату
[22:36:41] ygrek вышел(а) из комнаты: Replaced by new connection
[22:36:41] ygrek вошёл(а) в комнату
[22:53:06] gds вышел(а) из комнаты: Replaced by new connection
[22:53:07] gds вошёл(а) в комнату
[23:31:36] gds вышел(а) из комнаты: Replaced by new connection
[23:31:37] gds вошёл(а) в комнату
[23:40:28] digital_curse вышел(а) из комнаты
[23:48:41] digital_curse вошёл(а) в комнату