https://www.opennet.ru/opennews/art.shtml?num=62465

Рубрика "новости из дурки".

Еще один альтернативный броузер, some highlights:

* Написан на С, и на FixScript (язык от того же автора).

* GUI toolkit - GTK2 (GTK2, Карл!!!)

* Вместо javascript - набор регулярок, которые фиксят сайты так, что они могут как-то отрисовываться без JS. 1200 сайтов уже поддержано!

https://www.opennet.ru/opennews/art.shtml?num=62471

У #ghostty случился релиз.

Доставляет способ тестировать производительность терминала (нет, реально, все как у великих - https://www.tgoop.com/itpgchannel/306):

"В проведённых тестах Ghostty оказался быстрее эмуляторов терминала iTerm и Kitty в 4 раза, а Terminal.app - в 2 раза, при выводе на экран содержимого большого файла, например, при помощи команды "cat big_file.txt". При сравнении с Alacritty производительность Ghostty была примерно на том же уровне, но Alacritty отстаёт по функциональности от Ghostty"

В общем, пока эталонное "не нужно".

#terminal

Как обычно, первое решение оказалось не самым подходящим, но, по результату его применения, получилось еще более простое и изящное решение:

https://github.com/pg83/ix/blob/main/pkgs/bld/rust/helpers/patch/bindgen/patch.sh#L11-L14

cat << EOF > .../clang-sys/build/static.rs
pub fn link() {
}
EOF

Вот так вот, грубо, к херам, изничтожить всю логику поиска libclang, полагаясь на то, что мой враппер и так установит нужные пути поиска библиотек от LLVM.

Работает, как часы!

Буррито "рекурсивный"

Кстати, про рекурсию.

Читал тут исходники https://github.com/meyfa/CobolCraft/

Это такой сервер minecraft, но на Cobol.

А я раньше код на Cobol особо не читал, потому что зачем?

Читал, читал, и стали у меня закрадываться нехорошие предположения.

В Cobol из коробки нет рекурсии! Вы знали? Я не знал.

Вообще, конечно, есть, если через жопу, и со странностями, но не рекомендуется:

https://www.ibm.com/docs/en/cobol-zos/6.3?topic=subprograms-making-recursive-calls

https://stackoverflow.com/questions/27806812/in-cobol-is-it-possible-to-recursively-call-a-paragraph

Судя по ссылкам, рекурсивный вызов без явного на то объявления - это что-то типа местного UB. Наверное, связано это с тем, что в программе нет стека.

Впрочем, зачем рекурсия в языке, которым выставляются счета на оплату?

https://www.ryanliptak.com/blog/every-rc-exe-bug-quirk-probably/

https://github.com/squeek502/resinator

Чувак запилил альтернативный windows resource compiler. Это такая штука, которая позволяет включать в выполняемый файл иконки, и прочую лабуду.

Зачем?

Потому что все предыдущие open source реализации (windres от GNU, llvm-rc от LLVM, и какая-то еще) обладали фатальным недостатком - были написаны не на Zig Нет, реально, они все не совпадают с оригинальным rc.exe в каких-то краевых случаях.

Тут, конечно, интересен подход, с которым коллега подступился к этому "говну мамонта" "от дидов" - а давайте пофаззим новую реализацию до тех пор, пока не перестанет падать функция if (new(input) != rc.exe(input)) { abort(); }. Заодно получим корпус всяких смешных ошибок, и странностей оригинального rc.exe.

Подход, безусловно, интересный, привел к очень качественной реализации, которая ближе всех к rc.exe. Жалко, что на выдуманном языке программирования.

В общем, труд титанический, текст интересный, разбор получившегося корпуса included.

PS: оказывается, коллега уже про это писал, а я и не заметил - https://www.tgoop.com/gepardchan/151

If you'd like to skip around and check out the
strangest bugs/quirks, Ctrl+F for 'utterly baffling'

https://mostlynerdless.de/blog/2024/09/10/hello-ebpf-writing-a-linux-scheduler-in-java-with-ebpf-15/

Я в растерянности, потому что, с одной стороны, это годный текст про еще один userspace scheduler, на основе #sched_ext/#ebpf, а с другой - явный (pun intended) кандидат в серию "новости из дурки", потому что писать userspace scheduler на Java - это, конечно, за гранью.

Все же, пока чуть медленнее:

real  0m4.624s
user  0m0.004s
sys  0m1.152s

vs

real    0m4.929s
user    0m0.004s
sys     0m1.155s

Тестировал выводом большого текстового файла.

Тест на вшивость (выводим в терминал всякий треш, ждем, что упадет) ghostty тоже вполне прошел.

#alacritty #ghostty

#Lean
Многие знают, что после успешно завершённого Liquid Tensor Experiment Кевин Баззард и команда отдохнули немного, и вновь взялись за работу. Они занимаются формализацией доказательства Великой теоремы Ферма.

В своём блоге Кевин рассказал об их продвижениях до сих пор. И это совершенно прекрасная история, написанная живым и слегка ироническим языком.

Кратко, его товарищи в процессе работы, прописывая основания кристальных когомологий, обнаружили, что оригинальное доказательство не компилируется. В нём нашлась неустранимая дыра: доказательство ссылается на статью N.Roby 1965 года, Лемма 8 из которой неверна. Что удивительно, N.Roby доказывает её, неправильно цитируя свою же статью 1963 года.

Кевин пишет, что для него в этот момент обрушилось всё доказательство; теорема Ферма стала вновь стала открытой проблемой. Но он знал, что раз теория кристальных когомологий используется последние пятьдесят лет, то она работает, и нужно лишь по-новому обосновать верное утверждение.

Кевин, чем писать электронные письма экспертам, выпил кофе с одним профессором, пообедал с другим, и в конце концов нашёлся текст Артура Огуса, который закрывал дыру, а сам Артур взялся закрывать известные ему дыры в этом своём тексте.

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

Меня в этой истории вдохновляет, что к нам в математику как будто приходит живой трибунал, универсальный калькулятор истинности. Пока утверждение не компилируется Lean'ом, оно не считается доказанным.

Похожая история была в XIX веке: Вейерштрасс, Коши, Пеано, Гильберт, все занимались отделением математики от натурфилософии, постановкой её на формальные рельсы. Их критиковали за излишнюю строгость, за изгнание творчества из математики; но, как и в случае с Lean'ом, ответ есть лишь один: если мы занимаемся математикой, хотим быть уверенными в истинности утверждения, всегда иметь опору под ногами, иметь проверяемые универсальные результаты, нужно модернизировать наш средневековый цех всеми доступными современными технологиями. За Lean'ом будущее!

Админ дорезал оливье, и прощается с вами минимум на сутки! С наступающим!

https://www.opennet.ru/opennews/art.shtml?num=62490

"Проект основан Ниной Колеса (Nina Kolesa) из компании Igalia"

https://www.opennet.ru/opennews/art.shtml?num=56015

"Даниэль Колеса (Daniel Kolesa) из компании Igalia"

Да еб твою мать, никогда такого не было, и вот, опять. Это такой обряд инициации что ли?

https://www.opennet.ru/opennews/art.shtml?num=62499

Очень упорный товарищ, таки подчистил код от наследия из AMD, и продолжает пилить #zluda. Наверное, из этого получится что-то интересное.

Будни #bootstrap

Обновился gnu bc, до версии 1.08

Сборка стала падать с ошибкой:

make[2]: *** No rule to make target '-lreadline', needed by 'dc'.  Stop.
make[1]: *** [Makefile:368: all-recursive] Error 1
make: *** [Makefile:309: all] Error 2

Непродолжительные раскопки привели к вот такому сниппету в сборке:

LDADD = $(LIBBC) @READLINELIB@

$(PROGRAMS): $(LDADD)

Ну вот мы и получаем -lreadline -lncurses в READLINELIB, и такое всратое поведение.

Что имел в виду автор, непонятно. Возможно, полные пути в файловой системе. Но откуда бы?

Может быть, проверил сборку только с inplace readline, тогда это были бы пути относительно корня build root.

В общем, починил я это так - взял да добавил "недостающие" файлы:

{% block patch %}
...
echo > "dc/-lreadline"
echo > "dc/-lncurses"
{% endblock %}

Отнесу ли я это в upstream?

Конечно, нет, потому что я этот upstream (помимо полудохлого mailing list) в гробу видел и в белых тапках даже не сумел найти, ну или покажите, где эти исходники есть online, не в виде готового tgz.