kframework - 我们如何使用 --pdf 标志来生成文档？

Question

http://www.kframework.org/index.php/Lesson_4,_LAMBDA:_Generating_Documentation;_Latex_Attributes中的视频教程建议我们应该使用kompile lambda --pdf，但是当我运行它时出现以下错误：

[Error] Critical: Unknown option: --pdf (Unknown option: --pdf)

该kdoc --help选项也会导致Command 'kdoc' not found错误。

如何正确使用此选项来生成格式化的 K 定义？

Answer 1

该kdoc功能（和--pdf）已经有一段时间没有工作了。

如果您想要给定单个术语的 LaTeX AST 输出，您可以使用--output latex、或. 不幸的是，这不适用于整个定义，并且不会为您自动格式化（它只输出一个 AST，您仍然需要告诉 LaTeX 如何渲染所述 AST 中的节点）。kastkrunkprove