Как собрать для блога HTML с подсветкой кода из Markdown

TL;DR: Как запостить Markdown пост с примерами кода (и картинками) в бложик, поддерживающий только HTML

# install using pip
pip install -U markdown Pygments
# or (on Debian based)
sudo apt install python3-markdown python3-pygments

edit post.md
(echo '<style>';
    pygmentize -S native -f html -a .codehilite;
    echo '</style>';
    markdown_py post.md -x codehilite -x fenced_code
) > post.html

Вчера написал пост с заметками по ходу решения задач к Coq'Art. Начал я его писать как короткий комментарий в локальный tg чат с друзьями. Но сначала понял, что хочется поделиться на большую аудиторию (может кто прокомментирует чего полезного), поэтому решил запостить в point.im или juick.com в которые изредка что-то пишу, а потом, пока писал, обнаружил, что размер поста уже больше подходит для полноценного поста в бложек. На этом месте я вспомнил что у меня даже был такой).

Размечал текст я по привычке в Markdown - это очень простой, привычный мне формат, и он легко переделывается в другие вики разметки, поэтому я в нём часто пишу даже заметки рядом с кодом и пр. Ну и про поддержку в GitHub не забываем. Когда же я открыл blogspot, то обнаружил, что там только два варианта ввода разметки: HTML и их редактор. Поэтому пришлось вспоминать, как собирать из Markdown файлов HTML.

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

Простого вызова markdown_py post.md -f post.html уже бы хватило, если бы в посте не было вставок с кодом. Но т.к. они были, то сначала обнаружилось, что блоки в бэктиках

```

```

это нестандартная фича, и весь код у меня слился с текстом.

Этот и следующий скриншоты - из Firefox'а в reader view, чтобы лишний раз в blogspot не лезть, но и чтобы от белого фона глаза не вытекали.

Картинки, к слову, в Markdown тоже можно вставлять, но надо сначала их куда-то захостить. Пока ручками сложил в Dropbox и воспользовался рецептом (поменять в публичной ссылке ?dl=0 на ?raw=1), чтобы получить прямую ссылку на картинку. Надо попробовать перехостить всё это дело на GitHub Pages - там такой проблемы быть не должно, да и с форматированием меньше возни. Или как-нибудь автоматизировать заливку картинок.

Чтобы поправить отображение блоков с кодом, надо подключить (идущее в комплекте) расширение Fenced Code Blocks.

И, конечно, сходу нет никакой подсветки для блоков с кодом, поэтому надо ещё подключить расширение CodeHilite, которое тоже идёт в коробке, но зависит от библиотеки Pygments, которую надо ставить отдельно.

Т.о. получилась такая команда:

markdown_py post.md -x codehilite -x fenced_code -f post.html

Выглядит уже прилично, но код всё ещё не раскрашен. Это потому, что надо сгенерировать стили для Pygmets. Об этом написано в инструкции к CodeHilite:

pygmentize -S default -f html -a .codehilite > styles.css

Ну и вставил это дело в результирующий html максимально тупым способом:

(echo '<style>'; cat styles.css; echo '</style>';
    markdown_py post.md -x codehilite -x fenced_code) > post.html

Уже совсем хорошо. Но когда запостил в blogspot, то понял, что фон явно указан белый.

Это уже скрин с blogspot, чтобы была понятна проблема.

Поглядел другие темы и выбрал native. Окончательное решение одной командой приведено в начале статьи.

Выглядит так:

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

img {
  border: 1px solid darkgrey;
  width: 400px;
}

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

В целом, для первого подхода, этого должно бы уже хватить. Но я подумал, что стоит записать команды на память, чтобы для последующих постов, если такие будут, не вспомнить или не выискивать их в истории команд. А лучшая заметка - это исполняемый код! Соответственно рассмотрел два варианта: написать скрипт или пихнуть нужные команды в Makefile. Т.к. если постов будет несколько, то прописывать каждый раз при генерации пути ко входу и выходу лень, и к тому же тут уже несколько ресурсов, то решил остановиться на втором варианте.

Сразу обнаружил, что мейком то я пользоваться, оказывается толком не умею. И пришлось долго читать ман и интернеты прежде чем у меня получилось его заставить выполнять одну и ту же команду на каждой паре *.md -> *.html, но в итоге я написал вот такой Makefile:

# задаём цель по умолчанию
default: all
# следующие цели - это не файлы
.PHONY: all clean list-md-files list-html-files

