田春冰河

2026-07-01 20:12来自 微博网页版

[2/3] 今天试着写了一段 AXIOM 代码（简单的选择排序），然后发现这个软件与其说是个数学软件，不如说是个强类型通用编程语言——比 ML 系还要强类型。AXIOM 编译器实际干的事情就是把它的语言代码转译成 Common Lisp（但是几乎不可读），然后剩下的事情就交给 Lisp 编译器了。至于它作为数学软件的各 ​

1

0

15

田春冰河

2026-07-01 19:29来自 微博网页版

[1/3] Mathematica 官方文档里的各种画图代码，真的是…… 好不容易才看懂，专家写的示例代码一不小心就把整个语言里所有精妙的设计全用上了。三大数学软件里要单论画图的话，这软件排第一毫无问题。但是最难能可贵的是，这个语言的背后是一个类似 Lisp S-表达式的系统——所有的特殊符号和语法糖背后 ​

1

2

26

田春冰河

2026-06-30 18:52来自 微博网页版

[2/3] 我 2014 年在博洛尼亚大学期间有一门 “计算数学” 的课程讲的是 Mathematica。虽然学校在机房里提供了软件，但我为了使用方便直接花 240.5 欧元买了个学生版，当时是永久序列号（而且最多可以安装两台电脑）。根据我的邮件记录，这个一口价的软件它一直给我免费更新到了 2021 年，最后的版本是 ​

1

7

26

田春冰河

2026-06-30 18:35来自 微博网页版

[1/3] 没想到 GNU Common Lisp (GCL) 的作者从年初开始发力，竟然成功地把 GCL 移植到 ARM64 macOS 上了。我使用来自 Debian 镜像的最新 Axiom 源代码（带有 Debian 维护者的补丁），只改了几行老式 K&R C 代码就成功地在 M4 Mac mini 上编译运行起来了（去年底的时候我还试过，无论 OpenAxiom 还是 Fr ​

2

3

25

田春冰河

2026-06-21 09:25来自 微博网页版

[1/3] 我的正版 Windows 7 旗舰版（VMware 虚拟机），大约 2012 年安装的，内有我当年斥巨资采购的正版 Acrobat XI Pro，FrameMaker 12, FileMaker Pro 12 和 Office 2010 等重要软件，目前是我打开和编辑微软 Office 文档的唯一正规渠道（再没有其他 Office 套件了）。唯一的痛点是自从去年开始已经收 ​

1

3

25

田春冰河

2026-06-20 17:33来自 iPad Pro

[1/3] 没想到我的意大利硕博母校都挺争气的，一直保持在世界 500 强之内（尤其是读博的地方，山坡上那么小的一个学校）。就因为这个数字（500），甚至有望拿到某市的人才补贴…… ​

0

7

61

田春冰河

2026-05-19 14:26来自 微博网页版

[1/3] 终于完成了无类型 λ-演算中 Böhm 分离定理的形式化证明，改进了去年 ITP 2025 论文里给出一个较弱的结果。一个多月时间，1万多行新代码，不简单，因为前面证的所有那些引理（根据直觉）究竟有没有用，只有到了最后一天才能知道。那些在其他定理证明器里搞 λ-演算形式化的人，我只能呵呵了，几 ​

4

27

96

田春冰河

2026-04-12 12:48来自 微博网页版

[1/3] 当初我从澳洲返回国内时犯的最大错误就是没把我那两瓶没用完的白金（Platinum）碳素墨水合二为一带回来，而是只带回了一瓶鲶鱼（Noodler's）的非碳素黑墨水。鲶鱼墨水初次使用时看起来黑度更高，可一旦装在钢笔里长期不书写的话就会因为氧化而褪色，第一笔写出来经常是透明的，然后接下来是掺水 ​

1

25

43

田春冰河

2026-04-11 20:27来自 微博网页版

[1/3] 我一年前写的形式化证明（λ-演算相关的），我自己只能勉强看懂，这是还多亏了当初在注释里留下的 ASCII 插图。至于这个单体 4000 多行的证明，我已经不敢想象自己竟然写出来了（被逼上绝路的产物）。现在要改进这个证明（恐怕要膨胀到单体 6000 行的程度），为了找回手感我只能从头到尾把我自己 ​

1

9

51

田春冰河

2026-04-08 10:59来自 微博网页版

[1/3] 《哈利波特》衍生（同人）小说《[HP]魔法界的生活》（作者：夏夜的小猪，故事主人公：水蓝儿），以及由此再衍生出的（吐槽）小说《 [HP]和玛丽苏开玩笑》（作者：打酱油而已），终于被我蹲厕所逛小红书的时候意外发现了…… 这个世界的阴暗面还真多[允悲] ​

1

2

4

田春冰河

2026-04-03 16:54来自 微博网页版

[1/3] 跟根本不会用 Git 的人在一个仓库里一起写代码，想死的心都有了。烂泥扶不上墙。 ​

5

13

30

田春冰河

2026-03-27 07:13来自 iPad Pro

[1/3] 早上一觉醒来，CICM 投稿截止时间延期了两周（昨晚我临睡前检查还没有呢）。关键是学生也把最后一个定理证完了，现在也建议投稿。那就没什么可商量的了。CICM 会议没有 CCF 评级（事实上也等级不高，因为每年的投稿也就不到50篇），但这可是形式化数学最对口的会议，录用门槛其实不高（当然前提 ​

