• 我们是怎么发现C++异常从堆栈追踪中消失的原因的

    每当我的程序崩溃的时候,我都会用核心转储 (core dump) 文件来找出来崩溃发生的具体位置。(关于怎么产生和使用核心转储可以看我之前的文章。)一直以来我调程序的时候都是很开心的……直到我遇到了这个新的 bug。当我把它的核心转储文件载入到 GDB 之后,我很失望地发现所有的堆栈追踪 (stack trace) 都是关于系统库的,没有一行是关于我的代码的。

    太长不看:那就看看这个补丁就好了。

    让我们踏上探索未知的旅程吧。

    Read on →

  • Coq 小技巧

    我第一次听说 Coq 是在本科的时候。从那以后我就一直很想学 Coq,但是并不知道怎么开始。大部分的 Coq 教程都是在讲逻辑,我觉得并不是很有趣。

    上个学期我选了 UW CSE505 这门课。Prof. Zach Tatlock 和 TA Talia Ringer 设计了一系列非常棒的作业来帮我们学习 Coq。在这个课里面,我们证明了一些更加实际的东西,包括一个简单的编程语言的解释器还有一个简单的正则表达式引擎。事实上,我发现我对在 Coq 里面写证明还蛮在行的(但是写规范就完全是另外一回事了),至少在做作业的时候我是这么觉得的。

    如果你在自学 Coq,我推荐以下资源:

    • UW CSE505 的作业
    • Formal Reasoning About Programs 这本书是我们上课的教材。这本书很短,边距很大,空白很多,每一章附带了详细的 Coq 代码。这本书还自带了一个很好用的 Coq 库 frap
    • Software Foundations 如果你真的对形式化验证很感兴趣的话。

    我非常高兴我终于能把 Coq 从我的愿望单里面划掉了。不过我并不是形式化验证的狂热粉丝,我觉得我之后也不用用到 Coq。我决定趁我还没完全忘记 Coq,赶紧把我做作业时学会的 Coq 技巧写下来,万一以后哪天我又用到 Coq 了呢,希望也对读者有所帮助。

    Read on →

  • 为 CS140e 适配 Raspberry Pi 3B+

    这算是开了 CS140e 的坑了吧。在淘宝上买树莓派的时候发现了出了3B+版本,而课程用的是3B版本。新的性能要强得多,肯定要买新的呀。但是,3B的CPU是BCM2837,3B+的是BCM2837B0,买的时候有点担心能不能正常地运行 CS140e 的程序。

    收了货试了下,果然不行。ACT灯先慢闪4下再快闪4下,循环往复。搜索 raspberry pi act led,找到了这么一个wiki,上面说闪4下是 start.elf 无法载入。

    我猜测这个 start.elf 可能不是课程专用的,于是搜索 start.elf raspberry pi 3 “b+”,找到了这个帖子,发现了官方的固件,用里面的 start.elf 替换就能成功启动了!

    Read on →

  • macOS 矢量作图小贴士

    “放大放大再放大,每一根毛都看的清清楚楚。”

    ——[欢乐笔记本]内置病毒AIPC笔记本电脑

    前些天我在写毕业论文,自然免不了作图。我相信有很多读者像我一样有这样的强迫症:插图不是矢量图就浑身难受。插矢量图的好处都有啥?

    • 放大看也不会模糊
    • 可选中图片中的文字(似乎也没啥用)
    • 看起来更像是自己画的而不是从网上截图

    LaTeX 作矢量图的一大流派是 tikz,但是这个包对我来说还是太难了,总是学不会。而且我总是觉得,作图这种事情,就应该是在图形化界面里面拖拖点点更加直观清晰。之前我也听说有人用 InkScapeIpe 等等软件的,但试了一下用起来总是不顺手。

    可能是因为做幻灯片的机会比作图多得多吧,我发现我对 Keynote 非常习惯,于是理所当然地,我就顺带用 Keynote 来作图了。下面就介绍一下我在 macOS 下面作矢量图的经验,里面也包含了一部分用来做幻灯片的技巧。

    Read on →

  • PUBG“挖矿”

    PUBG?是的就是你正在玩的《绝地求生:大逃杀》。

    “挖矿”?蓝洞也出区块链骗钱了?呵呵,不是的呢亲。

    TLDR: 自己还是太年轻,赚钱的机会千千万,只是当自己意识到的时候已经错过了末班车。所以啊,还是要提升自己的姿势水平。

    Read on →