Mac Catalina下回退Emacs后PG中SSReflect的.+1 notation显示异常排查

• Proof General 4.5-git 与新版SSReflect的内置notation适配断层：这个版本的PG是较早的开发分支，内置的语法渲染规则仅对应其开发期配套的旧版SSReflect，没有收录nat类型专属的.+1 notation的映射规则，会自动将无法识别的内置notation token回退显示为底层原始构造子succn。而你使用的Nix打包版Coq自带的SSReflect版本远新于Proof General 4.5-git适配的版本，版本差异直接触发了这个显示异常；你自己编写的自定义notation因为是在Coq会话运行时动态注册的，PG有对应的上下文识别逻辑，所以不会受这个规则缺失的影响。
• 跨系统版本迁移导致Emacs 26.1字符映射、字体配置缺失：你当前的Emacs 26.1是从High Sierra直接迁移到Catalina的，迁移过程中缺失了Catalina环境下对应配置路径的SSReflect特殊符号字体映射、字符集加载规则，PG在渲染.+1这类带特殊上下文标记的notation时，找不到对应的渲染规则，就会还原显示为原始构造子succn；自定义notation多为纯ASCII字符组合，不依赖额外的特殊字体映射，因此显示正常。
• Coq与Proof General的通信协议版本不匹配：Nix打包的Coq默认输出的Goals buffer信息格式，与Proof General 4.5-git约定的老版通信协议存在差异，PG解析目标缓冲区返回内容时，会把无法匹配协议规则的SSReflect预加载内置notation，直接替换为底层构造子展示。动态注册的自定义notation因为在会话上下文中有明确标记，能被PG正常识别，不会触发替换逻辑。
• 版本回退过程中丢失了配套的notation补丁配置：你此前尝试升级Emacs时，曾在可正常运行的新版本Emacs环境下配置过补全PG对SSReflect内置notation支持的elisp规则，回退到旧版Emacs时，这些自定义补丁配置没有被同步到当前旧版Emacs对应的用户配置目录下，直接导致notation映射规则缺失。

内容的提问来源于stack exchange，提问作者Pierre Jouvelot