0

4

43

田春冰河

2026-03-26 16:51来自 微博网页版

[3/3] 经人指点，今天我才第一次注意到《中国计算机学会推荐国际学术会议和期刊目录》。原来我博士期间的论文有1篇A类，2篇B类（其中一个其实是B类会议的下属workshop）和3篇C类，就算是不多不少，很平庸的科研工作者吧。而我最后发表的，同时也是最看重的成果（Böhm 树的那篇）所在的交互式定理证明（ ​

1

18

48

田春冰河

2026-03-26 12:39来自 微博网页版

[2/3] 我发现不同的概率论书籍里的 “李雅普诺夫”（俄文：Ляпунов）的英文拼写不尽相同，至少有 Lyapunov, Lyapounov, Ljapunov, Liapounov 四种。所以我听谁的？我不可能翻遍所有的英文教材然后取多数意见。想来想去我决定听俄罗斯数学家 Albert N. Shiryaev 的，在论文和代码中一律使用 “Ly ​

0

6

29

田春冰河

2026-03-26 11:55来自 微博网页版

[1/3] 上午在本地宏伟的图书馆里写论文，把 LaTeX 模版和定理自动导出 LaTeX 调通了，然后写了个摘要。我（前）导师是个学术上非常可靠的人，只要我能把整篇论文大致写个草稿，他就能帮我改到天衣无缝、每投必中。所以虽然他在我离职的事情上没帮我说话（再说也帮不上忙），我一点儿都不怪他。我现在就 ​

0

10

41

田春冰河

2026-03-25 22:27来自 微博网页版

[4/3] 一边写概率论形式化的论文（刚准备好模版），一边重操旧业开始为下一篇 λ-演算形式化的论文写代码。早上收到学生的回复说时间太紧了建议一周后的 CICM 就不投了；我尊重学生的意见（但我还是会把草稿尽快写出来好让他俩帮忙改）。导师则回信建议投 ACM 主办的 CPP 2027（POPL 2027 的子会议，真 ​

3

11

45

田春冰河

2026-03-25 21:51来自 微博网页版

[3/3] 我回国以后最大的欣慰就是 GitHub 虽然时断时续但还是有能用的时候的，因此我的定理证明工作未受影响，趁着网站能连上的时候 pull request 照发不误。别人写不出来的形式化代码我能写出来，眼下这就够了。其他都是次要的。 ​

4

13

46

田春冰河

2026-03-25 07:27来自 iPhone SE

[2/3] 小龙虾（鳌虾）赞大龙虾，都不是同一个物种，能是真心赞美吗？这个带 lobster 的名字估计是丁总亲自给起的，有道词典的人对英语有深刻理解绝不会犯这种“河马非马”的错误。

#OpenClaw之父评价中国龙虾#刚才朋友转给我一张X上的截图，OpenClaw那老哥（创始人）点赞了有道的LobsterAI。 关键不是点赞，关键是截图里显示他是在一排“中国龙虾”里挑出来的，31个里面单点了这一个。 这就很有意思了。现在的AI圈有点像当年百团大战，各家都在发“龙虾”牌照。但能被原教旨主义的 ​

0

9

6

田春冰河

2026-03-25 06:04来自 iPad Pro

[1/3] 北京时间 3月25日 早上6点，折算成论文投稿截止日期使用的 AoE（Anywhere on Earth）时区，其实是24日的早上10点，距离CICM 2026 目前的摘要截止时间还有一天零14个小时呢，绰绰有余。别说摘要了，写完整篇论文初稿应该都够了…… （这个app真是养兵千日 用兵一时） ​

1

6

26

田春冰河

2026-03-24 23:09来自 微博网页版

[6/3] 我查了去年的 CICM 2025 会议网站，投稿截止日期确实延长过两周。去年那个时候我和我的学生本以为能赶上投稿，结果日期临近发现无法完成所有证明（没想到我就这么一直写呀写的，多写了一年时间。）这样的话投稿时间应该足够了。我写完论文草稿以后回过头来帮学生写代码都来得及。这个会议其实规 ​

0

5

23

田春冰河

2026-03-24 22:41来自 微博网页版

[5/3] MLGBD，我运气太差了，今年的形式化数学 “顶会” CICM 2026 的摘要投稿截止日期就是明天，然后一周内提交完整论文，时间太紧了。这种论文我写一篇只要三四天就够了（上次的 ITP 论文也是不到一周时间写完的），但是现在还差一个引理的证明外包给学生了，她未必能按时完成。现在唯一的希望就是会 ​

0

10

26

田春冰河

2026-03-24 22:11来自 微博网页版

[4/3] 概率论中心极限定理（李雅普诺夫的版本）的形式化证明基本完成了。我这边已经没什么可写的了，还剩最后一个比较麻烦的积分运算（正态分布的四次方）外包给我的越南学生了（毕竟她是论文的第一作者）。我就等她先向 HOL4 提交 PR 然后我就可以提交我的代码了（过去一周时间写了四千多行）。同时我 ​

0

1

19

田春冰河

2026-03-24 18:22来自 微博网页版

[3/3] 自从多年前把小时候听过的一段乐曲（用手机键盘弹出来）发到微博上被热心网友识别出是肖斯塔科维奇的第七交响曲《列宁格勒》以来，我就对肖斯塔科维奇及其一生创作的15部交响曲产生了浓厚的兴趣。我本来在 iTunes 里买了他的全集，但前两天突然想到或许可以再听听其他指挥家的版本（尤其是俄罗斯 ​

