[03:03:40] <ada_ru> (Oleg) Парни, есть ли что-то новое в ОС строительстве ? Интересует RTOS, одно время набирала популярность one shot task методология. Но что-то похоже не пошло
[03:04:11] <ada_ru> (Oleg) Хотя есть очевидные плюсы - меньше расход памяти и ещё много всего
[03:04:28] <ada_ru> (Oleg) Хочу модельку на SPARK запилить
[03:04:36] <ada_ru> (Oleg) Пока под ПК
[03:04:47] <ada_ru> (Oleg) Потом под микроконтроллер
[03:05:13] <ada_ru> (Oleg) Мне 100500 задач то не надо , надо 3-5
[03:06:58] <ada_ru> (Oleg) Переключение контекста очень расточительно и Геморой с драйверами начинается , короче есть плюсы есть минусы - хочу начать с простого , пока one shot - по сути каждая задача - машина состояний
[03:07:44] <ada_ru> (Oleg) И кстати аллокатор пригодится :-)
[08:50:27] <ada_ru> (anisimkov)  отвечает (Максим) на <Есть у них continues…>
Не continues а developer. https://www.adacore.com/gnatpro/developer Continues это не про цену, а про способ выдачи клиентам новых релизов.
[09:57:23] <ada_ru> (vasil_sd)  отвечает (Oleg) на <Парни, есть ли что-т…>
Мне очень понравился подход к разработке в OpenCom RTOS.
Они изначально начали с формальных спек и моделирования. В результате объем кода упал на порядок, по сравнению с прошлой Virtuoso. И практически не нужно было отлаживаться и тд.
В общем очень интересный промышленный опыт.
Они даже книгу опубликовали: https://www.academia.edu/10650560/Formal_Development_of_a_Network-Centric_RTOS
[10:02:34] <ada_ru> (vasil_sd)  отвечает (Oleg) на <И кстати аллокатор п…>
Ага, как раз допиливал вчера why3 модули для доказательства свойств битовых операций в tlsf аллокаторе :)
Думаю сегодня выложу пока в сыром виде, он вроде бы нормально работает. А потом потихоньку отверифицирую со временем.
[11:38:35] <ada_ru> (vasil_sd)  отвечает (Максим) на <Может в логах gps по…>
А он разве не всё в messages пишет?
Поищу, где он логи пишет...
[11:39:21] <ada_ru> (Максим) Нет, там есть ~/.gps/ и там логи
[11:46:45] <ada_ru> (vasil_sd)  отвечает (Максим) на <Нет, там есть ~/.gps…>
Понял, спасибо
[13:09:26] <ada_ru> (vasil_sd) https://abcnews.go.com/Politics/software-issues-delay-return-boeings-737-max/story?id=68357961&cid=social_twitter_abcn

Пишут, что Боинг вроде как собирается весь софт для 737 max переписать
[13:10:34] <ada_ru> (vasil_sd)  отвечает (vasil_sd) на <https://abcnews.go.c…>
Интересно, на плюсах или расте, что там сейчас в моду в авионике входит? :)))
[13:24:42] <ada_ru> (Oleg) Индусы в моду входят :-)
[13:29:07] <ada_ru> (Oleg) Странно вот что, в своё время было много разных схем самолётов , двигатели сзади как на 154, и ещё много разных. В итоге пришли к тому что двигатели на пилонах под крылом , хвостовое оперение с нижним стабилизатором , самая стабильная схема, так как стабилизатор не затеняется , и в целом самолёт ведёт себя очень стабильно.
[13:29:57] <ada_ru> (Oleg) А теперь сделали нестабильный самолёт и компенсируют его плохие качества , электроникой
[13:34:34] <ada_ru> (Oleg) Вот с истребителями там да, без компьютера это железяка - как топор летает примерно
[13:53:17] <ada_ru> (vasil_sd)  отвечает (Oleg) на <Вот с истребителями …>
Ага. Читал как-то, что су47 с обратной стреловидностью, без стабилизации полета электроникой вообще никак летать не может....
[16:04:50] <ada_ru> (Eugene) у су-47 беркута проблема только в том, что малейшее повреждение композитного крыла приводит к его необратимому разрушению, а без композитных материалов там никак — силшком сильные нагрузки на крыло из-за обратной стреловидности
[20:28:53] <ada_ru> (vasil_sd)  отвечает (Максим) на <Нет, там есть ~/.gps…>
Смотрел логи, но так и не нашёл в чём была проблема.

Максим, у меня есть вопросы по использованию gnatprove, есть ли какой-нибудь форум, где можно их поспрашивать?

