Agda 2.7.0.1 编译时启用性能分析(Profiling)的GHC内部错误分析
在Agda 2.7.0.1版本中,当尝试使用GHC的性能分析(profiling)功能编译某些Agda程序时,会遇到GHC编译器的内部错误(panic)。这个问题主要出现在使用GHC 9.12.2版本时,但在GHC 9.10.2版本中部分情况可以正常工作。
问题背景
Agda作为一种依赖类型的函数式编程语言,最终会通过MAlonzo后端将代码编译为Haskell,再通过GHC编译为可执行文件。当开发者尝试使用GHC的性能分析功能(通过--ghc-flag=-prof和--ghc-flag=-fprof-auto选项)来优化Agda程序时,在某些特定情况下会触发GHC的内部错误。
错误表现
典型的错误信息如下:
ghc: panic! (the 'impossible' happened)
GHC version 9.12.2:
getStgArgFromTrivialArg
case sat_s1qM @(*) @Any @(ZonkAny 67) of { UnsafeRefl co7_s1r4 ->
ww2_s1qK
`cast` (Sub (Sym co7_s1r4)
; SelCo:Fun(arg) (SelCo:Fun(res) (Sub co6_s1qU))
:: Any ~R# [ZonkAny 68])
}
这种错误发生在GHC的核心到STG(Spineless Tagless G-machine)中间表示转换阶段,具体是在处理类型转换(cast)操作时。
最小复现案例
通过分析,可以提取出一个最小复现案例。以下Agda代码在启用性能分析编译时会触发该错误:
module OfSemiring where
record Sigma (A : Set) (B : A → Set) : Set where
constructor pair
field
fst : A
snd : B fst
data Nat : Set where
zero : Nat
suc : (n : Nat) → Nat
data List (A : Set) : Set where
nil : List A
cons : (x : A) (xs : List A) → List A
{-# BUILTIN LIST List #-}
foldr : {A B : Set} → (A → B → B) → B → List A → B
foldr c n nil = n
foldr c n (cons x xs) = c x (foldr c n xs)
record Semiring : Set₁ where
field
Carrier : Set
plus : Carrier → Carrier → Carrier
zero : Carrier
trans : {x y z : Carrier} → x ≡ y → y ≡ z → x ≡ z
module SemiringList (R : Semiring) where
open Semiring R
dotProduct : List Carrier → List Carrier → Carrier
dotProduct xs ys = foldr plus zero (zipWith times xs ys)
testSubList : List Carrier → List Carrier → Set
testSubList bs cs = ∀ x → x ∈ bs → x ∈ cs
where
_∈_ : Carrier → List Carrier → Set
x ∈ bs = Σ (List Carrier) λ qs → dotProduct qs bs ≡ x
问题分析
经过深入调查,发现这个问题与以下因素有关:
-
GHC版本:该问题在GHC 9.12.2中首次出现,在GHC 9.10.2中部分情况可以工作,但在更复杂的场景下仍会出错。
-
Agda编译选项:启用
--auto-inline优化选项会增加触发此错误的概率。 -
代码结构:当Agda代码中包含特定的递归定义和抽象块(abstract blocks)时更容易触发此错误。
-
内置类型:使用
BUILTIN LIST定义列表类型也是触发条件之一。
解决方案
目前推荐的解决方案包括:
-
降级GHC版本:对于简单场景,使用GHC 9.10.2可以避免此问题。
-
简化代码结构:通过重构代码,避免复杂的递归定义和抽象块组合。
-
等待GHC修复:该问题已上报至GHC开发团队,未来版本可能会修复。
-
避免特定优化:暂时不使用
--auto-inline选项可以减少问题发生概率。
性能分析替代方案
在等待GHC修复期间,开发者可以考虑以下替代性能分析方案:
-
手动插入计时点:在关键函数处手动添加时间测量代码。
-
使用Agda的调试功能:通过
--verbose选项获取更详细的编译信息。 -
模块化测试:将大型程序拆分为小模块单独测试性能。
总结
这个问题展示了当高级语言(Agda)通过中间编译器(GHC)生成代码时可能遇到的底层问题。虽然性能分析是优化程序的重要工具,但在当前情况下需要谨慎使用。开发者应当根据具体情况选择合适的变通方案,同时关注GHC未来的更新以获取永久性修复。
对于Agda开发者来说,理解这类问题的本质有助于更好地设计代码结构,避免触发编译器边界情况,同时也为参与开源编译器开发提供了宝贵的实践经验。
PaddleOCR-VLPaddleOCR-VL 是一款顶尖且资源高效的文档解析专用模型。其核心组件为 PaddleOCR-VL-0.9B,这是一款精简却功能强大的视觉语言模型(VLM)。该模型融合了 NaViT 风格的动态分辨率视觉编码器与 ERNIE-4.5-0.3B 语言模型,可实现精准的元素识别。Python00- DDeepSeek-OCR暂无简介Python00
openPangu-Ultra-MoE-718B-V1.1昇腾原生的开源盘古 Ultra-MoE-718B-V1.1 语言模型Python00
HunyuanWorld-Mirror混元3D世界重建模型,支持多模态先验注入和多任务统一输出Python00
AI内容魔方AI内容专区,汇集全球AI开源项目,集结模块、可组合的内容,致力于分享、交流。03
Spark-Scilit-X1-13BFLYTEK Spark Scilit-X1-13B is based on the latest generation of iFLYTEK Foundation Model, and has been trained on multiple core tasks derived from scientific literature. As a large language model tailored for academic research scenarios, it has shown excellent performance in Paper Assisted Reading, Academic Translation, English Polishing, and Review Generation, aiming to provide efficient and accurate intelligent assistance for researchers, faculty members, and students.Python00
GOT-OCR-2.0-hf阶跃星辰StepFun推出的GOT-OCR-2.0-hf是一款强大的多语言OCR开源模型,支持从普通文档到复杂场景的文字识别。它能精准处理表格、图表、数学公式、几何图形甚至乐谱等特殊内容,输出结果可通过第三方工具渲染成多种格式。模型支持1024×1024高分辨率输入,具备多页批量处理、动态分块识别和交互式区域选择等创新功能,用户可通过坐标或颜色指定识别区域。基于Apache 2.0协议开源,提供Hugging Face演示和完整代码,适用于学术研究到工业应用的广泛场景,为OCR领域带来突破性解决方案。00- HHowToCook程序员在家做饭方法指南。Programmer's guide about how to cook at home (Chinese only).Dockerfile013
Spark-Chemistry-X1-13B科大讯飞星火化学-X1-13B (iFLYTEK Spark Chemistry-X1-13B) 是一款专为化学领域优化的大语言模型。它由星火-X1 (Spark-X1) 基础模型微调而来,在化学知识问答、分子性质预测、化学名称转换和科学推理方面展现出强大的能力,同时保持了强大的通用语言理解与生成能力。Python00- PpathwayPathway is an open framework for high-throughput and low-latency real-time data processing.Python00