3

14

33

田春冰河

2026-03-24 16:30来自 微博网页版

[2/3] 也许有人觉得形式化（数学）证明就是把书上的证明过程在定理证明器里换个语法抄一遍，就是个纯工程性的行为谈不上科研，那你可能是对的但经常是错的。那些书面证明要真是 “完全正确的”，运气好的话连语法都不用改，真的可以逐行抄下去，但你未必有这种 “运气”。比如图1是中心极限定理某个版 ​

3

8

53

田春冰河

2026-03-24 15:54来自 微博网页版

[1/3] 最近我的感受是：那些较大的大模型有时太聪明了不好骗（拒绝回答我的问题），反而相对较小的那些相对耿直一些，问什么答什么。这跟企业用人似乎异曲同工…… ​

0

6

14

田春冰河

2026-03-22 19:04来自 微博网页版

[1/3] Lean 数学定理库现在充斥着大量 AI 生成的 PR 代码，都用 LLM-generated 标签标记出来了。我随手挑了几个有意义的标题（那些重构改名类的除外），目前还没发现一个被合并的。2300 多个等待合并的 PR，昨天一天合并了 74 个，最大的也就100来行改动。几百人一起号称构建整个形式化数学，绝大多数 ​

1

4

14

田春冰河

2026-03-21 22:23来自 微博网页版

[2/3] 我还有最后三个（相似的）小引理就完成了随机变量依分布收敛的一个重要等价定理，进而相当于完成首个超越 I.I.D. (独立同分布) 情形的更复杂的中心极限定理（CLT）的形式化证明了，HOL4 重夺兵器谱排名第一位（之前 Isabelle/HOL 下有人完成了中心极限定理的 I.I.D. 版本，那个基于特征函数的证 ​

0

3

30

田春冰河

2026-03-21 17:52来自 微博网页版

[1/3] 拉赫玛尼诺夫第二和第三钢琴协奏曲加起来总长度 79 分钟（iTunes Store 上的版本），分别来自我很久以前购买的两张专辑。但由于 CD 刻录盘的长度是 80 分钟（700MB），比那种批量压制的 CD 光盘（应该是最大只有 650MB，不知道为什么）大一些，所以幸运地被我刻录在了同一张盘里。 ​

0

2

11

田春冰河

2026-03-17 20:26来自 微博网页版

[3/3] 话说 ollama 的 Modelfile 格式跟 Docker 的 Dockerfile 很像，允许用户以原有的模型为基础构建自己的模型。我不知道这个构建过程究竟有多大灵活度（比如在嵌入的额外文本消息之外是否允许用户用自己的大量数据继续训练现有的模型），但这就表示我目前的用法（拉取模型后直接问它问题）其实还是 ​

3

13

22

田春冰河

2026-03-17 20:10来自 微博网页版

[2/3] 过去几天里我着实试用了一下大模型（仅限于 ollama 命令行）。我之前的 2+2 实验是模型没选好以及任务安排错误，因此产生了错误的结论。后来经网友指点，我试了几个不同的大模型之后发现表现最好的还是阿里千问的 qwen3.5。我的 M4 Mac mini 能流畅地跑 9b 版本；最多可以跑 27b 版本（大约每秒 ​

7

25

38

田春冰河

2026-03-17 19:02来自 微博网页版

[1/3] 唉，卡了我三个月的（微积分）定理，终于证出来了…… ​

1

18

110

田春冰河

2026-03-14 23:47来自 微博网页版

[3/3] 话说去年底回国前夕我的形式化证明（中心极限定理的一部分）卡在一个可以交换偏导数和积分号的 “小” 定理上，但是我在《Measures, Integrals and Martingales》那本书里找到的版本带有苛刻的前置条件，在应用的时候根本无法满足。1月中旬的时候无意中在同一本书的某章习题部分找到了另一个版本 ​

0

5

44

田春冰河

2026-03-14 22:50来自 微博网页版

[2/3] 不论性能如何，ollama 的安装文件在 macOS 下最小（70MB），解压之后除了主程序就只有 MLX 库而已。我目前无法高速访问 GitHub（而且时断时续），唯一能下载的也就只有 macOS 版本的 ollama 了，然后正好运行在 M4 Mac mini 上（性能还不错）。 ​

1

12

21

田春冰河

2026-03-14 09:16来自 微博网页版

[1/3] 试了一下传说中的大模型。问它 1+1 的时候还好，2+2 就突然开始不着调了。幸好这是纯本地部署的，要是付费的云模型是不是 10 块钱就没了？这玩意真有用么？ ​

2

50

44

田春冰河

2026-03-07 19:18来自 微博网页版

[2/3] 安装了一个新版 Solaris 11 虚拟机（以及 Oracle 19c），想来想去还是不玩 Solaris 物理机了，因为我不喜欢双启动（总是会切来切去）。跟我手头原有的 Solaris 11 虚拟机相比的话内核版本从 11.4.42.111.0 升到了 11.4.90.212.0，看起来不小。其实这些年 Oracle 一直在默默更新 Solaris 11，不断 ​

1

8

17

田春冰河

2026-03-07 00:06来自 微博网页版

