Objective Caml - Четверг, 14 июня 2012

Objective Caml

ocaml@conference.jabber.ru

Четверг, 14 июня 2012< ^ >

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

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

GMT+4
[00:00:04] <Kakadu> нужны телепаты. http://paste.in.ua/4365/raw/
[00:09:42] Vinzent вышел(а) из комнаты
[00:10:09] Vinzent вошёл(а) в комнату
[00:13:21] Vinzent вышел(а) из комнаты
[00:19:03] Typhon вошёл(а) в комнату
[00:30:37] <gds> Kakadu: попробуй не телепатией, а анализом.  Например, можно выяснить, что нужно что-то типа -lcamlrun или -lasmrun сишному линкеру.
[00:31:23] <Kakadu> -lasmrun есть
[00:34:21] <gds> ну тогда ищи, чо-как оно пытается слинковать.  Ещё важен порядок либ для сишечки, причём противоположным (и менее естественным) образом, чем для окамла.
[01:01:05] ermine вышел(а) из комнаты
[01:09:37] Kakadu вышел(а) из комнаты
[01:22:35] bobry вышел(а) из комнаты
[01:38:53] ludovik вышел(а) из комнаты
[02:00:09] f[x] вышел(а) из комнаты
[03:00:18] akovbovich вошёл(а) в комнату
[03:19:19] akovbovich вышел(а) из комнаты
[03:20:28] ftrvxmtrx вышел(а) из комнаты
[04:39:09] letrec вошёл(а) в комнату
[06:04:26] letrec вышел(а) из комнаты
[06:14:13] Sun][ вошёл(а) в комнату
[06:32:07] Sun][ вышел(а) из комнаты
[06:33:25] Sun][ вошёл(а) в комнату
[06:51:21] Sun][ вышел(а) из комнаты
[08:41:03] bobry вошёл(а) в комнату
[09:42:31] bobry вышел(а) из комнаты
[11:29:13] ermine вошёл(а) в комнату
[11:32:54] ftrvxmtrx вошёл(а) в комнату
[12:15:33] letrec вошёл(а) в комнату
[12:17:40] Kakadu вошёл(а) в комнату
[13:42:39] Vinzent вошёл(а) в комнату
[13:44:30] ludovik вошёл(а) в комнату
[14:00:43] Typhon вышел(а) из комнаты
[14:08:41] ftrvxmtrx вышел(а) из комнаты
[14:10:06] ftrvxmtrx вошёл(а) в комнату
[14:26:31] ftrvxmtrx вышел(а) из комнаты
[14:32:24] ftrvxmtrx вошёл(а) в комнату
[14:57:24] Typhon вошёл(а) в комнату
[15:14:30] f[x] вошёл(а) в комнату
[15:25:21] tilarids вошёл(а) в комнату
[15:34:52] <f[x]> Kakadu: так выведи хотя бы как конкретно линкер вызывается
[16:39:43] f[x] вышел(а) из комнаты
[16:52:27] f[x] вошёл(а) в комнату
[17:02:27] <f[x]> ast_rewriter в транке
[17:06:50] <gds> f[x]: аштойта?  судя по названию должно быть вкусно.
[17:11:17] Sun][ вошёл(а) в комнату
[17:11:52] tilarids вышел(а) из комнаты
[17:12:04] tilarids вошёл(а) в комнату
[17:13:28] <gds> хотя вот, этого достаточно оказалось: http://gitorious.org/ocaml-svn-mirror/ocaml-dev/commit/89eb2bfa298132c26df446deedd7d5ebeb266c50
[17:13:40] <gds> круто, чо.
[17:14:35] <f[x]> ага
[17:15:21] <f[x]> т.е. это camlp4astfilter только без camlp4 и quotation'ов
[17:15:46] <f[x]> low tech, зато просто и прозрачно
[17:15:59] <gds> ровно то, что я и хотел.
[17:17:17] <gds> и не могли они это раньше запилить, а.  Тогда бы за coq может и не брался бы.
[17:20:27] <f[x]> а что, на camlp4 не осилил?
[17:21:25] <f[x]> а, ещё один бонус - реврайтеры конфликтовать друг с другом меньше будут чем расширения грамматики
[17:22:06] <gds> мутный этот camlp4.  документацию хрен найдёшь, документация гадкая.  rtfs не предлагать.
впрочем, реализовывать более мощную типизацию на camlp4 -- тоже не сахар, браться сходу не стал бы, не подумав дважыды.
[17:22:49] <f[x]> всё так
[17:29:23] <gds> а в coq, если не задрачиваться (и сразу решить с императивщиной; чего я долго сделать не мог) есть преимущества, даже если не думать головой: 1. любое значение из сорта Prop стирается в рантайме, 2. для индивидуальных функций доступна опция "инлайнить при экстракции", 3. ну и гарантии, даваемые более хитрыми типами (но можно и без них -- просто использовать окамлоподобные типы).
Вот только сейчас, уже как джва дня, вышел на нормальную производительность кодинга.  До этого было оналище.
[17:33:25] <f[x]> т.е. юзаешь coq как продвинутый компилятор?
[17:33:31] <f[x]> точнее препроцессор :)
[17:37:17] <gds> именно :)
ну и типы, таки.  Они хороши.
то есть, фактически, пишу на окамле, но там, где надо, использую хитрые типы.  (например, функция сравнения на равенство, которая в окамле 'a -> 'a -> bool, в coq имеет тип forall a b : t, {a = b} + {a <> b}, и это можно использовать в дальнейших доказательствах свойств функций.  (кстати, а экстрактится это дело таки в 'a -> 'a -> bool, миленько.))
императивщину представляю как unit -> 'a, ну и вот, всё получается.  ref'ы наколбасил, остальное тоже примерно понятно.
[18:09:17] <f[x]> крутотень
[19:24:15] Typhon вышел(а) из комнаты
[19:25:38] Kakadu вышел(а) из комнаты
[19:34:27] Sun][ вышел(а) из комнаты: Replaced by new connection
[19:34:28] Sun][ вошёл(а) в комнату
[20:19:34] Sun][ вышел(а) из комнаты
[20:24:16] Kakadu вошёл(а) в комнату
[20:25:55] Typhon вошёл(а) в комнату
[20:51:50] tilarids вышел(а) из комнаты: Machine going to sleep
[21:01:51] bobry вошёл(а) в комнату
[21:03:07] f[x] вошёл(а) в комнату
[21:09:52] Typhon вышел(а) из комнаты: Replaced by new connection
[21:10:12] Typhon вошёл(а) в комнату
[21:14:30] ftrvxmtrx вышел(а) из комнаты
[21:39:37] Typhon вышел(а) из комнаты
[21:49:59] letrec вышел(а) из комнаты
[23:07:57] tilarids вошёл(а) в комнату
[23:25:14] ftrvxmtrx вошёл(а) в комнату
[23:29:16] tilarids вышел(а) из комнаты: Machine going to sleep
[23:38:51] tilarids вошёл(а) в комнату
[23:41:28] Typhon вошёл(а) в комнату
[23:44:14] ftrvxmtrx вышел(а) из комнаты
[23:44:25] ftrvxmtrx вошёл(а) в комнату