Category: образование

Category was added automatically. Read all entries about "образование".

Book

WSL пошла по пизде

https://devblogs.microsoft.com/commandline/shipping-a-linux-kernel-with-windows/

TLDR: собираются пускать Linux-ядро в WSL

На кворе как обычно набежала толпа долбоёбов.

А я не могу развидеть статью про булшиттинг. Как теперь жить? Там на кворе же все ответы в духе "тон его взят был слишком высоко и не позволял ему горячиться, из одного уж презрения к факту. Основания, на которых стоял он, были самые первоначальные, приличные разве лишь тринадцатилетнему школьнику".
Book

Погнила системка

Есть у меня компонентик, работающий на линуксе. Девелопю там же, в (н)виме. Решил сегодня обновить плагинчики (deoplete и LanguageClient-neovim) - погнили оба. То есть оба плагина, поставленных "по-говняному" через vim-plug, потребовали для обновления пойти на хоумпейж и посмотреть обновлённые инструкции по установке. Чего бы не произошло, если бы они ставились через системный пекедж-менеджер и мейнтейнились специально обученным человеком, и-или если бы vim-plug был менее говняным менеджером.

Пидарасы!

Далее, при попытке обновить сам nvim, произошло туча странного. Он отказывался запускаться, ссылаясь на отсутствие libunibilium.so.0. Пришлось "выйти и зайти": снести нахрен nvim со всеми зависимостями (включая оный unibilium) и переставить nvim из репозитория. После чего nvim-git внезапно собрался!

Пидарасы!

Далее, есть у меня говноскриптик парсящий вывод strace и составляющий по нему список файликов, к которым был доступ. Раньше надо было трейсить только сисколлы execve и open (трассируемый код других, типа chdir, не делает). И оказалось, что теперь вместо open у нас "openat(AT_FDCWD,".

Пидарасы!
Book

Унивалентность на кубических типах

https://github.com/mortberg/cubicaltt/tree/master/lectures (там же чекер на х-е) позволяет понять, как примерно будет выглядеть обещанное Воеводским счастье ("his vision of a foundational system for mathematics in which the basic objects are homotopy types, based on a type theory satisfying the univalence axiom, and formalized in a computer proof assistant")

Идея заключается в том, чтобы усилить identity type так, чтобы больше вещей можно было доказать "в одно действие" через аналог идрисовского replace (названный в лекциях subst):

replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y

Для этого из гомосексуальных гомологических примитивов собирается тип Path X a b, играющий роль {X} -> (a: X) = (b: X), который можно населить:

- "рефлом", т.е. definitionally equal terms

refl (A : U) (a : A) : Path A a a

- экстенсионально равными функциями (версия для dependent product тоже есть)

funExtNonDep (A B: U) (f g : A -> B) (p : (x : A) -> Path B (f x) (g x)) : Path (A -> B) f g

- изоморфными типами (т.е. если у нас есть функция между значениями типов A и B с левой и правой обратной - то типы "равны"):

isoPath (A B : U) (f : A -> B) (g : B -> A)
      (s : (y : B) -> Path B (f (g y)) y)
      (t : (x : A) -> Path A (g (f x)) x) : Path U A B
Интересно, что всё это работает и с функциями уровня типов.

В результате можно написать такую функцию:
functor_transport (F G: U -> U) (p: Path (U -> U) F G) (f: functor F): functor G
  = subst (U -> U) functor F G p f
То есть, для изоморфных типов F и G (с кайндами * -> * в терминах х-я) по инстансу функтора для F можно родить инстанс для G, при этом тело и сигнатуры fmap и теоремы о соблюдении законов функтора переписываются "автомагически".

Ну а дальше оказывается, что изоморфизмы у нас повсеместно. Скажем, таплы у самоизоморфны - т.е. есть Path U (A, B) (B, A), ну и из (first, fst, functorForA) "в одно действие" получаются (second, snd, functorForB). А дальше из (first, fst, functorForA, second, snd, functorForB) "в одно действие" получается реализация 6 функций и док-во 4 теорем (1 ф-ция и 2 теоремы внутри functorA/B сидят) для пар в кодировках чёрча и остальных over 9000 возможных представлений пар.

Ну, на самом деле требуется доказать в каждом случае соответствующий Path, но это проще чем передоказывать теоремы.

Кроме того, есть техника метапрограммирования: есть изоморфизм bool самого с собой (через not). И мы можем написать функцию, автомагически заменяющую все булы в любом терме вида F bool на их отрицания (и функции что самое смешное тоже переписываются). Типа

data food = cheese | beef | chicken

-- Predicate encoding which food someone eats
eats (X : U) : U = list (and food X)