[1/3] Oracle 真是良心发现，竟然发布了一个新的 Solaris 11 编译环境，就在 4 天前，而且还被我意外发现了。我准备找一块闲置硬盘（首次）装个 Solaris 11 物理机。 ​

0

4

16

田春冰河

2026-03-03 18:38来自 微博网页版

[6/3] 话说当初 Git 刚出现的时候我一直不理解它的 “分布式” 究竟体现在哪里，因为从表面上看 Git 相比 SVN 最大的不同无非是 Git 能把整个仓库的全部信息都克隆到本地。除此以外，还是有那么一台中央 Git 服务器，然后每台机器上的 Git 客户端去同一个中央服务器（比如 GitHub 上的）推拉代码。我现 ​

7

12

48

田春冰河

2026-03-03 17:09来自 微博网页版

[5/3] 薛之谦？从来没听过他的歌。李雨桐，名字好像有点儿耳熟，莫非是她？然后上网一查，原来耳熟的那个叫李一桐[笑cry] ​

2

7

4

田春冰河

2026-03-03 16:07来自 微博网页版

[4/3] 我发现英语里有时情态动词 “should” 会出现在连词的位置上引导一个条件状语从句（大概相当于一个委婉的 if 或者 when），有什么合理解释吗？ ​

1

10

19

田春冰河

2026-03-03 12:58来自 微博网页版

[3/3] 话说我十年前买的 Bose QC35（第一代）耳机的连接线已经包浆了，虽然还能用但是打算换一根。其实那就是一根 3.5mm 转 2.5mm 的标准音频线，但是 2.5mm 插头那端要保证可以稳定地插上不会轻易脱落。号称原装的线在京东上普遍卖 50 元，关键是那根线很细，看起来弱不禁风的。我幸运地找到一个绿联 ​

0

19

15

田春冰河

2026-03-03 12:02来自 微博网页版

[2/3] Oracle 数据库 26ai free，表面上看挺有诚意的，其实资源限制还挺大的，简单地说就是跟过去（Express Edition）一样，CPU 只支持双核，内存只支持 2GB，数据库本身不能超过 12GB，基本上难堪大用。如果一个项目要用到数据库并且必须控制成本的话（甚至规定必须用国产数据库产品），那么应该肯定 ​

0

9

6

田春冰河

2026-03-03 11:45来自 微博网页版

[1/3] 科研工作往往离不开数据处理（尤其是 AI 和大模型相关），管理各种数据最佳的方式是把他们存储到关系型数据库里，可到了查询数据的时候往往受限于数据库查询语句的能力，比如标准 SQL 语言最多支持用 LIKE 匹配带有通配符的字符串，然后每个数据库平台都有自己的正则表达式扩展。但要想做到搜索 ​

3

3

19

田春冰河

2026-03-02 20:10来自 微博网页版

[1/3] 在 Linux 下安装 Oracle 数据库最新版本（26ai）已经相当方便了，因为可以通过 rpm 包来安装了（只支持 Oracle Linux 8 或 9），完全绕过了那个传统的 Java 写的安装程序。但是对新手来说还是有几个小坑，比如远程连不上 1521 端口（即便防火墙关掉也不行），默认创建的可插入数据库（PDB）一旦 ​

2

1

17

田春冰河

2026-03-01 22:01来自 微博网页版

[1/3] 跟着 Oracle 10g 数据库文档学习新知识，结果在执行一个叫 CTX_DDL.CREATE.INDEXT_SET 的存储过程的时候卡住了（语法错误）。我可以想象当年那些同样照着文档学习的人会有多困惑，甚至会怀疑遇到 bug 了（打的补丁不够）。我很幸运，打开 12c 的对应文档发现这个存储过程少了一个字母，变成 ​

1

3

23

田春冰河

2026-02-27 22:53来自 微博网页版

[2/3] 这几天在玩 Oracle 数据库，终于学会了 LispWorks 的 Oracle 大对象（LOB）接口，然后成功地把我一张含有图片数据的 “重要” 表从 FileMaker Pro 里读出来（通过 ODBC）再转换格式后插入到跑在 Windows 10 物理机上的 Oracle 数据库里（版本是 12c 和19c）。这里面涉及到时间格式、中文编码，OD ​

2

1

31

田春冰河

2026-02-27 22:18来自 微博网页版

[1/3] 将CD光盘上的音轨通过iTunes软件导入到电脑里（然后就可以脱离CD光盘来播放了），这件事我好像已经十多年没干过了（幸好我的ThinkPad上还有个光驱）。不为别的，我就想对比一下同一个耳机从电脑和CD随身听上听同一首歌，到底有没有区别（应该是有，但我不确定我那不值钱的耳朵真能听出来）。 ​

1

4

9

田春冰河

2026-02-26 18:45来自 iPhone SE

[2/3] 刚刚听完了一张迪克牛仔的老 CD，真好听。相比之下，前几天春节晚会上那些歌都是什么玩意儿…… ​

1

10

36

田春冰河

2026-02-26 16:28来自 iPhone SE

[1/3] 当年高考结束后买的 CD 随身听，25 年过去了竟然还能用（新买了两条口香糖电池），不过原配的耳机只有一只能响，被我给扔了，换上 Bose 降噪耳机似乎音效更胜当年。最难能可贵的是当年买的那些 CD，凡是盒上印着 “正版CD品质保证” 的，也都还能听！ ​

2

19

48

田春冰河

2026-02-25 16:49来自 微博网页版

