?

Log in

Ничем не примечательный ЖЖ
 
[Most Recent Entries] [Calendar View] [Friends]

Below are the 20 most recent journal entries recorded in gds' LiveJournal:

[ << Previous 20 ]
Monday, July 13th, 2015
1:44 pm
бестемы бездаты
…и это ещё nivanych не имеет отношения к деньгам. CTO, видите ли.
http://nicka-startcev.livejournal.com/2975891.html
http://nicka-startcev.livejournal.com/2976243.html
Рашкован типичный ищет, где светло, а не где потерял.
Николай Иваныч — культурный, спокойный человек, учоный нах. А Миша, управляющий, не настолько культурен, хотя и вполне эффективен. Может и нахуй послать, и в ёбыч прописать. Ну или Валеру бы позаёбывать, который собственно платит деньги — реального босса, владельца бизнеса.
Но, конечно, публично опускать Иваныча легче и приятнее. Тем более, у него есть жж-аккаунт, в отличие от других упомянутых (чью манеру ведения дел я не одобряю, но это совершенно не относится к теме поста).
Sunday, September 22nd, 2013
11:44 pm
Репост репост riposte
Сделал репост -- не человек.
Объяснять надо?
Wednesday, August 14th, 2013
6:28 pm
coq + imperative algorithm proving
Делаю вот одну шнягу на окамле. Там есть файл, в нём "блоки данных", состоящие из подблоков малой длины.
И подумал я, что дёргать каждый раз Unix.read (обёртку над read()) не очень гуманно в плане количества вызовов ОС, например.
И решил я реализовать более умный алгоритм чтения-кеширования, читающий в блок размера "дисковый блок * 2", по выравненным смещениям, стараясь читать по границе блока, чтобы не читать ненужные блоки. Однако, кое-где явно нет нужды пропускать данные через буфер, когда ясно, что "цельные блоки" можно прочитать напрямую в строку-получателя.
Но оказалось, что я не смог отладить этот сугубо императивный алгоритм руками, и у меня вообще не было уверенности в том, что он работает правильно. Эти гадские смещения, длины! Невозможно интуитивно проверить, правильно ли сделал. Очень БЕСЕД, знаете ли.

Тогда я взял Coq.
Collapse )
Thursday, April 4th, 2013
2:14 pm
постгрес, хранимые процедуры
Наткнулся на говно. Имею в постгресе хранимку вида
declare
  l_bool boolean;
begin
  l_bool := somefunc();
  return query select * from
    (select * from table where l_bool
     union all
     select * from table where not l_bool and ...
    );

И вот, при замене в запросе переменной l_bool на литерал с реальным значением я получаю 5мс вместо 1600мс.
Это -- не то "кеширование планов", которое хорошо задокументировано в мануле, это что-то другое, так как "кеширование планов" работает при первом вызове функции в пределах сессии, а я вызываю эту функцию с одним и тем же параметром как до, так и после изменения. И это не затраты на парсинг + построение планов, так как последующие запуски показывают примерно то же время.
А план запроса "с переменными" не посмотреть, так как explain хочет на входе полноценный, умеющий выполняться запрос.
В оракле такой хуйни не было!
Wednesday, March 20th, 2013
7:23 pm
coq-breakpoints
Зарелизил мелкую библиотечку для отладки редукций выражений в пределах coq: https://bitbucket.org/gds/coq-breakpoints
Monday, February 11th, 2013
7:58 pm
построение термов тактиками в coq -- безопасно
Сегодня thedeemon показал ужосы, от которых у меня волосы в жилах стынут.
А мне стало интересно, можно ли накосячить подобным образом в coq.
Но писал я быстро, поэтому код некрасивый. Например, можно спокойно попрятать многое в implicit arguments, да и для vec выбрать более кошерный тип (например, кошерный в плане strict positivity).

Collapse )

Однако, кое-какая лажа у меня таки была. Если rewrite, ныне вынесенный в vec_cast, натравить не на чистый пруф-терм ("n = m -> length l = n -> length l = m"), а на computational term (в том числе содержащий пруф) ("n = m -> vec A n -> vec A m"), то Eval compute выдаёт совершенно аццкий терм, содержащий в том числе пруф того, что длины равны. Но в #coq быстро объяснили, в чём дело. В этом состоит мой личный профит от этой задачки. Ну и развлёкся, и убедился, что в coq подобные косяки допустить трудно, даже если используются тактики.
Monday, November 5th, 2012
9:15 pm
Опыт использования Coq на практике, или Как я сам себя отпетушил COQОКОКОКО