В частности, столкнулся с проблемой, когда внешняя аксиоматика  в одном проекте не подключается нормально, если этот проект импортируется в другой через with, gnatprove не находит соотв. .mlw файлы.
Нашёл обходной путь - приходится эти файлы копировать в другой проект и там настраивать Prove'Proof_DIr в файле проекта. Но это неправильно, так как файлы не относятся к этому проекту, они оносятся к подключаемому.
Документацию уже просмотрел вдоль и поперёк - и так и не понял как сделать это всё нормально.
[21:12:59] <ada_ru> (Лекс) Автор написанного на языке Rust web-фреймворка actix-web удалил репозиторий после того, как на него обрушилась критика за "неправильное использование" языка Rust.

https://www.opennet.ru/opennews/art.shtml?num=52208
[21:14:59] <ada_ru> (Лекс) Автор не выдержал психологического давления, удалил репозиторий и написал, что завязал с Open Source.
[21:15:43] <ada_ru> (Лекс) вот и правильно сделал, имхо, в этом мире сплошного долбоебизма
[21:36:48] <ada_ru> (FROL256) не стоит прогибаться под изменчивый мир
[21:36:58] <ada_ru> (FROL256) подумаешь тролли набежали, это же опен сорс
[21:37:01] <ada_ru> (FROL256) не нравится — не ешь
[21:37:05] <ada_ru> (FROL256) ерунда какая-то
[22:07:28] <ada_ru> (Oleg) В раст чате обсуждали вчера вовсю
[22:07:31] <ada_ru> (Oleg) :-)
[22:07:52] <ada_ru> (Oleg) Новость дня :-)
[22:13:47] <ada_ru> (Oleg) Точно про опен сурс :-)
[23:47:12] <ada_ru> (vasil_sd)  отвечает (Лекс) на <Автор не выдержал пс…>
Истеричная реакция на пачку троллей не красит автора. Его приложение было полезно многим другим людям и из-за небольшого (относительно) количества каких-то уродов он по сути сделал хуже большому количеству нормальных и адекватных людей.

Уродов везде хватает, нужно уметь не обращать на них внимание.
[23:50:39] <ada_ru> (Лекс)  отвечает (vasil_sd) на <Истеричная реакция н…>
Хуже сделал не автор, а кучка уродов.
[23:51:03] <ada_ru> (vasil_sd)  отвечает (Лекс) на <Хуже сделал не автор…>
Автор повёлся на провокации.
[23:51:13] <ada_ru> (vasil_sd) И принял эмоциональное решение
[23:51:34] <ada_ru> (Лекс) Автор никому и ничего не обязан, а ответственность за провокацию и её последствия должны лежать исключительно на провокаторах.
[23:55:41] <ada_ru> (vasil_sd)  отвечает (Лекс) на <Автор никому и ничег…>
Не согласен. В любой области жизни есть определённый процент уродов, психопатов, нарциссов, просто психически больных и тд. И нужно просто это иметь ввиду и не реагировать на них. В данном случае смысла об ответственности говорить нет, ибо автор действительно никому и ничего не должен был.
И эти уроды, кстати, тоже никому и ничего не должны. Они просто уроды.
Но поведение автора - это юношеский максимализм, обида из-за небольшой кучки уродов.
И такая эмоциональная реакция его совершенно не красит.
[23:56:52] <ada_ru> (Лекс)  отвечает (vasil_sd) на <Не согласен. В любой…>
Не согласен, но поддерживать дискуссию не намерен
[23:56:54] <ada_ru> (Oleg) Это показывает только то , что надеятся на сообщество нельзя, сегодня есть проект - завтра нет
[23:57:16] <ada_ru> (Лекс)  отвечает (Oleg) на <Это показывает тольк…>
Делай форк :)
[23:57:18] <ada_ru> (vasil_sd)  отвечает (Oleg) на <Это показывает тольк…>
Ага. left_pad тому пример
[23:57:35] <ada_ru> (Oleg) Вот , форки всего :-)
[23:57:38] <ada_ru> (Oleg) Нужного
[23:57:46] <ada_ru> (Лекс) кстати пойду red форкну, пока он не исчез 😃
[23:58:56] <ada_ru> (vasil_sd)  отвечает (Oleg) на <Вот , форки всего :-…>
Всё-равно тупик. Так как проекты без поддержки через какое-то время протухнут (тулы уйдут вперёд, либы от которых они зависят, железо поменяется, ось, api и пр).
[23:59:55] <ada_ru> (vasil_sd) Нужна более-менее адекватная регуляция на площадках, которая бы минимизировала возможности травли разработчиков.