[2/3] 话说 Emacs 的单字符方向快捷键主要根据对应含义的英文单词，上下左右分别是 C-p (previous) C-n (next) C-b (backward) C-f (forward) ，一旦理解了就很好记了；至于以单词、句子和段落为单位的移动快捷键我从来就没记住过。Vim 的方向键则是为了操作方便，比如上下左右分别是键盘上相邻的 kjhl ​

1

5

14

田春冰河

2026-02-25 14:41来自 iPad Pro

[1/3] 原来我昨天买的这种叫做60%键盘，只有五排，且右下角没有方向键。但是安装了专门的驱动程序以后就可以把方向键重新映射到右下角那些多余的Ctrl和Alt等键上（我设置的是需要同时按下Fn键），这样就完美了，竟有些爱不释手，想用它多写点儿代码。看来物品不在贵贱，自己喜欢就好。 ​

0

31

21

田春冰河

2026-02-24 16:04来自 微博网页版

[1/3] 今天去本地电子市场给电脑机箱买风扇，顺便买了狼蛛（AULA）MINI 60HE Pro 磁轴键盘。之前我就想买个独立键盘，希望同时连接多台电脑并可以快速切换。我先是看了看传说中的樱桃、雷蛇等高端品牌，觉得太贵了（400+，市场里大部分杂牌键盘也要300多）最后图便宜才买了这个。此物外观典雅大方、做 ​

6

19

49

田春冰河

2026-02-14 19:58来自 iPhone SE

[2/3] 我在 GitHub 的 vivado-risc-v 项目贡献者里已经排到第五位了，在定理证明领域之后勉强开辟了 FPGA 新赛道。 ​

0

6

75

田春冰河

2026-02-13 18:05来自 微博网页版

[1/3] 终于把我 Alveo U200 加速卡上的全部4条16GB DDR4内存都利用起来了，成功搞出了一个16 核 riscv64 加 64GB 内存的 Linux 无盘站，可惜主频只有 100MHz，再高就无法满足 FPGA 的时序要求了。原来每条 16GB 内存都需要一个独立的 DDR4 内存控制器，每个控制器占用约2万个 LUT——比一个 riscv64 CP ​

2

2

24

田春冰河

2026-02-08 22:38来自 微博网页版

[2/3] 学会写自定义 VHDL 库函数（工具包）了。其实 VHDL 语言里有很多结构是无法综合到硬件的（比如实数的运算等），但这门的语言的思想跟 Lisp 有些相似——如果运算发生在 “编译期”（硬件里只需要一个计算结果）那就什么都可以算了，包括递归函数。我原本输出的硬件里有个最大值为1亿的计数器，偷 ​

2

7

10

田春冰河

2026-02-08 16:40来自 微博网页版

[1/3] 今天一整天就写了一段代码——把我昨天那个用 LED 灯当计数器的代码用 VHDL 重新实现（不用软核处理器），结果连续遇到各种困难。一开始不知道如何转化开发板上的差分信号时钟，然后不知道怎么在 VHDL 里定义保存中间结果的寄存器——我需要一个很长的整数保存时钟循环数，每当达到1亿次（100MHz ​

1

3

21

田春冰河

2026-02-07 13:48来自 微博网页版

[1/3] 成功地实现了一个比 hello world 略复杂的 FPGA 嵌入式应用。我把开发板上的 LED 灯（总共 8 个）连在软核处理器上，这样它就在系统总线上被分配了一个地址段。将硬件导出成 Vitis 下可用的 BSP 包时，这个地址段被写在一个 C 头文件里。只要我用专门的函数将一个数字写在这个地址上，这些 LED ​

6

8

18

田春冰河

2026-02-06 16:26来自 微博网页版

[2/3] 原来 Linux 无盘站既不需要网络配置文件，也不需要在 fstab 里挂载根目录，更不允许有（远程）交换分区，它的网络和 NFS 配置完全是在启动时通过内核参数传递的。只要局域网络稳定、速度够快，经过 NFS 的硬盘 I/O 就不太会成为瓶颈，至少在使用 FPGA 软核 CPU 时不会。 ​​​​

0

0

9

田春冰河

2026-02-06 09:17来自 微博网页版

[1/3] 这应该是足以载入电脑装机史册的（奇怪）配置，Alveo U200 加速卡和 Digilent Genesys2 开发板被我塞进了同一个电脑机箱，解决了开发板长期以来暴露在外、缺乏保护的问题。该机可同时用于学习基于 FPGA 的数据中心加速和嵌入式系统等应用，其中加速卡走 PCIe x16 接口，开发板使用网桥连在主板自 ​

1

6

24

田春冰河

2026-02-05 17:39来自 微博网页版

[2/3] 原来网桥还可以这样用。我的 Linux PC 上因为额外插了块 2.5G 网卡，现在有两个网口。我把它们桥接在一起，这样理论上两个网口哪个插网线都能用，如果都连到交换机上也不会出错，算是负载均衡或高可用解决方案。但还有更妙的应用：我的 FPGA 开发板也要连网但是交换机上没有额外端口了，现在它就 ​

0

8

14

田春冰河

2026-02-05 16:36来自 微博网页版

[1/3] 昨晚尝试给我在 Genesys2 开发板上用开源 vivado-risc-v 项目生成的软4核 riscv64 处理器 “超频”——把主频从满足时序要求的 62.5MHz 提升到 100MHz，然后尝试 Vivado 的各种时序优化策略，最后虽然有少许时序警告但实测表明这个软核处理器实打实地以 100MHz 稳定运行起来了。其实 1ns 的启动 ​

