ну пишешь обычное доказательство
Это как? Как я напишу машине, что пи - это трансцендентное число?
Alex
Evgenii
Это как? Как я напишу машине, что пи - это трансцендентное число?
ну соре, объяснять как работают пруферы это оффтоп
Berkus
даже про tla+ можно
Evgenii
ну тогда у меня не остается выхода кроме как признать что я не знаю)
Berkus
ихихих
Berkus
но вообще тема интересная, гораздо интереснее кодировок вывода в виндовой консоли
Vsevolod
Парсить argv?
Egor
Вопрос: как доказать через ЯП, что в числе пи есть любая комбинация цифр, например, мой номер телефона?
Ну вот, например, тут на Coq доказывают большую теорему Ферма для n=4: https://github.com/coq-contribs/fermat4/blob/master/Fermat4.v
А вообще гуглить в сторону матлогики и аксиом теории чисел (скажем, аксиомы Пеано для натуральных). Дальше надо будет как-то аксиоматически определить вещественные числа, само число пи (скажем, через ряды) и так далее.
Egor
Вопрос: как доказать через ЯП, что в числе пи есть любая комбинация цифр, например, мой номер телефона?
Если что, то свойство, которое вы назвали, называется "нормальностью по основанию 10" (https://ru.wikipedia.org/wiki/%D0%9D%D0%BE%D1%80%D0%BC%D0%B0%D0%BB%D1%8C%D0%BD%D0%BE%D0%B5_%D1%87%D0%B8%D1%81%D0%BB%D0%BE). Оно не следует из иррациональности или трансцедентности. Человечество пока не знает, нормально ли пи по основанию 10.
Oleg
Если что, то свойство, которое вы назвали, называется "нормальностью по основанию 10" (https://ru.wikipedia.org/wiki/%D0%9D%D0%BE%D1%80%D0%BC%D0%B0%D0%BB%D1%8C%D0%BD%D0%BE%D0%B5_%D1%87%D0%B8%D1%81%D0%BB%D0%BE). Оно не следует из иррациональности или трансцедентности. Человечество пока не знает, нормально ли пи по основанию 10.
Хочешь сказать, что если взять пи и разбавить нулями через одну цифру, то трансцендентности не убавится, а вот большинство телефонных номеров там точно не появятся?
И, видимо, для любой строки из цифр мы не можем доказать, что её нет в пи, зато если она есть где-то недалеко, то можем найти и предьявить.
Evgenii
но вообще тема интересная, гораздо интереснее кодировок вывода в виндовой консоли
+, но надо ботать теории типов и все такое чтобы норм вписаться в это
Александр
реквестирую ссылку на пи-fs
Egor
+, но надо ботать теории типов и все такое чтобы норм вписаться в это
Необязательно ботать теорию типов (а вот функциональное программирование может помочь), есть офигительная книжка: https://softwarefoundations.cis.upenn.edu/
🦥Alex Fails
🦥Alex Fails
@antoshkka , @NataMakarova еще четырех людей надо призвать в РГ21, чтоб в чате было 2100 участников )
RattenKong 🦧🐀🦍️
а буст кукбук не будут сливать?...
Alexander "SonnySlave"
а буст кукбук не будут сливать?...
так ты попроси у @antoshkka . мб у него есть ссылка на торрент
Evgenii
Необязательно ботать теорию типов (а вот функциональное программирование может помочь), есть офигительная книжка: https://softwarefoundations.cis.upenn.edu/
ну меня скорее всего интересует формальная верификации чем матемвтические пруфы, поэтому я не совсем представляю как там все
Egor
ну меня скорее всего интересует формальная верификации чем матемвтические пруфы, поэтому я не совсем представляю как там все
Норм, там книжка как раз про формальную верификацию программ, а не теоремы. Вот, например, формально доказанный компилятор C:
http://compcert.inria.fr/
https://github.com/AbsInt/CompCert
Evgenii
Норм, там книжка как раз про формальную верификацию программ, а не теоремы. Вот, например, формально доказанный компилятор C:
http://compcert.inria.fr/
https://github.com/AbsInt/CompCert
ну как раз в формальной верификации я понимаю немного больше чем ничего
Evgenii
в отличии от
Vladislav
Вопрос по организации работы с множеством репозиториев(7 штук на данный момент). Проект состоит из модулей друг от друга фактически зависимых - клиент, бэкэнд, конфигурации, статика и т.д. каждый живет в своем репозитории. Сейчас все работают только в двух ветках - develop и release. Все это собирается через CI и деплоится по кнопке аля teamcity. Минусы подхода очевидны - только 2 ветки не дают возможности раздельно тестировать\разрабатывать фичи.
В виду коммерческого характера проекта - не все члены команды должны иметь доступ ко всем репозиториям- например в статику имеют доступы художники поддержки(льют картинки), но к репозиторию с серверным кодом они доступ не имеют.
Хотим перейти на git-flow-подобную схему работы, но заводить по ветке в каждом репозитории накладно, когда не каждый реп нужно менять. Ситуацию осложняет то, что есть несколько однотипных проектов и например бэкэнд посути у них общий.
Vladislav
1) все в один большой репозиторий, но уйти с git и попытаться разделять доступы(правда не очень понятны некоторые моменты мерджа) в типа SVN...
2) мучаться и заводить ветки, но попытаться это автоматизитровать?
Vladislav
Наверняка мы не первые, может кто-то придумал как красиво решить данный момент)
Nikita
но с icache у c++ и так все плохо за счет over inlining в огромном множестве проектов
Ну а префетч для кого придумали?
🦥Alex Fails
1) все в один большой репозиторий, но уйти с git и попытаться разделять доступы(правда не очень понятны некоторые моменты мерджа) в типа SVN...
2) мучаться и заводить ветки, но попытаться это автоматизитровать?
у каждой команды свой репозиторий. А что шарится - то пусть лежит в общем
Vladislav
у каждой команды свой репозиторий. А что шарится - то пусть лежит в общем
Очень часто для фичи требуется редактировать конфигурацию(в ней настройки некой фичи) и например клиент, но редактирование конфигурации требует пересборки еще и сервера, хотя по факту изменений в нем не будет мы все-равно должны завести ветку, но как минимум мы должны прогнать тесты с новой конфигурацией
Vsevolod
@urandon, как поможет префетч при джампах, больших размера страницы?
Berkus
держите конфиг из repo:branch в отдельном репо, стягивайте через google repo и собирайте
Vsevolod
а при аггрессивном инлайнинге это вполне себе кейс
🦥Alex Fails
Vsevolod
ну и tlb не резиновый
Anatoly
Дмитрий ⬡
но поскольку надо использовать gcc8 а не 5, то это проблема надуманная
Хотели сказать 4? :)
Constantine
Constantine
Точнее так: человечество не умеет решать эту задачу
Constantine
Еще точнее так: википедия уверена, что эта задача до сих пор не решена
Constantine
Можно начинать гуглить с вот этого
https://ru.wikipedia.org/wiki/%D0%9D%D0%BE%D1%80%D0%BC%D0%B0%D0%BB%D1%8C%D0%BD%D0%BE%D0%B5_%D1%87%D0%B8%D1%81%D0%BB%D0%BE
kitsu
Как можно сесурно и портабельно обнулить данные по указателю? Есть memset_s, но мб в крестах тож есть что-то подобное
Matwey
std::memset ?
Egor
В C11, говорят, мог появиться memset_s
Anonymous
Как можно сесурно и портабельно обнулить данные по указателю? Есть memset_s, но мб в крестах тож есть что-то подобное
https://gist.github.com/foxcpp/0938ecddf71d6258dd985a882e89caef#file-secure_memory-cpp-L49
Что-то типо того?
kitsu
Vasily
Как можно сесурно и портабельно обнулить данные по указателю? Есть memset_s, но мб в крестах тож есть что-то подобное
https://wiki.sei.cmu.edu/confluence/display/c/MSC06-C.+Beware+of+compiler+optimizations
https://stackoverflow.com/questions/13299420/mac-os-x-equivalent-of-securezeromemory-rtlsecurezeromemory/13299459#13299459
kitsu
Vsevolod
недостаточно, но с современными компиляторами работает
Vasily
А почему недостаточно?
Vladislav
а, все таки volatile + явного цикла достаточно
volatile испортит все оптимизации, касающиеся этого указателя
Vsevolod
по стандарту, volatile pointer не значит убирать оптимизации над памятью, на которую этот pointer указывает
Vsevolod
side effect относится к поинтеру, а не к памяти
Vladislav
тоже верно
Vsevolod
http://www.daemonology.net/blog/2014-09-04-how-to-zero-a-buffer.html
Vsevolod
The C standard states that accesses to volatile objects are part of the unalterable observable behaviour — but it says nothing about accesses via lvalue expressions with volatile types.
Vsevolod
возможно, в c++ этот странный момент описан иначе
Дмитрий ⬡
Можно посмотреть, как OpenSSL справляются)
Дмитрий ⬡
А, там тоже Си, соря.
Egor
side effect относится к поинтеру, а не к памяти
В смысле «если я записываю по volatile указателю и больше ничего с ним не делаю, то компилятор имеет право это убрать»?
Anonymous
В смысле «если я записываю по volatile указателю и больше ничего с ним не делаю, то компилятор имеет право это убрать»?
Имеет, но на практике никто так не делает, ибо все понимают, зачем люди обычно записывают через volatile-указатель.
Aidar
Дмитрий ⬡
Указателю на волатильные данные же!
Egor
А, да
Дмитрий ⬡
А ещё лучше волатильные данные по волатильному указателю
Дмитрий ⬡
А ещё лучше почитать как твой компилятор это решает
Дмитрий ⬡
зачем
Как-то играл с segfault-ами, чтобы его получить разименовывание указателя на волатильные данные не работало, а вот волатильного указателя работало)
Aidar
потомучто это уб
Aidar
скорее всего он предподсчитал заранее какието смещения
Anton
Vladislav
секурно
Anton
Ну, если используется указатель, то о какой секьюрности может вообще идти речь)