# получаем список Markdown файлов с помощью функции wildcard
# см. https://www.gnu.org/software/make/manual/html_node/File-Name-Functions.html
# '::=' - это полустандартное присваивание нерекурсивной переменной
# см. https://www.gnu.org/software/make/manual/html_node/Flavors.html
MD_FILES ::= $(wildcard *.md)

# Строим по списку md файлов список html файлов.
# Будем складывать их в ./out
# patsubst делает замену по шаблону
# см. https://www.gnu.org/software/make/manual/html_node/Text-Functions.html
HTML_FILES ::= $(patsubst %.md,out/%.html,$(MD_FILES))

# команды для диагностики
list-md-files:
    @echo $(MD_FILES)

list-html-files:
    @echo $(HTML_FILES)

# т.к. clean удаляет папку ./out полностью, то надо её пересоздавать 
out:
    mkdir -p out

# стили для раскраски 
out/pygments.css: out
    pygmentize -S native -f html -a .codehilite > out/pygments.css

# Самая магия. Не разобрался, как использовать тут MD_FILES и HTML_FILES,
# чтобы для каждой пары md и html генерилось отдельное правило,
# поэтому воспользовался шаблонами с %:
# https://www.gnu.org/software/make/manual/html_node/Pattern-Intro.html
# '$<' и '$@' - это "автоматические переменные"
# https://www.gnu.org/software/make/manual/html_node/Automatic-Variables.html
out/%.html: %.md out styles.css out/pygments.css
    ( echo '<style>'; cat styles.css out/pygments.css; echo '</style>'; \
        markdown_py $< -x codehilite -x fenced_code ) > $@

# в текущей версии MD_FILES и HTML_FILES нужны только для того,
# чтобы подвязать все цели по генерации html в all
all: $(HTML_FILES)

# чтобы точно не оставлять мусора (при удалении md файлов например)
# удаляем папку ./out целиком
clean:
    rm -rfv out

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

Coq'Art. Заметки на тему. Ex 6.47 Trees with fixed height

Читаю Coq'Art. Доказал только что очередной (достаточно очевидный) факт, и внезапно захотелось поделиться и успехом (это было не очень просто), и мыслями на тему. А за одно решил обновить бложек - кучу лет сюда не заходил, а тут такой лонгрид получился.

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

Inductive htree (X : Type) : nat -> Type
  := hleaf : X -> htree X 0
   | hnode : forall h : nat, X -> htree X h -> htree X h -> htree X (S h).

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

