Маргинальщина во все поля

годно.

только неплохо бы выбросить крысу и поставить тайловый wm типа осома, wmfs2, subtle например.

выбросить крысу

это же гном2

за софт зачёт, но скрин глазовыдирательный

Шрифт жестокий в емаксе, разве EDTS не использует erlang-mode?

Для ускорения эрланга в узких местах иcпользую ocaml.

Можно попробовать такое: https://github.com/goerlang/port, авторы говорят что работает, не придется возиться с доказательствами.

не придется возиться с доказательствами

иногда необходимо доказывать корректность кода.

Работа мечты, к вам стажеров не берут случаем?

Челябинск, Erlang, 40 тыр.

Спс!

есть еще похожая вакансия для молодых специалистов без опыта и студентоты.

можно привести пример использования coq? какие, например, утверждения о коде вы доказываете?

Комментарии в коде на испанском? Зачем?

Опыт есть, но м.б. уровень немного не ваш. Выслал всё на мэйл.

А в других городах?)

Мне кажется, не его это код, или я не прав?

Слева, где эрланг, комменты и правда на испанском (а может и нет, но похоже)

Что модуль делает? Окамель сильно ускоряет?

получил, ага. передам начальству после выходных.

вообще проект ejabberd поддерживает вот эта контора http://www.process-one.net/en/ejabberd/ так что часть кода досталась в наследство. есть проект mongooseim — форк ежаббера от конторы эрланг солюшнс, который уделывает ежаббер по многим характеристикам.

есть еще центр разработки в г. Трехгорный, Челябинская область. но туда просто так не попасть, ибо ЗАТО со всеми вытекающими: пропускной режим, ограничение передвижения и т.п.

тут вариантов использования несколько: пишем на coq, колбасим на нем хитровыдуманную работу с типами и т.п. вещами, которые в окамле делать лениво/долго/сложно, пишем/проверяем/отлаживаем/экстрактим в окамл и спокойно юзаем.

про доказательство утверждений: есть в окамле модуль obj:

module Obj: sig .. end

Operations on internal representations of values.

Not for the casual user.

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

http://www.cs.uoregon.edu/research/summerschool/summer13/curriculum.html можно глянуть про верификацию если интересно

всякая числодробилка

Легче в Челябинск переехать)

спс vol. 2

Очень интересно взглянуть на модуль для ejabberd с вкраплениями ocaml и даже coq - планируется открыть исходники?

И что этот модуль такое хитрое делает, что понадобилось притягивать coq с окамлем?

есть проект mongooseim — форк ежаббера от конторы эрланг солюшнс, который уделывает ежаббер по многим характеристикам

Что-то исходники сходу ненагугливаются - где можно приобщиться?

с вкраплениями ocaml и даже coq

coq в готовой системе нет. все в итоге экстрактится в окамл.

И что этот модуль такое хитрое делает

числодробилка и особая уличная магия. без подробностей, ибо nda.

А исходники выкладывать nda позволяет?)

А исходники выкладывать nda позволяет?)

GPL же.

Гном с емаксом не очень сочетается. В самую тему будет тайловый манагер, который по кнопкам с емаксом совсем не пересекается.

Вместо концов строки лучше whitespace-mode как следует настроить, чтобы человеков лучше ненавидеть.

Ну и emacs-jabber, нафиг этя гуйня в трее висящая не нужна.

Можно попробовать такое: https://github.com/goerlang/port, авторы говорят что работает, не придется возиться с доказательствами.

Ну и чем это позволяет «не возиться в доказательствами»? Что, Go самым своим гугловым естеством освящает и приобщает к Великому?

GPL же.

man GPL

Эта лицензия позволяет в ряде случаев не выкладывать исходники.

<vanga_mode> Вы прогуляли уроки юриспруденции? </vanga_mode>

Эта лицензия запрещает публиковать скриншоты с исходным кодом?

Это, конечно, все круто, но дебиан-то по факту дефолтный :)

так исходники под gpl мы юзаем как есть, без изменений: https://bitbucket.org/gds/coq-breakpoints плюс репа от process-one https://svn.process-one.net/ejabberd-modules/

все что попадает под nda нет на скриншоте.

Зато имакс недефолтный.

в качестве ШГ уже достаточно давно использую terminus;

Фраза замечательная. Надо вставить в правила оформления скрина на LOR.

А дефолт там, имхо, весьма недурственный.

А у кого он дефолтный?

У меня.

только неплохо бы выбросить крысу и поставить тайловый wm типа осома, wmfs2, subtle например.

xmonad | stumpwm же. И дебиан впридачу на что-нибудь помаргинальней. =)

Как же ты живёшь без менюбара и без globalmenu? Или он у тебя по Alt отображается (вендопривычки)?

только неплохо бы выбросить крысу

Зачем?

А зачем в имаксе менюбар?

А зачем в имаксе менюбар?

А, только в нём... Я думал, вообще...

Привет сокамернику )))

маргинальность должна быть маргинальной.

Gnome 2 не люблю. В остальном - годно. Zenburn очень нравится. А вот к хоткеям Emacs привыкнуть не могу, они такие странные... Не могу привыкнуть к хоткеям. Мне проще работать с Gedit и vim.

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

Эта лицензия запрещает публиковать скриншоты с исходным кодом?

Ты не видишь разницу между «разрешает не публиковать» и «запрещает публиковать»?

И да, товарищ уже упомянул NDA.

Я думал доказывать надо для использования окамла.

Очень странно, что так думал. А тем более, что при переходе на Go доказывать будет не нужно.

Но в любом случае го гораздо перспективней и вполне может заменять э-г в узких местах.

И чем он перспективней? Чем erlang? :-)