其实在挺久以前有试过啃 coq 来着，虽然后来就放弃了（大概停留在 Logic 和 Tactics 两章之间）。 这次重新开坑倒是还算顺利，可能因为这之后在fp方面有了一些积累，对于命题的归纳证明也有了更直观的认知。借着万圣节放假的时候半个星期左右啃到了 Logic 一章。 当然这里面也有一部分原因是因为有参考到之前的题解，well，not really，一方面因为有许多题目自己直接 intros

之前在学Haskell的时候碰到过一段这样的实现： 1fibs = 0 : 1 : zipWith (+) fibs (tail fibs) 感觉很优雅，主要是因为用到无限序列自己来定义自己，然后就等于把 fib 的定义直译一遍，就得到了对应的函数了（ 然后就一直念念不忘是不是可以在命令式里面搞这个。 现在既然有了 Lazy 和 Stream 这两个工具（这里的 Stream 只是一个可以无穷延伸

于是上次提到的那个客户端的进展……大概是完工了（。这里记录一下第二阶段踩的一些坑，一些关于BitTorrent协议的有趣的地方，也有一些我自己觉得值得记录下来的一些实现细节吧。 续篇 首先提一下在解析PeerResponse的时候，遇到了值的类型为List<Result<*>>但是需要获取Result<List<*>>的情况。这个是很经典的Resul

前段时间没事做，然后朋友安利了一下手写torrent的项目。喵了一眼各种新手向的实现，有C++的也有go的，但是没有kotlin的，就想手写一个了。然后发现简直就是超级大坑，从一个坑跳到另一个坑…… 从零开始用Kotlin写一个超简陋的BitTorrent客户端 不管怎样，目前的状态是可以（仅可以）从一个叫academictorrents的网站的单文件种子里面提取出链接，然后去获取Peers的程度

其实 hexo 本身倒是没有什么坑？不过这次按照朋友的推荐上了 GitHub 的 CI，因为自己粗心大意所以还是有点磕磕碰碰。就把中间遇到的一些问题和解决方案写一下吧。 首先需要准备一对密钥，私钥存在仓库的设置里面的 Secret > Actions Secrets 里，我这里叫做 HEXO_DEPLOY_PRIVATE。 然后在 CI 脚本里面对应部署 Hexo 的地方，加一行 12en

似乎以前也有过一个blog的样子呢，不过已经不记得是什么样的了。 好不容易下决心再开一个blog，希望可以一直写下去吧。