1

0

10

田春冰河

2026-02-04 20:44来自 微博网页版

[3/3] 前段时间提到的那本用 Vitis HLS 实现 RISC-V 处理器的书我还在看，今天终于成功运行了配套的源代码（在 GitHub 上），亲眼目睹了用 C 语言实现的 RISC-V 指令解码。这些 C 代码既可以用普通编译器编译执行，也可以在转换为 Verilog 以后通过仿真程序跟测试代码一起执行，而且看起来对 FPGA 的资 ​

6

0

32

田春冰河

2026-02-04 10:51来自 微博网页版

[2/3] 原来 Xilinx Kintex7 上的 Microblaze 软核处理器，200MHz 是可以满足时序要求的，而内存控制器原本输出的 225MHz 就爆掉了，就差这么一点点。这个事情很可能跟 Vivado 和相关 IP 的版本也有关系，几个版本之前可能还是可以支持 225MHz 的。所以芯片的制程提高以后，原有的设计由于电路更短，晶 ​

0

0

14

田春冰河

2026-02-04 09:01来自 微博网页版

[1/3] 终于成功地把 Xilinx FPGA 开发板的嵌入式开发流程走通了，成功地在 Microblaze 软核上运行了一个 hello world（输出到串口）。价值 8000 多元的开发板，目前我就能跑一个 hello world…… 这个 C 程序的代码是现成的，但是开发板的电路图是我在查询大量文档后自己画的，因为每个板子的情况都不 ​

2

7

24

田春冰河

2026-02-03 23:43来自 微博网页版

[1/3] 话说苹果两天前突然给我的第一代 iPad Pro 推送了 iPadOS 16.7.13 更新。我挺高兴的，因为已经好多年没升级过了。结果折腾了两天，死活无法安装（莫名其妙的错误信息），我甚至把整个 iPad 重置了然后先从 iCloud 备份恢复（几乎下载了一整天）再尝试升级系统也不行。结果刚刚抱着试试看的态度又 ​

1

7

11

田春冰河

2026-01-31 10:15来自 微博网页版

[1/3] 金晨事件，完全是那条农村散养不栓绳的那条狗的责任。演员最重要本钱的就是脸，脸受伤了自然第一时间得去医院，留下一个助理跟交警处理事故合情合理。这点儿小事根本不值得找人顶包，我不相信金晨去就医之前还有闲心特意交代助理为自己顶包。但是助理实际上这么做了（或许是出于忠心，或许是另有 ​

6

30

133

田春冰河

2026-01-28 21:42来自 微博网页版

[1/3] 终于给我的台式机换上 2.5G 网卡了，然后从 Ubuntu PPA 安装了最新的 RealTek 驱动（需要屏蔽内核自带的旧版模块）。貌似 PCIe Gen3x1 最多可以支持 5Gb 以太网卡，但我没有配套的交换机所以也就不必多花那个冤枉钱了。而且…… 我的加速卡上其实有个 10Gb 光纤链路，我知道怎么给它 FPGA 编程成 ​

1

2

33

田春冰河

2026-01-25 10:55来自 微博网页版

[1/3] 前些日子新配的 PC 只有主板自带的千兆网口，跟我的 2.5G 小交换机不匹配（需要时常拷贝些大文件），但是我主板上只有唯一的 Type-C 口偶尔要插键盘，不方便连接我那些 USB-C 转 2.5G 网卡。本想去京东上买个 USB 3.0 转 2.5G（绿联的大约 100 多元），但是临下单之前突然发现我主板上其实有个空 ​

0

9

24

田春冰河

2026-01-22 15:28来自 微博网页版

[2/3] 按说初学一门外语，在基本掌握了语法以后，最好从带有翻译和文法解析的散文例文开始学习。但是梵语的情况特殊，经典文学作品大都是韵文，翻译好的散文例文不多。常见的梵语韵文是以 “颂” 为单位的，每颂分上下两部分，各 16 音节（总计 32 音节），不像汉语诗句那样押韵（即最后一字的韵母相同 ​

3

16

23

田春冰河

2026-01-22 14:58来自 iPhone SE

[1/3] 全新的《梵语文学读本》（精装）终于落到我手上了。此书 2010 年出版（应该就印了一次），定价 98 元，十六年没卖完，如今被我 49.9 元网购拿下了（网上还有大量的库存）。这本书应该是目前国内唯一的梵语读本（其他都是附带在梵语教程里的长短不一的例文），特点是只收录少数几部梵文经典的精华 ​

1

16

30

田春冰河

2026-01-20 08:47来自 微博网页版

[1/3] 西贝关店不是因为他的老板公关没做好，而是他们价格高、做得难吃，改进后成本提高，无法盈利，说白了就是企业的核心竞争力不足。很多网友批评人家不会公关，这就好比一个出轨离婚以后周围的人只批评他（她）怎么这么不小心被发现了（或者善后工作做得不好）而完全不提出轨本身就是错误的行为。经 ​

7

11

79

田春冰河

2026-01-19 20:36来自 微博网页版