Есть время собирать опыт.

Есть время разбрасывать на вентилятор.




Уже довольно давно система типизации в окамле кажется мне слегка недостаточной.
Collapse )

По итогу -- впечатления смешанные.
Tuesday, September 4th, 2012
12:36 am
coq + inlining + "merge right"
Некоторые люди прочитали статью http://alaska-kamtchatka.blogspot.com/2012/08/merge-right.html , где была показана весьма общая функция для слияния/пересечения/разницы списков.
А господин ygrek в камлочятике прилюдно мучил MetaOCaml для инлайнинга функций-аргументов merge. Я не мог на это смотреть спокойно. Однако и сразу разобраться не смог, так как не знал многого, но вполне так узнал.
Чтобы было хоть сколько-нибудь интересно читать, рекомендую прочитать сначала исходную статью.
Потому что сейчас будет простыня.
Collapse )
Вроде ЗБС.
Можно было бы сравнение не инлайнить, но избавиться от вызова функции (будь то "(fun (a : int) b -> ...)", будь то Pervasives.compare) не получается сходу.
Мне Coq нужен не только для зависимых типов и доказательств кода, но и для инлайнинга. Я -- практичная скотина, да!
Если будут вопросы -- поясню. Потому что всё сразу пояснять -- руки устанут.
Tuesday, August 28th, 2012
5:36 pm
год
Интересно просуммировать, что же я сделал за год. (дата выбрана совершенно случайно, но "новый год" выбирать как-то неоригинально.) Не упорядочено никак. И не пишу, благодаря кому это делал -- слишком многих перечислять придётся.
Collapse )

upd1/
Collapse )

upd2/
Collapse )

upd3/
Collapse )
Sunday, July 15th, 2012
4:30 pm
вся правда про меня
Я считаю, что люди, читающие мою жыжыцу, должны знать всю правду про меня.
Автора данного текста я не называю, и вы не называйте, даже если знаете. Тем более, вытащено из подзамочного поста, что, в принципе, не очень хорошо. И каменты на всякий случай буду скринить. Да и не в авторе суть, а в тексте.
Просто учтите, что я вот такое вот говно.

Не тебе судить.
Да, для работы с ленивостью в реальных больших проектах, где условно говоря, много "IO", нужен некоторый опыт. А примеры твои ничего не стоят.
Остальное, в GHC/Haskell, ты откидываешь. И уже вполне приблизился к фанатизму "раз этого нет в любимом инструменте, то это не нужно".
Твои познания за использование ленивости только очень теоретические. Причём, специфической направленности — выискиывать различные fuckup'ы с ленивостью. Вот я тебя спрошу — а приведи примеров хороших и грамотных решений? Ты нормально не ответишь. Зато примеры fuckup'ов привести сможешь.
Ты не разбираешься в теме. Не тебе судить.
Tuesday, May 29th, 2012
2:12 pm
квас, как я его делаю
Обсуждали изготовление домашнего кваса, опубликую личный рецепт.
Collapse )
Tuesday, April 24th, 2012
12:46 am
ответ на очередное тупопёздничество этой леди, на этот раз тут: http://nicka-startcev.livejournal.com/1651259.html?thread=5538875#t5538875

(кстати, удивлён, что ребе Белнетмон как-то умудрился не хамить открыто.)

> когда меня манагер спрашивает, сколько времени займёт разработка такого-то девайса, я всегда говорю: столько, сколько нужно, плюс время, которое мы тратим сейчас на эту бесполезную болтовню :)

Разработка для разработки. Это так мило. Косвенно напоминает известный анекдот про "откуда деньги берутся? из тумбочки.". Ебануться можно. Налицо тупое непонимание того, что результат работы и сроки готовности результата _напрямую_ влияют на прибыль компании. (Или там такая компания, где делай что хочешь, забивай болт по необходимости, но деньги всё равно будут идти? Даже с заранее увеличенными в несколько раз сроками, определяемыми левой пяткой разработчика? Тогда я бы тоже поработал там, если не совсем нищенская зарплата.)


> чем больше разработчику предоставляется благ - тем эффективнее он работает.

