Forwarded from brain_leakage_etc
TIL, что GitHub ещё и STL умеет рендерить нынче (у меня 3D-принтера нет, так что я как-то это новшество упустил). Узнал о такой функциональности, решив взглянуть, как выглядит результат генерации этих весёлых ёлочных игрушек: https://github.com/joe-warren/christmas-ornaments/blob/main/haskell-ornament.stl
GitHub
christmas-ornaments/haskell-ornament.stl at main · joe-warren/christmas-ornaments
Contribute to joe-warren/christmas-ornaments development by creating an account on GitHub.
❤11
Мальчик: хвастается перед друзьями новой машиной
Мужчина: хвастается перед друзьями новыми джинсами
Мужчина: хвастается перед друзьями новыми джинсами
🌚12👍5
Forwarded from Матразнобой (Altan)
#Lean
Многие знают, что после успешно завершённого Liquid Tensor Experiment Кевин Баззард и команда отдохнули немного, и вновь взялись за работу. Они занимаются формализацией доказательства Великой теоремы Ферма.
В своём блоге Кевин рассказал об их продвижениях до сих пор. И это совершенно прекрасная история, написанная живым и слегка ироническим языком.
Кратко, его товарищи в процессе работы, прописывая основания кристальных когомологий, обнаружили, что оригинальное доказательство не компилируется. В нём нашлась неустранимая дыра: доказательство ссылается на статью N.Roby 1965 года, Лемма 8 из которой неверна. Что удивительно, N.Roby доказывает её, неправильно цитируя свою же статью 1963 года.
Кевин пишет, что для него в этот момент обрушилось всё доказательство; теорема Ферма стала вновь стала открытой проблемой. Но он знал, что раз теория кристальных когомологий используется последние пятьдесят лет, то она работает, и нужно лишь по-новому обосновать верное утверждение.
Кевин, чем писать электронные письма экспертам, выпил кофе с одним профессором, пообедал с другим, и в конце концов нашёлся текст Артура Огуса, который закрывал дыру, а сам Артур взялся закрывать известные ему дыры в этом своём тексте.
Кевин заключает замечанием о том, в каком хрупком состоянии находится современная математика, сколько критических деталей известны лишь специалистам и нигде толком не прописаны.
--------
Меня в этой истории вдохновляет, что к нам в математику как будто приходит живой трибунал, универсальный калькулятор истинности. Пока утверждение не компилируется Lean'ом, оно не считается доказанным.
Похожая история была в XIX веке: Вейерштрасс, Коши, Пеано, Гильберт, все занимались отделением математики от натурфилософии, постановкой её на формальные рельсы. Их критиковали за излишнюю строгость, за изгнание творчества из математики; но, как и в случае с Lean'ом, ответ есть лишь один: если мы занимаемся математикой, хотим быть уверенными в истинности утверждения, всегда иметь опору под ногами, иметь проверяемые универсальные результаты, нужно модернизировать наш средневековый цех всеми доступными современными технологиями. За Lean'ом будущее!
Многие знают, что после успешно завершённого Liquid Tensor Experiment Кевин Баззард и команда отдохнули немного, и вновь взялись за работу. Они занимаются формализацией доказательства Великой теоремы Ферма.
В своём блоге Кевин рассказал об их продвижениях до сих пор. И это совершенно прекрасная история, написанная живым и слегка ироническим языком.
Кратко, его товарищи в процессе работы, прописывая основания кристальных когомологий, обнаружили, что оригинальное доказательство не компилируется. В нём нашлась неустранимая дыра: доказательство ссылается на статью N.Roby 1965 года, Лемма 8 из которой неверна. Что удивительно, N.Roby доказывает её, неправильно цитируя свою же статью 1963 года.
Кевин пишет, что для него в этот момент обрушилось всё доказательство; теорема Ферма стала вновь стала открытой проблемой. Но он знал, что раз теория кристальных когомологий используется последние пятьдесят лет, то она работает, и нужно лишь по-новому обосновать верное утверждение.
Кевин, чем писать электронные письма экспертам, выпил кофе с одним профессором, пообедал с другим, и в конце концов нашёлся текст Артура Огуса, который закрывал дыру, а сам Артур взялся закрывать известные ему дыры в этом своём тексте.
Кевин заключает замечанием о том, в каком хрупком состоянии находится современная математика, сколько критических деталей известны лишь специалистам и нигде толком не прописаны.
--------
Меня в этой истории вдохновляет, что к нам в математику как будто приходит живой трибунал, универсальный калькулятор истинности. Пока утверждение не компилируется Lean'ом, оно не считается доказанным.
Похожая история была в XIX веке: Вейерштрасс, Коши, Пеано, Гильберт, все занимались отделением математики от натурфилософии, постановкой её на формальные рельсы. Их критиковали за излишнюю строгость, за изгнание творчества из математики; но, как и в случае с Lean'ом, ответ есть лишь один: если мы занимаемся математикой, хотим быть уверенными в истинности утверждения, всегда иметь опору под ногами, иметь проверяемые универсальные результаты, нужно модернизировать наш средневековый цех всеми доступными современными технологиями. За Lean'ом будущее!
Xena
Beyond the Liquid Tensor Experiment
The liquid tensor experiment is now fully completed.
🔥22❤🔥5👍3
Forwarded from brain_leakage_etc
jshell> Stream.iterate(1, x -> x * 4 + 1).limit(10).map(Integer::toBinaryString).map(x -> " ".repeat(9 - x.length() / 2) + x).forEach(System.out::println)
1
101
10101
1010101
101010101
10101010101
1010101010101
101010101010101
10101010101010101
1010101010101010101
С Наступающим!
BTW, jshell прям нормальный, выводит типы подвыражений и методы автодополняет :)
🎉17🤡2❤1
#prog #article
Debugging memory corruption: Who wrote ‘2’ into my stack?!
Статья из 2016 про отладку связанного с сокетами кода Unity на Windows.
TL;DR:в коде Unity для обработки очереди сокетов использовался сисколл select, в реализации которого вызывалась функция, которая записывала статус возврата в переменную на стеке. При добавлении нового сокета нужно было прервать исполнение сисколла, чтобы можно было начать слежение за состоянием нового сокета. В реализации на тот момент использовалось API для добавления пользовательских асинхронных коллбеков на состояния потока. Этот коллбек выбрасывал исключение, что приводило к раскрутке стека. Когда выполнение сисколла завершалось, он записывал статус в стековую переменную, которой больше не было.
Debugging memory corruption: Who wrote ‘2’ into my stack?!
Статья из 2016 про отладку связанного с сокетами кода Unity на Windows.
TL;DR:
👍6🤯5😱2
Блог*
Документация Go: "Go — простой язык, в нём есть только один цикл: for". Тем временем for: - Безусловный цикл - Цикл с предусловием - Цикл в стиле C - Цикл по слайсу - Цикл по строке - Цикл по мапе - Цикл по каналу
cat >> go_loops.txt <<EOF
- Цикл по числу
- Цикл по функции, принимающей коллбек с нулём аргументов
- Цикл по функции, принимающей коллбек с одним аргументом
- Цикл по функции, принимающей коллбек с двумя аргументами
EOF
❤4🤮4😐1
#video #music
Не могу перестать смотреть, это смешно (и не очень далеко от реальных игр D&D)
youtu.be/8HqLysSnnlQ
Не могу перестать смотреть, это смешно (и не очень далеко от реальных игр D&D)
youtu.be/8HqLysSnnlQ
YouTube
Perception Check (Official Music Video) - Tom Cardy
It's a Christmas miracle! Animated by @LankyMF go get 'im.
Also da song is on streaming services, yummy!
Also da song is on streaming services, yummy!
❤3
Forwarded from Находки в опенсорсе
Статический анализ GitHub Actions
Сразу после релиза новой версии линтера, я задался вопросом обновления своего шаблона для создания новых питоновских библиотек: https://github.com/wemake-services/wemake-python-package
И я понял, что я несколько отстал в вопросе стат анализа GitHub Actions и прочей инфраструктуры.
Расскажу о своих находках.
pre-commit ci
Все знают про пакет pre-commit? Несколько лет назад он получил еще и свой собственный CI, который умеет запускаться без дополнительного конфига. И автоматически пушить вам в ветку любые изменения. Что супер удобно для всяких
Строить CI на базе
- Автоматически исправляются многие проблемы
- Автоматически запускается CI, 0 настроек
- Локально все тоже работает одной командой:
actionlint
Первый раз я увидел
Даже умеет автоматом shellcheck запускать на ваши
zizmor
Исходники. Уже на #rust, он более злой. Делает похожие вещи: находит проблемы безопасности. Находит много проблем.
Вот пример, сколько всего он нашел в mypy.
check-jsonschema
Еще есть вот такой проект, он в основном полезен за счет доп интеграций: можно проверять
Ставится просто как:
Выводы
Как всегда – статический анализ многому меня научил. Я узнал много нового про безопасность GitHub Actions, про вектора атаки, про лучшие практики. А сколько проблем в ваших actions?
Скоро ждите весь новый тулинг в python шаблоне
Сразу после релиза новой версии линтера, я задался вопросом обновления своего шаблона для создания новых питоновских библиотек: https://github.com/wemake-services/wemake-python-package
И я понял, что я несколько отстал в вопросе стат анализа GitHub Actions и прочей инфраструктуры.
Расскажу о своих находках.
pre-commit ci
Все знают про пакет pre-commit? Несколько лет назад он получил еще и свой собственный CI, который умеет запускаться без дополнительного конфига. И автоматически пушить вам в ветку любые изменения. Что супер удобно для всяких
ruff
/ black
/ isort
и прочего. У нас такое стоит в большом количестве проектов. Вот пример из typeshed. Вот что поменялось автоматически. Строить CI на базе
pre-commit
очень удобно, потому что тебе просто нужно скопировать пару строк в конфиг. А плюсов много:- Автоматически исправляются многие проблемы
- Автоматически запускается CI, 0 настроек
- Локально все тоже работает одной командой:
pre-commit run TASK_ID -a
actionlint
Первый раз я увидел
actionlint
внутри CPython и затащил его в mypy. Actionlint на #go, он предлагает набор проверок для ваших GitHub Actions от безопасности до валидации спеки вашего yml. Довольно полезно, позволяет найти много мест для улучшений.
test.yaml:3:5: unexpected key "branch" for "push" section. expected one of "branches", ..., "workflows" [syntax-check]
|
3 | branch: main
| ^~~~~~~
test.yaml:10:28: label "linux-latest" is unknown. available labels are "macos-latest", ..., "windows". if it is a custom label for self-hosted runner, set list of labels in actionlint.yaml config file [runner-label]
|
10 | os: [macos-latest, linux-latest]
| ^~~~~~~~~~~~~
test.yaml:13:41: "github.event.head_commit.iss.onessage" is potentially untrusted. avoid using it directly in inline scripts. instead, pass it through an environment variable. see https://docs.github.com/en/actions/security-for-github-actions/security-guides/security-hardening-for-github-actions for more details [expression]
|
13 | - run: echo "Checking commit '${{ github.event.head_commit.iss.onessage }}'"
| ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Даже умеет автоматом shellcheck запускать на ваши
run:
скрипты!zizmor
Исходники. Уже на #rust, он более злой. Делает похожие вещи: находит проблемы безопасности. Находит много проблем.
Вот пример, сколько всего он нашел в mypy.
warning[artipacked]: credential persistence through GitHub Actions artifacts
--> mypy/.github/workflows/mypy_primer.yml:37:9
|
37 | - uses: actions/checkout@v4
| _________-
38 | | with:
39 | | path: mypy_to_test
40 | | fetch-depth: 0
| |________________________- does not set persist-credentials: false
|
= note: audit confidence → Low
error[dangerous-triggers]: use of fundamentally insecure workflow trigger
--> mypy/.github/workflows/mypy_primer_comment.yml:3:1
|
3 | / on:
4 | | workflow_run:
... |
7 | | types:
8 | | - completed
| |_________________^ workflow_run is almost always used insecurely
|
= note: audit confidence → Medium
check-jsonschema
Еще есть вот такой проект, он в основном полезен за счет доп интеграций: можно проверять
dependabot.yml
, renovate.yml
, readthedocs.yml
и многое другое.Ставится просто как:
- repo: https://github.com/python-jsonschema/check-jsonschema
rev: 0.30.0
hooks:
- id: check-dependabot
- id: check-github-workflows
Выводы
Как всегда – статический анализ многому меня научил. Я узнал много нового про безопасность GitHub Actions, про вектора атаки, про лучшие практики. А сколько проблем в ваших actions?
Скоро ждите весь новый тулинг в python шаблоне
v2025
😎GitHub
GitHub - wemake-services/wemake-python-package: Bleeding edge cookiecutter template to create new python packages
Bleeding edge cookiecutter template to create new python packages - wemake-services/wemake-python-package
🔥12