[1/3] 我本来是不会写 Python 的，但现在赶鸭子上架也能写点儿了，毕竟每月付给我两千欧元（然后我只花了一小半时间在工作上）。我现在只会写单个 Python 3 脚本，并且只引用 Python 标准库。我把 Python 解释器当做一个代码执行的平台，就是说但凡编译期能固定下来的数据都用 Lisp 代码把这些数据直接输出到 Python 文件里作为全局列表，然后 Python 代码启动后第一件事就是在内存里建一个 SQLite 数据库把所有数据狠狠地插进去，接下来的计算尽可能地用 SQL 查询来表达，SQL 语句和正则表达式都可以在 Lisp 代码里完成开发调试，然后直接拿到 Python 下面去用也不会错。我只能说凑合着用吧……
Discussion
[2/3] 虽然我只是个 Python 新手，而且从心里往外不喜欢这门语言，但我对 PyPy 这个项目观感极好，佩服得五体投地，合着 Python 官方实现也就是个纯解释器，连个 JIT 都没有。就我用 Lisp 输出的那堆烂代码，用标准 CPython 解释器执行需要 6.4s，但在 PyPy 下只需 4.7s。当然了，之所以性能提升没有达到 PyPy 官方宣传的标准（平均 4.8 倍）也很正常，因为我的 Python 代码思路就是尽可能减少纯 Python 代码的执行量，一切业务逻辑都交给 SQLite 引擎来完成。而且幸好我的代码里最高只用到了 Python 3.9 的语言特性，而目前 PyPy 也只支持到 3.9。所以日后再写 Python 代码的时候我也要注意，绝不用到 PyPy 尚不支持的语言特性。
[2/3] 那个什么 GPT 已经传染到欧路词典（和其他几个语言助手）的新版本了。我今天首次向 AI 提出了第一个问题，以后就不能再说没玩过 GPT 了[偷笑] 欧路（英语）词典兼容 mdict 词典格式，应该是目前下最好的桌面词典客户端了，我多年前就买了全套。我在欧路词典里主要安装的是意大利语词典，德语助手里安装的是梵语词典，西语助手里安装葡语词典，法语助手……就专心翻译法语吧。
[1/3] 刚刚入门了 Oracle Pro*C/C++ 预处理器。直接在 C 代码里嵌入 SQL 语句，然后用 proc 命令把整个代码翻译成真正的 C 代码——虽然极其冗长但是与原始代码是一一对应的关系，最后整个程序直接链接 Oracle 的 SDK 头文件和底层客户端 C 库。如果把程序启动和建立连接等时间都算上的话，目测这是访问 Oracle 数据库最快的方法，因为其他语言平台都需要动态加载庞大的 Oracle 客户端 C 库，初始化也需要时间，SQL 数据要在不同的内部数据类型之间反复传递，唯有 C 代码最简单粗暴。
[1/3] 我的正版 Windows 10 虚拟机最近只要安装了系统更新，开始菜单就再也出不来了。尝试了几种办法都无效，实在没办法只要把整个系统 Reset 了，所有用户文件和已安装的名贵软件都消失（不过应该还能再装回来，除了 VS2015 社区版，微软强推最新版，已经不让安装了）。心就是这么狠。
[2/3] 世界上最复杂的操作系统，不是 macOS，不是 Solaris，也不是 IBM 大型机上的 z/OS，更不是 Linux 和 FreeBSD（它们倒可以算是最简单的操作系统），而是几乎人人都在用的 Microsoft Windows。Windows 要是出了莫名其妙的故障，尤其是系统级的文件损坏以后除了重装（包括 Reset）我看就没其他路了。我现在这个虚拟机里除了正版序列号还在，其他的都没了[泪]
[3/3] Oracle 19c 的 JSON 支持：建表时可以在字段上添加 JSON 约束，不符合标准的数据无法插入；然后用 SELECT 查询的时候可以直接引用 JSON 数据键，然后返回对应的值。这要是用好了得给用户带来多大的方便。Oracle XML 数据库也是类似的思路，自从 9i 和 10g 的版本就有了。开源数据库上好像没有类似的支持。
[3/3] 前几天我请假去罗马做澳洲签证要求的体检（结果当然是一切正常），返回之前顺便去看了一眼地标建筑。回来以后小老板找我谈话，问我在工作合同的延长方面 “有何愿望”，我说我已经没有继续工作的意愿了（实在不想再写 Python 了），于是我们简单讨论了一下工作交接，就算是好聚好散。所以我还有一个月就在意大利失业了，不过没关系，钱暂时够花了，重要的是我终于可以每天在家专心写 HOL 形式化证明了，非常期待。
[2/3] 原来传说中的 COBOL 代码就长这个样子，可读性还挺强的，亮点是在定义全局变量时根据变量的缩进层级（由数字表示）自动生成结构体定义，然后拿来保存表记录刚刚好。Oracle 的那些 Pro*C/C++ 嵌入式语句放在 C 代码里其实挺突兀的，像宏又不是宏，可到了 Pro*COBOL 里竟然毫无违和感，仿佛就像是语言本身的一部分。由此可见 COBOL 在数据库领域的应用上比 C 早多了。不过这语言拿来干别的就很别扭了，没人学是正常的，怪不得会它的程序员要绝种了。真要逼急了其实学起来也很快，也就比 BASIC 语言复杂一点点。重要的是程序所表达的业务逻辑本身。
@田春冰河：当计算机还只有黑白字符界面的时候就已经足够把导弹送上天，或者处理股市和银行交易了。代码再难看也没关系，只要不出错，跑的足够快，并且后台的数据库稳定可靠，足够了。精美的图形界面在这种时候毫无用处。
[2/3] 古希腊文原版《新约圣经》里总共只有 5437 个不同的单词，其中 319 个单词的出现次数就占据了将近 80%。换句话说，只需背下来这 300 多个单词就能看懂五分之四的古希腊文原版《新约圣经》，这难道不是件很有诱惑力的事情么？
[1/3] 那个楼房被砸掉承重墙后出现裂缝的事件，多多少少触碰到了国人的底线。如果处理不好的话，以后恐怕没人再敢买房了。当几百甚至几千人住在同一栋几十层的高楼里时，根本无法保证家家户户都是正常人。假如你辛辛苦苦耗尽自己和父母两代人的积蓄（只够首付），再背上二三十年的债务才买得起一套属于自己的房子，结果住着住着突然有人告诉你这楼可能快塌了，且没人愿意赔给你另一套房，请问这房你还敢买么？
[2/3] 自古以来欧洲的学术著作所使用的语言，一开始是（古）希腊语，然后是拉丁语，接下来是德语，到现在是英语。年轻学者和程序员们应该对自己有更高的要求，不能只满足于熟练掌握英语（恐怕还有很多人连这个都做不到），还得孜孜以求、不断上进，最起码还应该学习一些德语。再往根儿上寻的话，就不指望你们了[挤眼]
[1/3] 耶稣说 “你们听说过 ‘不要通奸’，但我跟你们讲：任何人只要色眯眯地盯着女人看就已经算是跟她的心灵通奸了（这算神交吧）。如果是右眼（先）看的就把它挖出来扔了，因为失去身体的一部分总比你整个人下地狱要好些……” 太狠了点儿[挖鼻]
[1/3] 我们办公室里的女 Python 程序员（就哈萨克斯坦来的那位），每天穿着露肚脐眼儿的小衣服在办公区里晃来晃去（我们办公室里总共就俩女的，而且另外一个是 20 岁的实习生，还不是每天来）。我倒不是觉得这有什么特别性感的，也不是肚脐眼儿好看不好看的问题，而是我一看到别人的露在外面就立刻想到如果我自己的也露出来，过不了多久可能就会窜稀……（在这种心理暗示下立刻肚子就会不太舒服）[顶]
[1/3] 与人交流的时候经常需要强调自己所说内容的真实性，这时各有各的说法，最常见的大概是 “我对天发誓”。我一般说的是 “我没必要说谎 (I don’t need to lie)，精确的意思是我不敢说自己从没撒过谎，但眼下的这点儿屁事或者你这个人还不值得我赌上自己的所有诚信和声誉去撒谎。假如哪天我需要说一个谎言或者伪造些什么东西，那一定是关乎整个人类生死存亡的大事，并且干完这一票我就得去死。
[2/3] 纯靠 “说话” 来赚钱（比如主持人、相声和脱口秀演员）不是不可以，但是难度很大，技巧性很强。这个钱不是谁都能赚的，因为不光要靠努力，还得知道怎么防别人使坏。这方面我最佩服郭德纲和他的德云社，人家每天拿于谦的父亲和其他亲人开涮，国家有关部门只能干着急却罚不到钱；就连最接近军人的那段《西征梦》，最多也是映射联合国维和部队，只要联合国和美国总统不吃饱了撑得来找茬儿，其他人根本不在乎。这才是说话的艺术。
[2/3] 话说我们办公室里去年 20 岁的小姑娘（要是看胸最起码 30）昨天过生日（那现在就是 21 岁咯）。自从去年知道我比她整整大一倍以后就再没好意思跟她讲过话（我俩工作上也没交集）。这笔账我是这么算的：今年我俩的年龄比就已经没有 2.0 那么高而是 1.95 了；再过 20 年（她 41 我 61）就只有 1.48；再过 20 年（她 61 我 81）就只有 1.33，我俩谁先走可就不一定了；要是等她 81 我 101 的时候我还活着，那我有充分的信心比她晚几天闭眼（心态就是好）。虽然我俩都在写 Python，但我是 Lisp 程序员在亲身经历了 30 年计算机发展史、繁华落尽之后被迫用 Common Lisp 和 LispWorks 输出的 Python 代码，而她很可能只会 Python（用的是 VS Code），所以我并不觉得特别丢人，再说我过完这个星期就再也不用写了！
[1/3] 我在 FBK 还有 6 天，但是该做的工作都已经做完了，又不好意思最后几天请年假（年假不用也不会折现），所以我打算临走前把 “未了心愿” 还是圆了吧，那就是先把这本《Advanced CORBA® Programming with C++》快速过一遍，然后把我之前用纯 C 写的 CORBA 服务端代码（基于 ORBit2）迁移到 omniORB 4 上。2023 年还在学习 CORBA 算守旧么？很难接受新事物是变老的象征？你放屁！跟 CORBA 比起来其他所有的中间件和远程过程调用设计都是垃圾，玩具！ 
[2/3] 我在跟的那个项目里负责技术的同事以为明天就是我最后一天上班了（可见他也觉得我没必要呆到月底 31 号，可我似乎还有点儿舍不得），这才想起来让我教他如何重新生成我那些 Python 代码（因为配置上有些小变化，代码需要更新）。我这才首次告诉他我的原始代码是用 Common Lisp 写的，而且目前依赖于商业开发环境，含税价超过五千欧元而且是每个平台分开卖的（我给他看了价目表）。按说我不用费力移植代码，只要把那个更新程序编译成独立可执行文件就好了，但遗憾的是我只能编译出 macOS 应用，而他的笔记本装的是 Linux。我相信他心里不会很好受，顺便刷新了某种认知（运行个程序竟然要花这么多钱）[偷笑] 
[2/3] 话说今天组里搞活动去附近山头上烧烤，其中有个前不久离职的同事也参加了。我跟他寒暄时就随口问他现在在哪工作，结果他转身给我看他衣服背面的一行字，我记得好像是 “Lunar Lobster 2023”。于是我脱口而出 “餐馆？”，他笑死了（原来他在给 Ubuntu 工作，完全远程办公）。我丢的人可能比你们见过的人都多。 
[1/3] 今天最后一天上班，先是群发了上周末集体活动时拍的照片（可惜欠曝了，滤镜系数计算错误），然后群发了告别邮件，还给同事买了 50 欧元的甜点。这封邮件我构思了好久，原本很长，但最后决定删减到最低限度。基本的意思就是我要去写定理证明了，虽然不急着走但实在不想再在这里写 Python 和 C 代码了。就在我发这封群信前夕，我小老板竟然让我用今天剩下的时间再写点儿测试代码（用 Python），被我直接拒绝了（我说我不熟悉相关框架的 API），真是不知趣…… 
[2/3] （接上文）我今天最后一天上班，买了 50 欧元、大约 33 个小甜点带到办公室，临近 11 点的时候我发了之前提到的告别邮件并提到公共区域的甜点。因为再过一小时就吃饭了，我想他们应该会把我那些甜点留到下午2点左右当下午茶来吃吧。结果万万没想到，我刚发完邮件不到 5 分钟就全来了，然后自动围成一圈边吃边聊（幸好我正好在参加一个远程项目会议，不必起来寒暄和握手），把所有的甜点全给吃了，一个也没留到下午。然后 12 点照常去吃午饭……
[1/3] 真是活久见，竟然收到了 Gmail 的存储空间警告，15GB 空间用掉了 70%。我的 Google Drive 几乎就是空的，这些空间完全是多年来积攒的电子邮件占用的。我从 Gmail 刚发布不久就开始使用了，记得一开始最大存储空间只有 1GB（当时其他电子邮件服务商只给免费用户大约100MB空间，是 Google 彻底改变了游戏规则），然后每当存储空间用到一半时 Gmail 就会主动扩容一倍，我还以为它会这样继续下去呢。不过没关系，我还有一个更老的 Gmail 账号，15GB 只用了 1%。我把老邮件迁移过去就是了。
[1/3] 没想到集体烧烤那天拍的第二张彩色胶片（Ektachrome 64, 70mm）还算成功，分辨率比黑白的那张高多了。果然胶片还得是彩色反转片，哪怕过期三十年也能一战。我特地为喜欢看球的人士单独截了一张局部。 
[2/3] 也别光看球，再看看花。今天是我鼓起勇气第一次使用柯达原始配方的 E-6 彩色反转片冲洗套药，当初买它是因为 Tetenal 的缺货买不到。这个套药使用时有 7 瓶 500ml 药水，比 Tetenal 多了 3 瓶药水，而且有严格温度要求的步骤更多，但由于水洗的步骤较少，最后所需的时间跟使用 Tetenal E-6 套药是一样的。可惜我在混合彩色显影液的时候一开始忘记了倒入第二部分，后来补充倒入以后整体就变成了 600ml，浓度下降了。为了补偿可能引起的偏色不得不自作主张延长一些显影时间，但肯定估计不准，所以最后得到的胶片有些偏黄，所幸扫描时可以补偿回来。 
[1/3] 话说去年11月的时候那位波斯美女同学可怜巴巴地要求我们把小卫生间腾出来专门给她用（然后我们三个男生共用另外一个），理由是她的医生说她的尿路感染是因为跟其他男生公用卫生间导致的。这俩卫生间虽然一大一小，但其实大的里面有个浴缸和洗衣机，厕所的尺寸都是一样的，我还曾经就跟她共坐同一个马桶圈的事情而感到高兴。按说这种赤裸裸地污蔑（说我们把细菌传给她）就不该忍气吞声，但我私下里努力说服其他两个男生尽量配合，就当是尊重女性了。结果呢，由于她在淋浴室里刮体毛把下水道给堵了，然后也不在早期阶段用化学品疏通，可能水都没到脚面了还在继续洗，然后溢出来的水不但渗到楼下，甚至都流到隔壁伊朗男的卧室里了。她年初搬走的时候房东死活没退还她 500 欧元押金，原来是楼下住户要求赔偿墙壁粉刷费 450 欧元，加上税差不多 500 欧。房东要求我们其余三人签署声明，证明自己在漏水期间没用过小卫生间，当初她发的那个消息正好构成了决定性的证据（其他人要是敢用了岂不是要赔她医药费）。这就是报应。 
[3/3] 其实所谓 “学术妲己” 问题（或现象），跟博导的利益输送问题，乃至导师对学生的欺压（包括其他行业上级对下属的欺压），甚至家长打孩子，以及女方结婚时索要高额彩礼，本质上都是同一个问题：那就是当一个人处于某种优势地位时（即便不是通过自己的努力获得的），能否忍住不利用自己的优势去获取利益，或者说能否做到 “克己复礼”。俗话说 “有便宜不占王八蛋”，还有商人的逐利本质，但很多不该做的事很少会直接触犯法律，而是看周围的人都做了自己也就做了——社会风气使然。
[3/3] 我离职后我大老板（博导）给我发的邮件，竟然总结性地说 working with me was “nice”，这不是睁眼说瞎话么？然后还想让我帮他改课件。我本想回信告诉他我在他身上多花一分钟都是浪费生命，但是仔细斟酌以后觉得不回信才是最佳方案，就让他继续糊涂着吧。日后我肯定不会求他办任何事，但如果别人向他询问我的情况，只要有一句难听的传到我耳朵里，这封口不对心的邮件倒是可以用来证明他的话前后矛盾。 
[2/3] 此女屁股后面纹的黑字是 MCMXC?V, 红字是 ?X XXII?，其中问号代表看不清的部分。根据罗马数字的书写原则，必然是 MCMXCIV (1994)、IX (9) 和 XXII (22) 或 XXIII (23)，由此可见她的生日是1994年9月22或23日，很年轻嘛[微笑] 
[1/3] 昨天吃饭吃着吃着突然发现我炒的菜里有只绿油油的苍蝇。这一定是趁我不注意飞进去然后被油给淹死的。你说怪不怪，虽然这饭只吃到一半还没吃饱，但我立刻就不觉得饿了！虽然没有迹象表明我实际摄入了任何来自苍蝇的高蛋白营养物质，但我就是觉得想吐[吐] 我觉得自己很没用，好歹也是一口肉，怎么就是想不开呢？[二哈]
[1/3] 昨天给本地中国超市的老板娘和她俩孩子拍了四张 4x5 胶片，我又不收费（就是没事拿他们练练手），也不要求买东西打折，你说她能不高兴么？下次买东西时要是正好赶上哪个有毒她能不能给我提个醒么？[挤眼] 
[2/3] （接上文）后来我去中国超市给老板娘送那四张照片的原始胶片（反正我留着也没用）并告诉她用法（可以拿去洗照片或者装在透明相框里），顺便买了点儿东西。老板娘大概是看我买的东西不多（也就五六欧）就说要请我（意思是不用付钱了）。我连声拒绝并立马掏钱给她，请她务必收下。她说她要（以此）谢谢我，我说我也是代表本地中国留学生谢谢她；她问我谢她什么，我说我谢谢你们良心开店，从来没让我们吃坏肚子或者上医院；她没说话（大概是心说你对超市的要求也太低了），然后就结完账了，她说要不送我一个芒果吧（就在收银台边上摆着）。我看芒果实在是好，盛情难却也就收下了。我还特意跟她老公提了一下这个芒果，以免这位老板误以为我什么也不要而是惦记老板娘的美色。所以我赚了一个芒果，冰镇了一下切开，太好吃了！（我平时只舍得买1kg塑料装的普通苹果） 
[3/3] 话说我当初在博洛尼亚大学读硕的时候，密码学那门课是满分。我不但把整本教材全看完了，还在作为考试一部分的个人项目里仔细研究了 DES 加密算法和针对它的差分攻击（Differential Cryptanalysis），然后还用 Common Lisp 实现了整个算法和破解算法（但是只能攻击不完整的 DES）。我甚至给了这门课的教授一个小惊喜：我找到了 DES 设计者之一 Feistel 本人在 1973 年《科学美国人》上撰写的现代密码学科普文章。现在我要填补一个 HOL4 里面的小空白，形式化 DES（目前 HOL4 里面已有 AES 等算法的形式化）和它的一些主要性质。 
[1/3] 下面看看 Common Lisp 相对其他编程语言的 “特别之处”：图1. Acrobat 原始头文件里的一行；图2. 我用正则表达式把它摘出来并翻译成一行宏调用 (图3). 图4. 这个宏调用背后的宏生成了另一个宏，是要在最终代码里调用的（注意代码里复杂的引号、反引号和逗号嵌套写法）. 图5. 对图3的宏调用进行宏展开，看到的就是它生成的那个宏的最终内容。图6. 最终代码里的实际调用时的样子（就像一个普通函数）。图7. 对这个实际调用进行宏展开，看到的就是图1中原始C代码一一对应的 Lisp 代码。
[1/3] 昨天除夕夜做了个水煮鱼，有点儿辣，但是主打一个鱼（Barramundi，尖吻鲈）比较新鲜；今天初一吃的是芹菜、蘑菇片炒肉，自制黑凉粉，外加自产红黑西红柿拌糖。最近西红柿陆续开始熟了，每天都能采摘下来几个，且越来越多（我最大的那棵西红柿树整整挂了70个果）。明天可以再来个鸡蛋火腿炒四季豆。
[1/3] 我现在只要闭上眼睛就能看见梵语语法表格（基础部分），已经不太需要把它作为电脑桌面了。学习梵语十年才总算达到了这个境界。五月份我要给系里的同事们做一次内部讲座，首次正式介绍自己的研究内容。我决定给他们一个惊喜[偷笑]
[1/3] 书上一个不起眼的引理，卡了我一个半月，证明写了一千多行代码还没写到一半。然后其中有个关键步骤，又卡了我一个多星期，直到刚才才终于拨云见日，但要想完成它还要再写很多代码。形式化证明的繁重工作量，在一般情况下是无法避免的（少数情况下才可以自动推理）。
[1/3] 这就是卡了我一个多月的那个引理，证明过程举步维艰。我连续两个晚上工作到深夜，终于临近尾声了。现在得到的简化目标和 60 个假设看起来完全可行。λ 演算原本是最简单的形式化系统，但是却衍生出一些极其复杂和难以证明的定理来。我现在相信这个项目的潜在竞争者不太可能超过我，因为他们缺少破釜沉舟、证不出来就失业的压力。
[2/3] 话说一个男的要到堪培拉留学（交换生），拿他女朋友的女性微博 ID 跟我私信联系，问这问那（我知道的那点儿都告诉他了），还多次要求加微信，还说要给我带自家产的茶叶。我也是没好意思直接问性别，但是秉着坐怀不乱、不跟本校任何学生打交道的原则拒绝见面、收礼和加微信。然后这几天按说已经到澳洲了却没消息了，我怕他（她）乱带东西被原地遣返了所以就私信过问了一下，这才告诉我原来是个男的来澳洲。我甚至还好心说过可以去堪培拉机场接一下（但是因为那天刚好系里组织活动就算了），不然肯定接了个寂寞。
田春冰河
:这是怕用男性 ID 私信我询问信息我不回复么？未免太小人之心了。另外我现在甚至怀疑这里面甚至根本就不存在女的，就是个男的把微博 ID 性别改成的女。以后再有网友私信联系，我得先让它填个人信息表……
[1/3] 话说 Bose® 耳机几天前在美国发布了一个名叫 Ultra Open Earbuds 的新品，主打开放式设计，就是完全不会阻挡和减弱佩戴者听到周围环境的声音（此款并没有主动降噪的功能），并且这个耳机不会深入到耳洞内部，长时间佩戴时应该会更加舒适。我多年来不买这种蓝牙耳机主要是担心安全问题（就是听不到周围环境的声音），现在我终于想买了。
[2/3] 距离我到达澳洲开始新工作满半年，就只剩一个星期了，我的时间已经不多了。虽然看起来导师对我满意，但毕竟还没完成他交给我的第一个工作任务，所以严格来讲被辞退是有可能的。最近忙里偷闲重看了一遍《三体》电视剧（拍的太好了），没有证据表明我的形式化证明也被锁死了，只是我写呀写呀就是写不完了[挤眼]
[1/3] 整个上周末困扰我的那个重要引理终于被我在周一下班前1小时的时候顽强地搞出来了。回头看看这个证明过程，我自己都觉得不可思议。λ 演算的这部分的整个证明思路是我自己独立想出来的，我导师一开始建议我使用 de Bruijn 编码但我觉得更麻烦，所以硬着头皮按我自己的思路一路走下来了。教科书上的这一页，我整整翻了一个半月。我导师他不可能开了我，他得请我吃饭！
[2/3] 话说今天有个学生来我们楼层做项目报告，结果苹果笔记本死活连不上我们那台投影仪。它用的是苹果的那个多功能 HDMI 转接头，我自己也有一个，也连不上那台奇怪的投影仪。于是我赶紧回办公室给它拿我新买的 Belkin 转接头，我买回来以后自己一次还没用过。结果果然一击而中，成功地连上了。现在看来 Belkin 的转接头比苹果官方的产品兼容性更好。
[3/3] 没想到 Bose Ultra Open 这么快就出现在亚马逊澳洲站上了。我果断下单了一副黑色的（我怕白色的过几年会变黄），预计两天后到货。最近两三个月我忙的连照片都没心情拍了，平时上班埋头写代码（形式化证明），下班回家以后继续写到深夜，圣诞和春节期间我都是混过去的。最后的副作用倒是省下了不少钱。这副蓝牙耳机虽然不便宜，但我还是轻松买得起的（比我那把蓝宝石伞便宜多了）。
[1/3] 日本产的百乐（Pilot）V Board Master 系列白板笔应该是目前世界上最好的白板笔了，在世界各地都有销售。它主要有三大特点：1. 字迹（深色的那些，比如红、蓝和黑）清晰，远处可见；2. 稳定的输出，字迹不会因为墨水的消耗而逐渐变淡；3. 墨水可替换。不过很少人知道这款白板笔的笔尖（很容易磨损）其实也是可更换的，但仅限于日本（大概是为了满足环保要求），这个笔尖虽然便宜但是并不出口。我在 eBay 找这个替换笔尖可不是一天两天了，但就是找不到。直到昨晚我突然想到 Amazon 日本站上可能有，结果还真找到了。每包3个笔尖，售价1澳元多点儿，10包起卖，总价 10 澳元多点而，然后运费是 60 澳元。即便这样也划算，因为每支笔现在大约3澳元，这个替换笔尖到岸价是2澳元一枚，仍然比重新买一支笔要便宜些。我就算是为环保尽力了[挤眼]
[1/3] 上海那位勾搭学生的女老师，个人品德和职业道德上确实有问题，是应该把她开除出教师队伍，让她另谋生计。这就足以警告其他有类似行为的女老师们了（也包括男老师们），不想失业就别干这种事。但假如我国真的是法制社会，就别给人家判刑。至于那些拿隐私权说事的，我倒是觉得只要做了就别怕别人知道，也别怕别人说（否则你别做啊）。这件事之所以能得到充分的讨论就是因为各种细节被彻底地公开了，你吃完了瓜然后拿隐私说事，就等于端起碗来吃饭，放下筷子骂娘。
[1/3] 如果有人跟我一样在买 Bose® Ultra Open 耳塞的时候不确定该选黑的还是白的，或者担心万一没电了怎么办，学学我[酷] 不贵，1000 块钱一个，我这有 4 个[微笑] 不过我最喜爱的佩戴方式是戴一黑一白，同时听两个不同的音源，一个听郭德纲、于谦和他们的徒弟们，另一个听一衣带水邻国的老师们[偷笑]
[1/3] 前几天路过广州白云机场的时候，登机口旁边就是海鸥表的专卖店。我进去转了一圈，有的像劳力士，有的像宝玑，价格是他们的十分之一。后来一问走时精度，说是正负 45 秒（那就算了吧……）。不过后来看到他们的袖扣还不错（但是不便宜啊，2400 元不讲价），里面的齿轮是能动的，因为有玻璃罩保护着，不像我现有的那对袖扣有时齿轮会不小心挂到衣服的布料。我买它就算是支持国货钟表品牌了…… @海鸥表SEAGULL
[2/3] 我去年11月份花 420 澳元买的那条李维斯 501 牛仔裤，每天都穿着，也没敢洗（我怕它缩水），再说洗了也没得换。我前天突然想到不如索性再买一条，这样旧的就可以送去干洗了。另外我让它的腰围再大一号，这样我接下来冬天穿的时候里面还能再套一件衬裤。万万没想到，付款后不久就收到了全额退款，但是牛仔裤也照常发货了，今天就能到（拭目以待）。咱也不敢问啊，究竟是我作对了什么还是他们做错了什么……
[3/3] 终于完成了圣诞节至今卡住的一个阶段性工作，提交了将近 2000 行新代码——其中一半是在国内期间完成的。现在导师已经相信这个工作的难度前所未有了，因为我已经把他之前的相关代码量给翻倍了，而且我遇到的几乎每个新定理的证明都超长。试用期肯定没问题了，下周开始我要教书了（讲 HOL 定理证明器用法和形式化概率论）。
[1/3] 每天一壶茶、两杯咖啡，怪不得晚上睡不着觉[挖鼻] 自从上周五完成了重要定理以后我这个周末就没怎么干活，心理上急需歇息一下，喘口气。明天貌似是公共假日，我决定假装不知道，去办公室做课程幻灯片去。
[2/3] 能用来日常交流的小语种，除了意大利语以外，我觉得只要把法语和德语学好就行了，其他比如西班牙语什么的就放弃了，毕竟贪多嚼不烂[挤眼] 至于古代语言就专攻梵语好了，希腊语和希伯来语我就先不学了。
[3/3] 我当初刚到澳洲不久就给她发了 offer，打算供她在澳洲留学（幸好她拒绝了，后来实际计算了一下发现我那点儿工资得全搭进去才付得起ANU每年5万澳元的硕士学费）。因为跟本校学生发生关系会被开除，所以至少我说要把她当亲妹来养（就是不能碰她）是真心的（独生子，就想有个妹子）。现在看来我真的是太自作多情了。其实这些年来我没怎么变；她变了：从原本踌躇满志地去留学了一趟然后本科毕业了还要再去欧洲号称最好的商学院深造，逐渐变成了只希望呆在现有的舒适圈里，身边有几个朋友就好。我对那些变得平庸的人就不再有任何吸引力了；我也就是客气一下[拜拜]
[1/3] 现在科技排版用 LaTeX 的人多，因为相关教程多，而且科技论文投稿的时候模板也是 LaTeX 的。会用 ConTeXt 甚至知道这玩意的人相比之下就少多了，但其实用来做幻灯片最合适。我过去一直坚持用 MetaPost（主打一个根红苗正）给 LaTeX 文档配插图（其他用户一般选择 Pgf/Tikz），现在 ConTeXt 可是内置 MetaPost 的（扩展了命令以后叫做 MetaFun）。我今天把入门教程再看一遍，然后连夜赶制 HOL 课程的幻灯片（够第一课的就行了）
[1/3] 折腾了三天，成功做出了我的第一个基于 ConTeXt 的幻灯片。注意看那个列表项前面的红色小方框，每个都不一样，因为那是用 MetaFun 加了随机性画出来的（代码取自教程，不是我的发明）。更重要的是，我学会了用 LaTeX 去排版一些 ConTeXt 不直接支持的内容（比如基于 bussproof 宏包的逻辑推导公式），然后让 ConTeXt 去调用 PDFLaTeX，再把输出的 PDF 嵌入到 ConTeXt 文档里，这样 LaTeX 的海量宏包都还能用。
[1/3] 今天手把手教我的印度学生（女）用 Emacs（HOL4 的官方编辑器）。先用 Ctrl+@ 标记复制的起始位置，然后 Alt+w 复制，最后 Ctrl+y 粘贴。她问我为什么不都用 Ctrl？我通过演示单手操作的具体指法和键盘键位之间的垂直位置关系说明了这样设计的精妙之处。反正我自己是信了[拜拜]
[1/3] 又到了每年安装 TeXlive/MacTeX 的时候了，我有三台电脑（两台 Mac，外加 PC）要装，工作量还挺大的。从来没给 CTAN 社区做过一丁点贡献。其实我也就是勉强会用；要让我设计宏包或者修 bug，惭愧惭愧……
[2/3] 哈苏新出的 907X & CFV 100C 真是好东西，那个1亿像素数码后背装在我的大画幅相机上，通过平移分块拍摄，理论上可以9张数码照片拼在一起拍出超大尺寸的风景和建筑照。但是可惜我已经忙的好久没拍照片了，也没心情拍了，也没人可拍了。在状况发生改变之前我就没必要再在摄影上投资了[拜拜]
[1/3] 简单研究了一下英国王位继承顺序。有没有那么一丢丢的可能：威廉王子一家不小心全灭了（他自己稍后得去蹲监狱，总之就没他什么事儿了），结果一不小心让英国人民最不看好的哈里和梅根捡了个百年不遇的大漏，无业游民摇身一变成为英国国王[偷笑] 总之我是看热闹不嫌事儿大，看出殡的不嫌殡大[挤眼]
[2/3] 过去我穿的那些亚麻布唐装都是在上海田子坊里面一家叫“金粉世家” 的店里买的。自从疫情以来我就再没机会去他们店里买衣服，而且他们改名叫 “老克勒” 了，我在网上一直没找到联系方式。直到前几天绿头发姑娘帮我在美团上找到了他们的微信，我立刻订了两件，其中一件原样复制我穿旧了的那件，另一件女装给我意大利的朋友（女装比男装贵）。在此推荐给大家[挤眼]
[2/3] 最近的 XZ/liblzma 库里面那个处心积虑引入的漏洞和干这件事的那个叫 Jia Tan 的中国人——指不定是受谁指派的——简直丢尽了中国人的脸。这以后让国际上的开源项目开发者还怎么信任来自中国的那些积极参与者？就算活儿干的再好，也许这一切都是为了获取信任后在未来的某天突然开始干坏事…… （更正：不确定是否中国人）
玩家云风:一个叫 Jia Tan 的，看起来生活在 UTC+8 的人，三年来遵守晚上 20:00 开始活跃，干活干到第二天凌晨 2 点的作息。周末不干活，但清明节和春节工作都很努力，到了圣诞节去休假了。我觉得他是一个怪异作息时间的天朝程序员。
玩家云风:回复@田春冰河:我昨天在一个专门讨论这个后门的 discord 频道蹲了一晚上，主要是想看看大家的分析。分析包括了技术分析和对这个人的猜测。最后这个频道里的人没人相信他是个中国人，甚至有闲人分析他的英语语法。
玩家云风:回复@田春冰河:这个身份是为这个事情刻意制造出来的，包括并不限于 id ，github 上用的 publickey ，还有用这个关联 email 在各种邮件列表里的发言。都是 3 年前突然出现的。一切都为这个干这件事。所以这样的身份看起来是怎样的，无疑有人为刻意的成分。
玩家老C:现在并不确定是中国人的，只是起了一个类中国人的github ID。
田春冰河
:那拭目以待吧
[3/3] 这本《开封食谱》终于落到我手里了，哈哈哈哈。有了这本书，以后我的菜就是开封菜，简称 KFC（郭德纲说的）[鼓掌]
[1/3] 我上个学期含辛茹苦地给两个学生讲 HOL 定理证明和形式化概率论，其中那个印度女学生一直忙着打工赚钱，然后又因 ”家庭原因“ 回国了两个月，三天前她终于发给我阶段性成果。竟然是用 “生成式 AI” 从现有的 Isabelle 形式化证明代码翻译到 HOL4 的，还让我帮忙 “调试”。这些生成的代码表面上看像那么回事，其实根本狗屁不通，就是个 Standard ML+OCaml+HOL4+HOL-Light+Isabelle 的大杂烩儿。我今天跟这个学生开例会特地邀请我导师一同参加。我导师说的很含蓄——他说这些生成代码就是垃圾，调试它们比从头写要难多了。由此可见 ”生成式 AI” 目前在交互式定理证明领域毫无用处，除了能保证左右括号互相匹配以外，就只剩下满口喷粪了。
[2/3] 胖缅甸姑娘想让我投资她弟弟（上次跟我借钱就是为了他）在泰国开的咖啡馆（应该是还没开，正在筹钱），说是至少 4500 欧元，然后年投资回报率 5%。被我狠心拒绝了。我心说既然是投资那就不算借了，你弟弟要是赔了我这钱就直接打水漂了。再说上次借你 1900 欧元时国际转账本身就损失 5% 的手续费，我既没提利息也没要你承担手续费，甚至最后还给我的钱转身也重新分给你们俩了。
[1/3] 我的天呐，QEMU 现在已经能虚拟 SPARC v9 了。它直接使用当年 Sun 随 OpenSPARC T1 一起发布的 Solaris 10 映像文件和系统固件，一行命令就把 SPARC Solaris 10 跑起来了。我随便敲了几个命令，看起来一切正常。不枉我昨晚刚把 SPARC v9 指令集从头看了一遍（比 RISC-V 简洁多了）。
https://postimg.cc/gallery/v8TjcCN
[4/3] 我觉得硬件加速定理证明过程首先要解决的是如何让 CPU 把逻辑表达式当作基本数据类型来对待并在此基础上做符号计算，但这不就是之前 Lisp 机所做的事情吗？（可能也包括所谓第五代计算机——针对 Prolog 优化）所以其实定理证明器所需的硬件指令完全可以在 Lisp 机开发者制定的复杂指令集上再加几条就够了。前人留下的那些电路图已没有实际意义，重要的是指令集和相关的数据格式。我可以从 OpenSPARC 开始研究，只要我能彻底搞清楚一个现成的多核多线程 CPU 的全部细节，就可以对其指令集加以扩展，让它支持符号计算、类型检查和硬件 GC，到时候 Lisp/Prolog/SML/HOL 的硬件加速问题就直接一锅端了。（至于祖国的 RISC-V 社区，只能先对不起了，你们的指令集太乱了……）
https://postimg.cc/gallery/8G3KVSb
[1/3] 话说前两天瘦缅甸姑娘在 Instagram 上官宣名花有主，看这架势是有人求婚了。这我就放心了，我太高兴了，以后这俩缅甸姑娘的幸福就不用我管了（情同姐妹的胖姑娘去找姐夫拉投资去吧）。那是不是之前给的钱就算打水漂了呢？绝对不是。因为就算从此没事儿再不联系（约等于一刀两断）也毫无愧疚，因为我花钱了。
https://postimg.cc/gallery/F1GCcyb
什么情况你这是，这不写的挺好。
[1/3] 最近成功地在我较大的那块 FPGA 开发板上写入网上现成的 64 位 RISC-V 处理器并运行了 Debian Sid。借助 MacWise 的终端日志捕捉功能，这才首次看清了它的启动过程。一台计算机光有 CPU 和其他硬件是不行的，最开始启动后必须得从一个引导 ROM 里读取指令并执行。接下来是 RISC-V 世界独有的 OpenSBI，相当于 PC 世界里的 BIOS/UEFI。然后是 U-Boot，相当于 PC 世界里的 LILO/GRUB，它认识 FAT32 文件系统，负责读取并加载 Linux 内核。最后才是 Linux 内核本身。这一系列的软硬件全是开源的，代码就在那里。随着技术的进步，廉价的入门级 FPGA 开发板也已经大到可以支持在多核/软核上以可接受的性能运行 Linux 了，网上还有现成的示范项目，等于是真正从零搞出了一台计算机——然后可以随便改。
[1/3] 话说我同屋要离职的那位同事（今天在办公室最后一天）用的是大学发的 M 处理器 MacBook（具体型号不清楚），应该是用它读完了整个博士，再加上一年博后。他走之前得把电脑交还，询问我数据备份相关事宜。我一开始还担心他的移动硬盘空间可能不够，都要把我那名贵的 4TB SSD 给他一条了。结果仔细一看，原来这台电脑总共只有 500GB 磁盘空间，他这么多年用了 130GB（连同系统文件和所有应用程序），不够装满我那个小 U 盘的……
[1/3] 成功地在我的 FPGA 开发板上把 OpenPiton 项目预编译的 Linux 环境跑起来了，这可是 64 位 SPARC 处理器啊。可惜只有一核一线程（根据官方文档，我的这块板子上最多可以支持双核，但线程数不明），网卡似乎正常但是没有安装 DHCP 客户端。这我就放心了，起点正常。下一步我就可以自己重新编译双核的版本了。
[2/3] 不知不觉中，我在 HOL4 项目所有历史贡献者里已经在提交数上超越了已故的创始人 Mike Gordon（有点儿胜之不武，毕竟他已经不能再写了），目前排名第七。距离超越第六名 Thomas Türk（他已经不活跃了）只差 7 次提交。再往前 20 次提交就可以超越 Magnus Myreen（CakeML 项目创始人之一）。其实如果看新增代码行数的话我早已遥遥领先，但现在 GitHub 不再显示按代码行数的贡献排名了。而每个 PR 分支里的提交数其实是越少越好的（最好是临时分支，里面只有一次提交），所以我的排名里每次提交往往对应一个完整 PR，含金量是很高的。
[3/3] 话说前不久我买的那个二手 AMD 5700 XT 显卡以后，换下来的 980 Ti 放在办公室里占地方，想扔也没处扔，于是就在同事群（实为使用苹果手机的同事在校内咖啡厅碰头时的交流群）里免费送出去了，有个同事说 “他儿子的旧电脑正好需要”。结果万万没有想到，那个 5700 XT 昨天突然坏了，显卡风扇再也不转了，甚至造成所连接的笔记本死机，但我确认我的雷蛇 Core X 还是在正常供电的。现在好了，一个无用的 GPU 盒子里面装着个废显卡，很多 Steam 游戏我再也玩不了了。
[2/3] 我来澳洲以后采购的希腊产纯铜的盐和胡椒研磨器，服役了将近一年，完好无损。不久以后我可能就搬家了（美女都搬走了我也不想住了），我把它们拿回办公室，用砂纸稍微重新打磨了一下，再用抛光布擦一下，虽然不是全新但却更有岁月感。我准备以后刻上名字，今后走南闯北都随身带着，就算是要饭也得加点儿盐和胡椒再吃。
https://postimg.cc/gallery/cYSDLny
[3/3] 回想当年我上小学的时候在音乐方面就很突出，尤其擅长指挥，变声之前我的童声也不错，可以唱出极高的音调，深受音乐老师的喜爱。按说我们小学去参加全市合唱比赛的时候就该派我担任指挥，结果这个重要角色被水平不如我但是爱显摆的隔壁六年一班漂亮女班主任给抢走了。我学校有个西洋乐队，我当时最羡慕的就是那个乐队里吹长笛的几个人。一度以为自己只是不幸落选，后来我才想明白也许那些乐器不全是学校的，常见的那些可能是学生自己的，人家从小家里花钱请老师教的。学校只是把有乐器特长的学生组织在一起排练一下，并不负责从头教。我家穷，只能买个几块钱的竹笛自己瞎吹。
[2/3] 通过机器学习海量知识和文本的方式来实现人工智能，这个思路肯定是错的，学得越多就越能掩盖它其实不智能这件事。一个能代替人的聊天机器人程序不见得非得知道更多的事情才算合格，因为如果需要的话它可以花点儿时间自己去互联网上搜索答案（就像人一样）。把一个聊天机器人程序里所有通过后天学习也能获得的知识都去掉，最后还能剩下的那点儿东西，才是实现人工智能的关键。而这点儿东西，无论它是什么，都不可能是用机器学习算法从互联网上的海量数据里得到的。
[1/3] 开始移植 HOL 定理证明器背后的 PolyML 到 RISC-V 64 处理器。我先读了一遍现有的 ARM64 支持代码，再简单看了下 X86 的相关代码，再复习了一遍 RISC-V 指令集手册，然后再确认了一下 ARM64 指令集文档，最后信心十足地写下了肯定正确的这些代码（完成度大约百分之一）。感觉跟 RISC-V 相比，ARM 指令集设计得太啰嗦了，根本不配叫精简指令集。
https://postimg.cc/gallery/Kx2WNqV
[2/3] 你还真别说，DC-ROMA II 这台 RISC-V 笔记本上的 GPU 可用，而且 OpenCL 接口是工作正常的，虽然不知道具体性能如何，但有总比没有强。正所谓 “CPU 不够 GPU 来凑”，如果我能找到一个办法让 GPU 来参与 HOL 表达式的 β-规约（本质上就是个变量替换，可并行完成），那就完美了。
[1/3] RISC-V 指令集的一个特点就是它的 32 位和 64 位版本是同时设计的，64 位指令集并不是通过扩展 32 位指令集得到的，64 位处理器也不要求可以区分和执行 32 位的指令（编码后可能是一样的），而是额外添加了几条处理 32 位数据的指令。这就确保了一个 “纯” 64 位实现在软硬件实现上最简，没有像 x86 和 ARM 那样的历史包袱。
1/3] 理解一个数学证明就好像参悟一门武功（只有口诀的那种）：一开始完全不知所云，慢慢地有所领悟，等到豁然开朗的时候这个证明你就不会再忘记了，而且看似复杂的步骤也变得简单明了了。我每天只要能参悟半页的数学证明，再看几页技术书籍，然后再读几十行开源项目源代码（然后再写点儿），这一天就太充实了。
[1/3] 心血来潮搜索高性能 RISC-V 电脑，结果找到这台 Milk-V Pioneer，好像也是国产的，64 核 128G 内存 1T 硬盘，可惜我在国外看不到它在淘宝和京东上的人民币价格（谁帮我看看，谢谢）。这台机器并不主打 AI 性能和矢量指令，如果价格实惠的话拿来挂墙上当服务器跑跑常规 CPU 下的高性能和大内存需求的计算任务挺合适的。
https://postimg.cc/gallery/yDFySQc
[1/3] 刚刚在我的 Lenovo/ThinkPad P70 上安装完最后一批 Windows 10 更新，然后微软提示说已经结束支持了。这台笔记本大约是 2016 年买的，曾经助我完成硕士学业（一个需要 GPU 的课程项目），号称不支持 Windows 11（就算它支持我也不会升级）。我也算是保养的好，这么多年一直是出厂系统，从来没有重装过，目前可以通过外接硬盘盒双启动一个 Linux。由于我的 NVDIA 显卡太老，CUDA 版本也停在 12.9 了。
https://postimg.cc/gallery/Vzt9Bxm
[1/3] 前几天闭关写代码没怎么上网，结果刚一上网就同时看到两条重大新闻。一条自然是杨振宁教授不幸去世，就不多说了；另一条是我上小学时候就知道（甚至可能还捐过款）的 “张海迪” 阿姨（跟雷锋、赖宁等英雄人物齐名），竟然还活着…… 而且貌似能走路能开车。
[2/3] 话说 Linux 下可运行的兼容 BLAS/LAPACK 接口的线性代数库，除了原始版本和不开源的 Intel MKL 以外也就剩 OpenBLAS 和 ATLAS 两种了。ATLAS 的安装过程很有意思，首先必须想办法把 CPU 的变频（throtting）关闭，然后从源代码编译，让其自行根据你 CPU 的性能、指令集范围和各级缓存的大小来调节各种算法中的参数。我用网上找到的一个 R 软件的测试代码实测表明调节后的 ALTAS 性能确实略高于 OpenBLAS。
[1/3] 应该没有人玩过 sendmail 吧？Linux 系统安装以后总会带一个 SMTP 邮件服务器，没事儿给你发点儿系统通知。Ubuntu 默认装的是 Postfix（好几个进程，消耗资源），Debian 使用的是更加轻量的 exim4，但我的习惯是全改装 sendmail。这玩意的配置文件就是一门复杂的编程语言……
[2/3] 本月初开始，21 天时间，好不容易形式化证明了对于每一个 Lebesgue 可测集都存在一个测度略大但无限接近的 Borel 可测集，进而实际上存在测度相同的 Borel 可测集。这就打通了 Lebesgue 积分和 Gauge 积分等价性的主要障碍，我和导师、学生的概率论中央极限定理形式化项目马上就要全部完成了（那也得年底）。我的效率还是低，照这么写下去一年时间根本写不了多少代码。
[1/3] 终于又出现了一个 Macintosh Common Lisp 老用户，兴奋地在 Reddit 上发帖说都 2025 年了竟然还能轻松运行他（她）年轻时写下的 Lisp 代码（貌似跟绘图有关）。他找到的 MCL 6 下载链接是我的 GitHub，那个版本号 6.0 其实我是自作主张命名的，虽然确实在 5.2 的基础上打了一些补丁（多数都不是我写的，我只是搜集者），但其实不配称为 6.0。苹果当初从 PowerPC 转 Intel 的时候这个软件就废掉了，如今苹果转 ARM 了，连后继的 Clozure CL 也废掉了。
https://postimg.cc/gallery/n7F3Cmx
[1/3] 我的天，还有这种书，从头教你实现 RISC-V 然后在 FPGA 开发板上跑起来，而且用的语言既不是 VHDL 也不是 Verilog 而是 C——Xilinx 的高层次合成技术能把 C 代码直接编译成电路描述，这个软件我从来学过，现在正好搂草打兔子跟 RISC-V 一起学了。学习这样一门新知识需要时间、软件和硬件，但更重要的是兴趣和决心。
https://postimg.cc/gallery/ZCKbxqN
[2/3] 昨天有个同事（教授）在日常约咖啡的群里询问 HOL4 的 “top people” 都有谁。这个问题比较模糊，我就把 HOL4 的 GitHub 贡献者前排图标列表贴给他看（90 个人的前 14 名，其中我导师排第一，我在第五，其他包括已故的图灵奖获得者暨创始人，前代维护者和 CakeML 的两个最大的作者等人），他竟然反问我 “有相关性吗”。我听说他是 “研究” 编程语言的，自创了一门（但没人用）然后现在主攻 Rust，带的博士生在给 Rust 添加新特性，于是就去看了下 Rust 的贡献者列表（洋洋洒洒五千人），瞬间我就明白了……
https://postimg.cc/gallery/YtkDfy3
[2/3] 我在 Windows NT 4.0 虚拟机上用 VC6 编译了一个简单的示例窗口程序（不过并没有使用 MFC，只是最基本的 Win32 API），得到的可执行文件仅有 36K。把它复制到 Windows 11 arm64 里，无需任何额外 DLL，直接正常运行起来了，服不服！以后我写的 Windows 软件，x86 版就支持到 NT 4.0，x64 版肯定能在 Windows 7 上跑起来，arm64 版就不用说了。
https://postimg.cc/gallery/ycGqxM8
[3/3] 话说我自从开始玩 FPGA 以来已经断断续续过去一整年了，除了在我的开发板和那名贵的加速卡上成功跑起了 riscv64-linux 以外（比我那台 RISC-V 笔记本慢多了）并无其他建树。自从前些日子看了几集博洛尼亚大学某博士生的视频教程以后感觉好了很多，确实学到了一些之前不会的东西（但其实所有知识都藏在官网文档里）。可是视频一旦到了写代码（Verilog）环节我就有点儿跟不上了，因为之前从没有把任何一本 VHDL/Verilog 书籍真正看完过。这也不是语言的问题（因为也可以用 C 语言），而是硬件编程本身跟软件编程存在巨大的区别，软件代码只要不写错最多执行慢些，而硬件编程里有很多独特的奇技淫巧或代码组合，如果不那么写可能就根本无法综合或满足时序要求。所以我决定暂时抛开 FPGA 和汗牛充栋的各种技术文档，专攻一本书把 VHDL/Verilog 彻底学会（就是说用两种语言都能写出同样的电路）。
https://postimg.cc/gallery/mLZKJDz
[1/3] 在数字电路里，把迭代循环展开成流水线可以大幅提高吞度量，但要牺牲芯片面积（FPGA 通常最缺的就是这个）；去掉流水线中的寄存器可以大幅降低电路延迟，但要牺牲芯片的最大工作频率；要想提高工作频率可以增加中间寄存器将关键路径打断成较小的路径，但这又重新增加了延迟（不过幸好还有其他办法）。这些还都是小事，最缺德的是实现这些不同的设计思路对应的 VHDL/Verilog 代码从软件编程的视角看起来几乎没什么区别……
https://postimg.cc/gallery/fN34tD3
[2/3] 我靠，前段时间我 ThinkPad P70 的 Windows 10 每次启动都进入 BitLocker 恢复界面要求我输入系统盘的恢复密钥（特别长），我一开始还以为是双启动的 Linux 那边出了什么问题造成的，后来突然恢复正常了我就没在关心这事。结果刚刚看到新闻，原来是微软更新造成的 bug（然后微软又偷偷修复了）。谢天谢地 Window 10 以后停止更新了！
[3/3] 《7旬保洁爷爷因数学手稿火爆全网 谈痴迷数学的缘由：证明定理的快乐 胜过中500万！》我想告诉这位爷爷，用电脑（交互式定理证明器）来证明数学定理比在纸上证更快乐，因为你在纸上证不会有相关专家闲没事来帮你检查，他们十有八九会当你是民科，而你的证明十有八九有错误，最后也就自己图个乐罢了。可要是在某个定理证明器里证出来了，别人检查起来很容易，这些代码可以提交到公共库里，造福后人。
[1/3] macOS 自带的函数图像绘制工具（Grapher），偶尔用一次还真方便。这个小软件跟其他 macOS 系统自带软件几乎没有关系，但是竟然支持数学公式排版输入（否则用户就得再学一门数学语言），高亮显示多条数学曲线中的一条。我早已没有 Mathematica 最新版了，MATLAB 纯粹是浪费硬盘空间，这段时间一直在用 AXIOM/OpenAxiom/FriCAS 来辅助 HOL 定理证明。但画图还是 macOS 原生工具好。
[2/3] 谁能给我点儿提示：都知道指数函数的增长速度超过任何多项式函数，那么对于最简单的一次多项式 cn，其中 c 是一个很大的正常数，如何才能找出一个足够大的整数 n，使得 e^n 大于 cn？
https://postimg.cc/gallery/Q5tYTJJ
[1/3] 不知道从什么时候起，运行在 VMware 里的 Solaris 11 虚拟机一切正常了（VMware Tools 更新了）：屏幕分辨率可以正确设置，鼠标进入和退出虚拟机窗口也完全可用。再装个第三方 GNONE 主题，从来没用过这么舒服的 Solaris 环境。其实 Oracle Solaris Studio 是一个完美的 C/C++/Fortran 开发环境，开发/调试/性能分析一条龙。最重要的是 Sun C/C++ 编译器比 GCC/Clang 对语法和类型的要求更严格，很多其他编译器下面没有警告的代码在 Sun 编译器下面就能看出问题了。
https://postimg.cc/gallery/kdjM5XR
[1/3] 话说过去我在 Ubuntu 物理机上安装 Dropbox 从来没成功过（就是从官网下载 deb 安装包然后按部就班操作），具体现象就是每次启动时它都要重新把安装流程再走一遍（最后我被迫删除之前的同步目录然后再同步一次）。网上也能搜到很多类似的用户反馈，这么多人遇到同样问题一定是 Dropbox 官方的责任。这次我在 Debian 下面我换了个思路，只安装 Debian 官方的 caja-dropbox 包，然后寄希望于此包的维护者，结果一举成功了：MATE 桌面登录后 dropbox 后台进程自动运行，同步操作一切正常！只能说 Debian 开发人员做得更好更专业，每一个官方包都充分测试过，确保开箱能用。
https://postimg.cc/gallery/SjpjCRv
[1/3] 光阴似箭，我在澳洲买的翻新 2019 Intel MacBook Pro 还差一个星期就用满两年了。但是昨天它又无法充电了，于是我第一时间预约了堪培拉市中心的苹果天才吧，今天一早就把电脑送过去了——印象中好像是第五次了，不过距离上次维修已经无故障运行七个月了（几乎就没关过机也很少休眠）。经过一番常规检测，这次估计能给我换主板了，按照7个工作日来估算的话圣诞节之前应该可以拿回来。又赚了一千多澳元的修理费，这台机器的 AppleCare 三年质保买得太值了！反正我有完整的数据备份，手头还有四台电脑（ThinkPad P70、另一台 MBP 2019，Mac mini M4，以及那台不成器的 RISC-V 笔记本），研究工作不受影响。
[1/3] 送修的 MBP 2019
这么快就又修好了（这么短的时间不太可能是换主板），果然圣诞节前就能拿到。但是又来活儿了，拿回来以后还要重装系统，从 macOS 26 降级到 15。
[1/3] 喜提一台 “崭新” 的 MacBook Pro 2019，苹果这次把笔记本电池给我彻底换了。更难能可贵的是，没像以往数次那样直接抹除数据然后无脑重装最新版 macOS（号称可以排除软件故障，这帮天才+傻逼）。这台电脑就算是圣诞节礼物了，我很欣慰[鼓掌]
[1/3] 如果一个连续函数满足 f(0) = 0，那么一般来讲不存在一个邻域 (0,a) 其中 f(x) 非负或非正（图中的函数就是个例子）。但如果 f 的二阶甚至三阶导数都存在，能否证明这样的 “单调” 邻域必然存在？（网上搜了一下但是苦于没找对搜索关键字）
[2/3] 看来我需要把菲赫金哥尔茨的《微积分学教程》第一卷从头看一遍（我需要的答案应该在第四章），系统化地复习一下微分学。这套书很奇怪地从来没有被翻译成英文版（但是有德文版，找不到 PDF），但是因为地域的关系却有中文版，写论文的时候存在一定的引用困难。
[1/3] 在 M4 Mac mini 上试了一下最近流行的 MLX，轻松完成了编译安装，然后抄了一段并行数组加法的示例代码，也跑起来了（我只有 32G 内存应该不够跑大模型吧？）虽然代码看起来挺简洁的，但同样的事情用 OpenCL 来写也行吧？就是麻烦点儿。
[2/3] 女性向男性寻求帮助，如果成功了就是 “牺牲色相” 换来的（所以不但不用心存感激可能还觉得亏了），如果被拒绝或是对结果不满意那就更是亏大了，不恨才怪。
@李清晨
哈哈哈，这个解释有道理，有些恨，就是这么来的[笑cry]
qiazizju:妈呀，冰河居然经历了这个！怪不得那段时间微博发的少了。不知道哪个人举报的，肯定不是当事人
26-1-4 12:32 来自浙江
按热度
按时间
闪金镇猎人:回复@田春冰河:我也马后炮几句。当时看到伞哥在网上发女同事和校长的照片，也觉得有些不妥。当时又想可能微博基本上都是国人在用，澳洲的同事都不会使用，更不会关注到伞哥的微博。没想到可能还有微博的用户直接去写举报信[允悲]
26-1-4 17:11 来自四川
剁椒鱼头6047:回复@田春冰河:呜呜呜[泪]被伞哥感动了
26-1-4 16:20 来自北京
田春冰河
:回复@qiazizju:我不怪你。
26-1-4 16:17 来自辽宁
qiazizju:回复@田春冰河:不过马后炮一下，啥人都有，这种事迟早发生。
26-1-4 15:24 来自浙江
田春冰河
:举报人自然是微博网友了。我记得举报信里也有你的评论，等过两天我都贴出来。
26-1-4 13:29 来自辽宁
qiazizju:国内找个教职吧
26-1-4 12:34 来自浙江
[2/3] 话说回国的飞机上遇到一群尼泊尔人（悉尼-成都-加德满都）回国，我身边坐的是个漂亮的尼泊尔姑娘，周围坐的也全是（但就不是年轻姑娘了）。一开始是她让我帮忙吧手提行李箱搬到头顶的行李舱，坐下来以后就开始攀谈，我知道尼泊尔语跟梵语和印地语关系密切，就说自己能看懂她们的文字，然后她试了一下果然如此，还夸我的字比她写得还好。后来睡觉时她就自然地靠着我的肩膀睡了（我坐过道，她坐中间），分别的时候我送了她一支金尖钢笔。现在这个姑娘每天给我发邮件（带视频）。这年头，指不定哪块云彩上有雨！
李清涛2010:祝福伞哥，比越南那个泳装姑娘身材强太多， 但是感觉性格很强势 感觉不一定准[允悲]
26-1-4 11:39 来自北京
按热度
按时间
在植物园拍鸟才是正经事:回复@田春冰河:发生了什么？？？
26-1-4 17:45 来自浙江
triSCI:回复@田春冰河:[哈哈][允悲]
26-1-4 12:12 来自江西
OwlWinter_:回复@田春冰河:伞哥，推荐阅读这篇文章：http://t.cn/A6DGTIGY她举报了上千人——面具被揭开后，就连受害者都无语了
26-1-4 11:56 来自广东
李清涛2010:回复@田春冰河:[doge]还有其它故事？
26-1-4 11:43 来自北京
田春冰河
:就是这种对别人发的照片视频品头论足的表面善意实际恶意评论让我丢了工作的。
26-1-4 11:41 来自辽宁
mybigfish:第一次就送这么贵重的礼物！难不成要跨越珠穆朗玛峰。
26-1-4 11:27 来自湖北
田春冰河
:我看她用圆珠笔写日记，就帮她提升一下品味。我自己组装的 LAMY 金尖钢笔太多了，回国以后消费降级，今后不再使用彩色墨水，所以钢笔就过剩了。
26-1-4 11:37 来自辽宁
高梁桥行走:回头若干年后一小孩拿着钢笔找你要验dna
26-1-4 14:50 来自北京
田春冰河
:澳大利亚国立大学领导说因为我没删你这条评论（我指的是类似的），就构成了主观性骚扰。
26-1-4 14:51 来自辽宁
[3/3] 话说我送给尼泊尔姑娘的那支 LAMY 钢笔，是我自己组装的，直接买是没有的。其笔尖是 Z58 EF（14K 玫瑰金，部分镀钯），澳洲亚马逊上售价 190 澳元（需要从德国进口）；笔杆是透明的 Safari Vista（自带的钢尖拔下来扔掉），49 澳元；吸墨器是 Z28，3枚售价40澳元。加起来不算便宜了。此笔的特点是笔尖光滑柔软、笔身通透（一眼看出还剩多少墨）、手感也符合人体工学。这才是钱花在刀刃上的好钢笔，谁敢说这不是金笔？
https://postimg.cc/gallery/50BqcLd
千江入海蓝
:LAMY2000不考虑么？
26-1-4 14:38 来自广东
按热度
按时间
田春冰河
:回复@千江入海蓝:我不跟你谈感觉，太主观。
26-1-4 14:42 来自辽宁
千江入海蓝
:回复@田春冰河:黑白款塑料那款，感觉还可以啊
26-1-4 14:41 来自广东
田春冰河
:LAMY 2000 的包尖太小，钱都花在笔杆上了，我看不出它好在哪里。
26-1-4 14:40 来自辽宁
[1/3] 下面公布2025年4月10日18:01和18:31（间隔刚好半小时）澳国立Student Wellbeing 邮箱收到的两封举报信以及随邮件附带的截图证据。我能看到的版本不含有发信人姓名。它们能知道这个邮箱就说明至少有一个是本校的在读学生（我都不知道还有这么个邮箱）。第一封措辞粗鲁，英语水平较差，应该是学生本人；第二封信的措辞相对严谨，英语水平较高，目测是学生她妈。字字凶狠，上纲上线。这还不是全部的证据，后来学校派了一个女的继续调查，正式的指控文件里还有更多的微博截屏（含网友评论）。注意有些话（什么 “东方面孔” 之类的）本不是我说的而是网友的评论，结果也被栽在我的头上了……
https://postimg.cc/gallery/B67Mkb8
芒果自制剧:打⭕️吗，伞哥这么小众的账号，还有人关注，你们这帮乱评论的网友都有责任，我只关注某部经典翻译进度怎么样了[doge]
26-1-5 11:48 来自湖南
田春冰河
:回复@芒果自制剧:不用你提醒，在办了！
26-1-5 15:13 来自辽宁
芒果自制剧:补充一下，待翻译的经典[团圆时刻] http://t.cn/AXbcsR6p查看图片
26-1-5 15:11 来自湖南
[1/3] 下面公布2025年4月10日18:01和18:31（间隔刚好半小时）澳国立Student Wellbeing 邮箱收到的两封举报信以及随邮件附带的截图证据。我能看到的版本不含有发信人姓名。它们能知道这个邮箱就说明至少有一个是本校的在读学生（我都不知道还有这么个邮箱）。第一封措辞粗鲁，英语水平较差，应该是学生本人；第二封信的措辞相对严谨，英语水平较高，目测是学生她妈。字字凶狠，上纲上线。这还不是全部的证据，后来学校派了一个女的继续调查，正式的指控文件里还有更多的微博截屏（含网友评论）。注意有些话（什么 “东方面孔” 之类的）本不是我说的而是网友的评论，结果也被栽在我的头上了……
https://postimg.cc/gallery/B67Mkb8
[2/3] （接上文）后来大学从 HR 部门里派出一个女调查员（外国人，看不懂中文），她不满足于照抄投诉信，又在我的微博里找到了几条我抱怨那个印度女学生用生成式 AI 生成形式化证明代码（完全不可用）的微博，其中某个评论的回复里我提到（所有）印度人都这个尿性…… 这便构成了 “种族歧视”。指控信本身很无聊，附图是证据部分。请各位铁粉们找一下自己的名字吧（注意有些中文 ID 可能被强行翻译成了英文，纯英文 ID 则原样不变）
SwordfishAction:外国人上纲上线这么厉害，还是说就是大学研究机构没钱了就找个理由开人省钱？
26-1-5 12:08 来自广东
田春冰河
:你问谁呢？我怎么知道？你这种问题就跟那些问 “印度人是不是都作弊” 的人一样可恶，你钓鱼呢？
26-1-5 12:09 来自辽宁
SwordfishAction:外国人上纲上线这么厉害，还是说就是大学研究机构没钱了就找个理由开人省钱？
26-1-5 12:08 来自广东
按热度
按时间
田春冰河
:回复@SwordfishAction:我故意刺你一句，你没生气还自己反思了一下，已经算是不错了。更多的人因此就直接把我拉黑，从此反目成仇了。
26-1-5 15:01 来自辽宁
SwordfishAction:回复@田春冰河:你明显情绪激动了，我这评论提问其实也没啥益处和建设性，算了
26-1-5 13:56 来自广东
田春冰河
:你问谁呢？我怎么知道？你这种问题就跟那些问 “印度人是不是都作弊” 的人一样可恶，你钓鱼呢？
26-1-5 12:09 来自辽宁
[3/3] 下面讲一个故事，这件事跟我的其他事可能有关系也可能没关系。2023年10月，网友 @蓓蕾zhu https://weibo.com/u/2299752901 https://weibo.com/n/%E8%93%93%E8%95%BEzhu (账号性别女) 私信联系我（过去可能有过评论交流，属于比较眼熟的 ID），说是广西大学金融专业的，要来澳洲留学，二选一让我给拿主意，还要加微信。我没注意（再说也不是同专业的），只能礼貌地敷衍一下。后来她确定要来澳国立，我就把我所知道的注意事项都告诉她了。某条私信里她说她叫 “钟岷均”，我也没太在意（也许人家女的就叫这个名字），还要加微信。我再次拒绝（我为什么跟一个学金融的本校学生交朋友？）但后来我于心不忍都打算去机场接一下了，但是碰巧当天学院在校外开会就没去成。结果万万没想到，到了2024年2月时来留学的不是个女的，而是个男的（俩人用同一个微博跟我私信）。但我也不清楚具体这俩人是什么关系，就冒昧地猜测是男朋友（实为母子），于是发了一篇微博（微博正文https://weibo.com/1929185323/O0zGTrVG9?pagetype=profilefeed[2/3] 话说一个男的要到堪培拉留学（交换生），拿他女朋友的女性微博 ID 跟我私信联系，问这问那（我知道的那点儿都告诉他了），还多次要求加微信，还说要给我带自家产的茶叶。我也是没好意思直接问性别，但是秉着坐怀不乱、不跟本校任何学生打交道的原则拒绝见面、收礼和加微信。然后这几天按说已经到澳洲了却没消息了，我怕他（她）乱带东西被原地遣返了所以就私信过问了一下，这才告诉我原来是个男的来澳洲。我甚至还好心说过可以去堪培拉机场接一下（但是因为那天刚好系里组织活动就算了），不然肯定接了个寂寞。），谴责网络上伪造性别和共用账号的行为，可能因此就把他们给得罪了。2025年6月这孩子毕业归来，4月的时候大概是觉得毕业定下来了，不管干什么都不影响毕业了。注意，我可没说就是这娘俩举报的，但人数确实对得上。这算不算是处心积虑，伺机报复？咱俩到底谁错了？
https://postimg.cc/gallery/Sm6Gh3L
[4/3] 话说尼泊尔姑娘有每天写英文日记（然后每年换一个本子）的习惯，现在已经抛弃了她原先的破圆珠笔，对我送的金笔爱不释手。回想飞机临降落时她突然问我何时返回堪培拉（她在悉尼某医院里做护工），我知道她有些依依不舍，但不想透露实情，就只说自己要放个长假不知道何时返澳，然后她就不知道怎么回应了。我明白她的意思，于是掏出纸来留下了自己的名字和苹果邮箱（Gmail 主邮箱在国内不能用），说是如有电脑相关问题可以找我。她很高兴，也给我留下了她的。回到家以后还没等我主动发邮件给她，她就先联系我了。其实我在飞机上跟邻座的姑娘萍水相逢的事情不止一次，但最后留不留联系方式也要看情况的。要没这些烂事的话，等我返澳以后可能她真的会从悉尼跑来看我，或者我终于有理由去一趟悉尼市区看看了……
https://postimg.cc/gallery/gXKjWX0
[1/3] 今天去本地电脑城攒了一个小机箱的台式机，就为了把我那个斥巨资采购的 Xilinx Alveo U200 加速卡插进去，然后从 PS5 上拔下了那条我不差钱的时候买的 2TB SSD。内存现在虽然贵但还是配了 32G DDR4；然后机箱电源就是我的雷蛇 Core X 上面拆下来的。现在我终于首次通过了加速卡的自检（它自己说 hello world 运行成功了），终于可以在 Ubuntu 上使用此卡的全部功能了。说实话自从 ANU 要开除我那天我就在想这个事情了，只有回到家乡才有条件弄一个台式机。
https://postimg.cc/gallery/bNJCkDJ
胡乱吃此:伞哥申请一个欧洲的研究岗位吧
26-1-6 16:29 来自法国
田春冰河
:回复@qiazizju:switch2 我没买，switch 我自己玩着呢，你继续等吧……
26-1-6 17:16 来自辽宁
田春冰河
:回复@qiazizju:你盯上我的东西可不止一次了。上次是什么来着？
26-1-6 17:07 来自辽宁
共5条回复
HelloWorld_cpp:ANU的事情已经定下来了么？
26-1-6 17:50 来自山东
田春冰河
:这不是废话么？我人都回来了
26-1-6 17:51 来自辽宁
田春冰河
:注：此卡要求 PCI Gen3 x16 接口，笔记本电脑接 eGPU 扩展坞最大只能达到 x4，无法正确连接此卡的预设功能（但是可以当做通用 FPGA 设备来用）。
26-1-6 16:19 来自辽宁
畅想_2049:不巧啊，整好是涨价时
26-1-6 16:24 来自河南
田春冰河
:内存价格涨了一倍。
26-1-6 16:45 来自辽宁
丨Moonrise丨:回复@田春冰河:涨了三倍[允悲]
26-1-6 16:49 来自北京
[2/3] 知乎上看到一篇对我的评论文章（网页链接）。其实我导师确实有帮我联系新的工作机会：一是去瑞典参与 CakeML 项目（基于 HOL 的 ML 系语言编译器），二是去新加坡加入另一个资深 HOL 用户的团队搞形式化的安全验证，都是我很熟悉甚至见过面的人。而且开除这个事情原本是保密的，只要我自己不说，ANU 也是不会说的。但我觉得没有不透风的墙，回头人家问我为什么离职我总不能编瞎话吧？另外，我也有自己的研究计划，如果立刻去其他地方工作的话我就再也没时间干自己的事情了。所以我就婉拒了，说等一两年后再考虑。另外我还有澳洲的永久居留权（PR），五六年之内随便往返澳洲。
[3/3] 今天攒的这个台式机花了 3300 元（其中 1140 元是两条 16G 内存，570*2），我自己的机箱电源、固态硬盘。这个 12th Gen Intel i5-12400 (12) @ 4.400GHz 看着挺高端的（6核12线程?），并行算法测试表明也就比我的 2019 MBP 快了最多不到百分之五十。P. S. 尼泊尔姑娘继续每天给我发问候邮件，图3是从尼泊尔看喜马拉雅山。
https://postimg.cc/gallery/Sxz3w2K
[1/3] 按说我此次 “衣衫褴褛还乡”（姑且算是 “衣锦还乡” 的反义词），就应该众叛亲离、大家偷着乐之余避之唯恐不及。可事与愿违，还是有亲人惦记我（算计我），看我回家了就想第一时间来看我。我后来想明白了，比失业的人更惨的其实大有人在：那就是死人和病人。在东北，没钱算什么大事？没病就等于凭空多了几十万存款。而且身体上的疾病尚且有药（只要不是绝症），精神上的疾病（包括没病但就是长期想不开）那才叫无药可治，只有等死。我是个要脸面的人，向来主张 “饿死事小、失节事大”，这辈子没干过亏心事，如果将来我钱花完了还没找到工作也没取得重大学术成果就自己体面地走，根本不用得病。指望我来给谁养老，指不定我就走在您前面了（图文无关）
乔瓦娜的意大利语频道
:千言万语化作一句forza！
26-1-7 14:57 来自浙江
田春冰河
:谢谢老师[微笑]
26-1-7 14:59 来自辽宁
忧桑的coding:伞哥来我学校吧，二本小院校，入职没有岁数限制，无非升即走，无科研压力。可以选个大课题慢慢做。[微笑]
26-1-7 13:28 来自河南
田春冰河
:您哪个学校啊？
26-1-7 14:19 来自辽宁
田春冰河
:回复@忧桑的coding:我的科研不用经费，自己笔记本电脑就够了。安家费也不必了，租房挺好的。那麻烦你有空帮我问问领导，只要学校不在乎我是被 ANU 开除的，半年到一年以后我可以考虑过去。
26-1-7 16:18 来自辽宁
共9条回复
storm_house:我被焦虑症折磨10余年，近两年规律服药，舍曲林+枸橼酸坦度螺酮，状态平稳很多。之前每天心情就像是，刚睡醒就已落日黄昏
26-1-7 13:23 来自河北
田春冰河
:对不起我没有不尊重病人的意思啊！有病治病，谁都可能得病。
26-1-7 13:28 来自辽宁
[1/3] 终于首次完全在 Windows 下（借助 WSL 里的 Ubuntu）成功地给我的 Xilinx Alveo U200 加速卡重新编程，跑起了一个 32 核 riscv64 的 Linux 环境（Debian 13），FPGA 芯片资源用了 80%（已经很高了），CPU 主频应该不超过 300MHz。整个系统是个无盘站，连根目录都是 NFS 挂载的，然后通过 10G 以太网连在家用交换机上，可以正常上网（之前在学校里反而不行）。现在正在安装软件，然后试试多核并行计算的性能。
https://postimg.cc/gallery/pj4z1kt
[2/3] 闲着也是闲着，下面公布我对大学指控信的辩解信全文。我的主要论点：1. 对女性气质和业余爱好的真诚赞美是否算性骚扰；2. 学生作弊在先，教师作为受害者不点名公开批评也不行？3. 校长自身行为不检点，不尊重（调侃）不值得尊重的人也有错？4. 别人的评论我不负责且没有义务（及时）删除。
https://postimg.cc/gallery/97qStj9
[3/3] 我这个价值几十澳元的小交换机太值了，4个2.5G电口和2个10G光口，我用一个光电模块把其中一个光口转电口以后连 M4 Mac mini 确保满速；第二个光口用 40G 转 4*10G 光纤连到 FPGA 加速卡上；其他几个口通过 USB-C 转 2.5G 转接器连其他电脑；最后还有一个连到家用 WiFi 上。
七宫和猫吃烤鱼:这种小交换机买来家用真的非常香[笑cry]
等比图
26-1-8 23:26 来自湖南
田春冰河
:这个比我的还好，带管理和VLAN功能
26-1-9 07:55 来自辽宁
雁南飞_Oo:[doge]有网管功能吗？什么牌子的？
26-1-8 21:39 来自广东
按热度
按时间
雁南飞_Oo:回复@田春冰河:那就放心了，虽然中美一直不对付，国内电子通讯产品价格依旧还是有优势的
26-1-8 22:06 来自广东
雁南飞_Oo:回复@田春冰河:是啊，国内有个iKuai 爱快的小品牌，长得非常像你手上这个，160元左右！
26-1-8 21:57 来自广东
田春冰河
:回复@雁南飞_Oo:国内同类型的6口交换机也就100多元
26-1-8 21:48 来自辽宁
雁南飞_Oo:Binardat，国内没卖
26-1-8 21:43 来自广东
[1/3] 我发现网上有很多二尾(yǐ)子们连 “二尾子” 这三个字怎么写都不知道，还来给我纠错顺便讽刺我呢。但凡读过《红楼梦》和几本贾平凹小说也不至于连这都不知道，你们的语文水平还不如我一个搞计算机的，对得起中学语文老师和你们的二尾子身份吗？
https://postimg.cc/gallery/tYf9hCs
[2/3] 昨天在 Alveo U200 上成功运行了 32 个 riscv64 CPU 的 Linux 以后，性能测试放弃了——基于 R 的性能测试目测比我的笔记本慢 500 倍…… 后来我回到此卡推荐的使用方式上——作为数据中心加速卡，结果也不太顺利。Xilinx 的天才硬件工程师们在 FPGA 上实现了一个可动态修改自身部分电路的加速器——PCI 接口部分的电路保持不动，特定计算的电路可随时加载后执行。它的 OpenCL 接口就只支持 1.0 版本，设备类型是加速卡（而非 CPU 或 GPU），如果跟着 OpenCL 教材走的话立刻就会遇到无法以源代码的形式定义核函数的困难——必须在相同或另外的机器上用 Vitis 软件编译可加载的电路模块然后以二进制形式加载。我现在想知道在典型应用（比如深度学习和大模型）中我这块卡到底对标 NVIDIA 哪个 GPU，以及如何把 “典型应用” 实际跑起来……
https://postimg.cc/gallery/43xQF4T
