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

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.

Оказалось, что это just as planned:

https://www.gnu.org/software/make/manual/html_node/Libraries_002fSearch.html

Звучит интересно, но работать за пределами https://ru.wikipedia.org/wiki/FHS это не может.

(спасибо нашим слушателям за разъяснение!)

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

Очередной новогодний дайджест от opennet, не упустите!

#lab #home_lab

Теперь 3 vps, мир не без добрых людей.

Внезапно обнаружил, что 1 из vps помер месяц назад, из-за неуплаты, но весь комплекс продолжил работать, как танк.

Избыточность - хорошо!

https://devblogs.microsoft.com/oldnewthing/20100517-00/?p=14013

А вот, например, устройство (коротенько) windows 3.11

TL;DR - большие они там были затейники:

"there were actually three operating systems running at the same time. The operating system in charge of the show was the 32-bit virtual machine manager which ran in 32-bit protected mode. As you might suspect from its name, the virtual machine manager created virtual machines. Inside the first virtual machine ran… a copy of Standard mode Windows"

"The other virtual machines each ran a copy of MS-DOS and were responsible for your MS-DOS sessions. Recall that Enhanced mode Windows allowed you to run multiple MS-DOS prompts that were pre-emptively multi-tasked"

https://users.rust-lang.org/t/game-dev-in-rust-a-year-later/123522

Состояние rust gamedev.

TL;DR - смерть, смерть, кладбище.

Особенно зацепило

"Whenever there's been a serious problem that was hard to find, it was always because somebody built their own allocation system instead of using safe Rust constructs. Putting everything in an array and passing around array indices in multi-threaded programs is usually trouble"

Тема прямо ровно вот в этой постановке несколько раз возникала в нашем дискуссионном чате. Что вот люди пилят хранение объектов в массиве, и оперируют индексами в этом массиве, вместо указателей, чтобы как-то обойти неудобства Rust.

У индексов есть очень понятные минусы, по сравнению со ссылками и указателями на элементы:

* Код сложнее, больше вероятность ошибки.

* Указатель - он всегда в память, не промахнешься (хе-хе), а вот индекс - он куда? В этот массив, или в тот? К указателю приписан тип, к индексу - нет.

Наверное, это все решаемо, но явно это чего-то будет стоить.

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

"Накручивание звёзд также использовалось для продвижения продуктов, самоутверждения разработчиков, принижения конкурентов и повышения значимости в глазах пользователей. Приводятся примеры 7 коммерческих сервисов накрутки, стоимость работы которых составляет от $0.10 до $1.62 за звезду"

А вот и ответ на тему "откуда берутся потемкинские проекты", и я даже особо не стебусь, линкуя сюда эту тему про "звезды Rust проектов".

https://www.tgoop.com/itpgchannel/1679
https://www.tgoop.com/itpgchannel/1685
https://www.tgoop.com/itpgchannel/1688
https://www.tgoop.com/itpgchannel/2190
https://www.tgoop.com/itpgchannel/1483

https://x.com/elonmusk/status/1876174862747930717

Гля какой классный пример пресуппозиции!

Каждый, кто принял участие в опросе, исподволь согласился с тем, что в Британии "tyrannical government"!

#hyprland #rant

Рубрика "зумеры изобретают систему сборки".

Вот что вы делаете, когда система сборки не дает вам */** для исходников, а очень хочется?

(вопрос риторический)

Коллеги из #hyprland изобретают херобору:

https://github.com/hyprwm/Hyprland/blob/main/src/meson.build#L1

globber = run_command('sh', '-c', 'find . -name "*.cpp" | sort', check: true)

А то, что эта команда может зачерпнуть лишнего, и у кого-то появляется hard X11 dep, их, конечно, не волнует.