Objective Caml - Понедельник, 18 марта 2013

Objective Caml

ocaml@conference.jabber.ru

Понедельник, 18 марта 2013< ^ >

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

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

GMT+4
[00:07:55] komar вышел(а) из комнаты: Replaced by new connection
[00:07:55] komar вошёл(а) в комнату
[00:29:05] Typhon вошёл(а) в комнату
[00:31:56] Typhon вышел(а) из комнаты: Replaced by new connection
[00:32:06] Typhon вошёл(а) в комнату
[01:19:11] Typhon вышел(а) из комнаты
[01:43:16] Kakadu вышел(а) из комнаты
[02:28:04] Zbroyar вышел(а) из комнаты
[04:16:20] tilarids вошёл(а) в комнату
[05:02:31] f[x] вошёл(а) в комнату
[05:23:25] f[x] вышел(а) из комнаты
[05:26:32] tilarids вышел(а) из комнаты: Machine going to sleep
[05:50:07] f[x] вошёл(а) в комнату
[06:17:27] tilarids вошёл(а) в комнату
[07:35:20] ermine вошёл(а) в комнату
[07:43:11] tilarids вышел(а) из комнаты
[07:45:53] tilarids вошёл(а) в комнату
[08:52:00] tilarids вышел(а) из комнаты
[09:08:33] tilarids вошёл(а) в комнату
[09:13:23] tilarids вышел(а) из комнаты
[09:16:59] tilarids вошёл(а) в комнату
[10:04:39] komar вышел(а) из комнаты: Logged out
[10:09:33] ftrvxmtrx вышел(а) из комнаты
[10:27:43] Typhon вошёл(а) в комнату
[10:30:00] tilarids вышел(а) из комнаты: Machine going to sleep
[10:41:38] Typhon вышел(а) из комнаты
[11:26:57] Sun][ вошёл(а) в комнату
[11:34:03] zinid вошёл(а) в комнату
[11:58:46] komar вошёл(а) в комнату
[12:19:33] Kakadu вошёл(а) в комнату
[12:25:48] Typhon вошёл(а) в комнату
[13:06:49] ftrvxmtrx вошёл(а) в комнату
[14:08:33] Sun][ вышел(а) из комнаты
[14:15:03] Sun][ вошёл(а) в комнату
[14:16:41] Kakadu вышел(а) из комнаты
[14:29:25] Typhon вышел(а) из комнаты
[14:29:35] Typhon вошёл(а) в комнату
[14:32:29] Kakadu вошёл(а) в комнату
[14:49:54] <ermine> gds: твой любимый делим-сс появился в опаме
[14:50:16] <gds> ermine: не такой уж он любимый.  Я его даже не использовал.
[14:51:01] <ermine> gds: да я поерничать вылезла
[14:56:18] <aleksey> ermine: юзай coq!!!
[14:58:38] <ermine> aleksey: а сокеты там есть?
[14:59:39] <ermine> aleksey: можно доказать существование сульци, если есть сокеты и ssl и всё остальное
[15:01:19] ermine щас наверное будет программить на яве
[15:07:00] Typhon вышел(а) из комнаты
[15:09:09] f[x] выяснил что ocaml-java не умеет в внешние библиотеки и в результате тоже программил на яве на прошлой неделе..
[15:13:04] Typhon вошёл(а) в комнату
[15:13:16] <ermine> f[x]: мне aleksey тоже пытался сосвалать ocaml-java для программеража под андроид!
[15:26:37] f[x] вышел(а) из комнаты
[15:59:30] strobegen вошёл(а) в комнату
[16:09:37] <gds> http://gds.psto.net/tsiezf -- coq, ocaml, extraction.
[16:15:50] <aleksey> ermine: видишь, человек делом занимается!
[16:16:29] <gds> не такое уж это и дело.
[16:18:24] <aleksey> gds: а тебя не интересуют задачки на coq?
[16:19:04] komar вышел(а) из комнаты: Logged out
[16:19:30] <ermine> aleksey: а кто чувак, а кто не чувак???
[16:19:48] <aleksey> ermine: ась?
[16:20:22] <gds> aleksey: не совсем понял, разверни мысль.
[16:20:57] <ermine> gds: сажу тебе по секрету -- aleksey асилил coq!!!
[16:21:02] <aleksey> gds: ну типа такого: подставить вместо ??? что-то разумное и доказать
Lemma blabla : forall (f : R -> R), (forall (x y : R), f (x * f y) + f (y + f x) - f (x + y * f x) = x) -> (forall (x : R), f x = ???).
[16:22:19] <ermine> я же вам говорила!!!
[16:22:38] <ermine> осталось еще букву A научится переворачивать вверх ножками
[16:22:40] <gds> aleksey: конкретно это -- задачка не на coq, а на математику.
[16:22:55] <ermine> а то какие-то фораллы
[16:23:32] <ermine> gds: aleksey гений на projecteulers!!!
[16:23:39] komar вошёл(а) в комнату
[16:23:43] komar вышел(а) из комнаты: Logged out
[16:23:52] <aleksey> gds: нуу, тут и то и другое
[16:23:54] <ermine> наверное не видит разницы между coq и математегой
[16:24:55] <aleksey> gds: мечтаю чтоб на олимпиадах по математике решения писали на coq
[16:25:05] <gds> конкретно эту задачку решать влом (надо брать бугагу в ручку), но вообще -- задачки интересны.
[16:25:20] <gds> про олимпиады -- было бы неплохо.
[16:25:20] ermine кстати подписалась на мейллист cl-mirage, где заправляет Anil (avsm), там и про coq есть и про opam и вообще про всё
[16:25:28] <aleksey> но пока не видел ни одного школьника осилевшего coq
[16:26:20] <gds> учитывая, что в школах преподают (и очень надеятся в математике) на "классическую логику", и игнорируют "конструктивную", как бы понятно, почему мало асиливших.
[16:26:49] komar вошёл(а) в комнату
[16:27:09] <aleksey> в школах логику вообще не особо преподают
[16:27:43] <aleksey> на олимпиадах встечались дети, не понимающие что из P -> Q не следует Q -> P
[16:27:44] <gds> хз, у нас преподавали ок.  диаграммы в вену, логические формулы.
[16:27:58] komar вышел(а) из комнаты: Logged out
[16:28:35] <gds> конечно, в универе, где я отучился целых чуть меньше чем полтора года, логику преподавали чуть веселее, с огоньком, можно даже сказать.
[16:29:45] <gds> ну, поболтали о хорошем, и /me пошол трахаться с графами на жс.
[16:29:58] <aleksey> ужос
[16:33:02] <gds> кстати, пока вспомнил:
Section Women's_logic.
Parameter is_desirable : Prop -> Prop.
Axiom axm1 : forall (P Q : Prop), (P -> Q) -> is_desirable Q -> P.
или нет?
(к ermine это не относится, у неё другой модуль загружен.)
[16:34:05] <aleksey> хех
[16:34:19] komar вошёл(а) в комнату
[16:39:18] <ermine> сам ты параметр
[16:43:13] komar вышел(а) из комнаты: Logged out
[16:57:39] komar вошёл(а) в комнату
[17:11:50] zinid вышел(а) из комнаты
[17:15:58] Sun][ вышел(а) из комнаты
[18:07:49] strobegen вышел(а) из комнаты: Replaced by new connection
[18:07:51] strobegen вошёл(а) в комнату
[18:36:46] <ermine> gds: читал скучную бумагу?  http://staff.aist.go.jp/reynald.affeldt/documents/plpv2012-preprint.pdf
[18:45:56] f[x] вошёл(а) в комнату
[18:45:58] f[x] вышел(а) из комнаты
[18:48:21] <ermine> aleksey: кстати тебе тоже
[18:52:31] f[x] вошёл(а) в комнату
[19:03:20] Typhon вышел(а) из комнаты: Replaced by new connection
[19:03:30] Typhon вошёл(а) в комнату
[19:34:58] Kakadu вышел(а) из комнаты
[19:37:14] Kakadu вошёл(а) в комнату
[19:59:05] Kakadu вышел(а) из комнаты
[20:01:12] komar вышел(а) из комнаты: Logged out
[20:04:18] Typhon вышел(а) из комнаты
[20:05:16] Typhon вошёл(а) в комнату
[20:05:24] Typhon вышел(а) из комнаты
[20:40:50] Sun][ вошёл(а) в комнату
[20:45:39] ftrvxmtrx вышел(а) из комнаты
[21:16:17] <gds> ermine: не читал.  читаю.  мимими!
[21:22:47] <gds> однако, в 3.2.1, figure 3, очевидная опечатка.
[21:23:11] <f[x]> "диаграмму в вену" <- like!
[21:27:32] <ermine> gds: шо, надо почитать?
[21:28:02] <gds> ermine: дочитаю -- скажу точнее.
[21:28:10] <ermine> gds: ссылку кстати кидал anil, в свой мейллист для неущербных мозгом
[21:28:52] <ermine> там обсуждалось invertible protocol или invertible parsing и чуток tls упомянули
[21:29:07] <gds> свой мейллист -- это какой?
[21:29:23] <gds> адрес не нужен, интересно вкратце описание.
[21:29:43] <ermine> не, все могут подписаться на cl-mirage, в гугле оно первой ссылкой сразу подписаца
[21:30:01] <ermine> там правда не совсем мейллист - все пишут друг другу и cc в мейллист
[21:30:14] <ermine> чтобы остальные почитали чужую переписку
[21:32:24] <gds> ermine: дочитал.  Читать -- стоит, особенно тебе.
[21:32:59] <ermine> gds: ок
[21:33:40] <gds> они там говорят, что подход неэффективный, но можно кое-что покрутить, чтобы было приемлемо по производительности, как интуиция подсказывает.
[21:40:28] Kakadu вошёл(а) в комнату
[21:53:12] <ermine> в опаме у меня уже 104 пакета устаневлены
[21:53:12] f[x] вышел(а) из комнаты
[21:53:28] <ermine> остальные желаемые пока не ставятся
[22:08:46] ermine вышел(а) из комнаты
[22:13:41] komar вошёл(а) в комнату
[23:05:34] Typhon вошёл(а) в комнату
[23:35:09] strobegen вышел(а) из комнаты
[23:35:45] Zbroyar вошёл(а) в комнату
[23:40:47] tilarids вошёл(а) в комнату
[23:42:05] tilarids вышел(а) из комнаты: Machine going to sleep
[23:48:39] komar вышел(а) из комнаты