anders : eats bool = cons (cheese,true)
                    (cons (beef,false)
                    (cons (chicken,false) nil))

-- Cyril eats the complement of Anders
cyril : eats bool = substEquiv eats bool bool notEquiv anders
notEquiv тут как раз доказательство изоморфизма. Ну и понятно что заменяются не все вхождения Bool, а "все вхождения в позициях, отмеченных Х". Любопытно, что код ничего не знает о том как обходить списки - у нас нету fmap для eats :)

Дебильные комментарии, комментарии "практиков" и школьников - как обычно, скринятся. RTFM, do you homework, пиши развёрнуто и конструктивно! https://t.me/groupoid (но там банхаммер, так что лучше сюда)
Book

Отказ от просвещения

Да там море трудностей. См. лекцию Фейнмана https://www.youtube.com/watch?v=IPogLMRBZ4o

И если "область известного" у оппонента по теме вопроса маленькая - то чтобы ответить, приходится слишком много всего объяснять. И это затратно для меня как условного Фейнмана.

Ну и вопросы "что можно почитать по теме" аналогичны магнитам. Если вы вообще ничего не знаете - то вам надо пойти в школу в первый класс и постепенно-постепенно пройти все слои. А если вы не хотите (оппоненты как правило не хотят) - то на придумывание удовлетоворительного ответа, не содержащего обмана, типа "это одна из фундаментальных сил", всё равно уходит достаточно много времени.

В результате образуется (неприятный мне) коммуникационный вакуум, когда по теме поста никто не может сказать ничего вменяемого, хотя там часто и не космос никакой.

Решений тут два:
- выходить на другую площадку (и по-английски)
- идти на космическую-работу-с-офисом джуниором

Второй вариант пока отменяется - буду ещё пару лет сидеть на острове, продуктизировать свой говнопродукт на С++, Перле, Ноде, Винде, ESXi, шапке и говнохостингах за $2.5 c OpenVZ.
Book

Когда ОО-дизайн выучил, а в школе уроки прогуливал

https://github.com/song940/node-dns/blob/master/lib/reader.js#L20-L41

Товарищу надо парсить битовые поля. Он для этого переводит байты в массив битов, делает им слайс, а потом обратно. Через Math.pow(). Более того, и байтовые поля он тоже извлекает таким образом.

К счастью для таких маленьких библиотек, поправить код как надо и добиться принятия PR в апстрим легче в долгосрочной перспективе, чем самому писать. Т.к. код потом будут мейнтейнить.
Book

Пидарасы столкнулись с пидарасами

Короче, в Арче запилили мега-GHC, который идет только с динамическими либами, без этого статик-говна для любителей говна. Понятно, что всё в результате похудело, и 32-битный GHC занимает 300 метров, а не 900.

Но поскольку пидарасы, пишущие ghc, так и не сделали у либ никакого ABI (их объяснения я знаю не надо в комментах пересказывать), при попытках пекеджить GHC-либы так же, как пекаджат сишные либы, наступают жопы самого разнообразного плана. Т.е. нельзя просто так взять и выпустить 6-мегабайтный cabal-install, который будет зависеть от libHSCabal.so, при апдейтах начнётся пизда и борода и хуй. Чтобы не началось, надо делать разные приседания. Школ приседания с версиями системных либ есть минимум две в Арче, ну и в каждом другом дистре линукса своя схема.

Ну и эти двое пидарасов не дружат с третьими пидарасами, которые делают стек. Поскольку уже для сборки Setup.hs нужен ключик -dynamic, а стек в это не умеет.

Вроде бы не умеет, поэтому зафайлил ишшуй в стек: https://github.com/commercialhaskell/stack/issues/3409

Если интересно посмотреть на арчевых пидарасов, можно почитать https://wiki.archlinux.org/index.php/Haskell Там из абзаца, начинающегося с "For these reasons, you have to make sure" написано, что не только stack нинужен™, но и cabal-install. Я хуею, дорогая редакция! Интересно кстати, что там на страничке наслоения старых школ приседаний. А у второй большой школы приседаний есть отдельная страничка https://wiki.archlinux.org/index.php/ArchHaskell У них даже свой несовместимый GHC был. Но уже нету поскольку i686 is deprecated.

Upd: стек-пидарасы сказали что вы должны терпеть боль и билдить статически no matter what. Хорошее замечание.
Book

Декларативная геометрия

люди, я тут решил стать алгебраическим композабельным геометром, отцом бескоординатных 2д-фронтэндов для векторного WebGL фидонета.

не подскажете какие-нибудь пейперы или книжки для школьников по мат. основам diagrams c hackage? У них референсов я не нашёл, но должно же быть

