EG
Оказывается, постоянные айсы были вызваны тем, что я сделал
auto trait Sized вместо trait SizedSize: a a a
2020 October 17
SP
айс айс бейби
EG
Плейграунд только у меня лежит?
H
у меня тже лежит
С
Юзай второй - который integer32
b
кто шарит coq нормально?
b
я тут переписываюсь с профессором из сиднейского, который занимается tree calculus и предлагает делать вычисления натуральными деревьями, а не числами. тут у него доказательства на coq https://github.com/Barry-Jay/Tree-calculus кто–нибудь может глянуть и объяснить мне насколько далеко он продвинулся реально в формализации этой алгебры?
b
кстати насчет логоса у меня не было возможности отписать выше
KR
мб там поспрашивать? там шарящие в этом плане
b
секретным соусом для логоса является duct/deduct противостояние (в reinforcement learning среде)
b
потому что один является энкодером, а второй — декодером
b
почему это важно? да потому что мы можем улучшать языковую модель одновременно обрабатывая как диалекты, так и всякие истории (использования диалекта)
b
у меня пока нет алгебры чтобы можно было удобно компоновать вычисления в логике первого порядка, которые потом в futhark можно прямо через cuda направить по шине на карточку.
b
nvidia rtx3090 имеет пропускную способность 150 Gbit. то есть я могу брать огромные разреженные графы и направлять их на карту без каких–либо вспомогательных представлений
b
V=10^9 E=10^12
вообще без проблем на каждое вычисление прогонять весь граф целиком и даже не заморачиваться с сжатыми представлениями
вообще без проблем на каждое вычисление прогонять весь граф целиком и даже не заморачиваться с сжатыми представлениями
ШН
Посоны, всем привет. Кто писал кросс-платформ configure.ac скрипты?
ШН
Падает билд, если я добавляю проверку на
aarch64