profiling - Coq定理的高速计算

Question

即使在非常简单的情况下，我也要等到Coq完成其计算。

我知道“异步和并行证明处理”，但是我想我的代码具有固有的弊端，所以我想
获得一些有关样张指南/最佳做法的参考或建议。
例如。:

尝试使用定义而不是定理

使用编译器。使用并行处理。使用更好的硬件。

不要使用占位符，填写每个参数，例如(@functionname var1 ... varn)

分号(;)代替句点(.)

在“节”中使用“定义”而不是“set(f:= term)”要快得多。在证明中。 (可能是因为每个“设置”都有额外的打印时间。甚至要检查是否为空。)

如何加快Coq？ (如果上面的项目有误，请说。它们是根据我的实践得出的。)

什么是计算的最关键阶段以及如何使用它们？

Answer 1

圣杯是分析您的代码并优化热点。在Coq> = 8.6中，您可以使用Set Ltac Profiling.以及Reset Ltac Profile.和Show Ltac Profile.来描述战术。如果使用coqc参数调用-time，您将获得逐行计时信息。一点sed技巧可以为您排序信息:

coqc -time foo.v | sed s'/^\(.*\) \([0-9\.]\+ secs.*\)$/\2 \1/g' | sort -h

在Coq> = 8.8中，您可以 Set NativeCompute Profiling来分析本机计算(例如 Eval native_compute in (slow program here))。这将产生可在GNU / Linux上使用 perf report可视化的跟踪。有关更多信息，请参见 this bug report。

如果遇到其他瓶颈，您要么必须擅长猜测，要么说服开发人员添加更多性能分析工具，分析正在运行的coq二进制文件，或者说服开发人员值得花时间为您分析代码。 (当速度变慢指向Coq中的效率错误时，有时我可以让Pierre-MariePédrot来分析我的代码。)

一种有用的做法是始终在每次提交时都对代码进行概要分析。在Coq> = 8.7中，有 Makefile目标 make-pretty-timed-before， make-pretty-timed-after和 print-pretty-timed-diff可以得到存储库两个状态之间每个文件编译时间差异的排序表。您可以使用 make TIMING=before， make TIMING=after和 make all.timing.diff获取每行信息。

您可能也有兴趣查看 Experience Implementing a Performant Category-Theory Library in Coq(更多媒体 here)，并且可能还会看到介绍该论文的幻灯片( pdf)( pptx with presenter notes)。

尽管您提到的大多数内容都无关紧要，但Coq在许多地方可能会变慢。依次检查您的:

Theorem和Definition是同义词，唯一的区别是Definition支持:=，而Theorem不支持。

没有更好的Coq编译器，尽管更好的硬件，更多的RAM，更快的CPU绝对有帮助。和并行处理一样。在这一点上，文件级并行性往往比证明级并行性更好。我倾向于尽可能多地分割文件，进行细粒度的导入，以使库加载时间不成问题，并使用make -j。

填满每个参数都比提供帮助更容易受到伤害。您将承担额外的统一成本，尤其是当您要填充参数的术语很大时。通过填写参数来完成的真正工作是将evar创建与统一进行交易。统一通常比较慢。但是，如果您有任何空缺被规范结构解析，类型类解析填补，或者需要其他回溯和展开操作或刷新Universe变量，则将其填充可以大大加快操作速度。

我认为证明脚本中的分号和句点之间的区别仅在交互模式下才有意义(在coqtop / CoqIDE / ProofGeneral / etc中，在运行make时不重要)。让我知道您是否进行测试，否则发现其他问题。

这是真的，对打印和其他事物都有影响。 set本身不会因为打印而变慢，而是因为它会尝试查找目标中所有出现的词(愚蠢地，最大程度地减少(β-iota？我不记得了))，而是而不是句法平等)，并用新的假设取代它们。如果您不需要这种行为，请使用pose而不是set。此外，大的上下文变量可能会降低取决于上下文大小的策略，这就是为什么Definition在各节中更快的原因。

关于我遇到的事情的其他想法:

选择良好的抽象障碍，并认真地尊重它们。每当您打破抽象障碍时，您都会付出汗水和眼泪。 (选择良好的抽象障碍非常困难。通常，我通过复制现有的数学抽象或已发表的论文来做到这一点。在某种意义上，我设法在过去五年中完全从头开始完全形成了一个良好的抽象障碍。事后看来，障碍可以用“洞察力”来描述，即“在编写类似C的代码时，每个函数都将一个元组作为参数，并返回一个元组作为结果。”)

如果您要进行反射证明，请选择好的算法。如果您使用一元自然数，或者您的算法具有指数运行时间，则证明速度会很慢。

在Coq <8.7中，evar-map规范化会在很大程度上产生大量开销。 (向Pierre-Marie提出通过其EConstr分支解决此问题的建议。)

较慢的End Section(有时是较慢的Defined)通常是由重新哈希处理问题引起的。要解决此问题，请双手合十祈祷。 (或成为Coq开发人员并修复Coq。)

保护性检查器在检查具有大主体的裸fix时非常慢(也许仅在存在beta-iota-zeta还原的情况下？)。解决方法是将主体提取到单独的定义中。例如，而不是编写

定点长度A(ls:列表A):nat:=
与ls匹配
|零=> 0
|缺点_ xs => S(长度_ xs)
结束。

你可以写

定义length_step
(长度:全部A，列表A-> nat)
A(ls:清单A)
:nat
:=匹配ls与
|零=> 0
|缺点_ xs => S(长度_ xs)
结束。
定点长度A(ls:列表A):nat
:= length_step长度A ls。

请注意，Coq将自由地(有时会不一致)内联let x := ... in ...语句，这很容易导致指数定义的内部化时间。

进行规范化时，规范结构快速但难以阅读，Ltac慢约2倍，类型分类解析度又可以慢2倍(或可以与Ltac规范化相同的速度)。希望Ltac2完成后情况会更好。

simpl很大程度很慢

我可能会稍后再添加更多内容(并随时在评论中提出建议供我添加)，但这是一个不错的开始。