AFP Dijkstra's Shortest Path Algorithm

Question

For the AFP entry Dijkstra's Shortest Path Algorithm, both the proof outline and proof document were nonexistent *. Unfortunately, I did not find an IsaMakefile either to build those documents locally. What is the best way to get those documents?

Another question, as the Dijkstra.thy depends on a lot of other theories, is there a way to load everything faster?

*) It is fixed now.

Answer 1

(There seems to be something broken at AFP right now, please tell the editors about it.)

In general, you can download the sources of AFP entries and produce the documents yourself like this:

• Get and unpack all AFP sources -- downloading separate entries is offered as well, but then you have to disentangle dependencies manually.

• Invoke isabelle build like this:

  isabelle build -d afp-2013-03-02 -o document=pdf -v Dijkstra_Shortest_Path
  

  Here afp-2013-03-02 is the directory that was obtained by unpacking the current AFP sources.

See also the Isabelle System manual about "Isabelle sessions and build management", which is all new in Isabelle2013.

See isabelle build -b there to make things load faster, by producing persistent heap images from sessions.