终于换上 https 啦,新增 LAgda 子博客

by

前天有不少人向我反应(一开始我还开心了一下,以为是真的有很多人在看我的博客,后来发现只是因为刚更新了文章我到处在发导致的……), 我的博客打不开了。是因为我终于在两次尝试给博客开通 https 未果,终于想开了去联系了 GitHub 客服,把我的博客的 https 弄上了。

之所以之前失败了两次,是因为我的博客并不是 www. 开头的,设置 https 需要一个额外的步骤,感谢 Glavo 帮我把这事搞定了。 GitHub 客服态度也十分好,挺感动的。

以后这个博客就是强制 https 的了,经测试,在 chrome 中直接输入 ice1000.org 会跳转到 https://ice1000.org ,这很好。 我顺手更新了推和 StackOverflow 的信息,如果看到还有 http://ice1000.org 这种历史遗留的话请,如果不嫌麻烦可以提醒我一下, 谢谢了。

以后也请多指教了,另外最近弄了个子博客,欢迎阅读和斧正。我已经在里面放了两篇文章,分别是『把类型类做成语言特性』 和『写给有广义编程基础的同学的依赖类型传教文』,这周末还准备再写一个讲 SizedType 和 Copattern 的(对 Idris 教徒的信仰进行重度打击 www)。

这个子博客可以对里面的 Agda 代码进行跳转到定义,非常妙。


Tweet this
Top


创建一个 issue 以申请评论
Create an issue to apply for commentary


协议/License

本作品 终于换上 https 啦,新增 LAgda 子博客 采用 知识共享署名-非商业性使用-禁止演绎 4.0 国际许可协议 进行许可,基于 http://ice1000.org/2018/11/09/FinallyHTTPS/ 上的作品创作。
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
知识共享许可协议