Extreme 难度的 Slice 过关了，终于可以自称类型体操入门了（喜）
Zero Calorie Drink Shop
This blog post was inspired by my classmate who encountered pip’s dependencies hell when configuring machine learning python code. Yeah, for my academics-immersed amateur of industy, environment configuration and package managers are very unfamiliar things. It’s not strange to crash into hell.
Sometimes it’s simply impossible to find a combination of package versions that do not conflict. Welcome to dependency hell.
一时兴起想写一个随机句子生成器。正巧在学上下文无关语言 (Context-Free Language, CFL)，意识到句子的结构很大程度上是一个上下文无关语法。查阅 X-bar 理论得到也确实类似如此。
同时正好在学 Rust，所以试了一下拿 Rust 编写这个生成器，并编译到 WebAssembly (WASM)。效果很成功！
花了几个小时写下了 So Simple.
这是一个致力于“尽可能少写 CSS”的主题。实际上也确实，整个主题几乎全部是裸的 HTML。排列从上到下，没有什么值得插入的元素，就像在读报纸一样。
这个主题是返璞归真的一次尝试。希望它能让我满意。
一篇简短的笔记，为 Misskey 开启 Meilisearch 后，重新索引过去的帖子。
我是去年的 11 月知道的 Firefish。它是我当时找到的最美丽的联邦宇宙软件，相比于死板的 Mastodon，过于倾向于日语又太娱乐的 Misskey，它同时兼具美观大方与功能丰富。管理员可以自由配置最大帖子长度，Nodejs的后端也让它比 Ruby on Rails 编写的 Mastodon 对性能要求更低。我欣然安装上了它，并把它作为自己的主要联邦宇宙软件。
可惜，当时我还不知道它的状态已经岌岌可危。就在当时，原有的主要贡献者大多已经离开，panos 和 namekuji 离开了这摊烂摊子开启了新项目 Catodon。数个月后，Firefish 的 maintainer Kainoa 就直接撒手不管，在没有事先告知的情况下将maintainer更改给 naskya。naskya 非常负责且具有热爱，在伊的代理下 Firefish 回光返照了一段时间 —— 我也是那个时候尝试了为 Firefish 进行贡献。
可惜 maintainer 的名头为伊带来了巨大的压力与恶心的网络骚扰者。 naskya 的身体和精神状态都无法负担这样的项目，不到一年之后，Firefish 再次被抛弃。这次，大约再也没人能救 Firefish 了。
我在 2018 年建立这个博客以后，就一直没有换过其它博客平台。试过 Wordpress，也试过 Writefreely，总还是没有 Hexo 之类的静态站点生成器来得又快又好。当然现在似乎更流行别的结构了，Hugo，vuepress，毕竟 Hexo 已经是个有十来岁的老家伙了。在前端，十年足以发生翻天覆地的变化，而 Hexo 已经被远远的甩在后头。
实际上，我对 Hexo 多少有一点恋旧情绪，毕竟它是我第一次尝试自建博客，也是我第一次尝试 Contribute 到开源项目。截至我写的时候，这个博客使用的主题 Anatolo 还是我 Star 数最高的个人项目。
但 Hexo 的确是老了。正如我的朋友所说，Hexo 的表演该落幕了，让它退场吧。 Hexo 大多数主题都是用的是裸的 <script> 标签引入前端库，少有主题加入代码压缩，几乎没有主题使用过 typescript。 文档也疏于维护， hexo-utils 更是代码奇奇怪怪 。
但我还是不忍心彻底放弃 Hexo。因此，我花了一个晚上的时间，对我博客的 Client 进行了重写。同时也是为了探索，像 Hexo 这样的老东西还可不可能与现代化的前端技术相集成。
说真的，Hexo 这么烂下去我真要换 Hugo 了——为什么它甚至不支持给 hljs 添加语言插件？
好吧，这篇博客讲述如何让你的 Hexo 博客支持高亮 Lean，并且是后端渲染。
Lean 4 是一个功能强大的交互式定理证明器和编程语言，结合了逻辑推理与编程，主要用于形式化验证、数学证明以及高可靠性软件开发。Lean 4 提供了一个灵活的类型系统和高性能的编译器，使其在理论研究和实际应用中都有出色表现。 —— GPT 说的。
F*ck 我为什么要去看这种东西啊（悲） —— 我说的