[3/3] 其实我之前在澳国立（ANU）干得并不开心：每天从早到晚都在忙着写形式化证明，然后偏偏这个证明又非常难写——有个长达 4000 行的单体证明整整花了我半年时间，反复修改相关定义和引理最后才搞定。写不完就发不出第一篇论文，于是也就没业绩（就算有一篇论文也不足以升职或续合同）。手下带的学 ​

2

18

54

田春冰河

2026-01-19 19:13来自 微博网页版

[2/3] 前些日子郭德纲的《艺高人胆小》从内容上来看几乎每个段子以前都讲过，但为什么就在那次被人投诉了？我发现问题出在郭德纲的台词里明确提到 “黑粉” 了，仿佛是在挑衅。人都有逆反心理，黑粉们也不例外，于是那次就真的被举报了。我也犯了类似错误（见图3）我要不提醒可能她根本就想不到还能那 ​

0

7

16

田春冰河

2026-01-18 11:45来自 微博网页版

[2/3] 国内现在访问 GitHub 只能说勉强能用、时断时续。刚才我想发一个 pull request，结果网页的局部（比如分支的下拉列表）死活刷不出来，后来我观察了一下 GitHub 的 URL 格式，就在 FileMaker 里简单写了个小应用：输入相关信息自动生成 URL（然后一键即可在浏览器里打开），这才把 PR 成功发出去 ​

2

7

31

田春冰河

2026-01-17 15:50来自 iPhone SE

[2/3] 值钱的、不值钱的，反正只要是不太重的都顺利地带回来了（摄影器材就不拍了，都还在）。我这些年赚的钱基本上都花在这些装备上了，还有我那些 “捐款” 历史想必大家也还记得。把钱花在自己喜欢的东西（和人）上面不丢人，只不过这些东西将来怎么办…… ​

1

27

82

田春冰河

2026-01-17 10:31来自 微博网页版

[1/3] 昨天我发现其实 AMD/Xilinx 是允许最多5次迁移固定节点许可证的，于是就把 ThinkPad P70 上的 Vivado 许可证迁移到新买的那台 Linux 机上了，结果万万没有想到原本 10+ 小时的综合和实现过程，在新机器上不到 3 个小时就完成了（合着我是被过时的电脑给坑了），32G 内存好像也够了。但我为什么会 ​

1

3

24

田春冰河

2026-01-16 17:58来自 iPhone SE

[3/3] 前天去大连取寄存在朋友家的厨刀（高铁安检过不去，快递也不给寄），顺便去最大的新华书店转了一圈，买了一本 FPGA 时序分析的书（去年出版的）、一本钢笔字帖、一本长笛入门教材，加上我从澳洲带回来的法语和梵语教材，就是我每天的必修课了。这叫闲着也是闲着（再没人来催科研进度了），艺多不 ​

1

32

91

田春冰河

2026-01-16 12:13来自 微博网页版

[2/3] GPU 的计算原理基本上就是在显卡芯片里预先定制了数千个简化 CPU——每个只能执行很简单的计算指令，工作频率比 CPU 低（比如只有 500 Mhz）。FPGA 加速卡理论上可以更快，因为一来它完全不需要执行指令，而是把所需的计算任务直接编译成了电路——可复制多份（最大数量取决于 FPGA 芯片的可用面 ​

5

13

29

田春冰河

2026-01-16 11:46来自 微博网页版

[1/3] 终于第一次把 Alveo U200 加速卡的 hello world 从源码跑通了。跟 GPU 编程的入门代码差不多，只是个并行数组加法，但是用 AMD/Xilinx Vitis 工具把核函数编译成可加载的电路模块，花了差不多一个小时。宿主代码无非是加载并执行核函数，代码比 OpenCL 简洁（但比 CUDA 繁琐些），而且号称可以完 ​

1

5

18

田春冰河

2026-01-13 07:42来自 iPhone SE

[1/3] 佛山市硬笔书法协会禅城分会，成立不到一周年（还差两天），惨遭取缔…… ​

2

9

19

田春冰河

2026-01-12 16:36来自 微博网页版

