Objective Caml - Понедельник, 5 ноября 2012

Objective Caml

ocaml@conference.jabber.ru

Понедельник, 5 ноября 2012< ^ >

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

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

GMT+4
[00:13:13] dzhon вышел(а) из комнаты
[00:16:29] Typhon вошёл(а) в комнату
[00:21:41] Typhon вышел(а) из комнаты
[00:23:06] Typhon вошёл(а) в комнату
[01:38:35] Kakadu вышел(а) из комнаты
[01:44:49] <tilarids> к дневному обсуждению прожорливости окамля - хаскель съедает 5.5 гиг и погибает от руки oom_killerа. Так что из всех опробованных C++ - чистый победитель, OCaml/Java - справляются, но с большими затратами по памяти, Python/Haskell - погибают от рук oom_killerа, Scala - не справляется с heap size = 5GB и падает c OutOfMemory
[02:04:45] <tilarids> без таплов  и боксинга - 3.7 гигов и в 15 раз медленней, чем плюсы
[02:05:00] <tilarids> (на окамле)
[02:24:43] tilarids вышел(а) из комнаты: Machine going to sleep
[02:37:54] Andrey Popp вышел(а) из комнаты
[03:10:21] ftrvxmtrx вошёл(а) в комнату
[04:07:01] tilarids вошёл(а) в комнату
[05:22:28] Typhon вышел(а) из комнаты
[09:42:47] Andrey Popp вошёл(а) в комнату
[09:55:51] Andrey Popp вышел(а) из комнаты
[10:05:37] Andrey Popp вошёл(а) в комнату
[10:36:40] Andrey Popp вышел(а) из комнаты
[10:36:43] Typhon вошёл(а) в комнату
[10:37:38] Andrey Popp вошёл(а) в комнату
[10:43:27] dzhon вошёл(а) в комнату
[10:51:32] ludovik вошёл(а) в комнату
[11:42:36] ermine вошёл(а) в комнату
[11:49:46] Sun][ вошёл(а) в комнату
[12:51:44] Sun][ вышел(а) из комнаты: Replaced by new connection
[12:51:45] Sun][ вошёл(а) в комнату
[13:06:26] <ermine> <.<
[13:06:32] <ermine> >.>
[13:06:43] <ermine> а где gds?
[13:13:33] Sun][ вышел(а) из комнаты
[13:14:27] Sun][ вошёл(а) в комнату
[13:21:23] gds вошёл(а) в комнату
[13:26:49] <gds> ermine: чочо
[13:30:39] <gds> tilarids: если будет не влом, дай посмотреть окамловский исходник, который 3.7Гб жрёт.
[13:40:42] <ermine> gds: а можешь объяснить буззворд discriminate?
[13:40:56] <gds> это не buzzword.
[13:41:20] <ermine> ну такое же как reflexivity, надо полагать
[13:41:54] <ermine> пока не догадалась что ему в русской математике соответствует
[13:47:39] <gds> внезапно нашёл http://adam.chlipala.net/itp/tactic-reference.html , там про это есть.
но русского перевода нет, вроде.
суть тактики: в случаях, когда есть выражение Con1 .. = Con2 .., где это два разных конструктора индуктивного типа данных, тактика учитывает такой факт: если значение создано разными конструкторами, то значения неравны.  (и, например, если у нас есть равенство Con1 = Con2, полученное в какой-то абсурдной ветке доказательства, то, применив discriminate, можно доказать любое выражение, хоть False создать.)
[13:48:03] <tilarids> gds, http://codepad.org/fTbdA1Fw
[13:48:24] <gds> ermine: Inductive t := | Con1 | Con2. Goal (Con1 = Con2 -> False). discriminate. Qed.
[13:48:25] <tilarids> как я понимаю, Array флоатов должен быть unboxed
[13:48:33] <tilarids> отсюда 3.7 гига
[13:49:48] ftrvxmtrx вошёл(а) в комнату
[13:50:06] <gds> так тут в массиве туплы флоатов.  по крайней мере, туплы создаются.
[13:52:07] <gds> да, и если флоаты в тупле, то они boxed тоже, в этом же тупле.  То есть, получается: массив хранит указатель на тупл, тупл = тег + указатель на x + указатель на y, где каждый из x и y -- тег + double.
[13:52:49] <tilarids> где? я слепой, не вижу :(
[13:53:22] <tilarids> в енуме - туплы интов
[13:53:37] <tilarids> а потом должны быть просто флоаы
[13:58:14] <gds> увидел.  Заодно посмотрел код более плотно.  Но я бы не так делал, и было бы быстрее, очевидно.  И сомнительно слегка, что плюсовый код такой же гламурный.
[13:59:06] <tilarids> да почти один в один. только все in-place делается
[13:59:27] <tilarids> а как бы ты делал? Без list comprehension?
[13:59:42] <gds> ну а тут создаёшь промежуточные значения и хочешь такой же скорости.
[14:01:10] <gds> я уже понял алгоритм.  Сейчас есть реаллайф всякий, видимо вечером сделаю.
А обязательно вообще создавать полный массив и сортировать его?  (то есть, это критичное место для пиписькомерства в данной задаче?)
[14:02:00] <tilarids> и для решения задачи, в общем-то
[14:02:14] <tilarids> можно массив уменьшать, но это уже украшательства
[14:02:56] <tilarids> про енамы - это же O(1) по памяти промежуточные значения, а не O(n)
[14:03:43] <tilarids> плюс компилер должен что-то инлайнить. плюсовый вот инлайнит
[14:04:16] <Andrey Popp> tilardis, кстати ты в haskell использовал массивы с fusion?
[14:04:59] <Andrey Popp> для ocaml что то подобное интересно есть?
[14:06:32] <tilarids> Andrey Popp, нет. я даже marray не стал юзать, потому что кода становится сильно больше, чем обычно, нечестное сравнение
[14:07:15] <Andrey Popp> не понимаю про честность
[14:08:58] <tilarids> код на любом языке можно ускорить тем или иным способом. например, написав сишный биндинг
[14:10:30] <tilarids> а я хочу, чтобы код был написан красивым стандартным для языка почерком, но при этом работал быстро и мало ел памяти
[14:11:11] <Andrey Popp> ну массивы с fusion ничего страшного с кодом не делают...
[14:11:28] <tilarids> хаскель вот можно ускорить заюзав uvector и перейдя на unboxed float, от таплов тоже нужно отказаться
[14:12:07] <Andrey Popp> есть unboxed tuples
[14:12:24] <tilarids> Andrey Popp, я не знаю, как с fusion делать. Если покажешь - буду благодарен. Пока что использование uvector приводит к разбуханию кода :(
[14:12:46] <tilarids> ну, и это уже нестандартная для языка либа
[14:12:47] <Andrey Popp> tilardis кинь код на haskell
[14:13:21] <Andrey Popp> ну это в dph есть, он вроде как входит в ghc
[14:14:22] <tilarids> http://codepad.org/8il7IMrV
[14:14:38] <ermine> gds: не поняла совсем, цель discriminate - помочь согласиться с абсурдным значением?
[14:15:05] <Andrey Popp> не, ну ты конечно издеваешься, сравнивая массивы в плюсах и linked list в haskell :-)
[14:18:12] <gds> ermine: цель -- указать, что равенство значений, созданных разными конструкторами, невозможно.  Причём тут "согласиться".
[14:18:43] <tilarids> Andrey Popp, я в Array перегонял, разницы никакой
[14:19:06] <Andrey Popp> ну у тебя tuples тут же тоже боксинг делают
[14:19:09] <Andrey Popp> и даже Int
[14:20:08] <gds> tilarids: так какая конечная цель -- отсортированный массив или что-то более конкретное?
[14:20:15] <tilarids> к.о. :) я понимаю, почему хаскель страдает теми же проблемами, что и окамль
[14:21:00] <Andrey Popp> tilardis, это я про "я в Array перегонял, разницы никакой"
[14:21:02] <tilarids> gds, отсортированный массив
[14:22:00] <tilarids> Andrey Popp, в хаскеле еще проблема с Array в том, что их не так просто сортировать
[14:22:29] <ermine> gds: а.
[14:30:55] <tilarids> плюсы с линкед листами - 40 секунд, 3.4 гига по памяти (это с таплами)
[14:35:42] tilarids вышел(а) из комнаты: Machine going to sleep
[14:39:59] <ermine> gds: а кто именно делает assert на таких сравнивалках - сам discriminate (ассертит и отбрасывает в сторонку) или специальная гипотеза?
[14:43:11] <gds> ermine: можно применить discriminate и к текущей цели доказательства, если она содержит такое равенство, и к гипотезе, содержащую такое равенство, и вывести из неё False, таким образом доказав цель.  Вот возьми тот мой тупой пример и замени доказательство на "intro H. discriminate H.", вот как-то так.  Но если равенство содержится в цели доказательства, вроде discriminate умеет относительно умно работать с этим.
[14:43:16] <gds> всё, afk 3h.
[14:48:15] <ermine> gds: да кстати, а intro отличается от intros? :)
[14:48:30] ermine подправила парик блондинки
[14:58:26] tilarids вошёл(а) в комнату
[14:59:58] <f[x]> > 1. работа со списками -- дольше, обычно, чем с массивами.
вот это вот не всегда так, хотя казалось бы
[15:01:00] Andrey Popp вышел(а) из комнаты
[15:07:53] <f[x]> последняя ссылка на codepad отдаёт 500, оно видимо пытается код выполнять?
[15:49:35] <tilarids> я пропустил обсуждение?
[15:50:25] <f[x]> не
[15:51:14] <f[x]> стоило мне только отойти на 5 минут тут опять кокбеспредел начался!
[15:53:08] <tilarids> кокбеспредел - это хорошо
[15:53:50] <tilarids> клевые статические проверки чуть ли не важнее скорости и памяти
[15:55:51] ludovik вышел(а) из комнаты
[15:56:22] dzhon вышел(а) из комнаты
[16:08:27] Sun][ вышел(а) из комнаты
[16:16:12] letrec вошёл(а) в комнату
[16:16:28] letrec вышел(а) из комнаты
[16:16:43] letrec вошёл(а) в комнату
[16:31:39] UncleVasya вошёл(а) в комнату
[16:54:46] dzhon вошёл(а) в комнату
[16:55:10] dzhon вышел(а) из комнаты
[17:14:14] <tilarids> кстати, в моем искусственном бенчмарке неожиданно на второе место вырвался pypy - если переписать все без таплов и list comprehension - получается в 1.5 раза дольше, чем плюсовый вариант и всего 1.3 гига памяти
[17:37:07] <ftrvxmtrx> tilarids: а можно на c++ версию глянуть?
[17:39:40] <tilarids> ftrvxmtrx, http://codepad.org/ki9YML78 это без таплов
[17:47:14] Kakadu вошёл(а) в комнату
[18:10:20] ftrvxmtrx вышел(а) из комнаты
[18:13:32] Typhon вышел(а) из комнаты
[18:14:48] Typhon вошёл(а) в комнату
[18:18:28] <gds> tilarids: прошу, погоняй эту версию: http://paste.in.ua/7687/ , понятно, она в твой бенчмарк не вписывается, но интересно сравнение с твоей окамловской и с плюсовой, по памяти и по времени.
[18:20:03] <gds> ermine: intro -- одну стрелку кушает в гипотезы, intros -- много.  intros имя1 имя2 = intro имя1; intro имя2.  intros без аргументов -- все стрелки кушает.  Ну, стрелка -- forall обычно.
[18:22:38] <gds> ermine: про именование гипотез -- вопрос сложный, пока делай как хочешь, а потом по мере чтения cpdt одамчег тебе расскажет, как лучше делать.
[18:25:11] <tilarids> gds, как собирал? И каким окамлем?
[18:26:57] <f[x]> это же revised
[18:27:07] <gds> тьфуты.
[18:27:11] <f[x]> -pp camlp4r
[18:27:12] <gds> ocamlopt -warn-error A -pp camlp4r a.ml -o a.native
[18:27:21] <f[x]> норкоман
[18:27:51] <gds> да!  А что случилось?
[18:29:10] <f[x]> тк држт!
[18:29:21] <gds> збс!
[18:29:50] <tilarids> 85 секунд, 1.1 гига
[18:30:06] <tilarids> это чуть меньше, чем у pypy, но почти в 8 раз медленней
[18:30:31] <tilarids> у меня 3.12.1, староват, конечно.
[18:31:04] <gds> в 8 раз медленнее плюсов, в смысле?
3.12.1 -- особо не важно тут.
[18:33:51] <tilarids> 85 секунд. Плюсы и pypy справляются за 10-12 секунд
[18:34:02] <tilarids> но по памяти уже все совсем хорошо, спасибо
[18:35:19] <f[x]> tilarids, 32 бита что-ли?
[18:35:42] <tilarids> f[x], что именно? Система 64-битная
[18:35:57] <f[x]> у меня на amd64 2 гига занимает
[18:36:24] <f[x]> отрабатывает за 70 сек
[18:37:34] <tilarids> » uname -m -r -p
3.5.2-gentoo x86_64 Intel(R) Core(TM) i7-2635QM CPU @ 2.00GHz
[18:38:03] <tilarids> может, версия окамля таки играет роль?
[18:38:51] <f[x]> на память - нет
[18:39:03] <f[x]> там ничего не менялось уже миллион лет
[18:39:23] <f[x]> и я сейчас 3.12.1 смотрю
[18:39:34] <ermine> f[x]: я уже решила что буду пробовать на coq - свою камлевую либлу treap на coq воспроизводить
[18:39:35] <f[x]> Array.fast_sort надо юзать
[18:39:37] <f[x]> 30 се
[18:39:39] <f[x]> 30 сек
[18:39:49] <f[x]> ну и профилировать конечно в первую очередь :)
[18:40:14] <tilarids> ну, большой разрыв получается по памяти между 1.1 и 2 гига. Ты куда смотришь?
[18:40:35] <ermine> gds: но лучше буду пробовать, когда прочту половину книжки, а щас дочитываю третью главу
[18:41:05] <ermine> там муть про nested induction
[18:41:20] <f[x]> tilarids: top rss
[18:41:31] <ermine> Kakadu: ты уже пробовал читать про coq?
[18:41:38] <Kakadu> не
[18:42:33] <ermine> Kakadu: кстати, а ты часом не блондин как настоящий какаду?
[18:43:03] <f[x]> 3.12.1 - 30 sec
4.00.0 - 26 sec
[18:43:25] <tilarids> c fast_sort у меня получается 39 секунд и 1.7 гига
[18:43:47] <f[x]> у тебя OCAMLRUNPARAM в environment нету?
[18:43:52] <ermine> f[x]: а четвертое камло уже умеет smp?
[18:43:56] <tilarids> gds, ты как-то не совсем правильно алгоритм перенес, у тебя получается 150кк элементов против 75кк
[18:44:01] <f[x]> ermine: да, и кофе готовить :)
[18:44:02] <tilarids> f[x], нет
[18:44:30] <f[x]> tilarids: дай твои "каноничные" версии на камле и плюсах
[18:44:57] <tilarids> плюсы: http://codepad.org/ki9YML78
[18:45:10] <f[x]> опять рабочий день мне сорвали
[18:45:17] <f[x]> %)
[18:45:39] <ermine> сегодня выходной
[18:45:59] <tilarids> f[x], http://codepad.org/fTbdA1Fw камл
[18:47:10] <gds> tilarids: вполне мог ошибиться, факт.
[18:48:06] <f[x]> tilarids: а list comprehension откуда?
[18:48:48] <gds> tilarids: у тебя на каждую точку идёт по 2 значения или по 1?
[18:49:57] <ermine> три, судя по наличию угла
[18:50:23] <gds> ermine: на nested induction пока забей, разве что просмотри по диаговнали.  А что такое treap?
[18:51:17] <ermine> gds: не, я всяко дочитаю, оно массой должно надавить на меня и аукнуться
[18:51:39] <tilarids> gds, на каждую точку по два значения. Всего точек 9801*9801*pi/8
[18:54:50] <gds> всё, понял ошибку.
[18:55:25] <gds> перепишу правильно сейчас.
[18:56:39] <ermine> это напоминает конкурсы по перлу "напиши код, эквивалентный образцу, как можно покороче"
[18:57:37] <Kakadu> ermine: не. не блондин
[18:58:07] <ermine> Kakadu: жаль
[19:06:41] UncleVasya вышел(а) из комнаты
[19:17:24] <gds> tilarids: должно быть ровно 75475540 значений, или опять накосячил?
[19:22:06] <gds> да блин.  криво опять.
[19:22:37] <tilarids> плюсовый вариант выдает 75447816. Т.е., близко
[19:23:06] <tilarids> можно не париться из-за мелких расхождений, они погоды не сделают
[19:27:28] <f[x]> ещё в Array.fast_sort несколько ненужных bounds check'ов - стоило бы зарепортить как багу
[19:27:37] <f[x]> но не влияет наверное
[19:29:03] <f[x]> и blit вызывается вместо unsafe_blit - это ещё дофига сравнений
[19:29:10] <f[x]> и стдлиба не инлайнится
[19:29:35] <gds> tilarids: реально, где-то туплю, но лень париться.  хотя кое-что поменял, другое количество, но тоже не как у тебя.  http://paste.in.ua/7688/
[19:29:48] <f[x]> даже интересно - ща покручу sort - что получится
[19:33:19] <tilarids> 875 метров, 19 секунд. Идеальный результат пока 575 метров, 10 секунд (clang++ -O3)
[19:34:10] <tilarids> на удивление gcc продьюсит код чуть медленней, чем clang. Впервые такое вижу
[19:34:29] <gds> ну вот и ок.  "не более чем в 2 раза медленнее C" -- это приемлемо.
[19:35:23] <tilarids> gds, но при этом код превратился из красивого в некрасивый
[19:35:40] <tilarids> потерялся вообще весь смысл использования окамля
[19:36:33] <f[x]> вычисления - не самая сильная сторона камля, ага
[19:36:51] <f[x]> для логики надо юзать, там где есть поинт от типизации
[19:37:15] <f[x]> критичное по скорости пишется на плюсах, логика - на камле
[19:37:17] <f[x]> как-то так
[19:37:23] <tilarids> ну, меня больше всего потребление памяти расстроило изначально, а не скорость
[19:37:50] <f[x]> есть такое
[19:38:55] <tilarids> учитывая, что я камль собираюсь юзать для веба, мне скорость числодробления не столь важна. А вот потребление памяти в 5 раз больше, чем реально нужно, напрягает
[19:40:03] <tilarids> надо еще подобную микрозадачу с IO сделать. В прошлый раз на такой микрозадачке python2.6 всем раздавал
[19:41:34] <f[x]> tilarids: поэтому в вебе все юзают с++, да
[19:42:31] <f[x]> т.е. это вообще не критерий для 99% веба (фронтенды)
[19:45:40] f[x] вышел(а) из комнаты
[19:45:58] <komar> tilarids: по сравнению со всем остальным вебоокамл потребляет чуть меньше чем нихера памяти.
[19:46:21] <komar> Это большое, хоть и совершенно бесполезное преимущество.
[19:46:29] <komar> Память нынче дешева, увы.
[19:48:40] <tilarids> komar, я был и остаюсь мобильным девелопером. У меня до сих пор есть ограничения по памяти :)
[19:52:20] <komar> Веб в мобильниках?
[19:52:22] <komar> За что?
[20:01:11] <gds> tilarids: я понимаю твою точку зрения, и заранее сказал, что моё не вписывается в твой бенчмарк (мне было интересно другое, и ты удовлетворил моё любопытство).
Не понимаю другого: какие выводы можно сделать из этого бенчмарка в применении к вопросу "ocaml + web".  По-моему -- никаких.
[20:02:28] <tilarids> komar, не, веб отдельно, мобильники отдельно
[20:02:43] <komar> Нахрена тебе ограничения по памяти в вебе?
[20:03:02] <komar> Не, я понимаю, когда один инстанс в Ruby on Rails сжирает 1,5 гигабайта памяти.
[20:03:17] <tilarids> gds, вывод довольно простой - языков, которые позволяют красиво писать эффективный код - раз-два и обчёлся. И окамль не в их числе
[20:03:26] <ermine> tilarids: андроид?
[20:04:10] <tilarids> komar, выработанный рефлекс. Я люблю понимать, сколько памяти ест моя программа и очень расстраиваюсь, если она ест больше
[20:04:14] <tilarids> ermine, иос в основном
[20:04:34] <ermine> gds: а там посредством потоков без строительства структуры в памяти дело не решается?
[20:05:06] ermine любит потоковые решения
[20:06:42] <komar> tilarids: в данном контексте ты думаешь о бестолковой херне.
[20:07:13] <komar> Я все равно рад за тебя, потому что задроты-байтоебы — это куда лучше, чем ололо-петонщики, у которых планка DDR3 на 4GB 500 рублей стоит.
[20:07:21] <komar> Но все же.
[20:08:06] <komar> У меня сейчас mysqld жрет в два раза больше, чем ocamlrun с сайтом и кучей библиотек.
[20:08:26] <ermine> komar: память на мобильных устройствах нонче не расширяется, слотов под sd карточки даже нет
[20:08:30] <komar> (а больше всех жрет IRC-бот на руби, гы-гы)
[20:08:53] <ermine> грустная песня
[20:09:00] <komar> ermine: 1) он ищет применение окамла в вебе; 2) он ищет применение окамла в вебе не на мобильниках
[20:09:59] <ermine> komar: а, ну тогда слоты в настольных/наполочных компах тоже мало
[20:10:10] <ermine> у меня лично все слоты забиты
[20:10:19] <komar> > веб > десктопы
[20:10:27] <komar> Боже.
[20:10:38] <ermine> наполочные компы
[20:11:18] Typhon вышел(а) из комнаты
[20:11:26] <ermine> девелоперы вообще озверели
[20:11:50] <ermine> теорию графов давно бы применяли
[20:12:01] Typhon вошёл(а) в комнату
[20:40:23] letrec вышел(а) из комнаты
[20:49:53] <ermine> gds: дочитала третью главу, про индукцию! завтра будет четвертая глава про индуктивные предикаты.
[20:51:03] <ermine> в голове один хлам
[20:54:24] <ermine> gds: кстати в конце третьей главы показали как вручную делать нечто вместо discriminate, смешно выглядит
[20:55:26] <ermine> в coq есть <-, которой можно, не закрывая глаза, заменить true на false просто так
[21:33:42] Typhon вышел(а) из комнаты
[21:34:11] Typhon вошёл(а) в комнату
[21:35:11] <gds> ermine: хлам -- это нормально.  Возьми _несложное_ дело и вперде.
про "заменить true на false" -- наверное, речь про rewrite.  Так вот, если будет неконсистентный набор аксиом, то и не такое ещё можно сделать.  Это как использовать Obj в коде, ровно настолько же фатальные последствия.
[21:36:48] <ermine> gds: не про rewrite, а change
[21:37:15] <ermine> rewrite еще ладно, он вроде не искажает природу
[21:42:17] f[x] вошёл(а) в комнату
[22:01:39] dzhon вошёл(а) в комнату
[22:10:17] f[x] вышел(а) из комнаты
[22:33:41] <gds> ermine: где через change без левых аксиом можно заменить true на false?
[23:19:53] <gds> обещанная статья про coq: http://gds.livejournal.com/65879.html
[23:24:45] Sun][ вошёл(а) в комнату
[23:25:42] Sun][ вышел(а) из комнаты
[23:27:21] Sun][ вошёл(а) в комнату
[23:28:55] <tilarids> ура, thanks
[23:45:51] ermine порефакторила свой xsd и задумалась, зачем это сделала
[23:47:32] <ermine> gds: в конце третьей главы, там точнее false менялось на true в теореме true <> false