Пока не начинает понимать, что можно и не работать, а прокрастинировать, заниматься хуйнёй, чесать лиловую лысину на рабочем месте, драться саблями (пруф в xkcd). До наступления этого понимания проходит не так уж много времени (если разработчик умный), и тогда у организации начинает медленно подниматься вопрос про то, что и как делать дальше с этой вашей разработкой. Просто увольнять невыполняющего работу сотрудника -- гемор, я читал ТК рашки и приднестрашки. И не надо говорить, что все люди пиздец какие честные, и все просто одержимы тупым кодингом всякой хуйни.

> а заполнение бумажек только отнимает время, отвлекает от основной задачи и раздражает, заставляет лишний раз подумать о смене работы

А ещё бывает так, что разработчик долбится рогами в совершенно другие ворота, не в те, в которые нужно. Конечно, если дело не в тупых микроконтроллерах, где всё, что нужно от обезьянки-кодера -- это всосать несложную предметную область и хуярить на какой-нибудь сишечььке.
Кроме того, для лучшего результата, бывает, нужно сверху как-то повлиять -- показать более кошерный способ реализации, переосмыслить ТЗ, чуток поменять архитектуру. А если каждому разработчику дать полную свободу от бумажек (в том числе от тех, где он описывает архитектуру, планы и сроки) -- поимеем и хуёвую архитектуру, и кривые×неактуальные планы, и проёбанные сроки. И, в рот тебе ноги, проёбанную прибыль компании. Хотя, опять же, если дело ремесленное -- будь то настраивать проводки в 1С, будь то писать дейтинги и дорвеи на похапэ, будь то лепить тупой говнокод на микроконтроллерах -- вполне можно дать разработчикам швабодку. Проблемы начнутся попозже, в таком случае.
Thursday, April 12th, 2012
1:29 pm
Решил вынести ответ на камент в отдельный пост. Так как дело было в жыжыцэ, пост будет тоже жэжэшный.

Исходный комментарий -- http://diam-2003.livejournal.com/527676.html?thread=1267516#t1267516 :
> Но ведь с другой стороны, у людей, которые всё это пишут, тоже ведь есть мозг.

Конечно есть, но мотивы их писюлек далеко не всегда исходят из желания "сделать людям хорошо", и не из желания поделиться _работающим_ решением (особенно учитывая, что про подобные решения, работающие на практике, мало кто слышал -- а какая-то информация таки просочилась бы).
Collapse )

Теория такая теория.
Wednesday, March 14th, 2012
3:28 pm
coq, reversed lists
Взял несложную (как казалось) задачку, потыкал в неё палочкой, отчаялся, дошёл до #coq irc, изложил проблему, но не помогли. Зато теперь есть изложение этой проблемы:
Collapse )

Может, у вас будут идеи?

UPD/
Подсказали. Definition my_list_rev_mapped := Eval compute in предыдущее_определение. И всё, что оно может, оно вычисляет в compile time. Как же мне это нравится!
Monday, March 12th, 2012
5:53 pm
coq, true_neq_false
Кое в чём разобрался, близко к прошлой проблеме.
А вы посмотрите, правильно ли.

Definition true_neq_false
 : true <> false

Collapse )
Sunday, March 11th, 2012
2:54 pm
coq, zgtz
Решил вспомнить молодость и подоказывать кое-что. У известного Адама взял какой-то пример, который он доказывает через свою придуманную для книги CPDT тактику "crush", но мне это не нравится. Хотя бы тем, что тактики не нравятся. Я хочу что-то более приближённое к конструктивному построению доказательства.
Итак, "ноль не больше нуля" с моим тупым доказательством через классические тактики.
Lemma zgtz : 0 > 0 -> False.
intro H. inversion H.
Qed.
Print zgtz.

На что генерится какой-то совершенно дебильный код:
Collapse )
Конечно, должен быть способ как-то более прямым образом это доказать.
Если есть идеи, куда копать -- подскажите.
Monday, March 5th, 2012
3:17 pm
dependent types
(как бы разворачивая каменты из предыдущего поста)

