Isabelle 会话图作为点文件

Question

Isabelle 可以将一个开发的所有理论的图表生成为 PDF 文件，如 this example 中所示。这显然是使用 graphviz 呈现的，所以我想知道：有没有办法获得 Isabelle 用来生成此图的原始 .dot 文件？这对于以不同的样式呈现它很有用，例如更紧凑。

Answer 1

使用 Isabelle/Scala 这很简单。以下代码可以保存到文件中，并作为脚本直接执行，前提是 isabelle install some_bin_dir 之前已经执行过，其中 some_bin_dir 在 PATH.

中

#!/usr/bin/env isabelle_scala_script

import isabelle._

val options = Options.init()
val content = Build.session_content(options, false, Nil, "HOL")
val graph = content.session_graph

graph.dest.foreach {
  case ((x, _), ys) =>
    println(x.toString + " -> " + ys.iterator.map(_.toString).mkString("{", ", ", "}"))
}

这是此脚本的输出（摘录）：

ATP -> {Metis}
Archimedean_Field -> {Rat}
BNF_Cardinal_Arithmetic -> {BNF_Def}
BNF_Cardinal_Order_Relation -> {BNF_Cardinal_Arithmetic}
BNF_Composition -> {BNF_Fixpoint_Base}
BNF_Def -> {BNF_Composition, Basic_BNFs}
BNF_Fixpoint_Base -> {BNF_Greatest_Fixpoint, BNF_Least_Fixpoint}
BNF_Greatest_Fixpoint -> {Main}
BNF_Least_Fixpoint -> {Basic_BNF_LFPs, Num}
BNF_Wellorder_Constructions -> {BNF_Cardinal_Order_Relation}
BNF_Wellorder_Embedding -> {BNF_Wellorder_Constructions}
BNF_Wellorder_Relation -> {BNF_Wellorder_Embedding}
Basic_BNF_LFPs -> {Fun_Def, Transfer}
Basic_BNFs -> {BNF_Fixpoint_Base}

上面的代码可以很容易地更改为生成 dot 兼容的输出。

关于session_content方法的参数：第三个（Nil）是会话目录列表（对应isabelle build中的-d）和第四个是会话的名称。在脚本中，数组 args 可用，它对应于通过命令行传递的参数列表，允许您从用户那里获取这些参数。

Answer 2

Dot 并不是制作图形布局的唯一工具。 1996 年首次实现 Isabelle 图布局时，它的竞争者确实已经存在，但我们对此并不满意。所以我们实现了不同的算法。

2016年，情况大体相同。在此期间没有出现新的更好的工具，因此 Isabelle 仍然是相关的工具（最近移植到 Scala）。

Isabelle 会话图作为点文件

Isabelle session graph as a dot file

isabelle