@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

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

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

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

ERROR: S client not available

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

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

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 функциям

может помочь

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

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

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

ok. Спасибо, попробую

https://twitter.com/GabrielG439/status/945687191212081152

https://twitter.com/GabrielG439/status/952635551940624384

ну тогда ладно

для парсека введение лучше чем http://jakewheat.github.io/intro_to_parsing/ существует ?

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

там же вроде из типов всё очевидно

кроме отката

отката?

try (foobar)

я раз в сколько месяцев пишу что питон плохо?

Прошлый раз был неделю назад примерно

я понимаю что это неуместный канал, но как в питоне принято делать dependency injection/global state?

О, и тут антипитоновский холивар! Круто!

Хотя не. Месяц как раз прошел

Правда, мне нравится питон.

но это же больше недели

Но холивары я люблю ещё больше!