[3/3] （注：此测试中 M4 工作在省电模式下……）我用 @算法时空 PPLA 项目里的10亿数的串行和并行排序（billionsort.cpp 和 parallel_billionsort.cpp）对比了 Intel 12 代 i5-12400 (6 核 12 线程）和 M4（10 核）的单核和多核性能。编译器都是 GCC 13，并行排序链接了差不多新的 tbb 库。结果确实显 ​

1

21

10

田春冰河

2026-01-12 16:00来自 微博网页版

[2/3] EDA 软件（AMD/Xilinx Vivado）的运行速度实在是太慢了，从硬件描述到可编程的位流，在几乎填满一张较大的 FPGA 芯片的情况下，需要好几个小时。在我的 4 核至强 2.8GHz CPU 上，我每天最多只能跑两次[泪] 这堪比搞机器学习的那帮人（我也曾经干过几天）边调参数边撞大运了。 ​

4

14

23

田春冰河

2026-01-12 09:48来自 微博网页版

[1/3] 昨天把我台式机操作系统从 Ubuntu 22.04 升到了 Ubuntu Server 24.04。虽然内核版本没变（为了加速卡而被迫继续使用 6.8.0 内核），但现在系统能识别出我的核显是 Intel Alder Lake-S GT1 [UHD Graphics 730]，理论上我可以使用核显的 GPU 加速和硬件编解码了。我自从 2008 年以后就没买过这么便 ​

4

20

32

田春冰河

2026-01-09 16:25来自 微博网页版

[2/3] 昨天在 Alveo U200 上成功运行了 32 个 riscv64 CPU 的 Linux 以后，性能测试放弃了——基于 R 的性能测试目测比我的笔记本慢 500 倍…… 后来我回到此卡推荐的使用方式上——作为数据中心加速卡，结果也不太顺利。Xilinx 的天才硬件工程师们在 FPGA 上实现了一个可动态修改自身部分电路的加速器 ​

1

2

17

田春冰河

2026-01-09 07:14来自 iPhone 8

[1/3] 我发现网上有很多二尾(yǐ)子们连 “二尾子” 这三个字怎么写都不知道，还来给我纠错顺便讽刺我呢。但凡读过《红楼梦》和几本贾平凹小说也不至于连这都不知道，你们的语文水平还不如我一个搞计算机的，对得起中学语文老师和你们的二尾子身份吗？ ​

6

11

45

田春冰河

2026-01-08 20:50来自 iPhone SE

[3/3] 我这个价值几十澳元的小交换机太值了，4个2.5G电口和2个10G光口，我用一个光电模块把其中一个光口转电口以后连 M4 Mac mini 确保满速；第二个光口用 40G 转 4*10G 光纤连到 FPGA 加速卡上；其他几个口通过 USB-C 转 2.5G 转接器连其他电脑；最后还有一个连到家用 WiFi 上。 ​

3

9

41

田春冰河

2026-01-08 18:17来自 微博网页版

[2/3] 闲着也是闲着，下面公布我对大学指控信的辩解信全文。我的主要论点：1. 对女性气质和业余爱好的真诚赞美是否算性骚扰；2. 学生作弊在先，教师作为受害者不点名公开批评也不行？3. 校长自身行为不检点，不尊重（调侃）不值得尊重的人也有错？4. 别人的评论我不负责且没有义务（及时）删除。 ​

6

33

103

田春冰河

2026-01-08 13:53来自 微博网页版

[1/3] 终于首次完全在 Windows 下（借助 WSL 里的 Ubuntu）成功地给我的 Xilinx Alveo U200 加速卡重新编程，跑起了一个 32 核 riscv64 的 Linux 环境（Debian 13），FPGA 芯片资源用了 80%（已经很高了），CPU 主频应该不超过 300MHz。整个系统是个无盘站，连根目录都是 NFS 挂载的，然后通过 10G 以 ​

1

4

36

田春冰河

2026-01-07 11:57来自 微博网页版

[1/3] 按说我此次 “衣衫褴褛还乡”（姑且算是 “衣锦还乡” 的反义词），就应该众叛亲离、大家偷着乐之余避之唯恐不及。可事与愿违，还是有亲人惦记我（算计我），看我回家了就想第一时间来看我。我后来想明白了，比失业的人更惨的其实大有人在：那就是死人和病人。在东北，没钱算什么大事？没病就等 ​

6

37

114

田春冰河

2026-01-06 17:44来自 微博网页版

[3/3] 今天攒的这个台式机花了 3300 元（其中 1140 元是两条 16G 内存，570*2），我自己的机箱电源、固态硬盘。这个 12th Gen Intel i5-12400 (12) @ 4.400GHz 看着挺高端的（6核12线程?），并行算法测试表明也就比我的 2019 MBP 快了最多不到百分之五十。P. S. 尼泊尔姑娘继续每天给我发问候邮件，图3 ​

1

28

55

田春冰河

2026-01-06 16:34来自 微博网页版

[2/3] 知乎上看到一篇对我的评论文章（http://t.cn/AXbiNkdH）。其实我导师确实有帮我联系新的工作机会：一是去瑞典参与 CakeML 项目（基于 HOL 的 ML 系语言编译器），二是去新加坡加入另一个资深 HOL 用户的团队搞形式化的安全验证，都是我很熟悉甚至见过面的人。而且开除这个事情原本是保密的，只要 ​

3

14

57

田春冰河

2026-01-06 16:16来自 微博网页版

[1/3] 今天去本地电脑城攒了一个小机箱的台式机，就为了把我那个斥巨资采购的 Xilinx Alveo U200 加速卡插进去，然后从 PS5 上拔下了那条我不差钱的时候买的 2TB SSD。内存现在虽然贵但还是配了 32G DDR4；然后机箱电源就是我的雷蛇 Core X 上面拆下来的。现在我终于首次通过了加速卡的自检（它自己说 ​

2

17

39

田春冰河

2026-01-05 14:40来自 微博网页版

[4/3] 话说尼泊尔姑娘有每天写英文日记（然后每年换一个本子）的习惯，现在已经抛弃了她原先的破圆珠笔，对我送的金笔爱不释手。回想飞机临降落时她突然问我何时返回堪培拉（她在悉尼某医院里做护工），我知道她有些依依不舍，但不想透露实情，就只说自己要放个长假不知道何时返澳，然后她就不知道怎么 ​

0

22

55

田春冰河

2026-01-05 13:57来自 微博网页版

[3/3] 下面讲一个故事，这件事跟我的其他事可能有关系也可能没关系。2023年10月，网友 @蓓蕾zhu (账号性别女) 私信联系我（过去可能有过评论交流，属于比较眼熟的 ID），说是广西大学金融专业的，要来澳洲留学，二选一让我给拿主意，还要加微信。我没主意（再说也不是同专业的），只能礼貌地敷衍一下。 ​

4

36

140