LINUX.ORG.RU

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

 , , ,


2

4

Сменив работу, решил немного подправить свой боевой emacs и вот что из этого вышло:

  • в стабильный Debian был воткнут emacs-snapshot;
  • прикручена тема zenburn, убран меню-бар и всякая лишняя обвеска;
  • в качестве ШГ уже достаточно давно использую terminus;
  • кроме того, прикрутил подсветку текущей строки и выпирающих концов длинных строк, которые выделяются красным цветом.

Теперь по скриншоту. Слева видны полируемые исходники модуля для ejabberd. Для работы с Erlang использую EDTS, который может почти всё и не тормозит как erlang-mode.

Для ускорения эрланга в узких местах иcпользую ocaml. Когда возможностей окамла не хватает или нужно доказывать некоторые утверждения о коде, использую coq.

Работу с окамлом обеспечивает tuareg-mode, а исходниками на coq заведует ProofGeneral.

Ругайте.

>>> Просмотр (1920x1080, 77 Kb)

★★★★★

Проверено: JB ()

годно.

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

science ★★☆ ()

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

lazyklimm ★★★★★ ()

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

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

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

loz ★★★★★ ()
Ответ на: комментарий от loz

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

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

ymn ★★★★★ ()

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

proofit404 ()
Ответ на: комментарий от proofit404

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

ymn ★★★★★ ()

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

basp ()

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

metar ★★★ ()
Ответ на: комментарий от ymn

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

proofit404 ()
Ответ на: комментарий от aptyp

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

olibjerd ★★★★★ ()

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

olibjerd ★★★★★ ()
Последнее исправление: olibjerd (всего исправлений: 1)
Ответ на: комментарий от proofit404

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

ymn ★★★★★ ()
Ответ на: комментарий от metar

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

ymn ★★★★★ ()
Ответ на: комментарий от aptyp

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

ymn ★★★★★ ()
Ответ на: комментарий от basp

тут вариантов использования несколько: пишем на 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 можно глянуть про верификацию если интересно

ymn ★★★★★ ()

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

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

Lennart ()
Ответ на: комментарий от ymn

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

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

Lennart ()
Ответ на: комментарий от Lennart

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

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

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

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

ymn ★★★★★ ()
Ответ на: комментарий от aptyp

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

GPL же.

mv ★★★★★ ()

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

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

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

mv ★★★★★ ()
Ответ на: комментарий от loz


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

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

rtvd ★★★★★ ()
Ответ на: комментарий от mv

GPL же.

man GPL

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

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

rtvd ★★★★★ ()
Ответ на: комментарий от rtvd

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

mv ★★★★★ ()

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

farzeet ★★ ()

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

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

nihil ★★★★★ ()
Ответ на: комментарий от science

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

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

korvin_ ★★★★★ ()

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

MiniRoboDancer ★☆ ()

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

lucentcode ★★★★★ ()
Ответ на: комментарий от rtvd

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

loz ★★★★★ ()
Ответ на: комментарий от mv

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

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

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

rtvd ★★★★★ ()
Последнее исправление: rtvd (всего исправлений: 1)
Ответ на: комментарий от loz

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

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

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

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

rtvd ★★★★★ ()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.