можно просто работы почитать

это же HIW там нечего читать, разве только слайды

ну руками придется писать хранение зиллионов хешей, чтение, поиск, дерево здоровенное в памяти держать

Можно зиллион кешей в redis'е хранить

@int_index по software foundations есть learning group тут в телеграмме если что

ты кстати сделал там последнюю в induction (на 5 баллов) весьма прикольная задачка оказалась

?

вот вас вставило

я SF раза два откатал в прошлом и позапрошлом году чтоли

Это очень прикольно вставлять English words в русскую speach

вначале хорошо идет, а потом топливо начинает заканчиваться

s/speach/speech/

пишите хоть свой сарказм без ошибок

чего только не придумают, лишь бы хештаблицы и сортировки не писать

А по агде порекомендуйте материал? Лучше с задачками.

A64m в LF сортировки есть

Порт SF :trollface:

речь про те, которые работают быстро

высший пилотаж это доказать что они работают быстро

это бы неплохо было, конечно

s/speach/speech/

У меня Т9 баганый

бледная баганка

откатал в смысле два раза прочитал или два раза бросал?

его не читают, там упражнения делают

да, я в курсе. Окей, перефразирую вопрос, если это важно

я SF раза два откатал в прошлом и позапрошлом году чтоли

откатал в смысле два раза прорешал упражнения или два раза бросал?

два раза прорешал, не знаю как можно понять иначе

незнакомое слово можно понять как угодно, особенно после слов "потом топливо кончается" значение "бросал" кажется вероятнее

прикольно, что эта задачка в induction не видна в книге на сайте

да, там в коде есть разделитель (* ** *)

после него ничего не видно на сайте

прикольно, что эта задачка в induction не видна в книге на сайте

Зачем сайт? Там literate файлы же фактически.

да

но просто

Vs code норм с coq? Ну или чем там ещё пользуются

ed

да, vscoq классный плагин

ed

Такие рофлы

emacs норм

spacemacs, даже для вимера

emacs норм

Ну обычно опыт такой что даёт не больше обычного редактора + необычный опыт установки и настройки + необычный опыт пользования Так и не дошёл до этапа где балдею от подсветки в репле (Не исключаю что я тупой, тем более что пишу с такими повторами)

spacemacs ставится как установка emacs пакетным менеджером и запуск скприпта с гитхаба

company-coq layer добавляется через 2 консольные команды

больше в этот раз в конфиги я не лазал

скрипты с гитхаба, императивные конфиги...

да, с установкой спейсмакса у меня проблем не было, но он неудобным мне показался, тот же поисковый интерфейс, который теперь стандартный вор всех этих саблаймах-атома-вскодах там хуже работает, репл тормозит хуже яваскриптовых терминалов и т.д.

company-coq кстати не обязательно, но он прикольный(за исключением того что он мне емакс сегфолтил(уже запатчено))

(лиспокомменты)

мне нравится все эти доказательства искать и туда-сюда по ним бегать

вообще интерактивность в доказательствах это круто

не то что эти ваши идрисы

ну а то

Всем привет, а может кото обеснить что надо использовать в нових версиях persistent-mongoDB вместо MongoBackend можит есть где то новый пример?

company-coq кстати не обязательно, но он прикольный(за исключением того что он мне емакс сегфолтил(уже запатчено))

А у меня до сих пор падает. https://github.com/cpitclaudel/company-coq/issues/159 (везде одни и те же лица ;))

А у меня до сих пор падает. https://github.com/cpitclaudel/company-coq/issues/159 (везде одни и те же лица ;))

какая версия emacs?

25.3 (macOS)

а у меня ещё не падал ни разу

иногда интерпретатор зависает к чертям правда

то что починили падало из-за line numbers в evil

может там несколько проблем

Это потому что у меня вот эта штука включена (https://github.com/cpitclaudel/company-coq#for-all-coq-files)

дебажили на deepspec с джоном уигли

Proof. рендерится как ∵

ага

без этой штуки работает у меня, с ней сегфолт

это второй сегфолт в company-coq

из тех что я видел

в общем я отключил в итоге и забыл

я в сентябре с Клементом дебажил, нашел функцию после которой падает, но пока все стоит

я в сентябре с Клементом дебажил, нашел функцию после которой падает, но пока все стоит

я думаю надо до мейнтейнеров емакса донести, чтобы дело пошло

Eli очень быстро среагировал в тот раз, но я тупо эту фичу отключил и не стал дальше разбираться

Всем привет, а может кото обеснить что надо использовать в нових версиях persistent-mongoDB вместо MongoBackend можит есть где то новый пример?

Привет Андрий, Пробовал persistent-mongoDB-2.6.0 ?

ево и использую.

там просто уже нет MongoBackend

наверное нада использовать MongoContext так у меня роботает, но я не знаю что дальше делать с монадой как ее преоброзовать.

код - https://gist.github.com/anasinnyk/631d55800bc31b44d2983d34660d5161 ошибка - https://gist.github.com/anasinnyk/e1dbae05d947274e3381ec8e9aaaed07

я спрашивал в Haskell Learn но мене посоветовали обротится сюда.. я думаю ето немного не по адресу. но всьо же.

тип пропиши всем top-level функциям

может помочь

он из использования не может тип вывести

а если и может, то поможет выявить проблему все равно

явный тип для всех топ-левел объявлений это всегда хорошая идея