ну и вообще по теме отвязывания графики от координат и перехода к высокоуровневым представлениям, не обязательно в разрезе diagrams

Нашел тут пейпер.

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.220.4802

В-общем, от линейных пространств переходим к аффинным, а от них к геометрической алгебре (не путать с алгебраической геометрией).
Book

Схемы образования телефонных номеров

Захотелось мне зайти на Одноклассники, и Большой Брат предложил ввести доминиканский номер телефона, "чтобы вы не потеряли доступ к вашему профилю".

Но интересно, что он предложил дебильную схему именования: +18 и 9 цифр.

https://www.countrycode.org/dominicanrepublic предлагает такую схему: 3 кода страны +1-809, 1-829, 1-849 и 7 цифр. При этом "The Dominican Republic does not use city codes."

Терминалы пополнения счёта предлагают ввести (...) ...-.... - 3 цифры "кода" (809 или остальные два) и 7 цифр. Такой же формат при местных звонках.

Украине тоже "не повезло" с кодом:

на мобильном из другой страны надо набирать +380 44 1234567
при звонках внутри города 123 4567
а при звонках из другого города 8 044 1234567

В результате на визитках чего только не писали, и +38 (044) 1234567, и +3 8 (044) 1234567.

В "новой" схеме, введённой несколько лет назад, от восьмёрки отказались, но "ноль" оставили. Так что теперь +380441234567, 1234567 и 0441234567. На визитках-вывесках-объявлениях по-прежнему допускается писать фигню. Мне кажется, 0 (44) 123-4567 никто не пишет. Или пишут?
Book

Duolingo Spanish

Галопом по европам прошёл весь испанский от дуолинго. Старт, как я раньше писал, очень хороший, а дальше - как везде.

Обучение языку можно поделить на три части: лексика (значения слов), грамматика (составление предложений) и прагматика (использование предложений в контексте других предложений и обстановки риал ворлда).

По прагматике там ноль - по сути перевод отдельных предложений. Нет заданий с текстами и диалогами.

По грамматике 3 из 5. Есть упражнения на определённые грамматические конструкции, но правила употребления конструкций не объясняются (по-крайней мере в телефонном аппе). Предлагается перевести на испанский не английские фразы (так по-английски не говорят). Требуют в английском переводе артикли там, где они есть в испанском, кроме случаев, когда в английском получается совсем уж дебильно.

По лексике 4 из 5 - сначала идут практически только нужные базовые слова. А затем начинается перекос - в курсе нету шкафа, пакета, розетки и вилки, зато есть, блядь, демократия и судебный процесс.

Ещё читить можно - вопросы из нескольких вариантов настолько разные, что всегда можно по смыслу догадаться. Или, например, один из вариантов начинается с маленькой буквы.
Book

Тормоза в каждый дом

В рамках программы по изучению мира говнолинукса я сижу в ArchBang - школьной поделке на основе Arch Linux с GUI на основе OpenBox из коробки.

Эта искоробочность, как я недавно выяснил, заключается в адхок-насирании в систему без использования системы пакетов. Насранные скрипты естественно не обновляются и со временем неизбежно деградируют.

Одним из кусков такого говна является скрипт /usr/bin/archbey2, незатейливо вставленный в bashrc установщиком системы.

Мне было наплевать на него, но несколько смущал долгий старт терминала, особенно в первый раз после загрузки системы.

Всё было бы хорошо, но недавно я обнаружил, что при загрузке и каждом запуске терминала сыпятся какие-то ошибки, связанные с подписями к ключам, которыми подписаны пакеты в репозитории. Помимо этого почему-то мне приходилось постоянно выкачивать и переподписывать ключи, которыми подписаны пакеты в подключенных мной нестандартных репозах.

Встал вопрос: а какого хуя что-то связанное с ключами (которые можно переписать только под рутом) происходит при запуске нерутового терминала.

Полез, и обнаружил фейспалм. Этот archbey2 печатает в псевдографике логотип Арчбенга и рядом с ним всякую инфу о системе вроде свободных памяти и месте на диске.

Исследование выявило, что исторически был питоновский скрипт, который с целью облегчения (чтобы можно было не ставить питон в систему) переписали на Баше. Скрипт отрабатывает 190 ms, из которых

Cобственно печать - 7 ms
Всего/свободно на диске - 7 ms
Тип шелла - 4 ms
Использованно памяти - 5 ms
Всего памяти - 5 ms
Название процессора - 3 ms
Кол-во установленных пекеджей - 130 ms

Facepalm. Наименее ненужная инфа жрет больше всего времени. И это в закешированном варианте, т.е. по старту системы медленнее.

Убрал из bashrc.