B
Для раста вроде больше не пытается сгенерить cmake
хотябы makefile
или возможность вручную указать где сорц файлы и где хедеры
или возможность вручную указать где сорц файлы и где хедеры
Size: a a a
2020 April 14
ML
ну для раста да, а вот дургие форматы проектов С/С++ нивкакую
Ну... страдать)
B
я как-то не сдуржился с CMake
кстати, СМаке умеет подключать СРР файлы все с папки, или надо реально по одному подключать, как в примерах, что я находил?
кстати, СМаке умеет подключать СРР файлы все с папки, или надо реально по одному подключать, как в примерах, что я находил?
ML
Чем тебе cmake не нравится бтв?
Это хоть какое-то стандартное автоматизированное решение для конфигурации билдов
Это хоть какое-то стандартное автоматизированное решение для конфигурации билдов
RP
я как-то не сдуржился с CMake
кстати, СМаке умеет подключать СРР файлы все с папки, или надо реально по одному подключать, как в примерах, что я находил?
кстати, СМаке умеет подключать СРР файлы все с папки, или надо реально по одному подключать, как в примерах, что я находил?
FILE(GLOB
B
Чем тебе cmake не нравится бтв?
Это хоть какое-то стандартное автоматизированное решение для конфигурации билдов
Это хоть какое-то стандартное автоматизированное решение для конфигурации билдов
да я его не осилил
Мне надо было скомпилить несколько СРР файлов и в итоге я пару часов ебался с симейком
Мне надо было скомпилить несколько СРР файлов и в итоге я пару часов ебался с симейком
P
ну вот и я запутался. вроде есть безопасный раст, а его безопасность заключается только в соблюдении правил, которые можно соблюдать в С++ при прямых руках
есть геометрия, где вся корректность теорем базируется на правдимости аксиом. как только аксиомы ломаются, ломается вся геометрия, но теоремы не ломаются, они просто рассчитаны на аксиомы, что более не выполняются. вот в расте аксиомы явно выделены в unsafe блоки. снаружи их -- только теоремы, которые базируются на аксиомах. в си и плюсах аксиомы можно ввести где угодно и ты не отличишь их от теорем, потому поверхность для анализа в случае проблем -- растёт.
B
а для чего-то по сложнее вообще не смог проект собрать
RP
есть геометрия, где вся корректность теорем базируется на правдимости аксиом. как только аксиомы ломаются, ломается вся геометрия, но теоремы не ломаются, они просто рассчитаны на аксиомы, что более не выполняются. вот в расте аксиомы явно выделены в unsafe блоки. снаружи их -- только теоремы, которые базируются на аксиомах. в си и плюсах аксиомы можно ввести где угодно и ты не отличишь их от теорем, потому поверхность для анализа в случае проблем -- растёт.
теперь осталось доказать, что твои слова про геометрию как-то соотносятся с растом
B
есть геометрия, где вся корректность теорем базируется на правдимости аксиом. как только аксиомы ломаются, ломается вся геометрия, но теоремы не ломаются, они просто рассчитаны на аксиомы, что более не выполняются. вот в расте аксиомы явно выделены в unsafe блоки. снаружи их -- только теоремы, которые базируются на аксиомах. в си и плюсах аксиомы можно ввести где угодно и ты не отличишь их от теорем, потому поверхность для анализа в случае проблем -- растёт.
аналогия хорошая, но наврно всеже раст не настолько мощный
ML
+1, отличная аналогия
P
теперь осталось доказать, что твои слова про геометрию как-то соотносятся с растом
что значит "мощный"?
ML
аналогия хорошая, но наврно всеже раст не настолько мощный
Ну вообще это не далеко от истины, см. Chalk
B
увсе-же это больше про ФП с формал пруфами)
P
увсе-же это больше про ФП с формал пруфами)
хз, при чём тут фп
RP
есть геометрия, где вся корректность теорем базируется на правдимости аксиом. как только аксиомы ломаются, ломается вся геометрия, но теоремы не ломаются, они просто рассчитаны на аксиомы, что более не выполняются. вот в расте аксиомы явно выделены в unsafe блоки. снаружи их -- только теоремы, которые базируются на аксиомах. в си и плюсах аксиомы можно ввести где угодно и ты не отличишь их от теорем, потому поверхность для анализа в случае проблем -- растёт.
Ральф для λRust доказал
> Theorem 7.1 (Fundamental theorem of logical relations).For any inference rule of the type system, when we replace all⊢by|=, the resulting Iris theorem holds.
теперь и тебе надо доказать, что правила геометрии распространяются на раст
> Theorem 7.1 (Fundamental theorem of logical relations).For any inference rule of the type system, when we replace all⊢by|=, the resulting Iris theorem holds.
теперь и тебе надо доказать, что правила геометрии распространяются на раст
B
хз, при чём тут фп
Есть всякие Coq и идрисы, в которых твой код реально теорема, которую компилер реально доказывает, что прога валидная)
ML
Есть всякие Coq и идрисы, в которых твой код реально теорема, которую компилер реально доказывает, что прога валидная)
Я же говорю, почитай про chalk
RP
"на ощущениях" раст действительно безопаснее, но ощущения к делу не припишешь
B
Я же говорю, почитай про chalk
У меня гугл нашел что-то не то, типо это какая-то ткань.
Но мне банально лень(
Но мне банально лень(