Fixpoint pn_tree_aux (h n : nat) {struct h} : htree nat h
  := match h with
     | O => hleaf n
     | S h' => hnode h' n (pn_tree_aux h' (2*n + 1))
                          (pn_tree_aux h' (2*n + 2))
     end.

Definition pn_tree (h : nat) : htree nat h := pn_tree_aux h 0.

А авторское - нумерация по обходу в глубину.

Fixpoint make_htree_aux (h: nat) (start : Z) : Z * htree Z h :=
match h with
  | 0 => ((1+ start)%Z, hleaf start)
  | S h' => let p := make_htree_aux h' (1+start)%Z 
            in let q := make_htree_aux h'  (fst p) 
               in (fst q, hnode start (snd p) (snd q))
end.

Definition make_htree (n:nat) : htree Z n := snd (make_htree_aux n 0%Z).

Я стараюсь про такие задания кроме самого решения ещё доказывать, что оно возвращает то, что нужно. В данном случае я решил доказать сначала, что все значения в получившихся деревьях попарно различны, а потом более сильное, что если разложить эти деревья одним из обходов в список, то получится интервал натуральных чисел от 0 до (2^(h+1) - 2). Факты, казалось бы, тривиальные, а попробуй докажи. Особенно много сложностей возникло с моим решением.

Первая часть ещё куда ни шло, но в моём варианте много проблем доставили операции со степенями и вычитанием, т.к. автоматические тактики вроде lia/nia, позволяющие не преобразовывать простенькую арифметику руками с помощью примитивных теорем, не справляются с выражениями, в которых результат как-то зависит от этих самых степеней или вычитания. Например для подобных неравенств мне пришлось отдельную теорему завести и доказать её по индукции:

2 <= 2 ^ h * (2 * n + 1 + 2)

А вот такое требует минут 5-10 размышлений и пяти довольно длинных строчек на доказательство:

S (2^(S h) - 1 + (2^(S h) - 1)) = 2 * (2^h + (2^h + 0)) - 1

Подбешивает, кстати, что тактика simpl разворачивает умножение на константу слева. Т.е. если написано 2*n, то после simpl будет n + (n + 0). Не знаю, как это запретить. Поэтому сделал теорему, которая переписывает выражение обратно. Но её приходится регулярно вызывать, чтобы можно было прочитать, что там теперь в goal.

А с доказательством, что уплощение построенного дерева образует интервал натуральных чисел проблемы начались уже с того, что для htree (дерева фиксированной высоты) нельзя просто так взять и написать обход в ширину, как для обычного. Пример для обычного дерева с Rosetta Code:

Fixpoint levelorder_forest (fuel: nat) (f: list tree) : list nat :=
  match fuel with
  | O => nil
  | S fuel'
    => let g := (fun t r => let '(x, f) := r 
                        in (value t :: x, children t ++ f))
      in let '(p, f) := fold_right g (nil, nil) f
      in p ++ levelorder_forest fuel' f
  end.

Definition levelorder (t: tree) : list nat
  := levelorder_forest (height t) (t :: nil).

Моя попытка повторить (все использованные тут определения можно найти тут же):

Definition flat_htree_bfs_aux1 {X : Type} (h : nat)
           (t : htree X (S h)) (acc : list (htree X h))
  := (htree_t1 t) :: (htree_t2 t) :: acc.

Fixpoint flat_htree_bfs_aux {X : Type} {h : nat}
         (q : list (htree X h)) {struct h}
  : list X
  := match h with
     | O => map htree_x q
     | S h' => let q' := fold_right (flat_htree_bfs_aux1 h')
                                    [] q in  (* <--- error *)
              let cur_layer := map htree_x q in
              let next_layers := (flat_htree_bfs_aux q') in
              cur_layer ++ next_layers
     end.

Definition flat_htree_bfs {X : Type} {h : nat} (t : htree X h) : list X
  := @flat_htree_bfs_aux X h [t].

Выдаёт ошибку "The term "q" has type "list (htree X h)" while it is expected to have type "list (htree X (S h'))" (cannot unify "h" and "S h'").". Т.е. coq не понимает, что S h' = h, хотя казалось бы должен - мы же тут как раз деструктурируем h на S h'.

Как оказалось это известная проблема, которая даже описана в книгах, а у воркэраунда даже есть собственное название "convoy pattern". Этот паттерн предполагает замену типа всего match-выражения на эквивалентное, но возвращающее функцию, которая в свою очередь принимает как аргумент проблемное значение (в моём случае q), и возвращает то что нужно. Т.е. нужно переписать так:

Fixpoint flat_htree_bfs_aux {X : Type} {h : nat}
         (q : list (htree X h)) {struct h}
  : list X
  := match h return list (htree X h) -> list X with
     | O => fun Q => map htree_x Q
     | S h' => fun Q => let q' := fold_right (flat_htree_bfs_aux1 h') [] Q
                    in let cur_layer := map htree_x Q
                    in let next_layers := (flat_htree_bfs_aux q')
                    in cur_layer ++ next_layers
     end q.

Почему без этого не работает, а с этим работает, я пока не очень понял, но надеюсь ещё пойму.

А дальше, конечно же возникла целая пачка сложностей в работе со столь громоздким определением обхода (и снова со степенями и минусами). Особенно всё усложняло то, что simpl часто разворачивал цели в слишком большую портянку, а попытка запретить ему некоторые преобразования, связанные с паттернматчингом по (S h') (высота дерева + 1. естественным образом постоянно возникает при доказательствах по индукции) выносом его в контекст (remember (S h') as h eqn:eq_h) часто приводили к ошибкам из-за того, что где-то в этом же выражении есть дерево высоты h, и получается выражение вроде такого (упрощённо) htree X h1 = htree X (S h), которое coq опять не может типизировать.

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

Поэтому в который раз, убедился, что из-за обилия в формальном доказательстве технических деталей тенденции к росту длин имён сущностей и тупо объёма кода, по которому не всегда просто навигироваться, любой нетривиальный факт надо сначала доказать более неформально на листочке, а уже потом переписывать формально. На фотке мои заметки к доказательству, что мой вариант разворачивается BFS'ом в интервал. Без плана в виде этих закорючек за деревьями леса уже было совсем не видно и я напрочь перестал понимать, что доказываю в данный момент, и что с этим надо делать.