[03:36:22] <ada_ru> (Gourytch) как грустно, когда решаешь смастерить кольцевой буфер через два индекса (head и tail), потом добавляешь в него последний элемент и он такой - херакс - и не полный, а пустой =)
[09:57:57] <ada_ru> (Oleg) :-)
[10:26:15] <ada_ru> (vasil_sd) отвечает (Gourytch) на <как грустно, когда р…>
Нужно Спарк использовать :) После недели доказательства, можно было бы быть уверенным, что такого не произойдет :)
[10:30:46] <ada_ru> (Gourytch) отвечает (vasil_sd) на <Нужно Спарк использо…>
как только под ESP32 в PlatformIO можно будет писать на Spark-е и библиотеки будут не только сишные и плюсовые - так и да =)
[10:49:25] <ada_ru> (vasil_sd) отвечает (Gourytch) на <как только под ESP32…>
Ну не проблема, Frama-C с кольцевым буфером тоже нормально справится :)
[10:49:56] <ada_ru> (Gourytch) отвечает (vasil_sd) на <Ну не проблема, Fram…>
а с плюсами она справится?
[10:50:28] <ada_ru> (Gourytch) (хотя должна по идее)
[10:50:31] <ada_ru> (vasil_sd) Возможно уже что-то и плюсовое умеет - нужно смотреть
[10:51:09] <ada_ru> (Gourytch) (* смотрит в https://frama-c.com/frama-clang.html ... может даже и да *)
[10:51:15] <ada_ru> (vasil_sd) Но для кольцевого буфера особо плюсы не нужны. абстракция от типа элемента через классический void* :)
[10:52:59] <ada_ru> (vasil_sd) отвечает (Gourytch) на <(* смотрит в https:/…>
Посмотрел. Ну с простым плюсовым кодом думаю будет ок.
Правда, как там сложный код странслируют в упрощенный сишник, и насколько это будет понимаемо - это вопрос
[10:54:13] <ada_ru> (nitrocerber) отвечает (Gourytch) на <как только под ESP32…>
Берём CCG, мутим спарк код, переводим в си, си компиляем на таргет чем душа прикажет
[10:54:30] <ada_ru> (nitrocerber) Правда ццг взять это такая себе задача
[10:54:54] <ada_ru> (vasil_sd) отвечает (nitrocerber) на <Берём CCG, мутим спа…>
Тут проблема доказательства корректности шага spark -> c
[10:55:49] <ada_ru> (nitrocerber) Оно ж вроде сертифицировано... чи ни. Хрен знает. Но контора очень кичится этим подходом
[10:56:25] <ada_ru> (vasil_sd) Хоть у adacore и есть компиляция sparka в С, но в опенсорсной сборке я этого не нашёл. А ручной перевод чреват граблями
[10:56:49] <ada_ru> (nitrocerber) Ну вот я о том и говорю, взять ццг забесплатно -проблема
[10:57:16] <ada_ru> (nitrocerber) Оформляйте суппорт контракт) мож мне зряплату подымут на цуцуть за привод клиентов...)))
[10:57:32] <ada_ru> (nitrocerber) Ну это я орирую, если что
[11:00:16] <ada_ru> (vasil_sd) отвечает (nitrocerber) на <Оформляйте суппорт к…>
Значит и ты тоже там работаешь :)
Оказывается тут много людей из AdaCore...
Может вы руководство уговорите демо-версии тулов давать бедным студентам поиграться? :)
Очень интересно codepeer пощупать, ну и ggc заодно...
А заморачиваться со всякими контрактами для этого - как-то не хочется
[11:00:33] <ada_ru> (I_vlxy_I) отвечает (nitrocerber) на <Ну вот я о том и гов…>
А за привод новых сотрудников бонусируют?
[11:01:43] <ada_ru> (nitrocerber) отвечает (vasil_sd) на <Значит и ты тоже там…>
А бедным студентам и дают. Если универ в GAP входит
[11:02:01] <ada_ru> (nitrocerber) отвечает (I_vlxy_I) на <А за привод новых со…>
Ну рукопожатность точно поднимается.
[11:02:09] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Значит и ты тоже там…>
Хотя бы в виде онлайн сервиса, кстати. На поиграться - хватит.
[11:02:37] <ada_ru> (vasil_sd) отвечает (nitrocerber) на <А бедным студентам и…>
Я уже давно не в универе :(
Да и найти универ, договориться на GAP и пр - это ещё та головная боль...
[11:02:42] <ada_ru> (nitrocerber) Так-то многие на собес попадают именно через личные рекомендации
[11:02:50] <ada_ru> (nitrocerber) Адский мир мал и тут рукопожатий сильно меньше 8
[11:03:43] <ada_ru> (I_vlxy_I) У нас за приведение кошерного кандидата, который потом принял оффер, таки бонусируют деньгами
[11:04:12] <ada_ru> (nitrocerber) Ну я еще никого не приводил, так что за это я хз
[11:04:44] <ada_ru> (I_vlxy_I) отвечает (nitrocerber) на <Ну я еще никого не п…>
Хватай Vasil и тащи в адакору!
[11:05:00] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <У нас за приведение …>
Это много где так. Но как по мне, так это порочная практика. Ибо нормальный профи и так будет стараться нормальную команду вокруг формировать и на нармальную работу будет приглашать нормальных людей без всяких бонусов
[11:05:22] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Хватай Vasil и тащи …>
Не надо меня пока хватать :)
[11:05:29] <ada_ru> (nitrocerber) Ну славянская мафия примерно так в конторе и наросла
[11:06:37] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Хватай Vasil и тащи …>
Я ещё TLSF недоверифицировал. :)
Сейчас между работами хочу успеть полезных вещей понаделать, а то потом опять со свободным временем проблемы будут...
[11:24:05] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Я ещё TLSF недовериф…>
Надо будет катить в продакшн!
[11:24:49] <ada_ru> (I_vlxy_I) Чтобы потестить прогу, нужно ее вначале на прод выкатить, а уж опосляяя...
[11:28:40] <ada_ru> (I_vlxy_I) Вспомнилось: https://m.vk.com/topic-13330381_21967022
[11:37:26] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Вспомнилось: https:/…>
Ага. Жизненна. Но к чему это вспомнилось? :) И что бы дедушка Фрейд по этому поводу сказал? :)
[11:43:07] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Ага. Жизненна. Но к …>
Ну, речь зашла о рабочих коллективах и методах найма... Бить промеж ушей и тащить в деревню!
[11:44:09] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Ну, речь зашла о раб…>
Ну это такое ;) Если сильно бить промеж ушей - это потом профнепригодный сотрудник будет. Если слабо - нелояльный :)
[11:44:53] <ada_ru> (I_vlxy_I) отвечает (vasil_sd) на <Ну это такое ;) Если…>
Да, силу удара надо правильно рассчитывать.
[11:45:00] <ada_ru> (vasil_sd) отвечает (I_vlxy_I) на <Да, силу удара надо …>
:)
[12:01:57] <ada_ru> (Максим) отвечает (Gourytch) на <как только под ESP32…>
https://github.com/jklmnn/gnat-llvm-xtensa вот есть уже
[12:04:41] <ada_ru> (Gourytch) отвечает (Максим) на <https://github.com/j…>
хммм... попробую щас.
[12:04:47] <ada_ru> (Gourytch) спасибо
[12:22:43] <ada_ru> (Oleg) Покажи нам твой буффер, я 15 лет назад их делал много :-)
[12:23:20] <ada_ru> (Oleg) Есть свежий под IP пакеты
[12:23:50] <ada_ru> (Oleg) Но не верифицированный
[12:28:15] <ada_ru> (Gourytch) отвечает (Oleg) на <Покажи нам твой буфф…>
сейчас. заодно репу пушну хоть.
[12:30:33] <ada_ru> (Gourytch) отвечает (Oleg) на <Покажи нам твой буфф…>
https://github.com/gourytch/heartbeat/blob/master/include/ring.hpp
[12:31:44] <ada_ru> (Oleg) Окей погляжу попозже чутка
[12:35:57] <ada_ru> (I_vlxy_I) О, стоит отвернуться, в группе начинают публично свои буфера демонстрировать...
[12:58:10] <ada_ru> (Oleg) Ж-)
[14:00:00] <ada_ru> (nitrocerber) О, кардиология пошла?
[14:01:10] <ada_ru> (I_vlxy_I) отвечает (nitrocerber) на <О, кардиология пошла…>
Ы?
[14:01:30] <ada_ru> (Gourytch) отвечает (nitrocerber) на <О, кардиология пошла…>
ну это я для самого себя, чтобы мониторить.
[14:01:51] <ada_ru> (nitrocerber) Хартбит монитор. Холтэр поди
[14:02:46] <ada_ru> (Gourytch) типа того. только на на три отвода, как у настоящего холтера, а на один. (или как оно зовётся)
[14:03:13] <ada_ru> (Oleg) Богомерзки C++
[14:03:20] <ada_ru> (nitrocerber) У нас с папашей вопрос больной прост, наследственный. Даёшь суточное экг на аде!
[14:03:23] <ada_ru> (Oleg) Нужно жеж на C
[14:03:39] <ada_ru> (Oleg) Еще только заглянул - прикольно
[14:03:45] <ada_ru> (Oleg) По ЭКД тоже работал
[14:03:54] <ada_ru> (Gourytch) отвечает (Oleg) на <Нужно жеж на C>
зачем на сях? добровольный бег в мешках?
[14:04:23] <ada_ru> (nitrocerber) Ну холтеры и 9канальные бывают, там помимо чсс ещё много интересного снимать можно
[14:04:29] <ada_ru> (Oleg) На сях бы такого не было 😊 все бы уже работало..... наверное
[14:04:51] <ada_ru> (Gourytch) отвечает (nitrocerber) на <У нас с папашей вопр…>
это надо тогда библиотеки переписывать. ну и яхз как оно будет в той ОСРВ-то жить. и как там всё переделывать чтоб жило нормально.
[14:05:50] <ada_ru> (Oleg) А ты без FreeRTOS?
[14:07:16] <ada_ru> (Gourytch) с нею. там же как: крутится FreeRTOS, на неё навешено нахлобучка-адаптер Arduino, а уже под него все библиолтеки типа картинки рисовать/фрешкуписать/ время считать
[14:07:39] <ada_ru> (I_vlxy_I) отвечает (nitrocerber) на <У нас с папашей вопр…>
А PPG не пойдёт? Я как раз это пилил для круглосуточного реалтайм мониторинга :-)
[14:07:54] <ada_ru> (Gourytch) PPG - эт что?
[14:08:12] <ada_ru> (I_vlxy_I) Фотоплетизмограмма
[14:08:34] <ada_ru> (I_vlxy_I) Заодно и SpO2 измерять можно
[14:09:18] <ada_ru> (nitrocerber) Эт как во всяких мибандах?
[14:09:21] <ada_ru> (Gourytch) а. ну фотометрией особо не померишь качественно, imho: она ж именно по кровотоку.
[14:09:41] <ada_ru> (Oleg) Де фотометрия фигня
[14:09:46] <ada_ru> (nitrocerber) Там точность плюс-минус километр, это всё фуфло
[14:09:57] <ada_ru> (Oleg) Надо 5 электродов на грудь
[14:10:05] <ada_ru> (Oleg) Остольное не актуально
[14:10:09] <ada_ru> (Gourytch) а через ЭКГ можно именно увидеть как прикольно себя кардиомышца ведёт в, скажем, аритмическом сокращении
[14:10:24] <ada_ru> (Gourytch) отвечает (Oleg) на <Надо 5 электродов на…>
можно и три.
[14:10:40] <ada_ru> (Oleg) Можно, но лучше 5 звезд 😊
[14:11:00] <ada_ru> (nitrocerber) Ну хотя бы два, баеровские нагрудные пульсометры достаточно близко к нормальному экг меряют
[14:11:25] <ada_ru> (Oleg) Шумы давить сложно на двух
[14:11:27] <ada_ru> (I_vlxy_I) отвечает (nitrocerber) на <Эт как во всяких миб…>
Типа того. Как в профессиональных пульсоксиметрах
[14:11:30] <ada_ru> (nitrocerber) Пучок гисса на них конеш не увидишь, но аритмию мою ловят
[14:12:12] <ada_ru> (I_vlxy_I) Аритмия и пропуски ударов - видны там. Вариабельность ритма тоже хорошо ловится :-)
[14:12:24] <ada_ru> (I_vlxy_I) Там даже частоту дыхания вылавливать можно :-)
[14:14:24] <ada_ru> (I_vlxy_I) После операции на сердце PPG ОЧЕНЬ интересная
[14:15:04] <ada_ru> (nitrocerber) Ну видать они стоить должны хорошо
[14:15:40] <ada_ru> (nitrocerber) Из масс маркета чот все ниочом
[14:17:28] <ada_ru> (I_vlxy_I) отвечает (nitrocerber) на <Из масс маркета чот …>
У масс маркета во-первых алгоритмы ни о чем, во-вторых они на руку крепятся (запястье), а это вообще не лучшее место для PPG
[14:17:49] <ada_ru> (nitrocerber) то есть там тоже нагрудник?
[14:17:51] <ada_ru> (I_vlxy_I) Там крови то, считай, нет.
[14:18:00] <ada_ru> (nitrocerber) или на шею там
[14:18:40] <ada_ru> (I_vlxy_I) отвечает (nitrocerber) на <то есть там тоже наг…>
Мочка уха очень норм. Лоб - норм. На груди - такое, мало крови, много жира.
Ну и подушечка любого пальца.
[14:19:12] <ada_ru> (nitrocerber) интересно, а как оно с трепыханиями? они до переферии-то не доходят
[14:19:20] <ada_ru> (Oleg) отвечает (I_vlxy_I) на <Мочка уха очень норм…>
Jabra делает гарнитуру с пульсл\омером
[14:20:08] <ada_ru> (Gourytch) вот мочка уха - это действительно ок: там разных помех гораздо меньше да и место удобное. наверное.
[14:20:17] <ada_ru> (I_vlxy_I) отвечает (nitrocerber) на <интересно, а как оно…>
Хез. Надо изучать. Но если это на кровоснабжение хоть как-то влияет и на удары сердца - это будет видно
[14:20:58] <ada_ru> (nitrocerber) ну оно бьётся, но в пустую почти, нормального забора нет. чсс 200+, а пульс не просулшивается. тока пену генерит
[14:21:05] <ada_ru> (Oleg) https://www.jabra.ru/sports-headphones/jabra-sport-pulse-wireless#/#100-96100010-60
[14:21:10] <ada_ru> (nitrocerber) но я тож хз, мож точные приборы и на переферии словят
[14:21:26] <ada_ru> (nitrocerber) я всё ж объект, а не субъект в этом вопросе)
[14:22:18] <ada_ru> (I_vlxy_I) отвечает (nitrocerber) на <ну оно бьётся, но в …>
Дык это будет видно или как отсутствие пульса, или как что-то странное. Ну и на SpO2 это должно повлиять
[14:29:48] <ada_ru> (I_vlxy_I) Хотя, без пульса SpO2 не измерить
[15:14:35] <ada_ru> (vasil_sd) С синтаксисом спарка нужно однозначно что-то делать. Очень тяжело в самом спарке выражать более менее сложные свойства и их доказывать.
Из-за отсутствия механизма указания гнатпруву, какие ассерты помещать в контекст для SMT солвера, приходится писать монструозный код: https://github.com/vasil-sd/ada-tlsf/blob/master/tlsf/src/proof/model/block/tlsf-proof-model-block.adb#L391 😩 Чтобы неявно рулить контекстом.
Из-за отсутсвия нормальных возможностей доказательств по индукции, приходится делать вот такие вот страшные штуки: https://github.com/vasil-sd/ada-tlsf/blob/master/tlsf/src/proof/model/block/tlsf-proof-model-block.adb#L245. То есть сначала пустым циклом с инвариантами косвенно создаём индуктивные схемы в контексте, затем их неявно используем. :(
Очень нехватает тактик нормальных. Их тоже приходится симулировать через Ж: https://github.com/vasil-sd/ada-tlsf/blob/master/tlsf/src/proof/model/block/tlsf-proof-model-block.adb#L270 😩
Возможно, конечно, это я криворукий, но пока на многие вопросы ответов не нашёл.
И нормального мануала по ручному доказательству тоже пока нет (судя по ответам в списке рассылки по спарку) :(
[15:28:05] <ada_ru> (nitrocerber) а чего ghost не пользуешься? за контексты и солверы ничего не скажу, не разбираюсь, но многоуровневые ифзенелсы из инвариантов я бы попихал по ghost предикатам
[15:28:36] <ada_ru> (nitrocerber) там и локалочки всякие пообъявлять можно, если надо
[15:29:04] <ada_ru> (Максим) отвечает (Oleg) на <https://www.jabra.ru…>
у меня валяются такие... мне показалось не особо точные
[15:29:06] <ada_ru> (vasil_sd) отвечает (nitrocerber) на <а чего ghost не поль…>
Так там у меня весь package ghost, это модель с операциями и доказанными свойствами
[15:29:38] <ada_ru> (nitrocerber) а, это всё гхост? ужос какой
[15:29:44] <ada_ru> (vasil_sd) отвечает (nitrocerber) на <там и локалочки всяк…>
И выношу и пользуюсь. Но не хватает конкретных вещей, которые описал
[15:29:49] <ada_ru> (nitrocerber) не писать мне на спарке никогда)))
[15:30:30] <ada_ru> (vasil_sd) Там просто модель точная, это не просто доказательство отсуствия переполнения, а доказательство корректности функционала.
[15:31:00] <ada_ru> (vasil_sd) И для таких сложных (относительно) моделей, спарк использовать тяжело :(
[15:32:57] <ada_ru> (nitrocerber) мне издаля чот кажется, что сложные модели это вообще тяжело
[15:33:10] <ada_ru> (nitrocerber) но я тупенький так то, не показатель)
[15:34:52] <ada_ru> (vasil_sd) отвечает (nitrocerber) на <мне издаля чот кажет…>
На самом деле там не так уж и много нужно. Если сделать возможность прагмами рулить контекстом, то уже писанины будет раза в два-три меньше.
Добавить ещё возможность прагмами задавать наборы тактик и вынести в прагмы часть функционала по ручному доказательству - ещё раза в два писанины можно уменьшить
[21:01:42] <ada_ru> (Максим) http://www.ada-ru.org/forum/p2540239052_1.html
[21:46:01] <ada_ru> (t91x0) Присоединяйтесь к голосованию
[21:46:02] <ada_ru> (t91x0)
[21:47:19] <ada_ru> (vasil_sd) отвечает (Максим) на <http://www.ada-ru.or…>
👍
[21:51:26] <ada_ru> (nitrocerber) А кто такой сто? Я тока станцию техобслуживания знаю. И специальную теорию относительности)
[21:52:03] <ada_ru> (t91x0) Техдиректор
[22:16:37] <ada_ru> (Лекс) пессимистичный опрос, намекает что у СТО нет шансов жить
[22:17:54] <ada_ru> (I_vlxy_I) отвечает (Лекс) на <пессимистичный опрос…>
Это правда
[22:20:37] <ada_ru> (I_vlxy_I) СТО - расходник
[22:23:33] <ada_ru> (Gourytch) техдиром я был. не. больше не хочу. я вообще не хочу быть в начальниках каких бы то ни было.
[22:39:56] <ada_ru> (Oleg) Я в меньшенстве
[22:40:00] <ada_ru> (Oleg) :-)
[22:54:08] <ada_ru> (I_vlxy_I) отвечает (Gourytch) на <техдиром я был. не. …>
Боль и страдания!
[22:54:35] <ada_ru> (I_vlxy_I) Дауншифтинг в яндекс.такси.технологии!
[22:56:19] <ada_ru> (Gourytch) не. я техдиром был в прошлом тысячелетии.
[23:01:03] <ada_ru> (I_vlxy_I) отвечает (Gourytch) на <не. я техдиром был в…>
Это не имеет значения :-)
[23:04:46] <ada_ru> (Oleg) отвечает (I_vlxy_I) на <Дауншифтинг в яндекс…>
Просто тогда в яндекс такси
[23:07:53] <ada_ru> (Gourytch) отвечает (I_vlxy_I) на <Это не имеет значени…>
ну я из техдира дауншифтнулся сперва в гис-программиста, потом в главпрога пишущего виндовое с MFC , потом в просто программиста В.К ковыряющегося в кишках db2, потом в начпроекта пишущего на платёжную систему питоне, потом чючють в сисадмина+постгрессиста+девопса, потом в программиста трекающего бомбы, несунов и лыжников, потом в z/OS программиста и только потооооом - в таксиста-программиста =)
[23:08:39] <ada_ru> (Gourytch) (а начинал я вообще - как санитар морга =) )
[23:13:41] <ada_ru> (nitrocerber) отвечает (Gourytch) на <(а начинал я вообще …>
вот это эпично
[23:14:06] <ada_ru> (Gourytch) отвечает (nitrocerber) на <вот это эпично>
ну так-то да =)
было запоминающееся
[23:23:02] <ada_ru> (I_vlxy_I) отвечает (Gourytch) на <(а начинал я вообще …>
После этого и с++ не страшен!
[23:23:20] <ada_ru> (I_vlxy_I) И даже это!
[23:23:21] <ada_ru> (I_vlxy_I) Проект Deno развивает защищённую JavaScript-платформу, похожую на Node.js https://opennet.ru/52387/
[23:24:02] <ada_ru> (Gourytch) Javascript на Rust =))
[23:25:20] <ada_ru> (I_vlxy_I) Растом прикрыли V8 :-)
[23:25:26] <ada_ru> (I_vlxy_I) Будто это поможет
[23:25:47] <ada_ru> (I_vlxy_I) Оно ж один фиг на js будет и на с++ сам v8