А расскажите, где вообще полезны dependent types?
Про примеры с массивами и их границами я в курсе, но это мало полезно лично мне на практике -- дело в том, что я как-то не нарывался на проблемы с этим уже несколько лет, причём dependent types не использовал для этого никак, ни разу. (а вот модульность и нормальные интерфейсы модулей -- как раз использовал.)
Далее, понятно, с помощью dependent types можно протаскивать какие-то утверждения в compile time. Очень хорошо, но с какими практическими целями?
Что я уже читал: первые несколько страниц выдачи гугла по "dependent types", в том числе известное "why dependent types matter". И, всё равно, либо dependent types это малонужная хуйня, либо я тупой. (не стесняйтесь, я прекрасно знаю свои интеллектуальные способности, поэтому последний вариант не оскорбителен.)
Sunday, March 4th, 2012
12:51 pm
vecN
Data.VecN в окамле: https://bitbucket.org/gds/vecn/src
И, чорт возми, опять зависимые типы не пригодились. Да что за беда...
Thursday, February 9th, 2012
6:03 pm
blog + jabber
Одна из частей моего интернет-общения с людьми состоит в том, что я шлю одинаковые/похожие сообщения по жабберу нескольким людям одновременно.
По идее, для автоматизации этого процесса нужен блог/микроблог (тьфуты, пойду помою язык) с поддержкой возможности постить через жаббер и с возможностью людей "подписаться" (так, чтобы им в жаббер приходили мои "посты").
Вот его и попытаюсь найти, а вы, читающие этот пост, может быть подскажете, что мне подойдёт. Вдруг сталкивались или слышали о подобном.
Сразу скажу, что твитор и жуйк мне не подходят, по разным, но весьма серьёзным причинам, их давайте откинем, даже если они удовлетворяют описанным мной требованиям.
От подобного сервиса очень желательно иметь возможность видеть в вебморде эти "посты", хотя бы чтобы можно было на них сослаться http-ссылкой, ну и для любителей эфпячить вместо более культурных средств. Ещё очень хочется rss/atom и подобное, для тех, кто предпочитает не реалтайм-доставку жаббером, а чтение фидов.
Это -- минимальные требования к сервису. Больше и не нужно. Всякие каменты -- хрен его знает, нужны ли. Будут -- хорошо, не будут -- проживу.
Подскажите, есть ли в интернетах бесплатный сервис, предоставляющий подобную функциональность?
Monday, February 6th, 2012
10:14 am
rdbms, global id / hosts
А теперь -- о тупой практике вопрос.
Задаю тут, так как знаю, что по крайней мере четверо из читающих меня людей сталкивались с этой проблемой.
Хочется в пределах реляционной базы данных сделать так, чтобы id записей с разных, но подконтрольных мне баз данных не перекрывали друг друга, и при этом могли генерироваться независимо и локально.
Конечная цель -- создавать такие строки таблиц, чтобы таблицы можно было сливать-разливать по необходимости.
Я знаю только два хака для этого.
1. Прямой хак: сделать так, чтобы первичный ключ записи включал в себя (local_id serial, host_id integer) (вариант -- host_name varchar). Хорошо тем, что индекс по (local_id, host_id) в большинстве случаев (для запросов по локальным данным) будет ровно настолько же селективен, как и просто по local_id. Хотя он будет жирнее, что не радует. Ещё больше не радует то, что соединять таблицы придётся по двум полям, внешние ключи тоже будут по двум полям.
1а. Вариант прямого хака: иметь local_id, host_id, но формировать из них уникальную строку (например, тупо, "123.456" для local_id=123 и host_id=456, или более умно, побитово), которую уже считать идентификатором. Нормально, но первичные/внешние ключи по строковым типам обычно медленнее, чем по numeric типам. И вообще, какое-то сомнительное решение.
2. Кривой хак: закодировать host_id в самом id, например, выделяя какие-то биты (старшие/младшие) под host_id, остальные биты оставляя под local_id. Не нравится тем, что этим сильно ограничивается либо диапазон host_id, либо диапазон local_id, и это потребует проверки со стороны программы (либо ошибки со стороны бд), попадает ли новый локально-сгенерированный id в то множество host_id, в которое он должен попадать. А мне нужно для постгреса, а там самый большой целочисленный тип хранит 8 байт, и не уверен, что их хватит в случае таблиц, с которыми будет вестись интенсивная работа. Кроме того, решение хуже тем, что где-то нужно централизованно выдавать host_id, тогда как решение из п.1 с host_name требует только разумной выдачи host_name, такой, чтобы они не пересекались.

Понятно, что я где-то загоняюсь, так как проблему таки решают как-то. Уверен, я не первый, кто думает об этом. Подскажите вот.

(думал поставить на этот пост "тематику только для взрослых", но уже запечатал конверт.)
[ << Previous 20 ]
About LiveJournal.com