Merge pull request #63 from yoshihiro503/yoshihiro503@file-dependenci…

…es-graph

The dependency graph on index.html

.github/workflows/deploy_static_site.yml

@@ -44,22 +44,25 @@ jobs:
             coq-released: https://coq.inria.fr/opam/released
             default: https://github.com/ocaml/opam-repository.git
 
+      - name: Setup Coq temporary fix for the Dependency Graph
+        run: opam install -y coq.8.19.2
+
       - name: Build Mathcomp Analysis
         run: cd analysis/ && opam install -y --deps-only . && opam exec -- make all install
 
       - name: Build coq2html
         run: opam exec -- make
 
-      - run: opam exec -- tools/generate-mathcomp-analysis.sh
+      - run: opam exec -- tools/generate-mathcomp-analysis.sh ${GITHUB_SHA::8}
 
       - name: Setup Pages
-        uses: actions/configure-pages@v3
+        uses: actions/configure-pages@v4
 
       - name: Upload artifact
-        uses: actions/upload-pages-artifact@v2
+        uses: actions/upload-pages-artifact@v3
         with:
           # Upload entire repository
           path: 'html/'
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v2
+        uses: actions/deploy-pages@v4

Makefile

@@ -1,10 +1,12 @@
-OCAMLOPT=ocamlopt -I +str
+OCAMLOPT=ocamlopt -I +str -annot
 OCAMLLEX=ocamllex
 
 GEN_IDX=generate_index
 
 PROJ_OBJS=common.cmx graphviz.cmx range.cmx xrefTable.cmx generate_index.cmx
 
+all: coq2html ocamldot/ocamldot
+
 coq2html: $(PROJ_OBJS:.cmx=.cmi) $(PROJ_OBJS)  coq2html.cmx
 	$(OCAMLOPT) -o coq2html str.cmxa resources.cmx $(PROJ_OBJS) coq2html.cmx
 
@@ -36,6 +38,7 @@ clean:
 	rm -f coq2html
 	rm -f coq2html.ml resources.ml
 	rm -f *.o *.cm?
+	$(MAKE) -C ocamldot/ clean
 
 PREFIX=/usr/local
 BINDIR=$(PREFIX)/bin
@@ -47,3 +50,7 @@ depend:
 	ocamldep *.mli *.ml > .depend
 
 -include .depend
+
+# ocamldot
+ocamldot/ocamldot: ocamldot/
+	$(MAKE) -C ocamldot/ ocamldot

coq2html.mll

@@ -668,6 +668,7 @@ let generate_css = ref true
 let use_short_names = ref false
 let generate_redirects = ref false
 let hierarchy_graph_dot_file = ref ""
+let dependency_graph_dot_file = ref ""
 
 let process_v_file all_files f =
   let pref_f = Filename.chop_suffix f ".v" in
@@ -737,7 +738,9 @@ let _ =
     "-short-names", Arg.Set use_short_names,
       "   Use short, unqualified module names in the output";
     "-hierarchy-graph", Arg.Set_string hierarchy_graph_dot_file,
-      "   Show the hierarchy graph of <dot-file> on the index.html"
+      "   Show the hierarchy graph of <dot-file> on the index.html";
+    "-dependency-graph", Arg.Set_string dependency_graph_dot_file,
+      "   Show the dependency graph of <dot-file> on the index.html";
   ])
   process_file
   "Usage: coq2html [options] file.glob ... file.v ...\nOptions are:";
@@ -757,7 +760,7 @@ let _ =
   List.iter process_glob_file (List.rev !glob_files);
   let all_files = Generate_index.all_files xref_modules in
   List.iter (process_v_file all_files) (List.rev !v_files);
-  Generate_index.generate !output_dir !xref_table xref_modules !title !hierarchy_graph_dot_file;
+  Generate_index.generate !output_dir !xref_table xref_modules !title !hierarchy_graph_dot_file !dependency_graph_dot_file;
   write_file Resources.js (Filename.concat !output_dir "coq2html.js");
   if !generate_css then
     write_file Resources.css (Filename.concat !output_dir "coq2html.css")

generate_index.ml

@@ -225,7 +225,7 @@ let overwrite_dot_file_with_url xref_table dot_file = (* dirty *)
   let node_with_node (mod_, path) =
     let name = String.sub path 0 (String.length path - String.length ".pack_")  in
     let url = mod_ ^ ".html#" ^ name in
-    !%{|%s [URL="%s"]|}  name url
+    !%{|"%s" [URL="%s"]|}  name url
   in
   let links = String.concat "; " (List.map node_with_node all_hb_defs) in
   let tmp = dot_file ^ ".sed" in
@@ -234,7 +234,7 @@ let overwrite_dot_file_with_url xref_table dot_file = (* dirty *)
   Common.shell (!%"mv %s %s" tmp dot_file)
 
 
-let generate_hierarchy_graph xref_table output_dir dot_file =
+let generate_hierarchy_graph title xref_table output_dir dot_file =
   overwrite_dot_file_with_url xref_table dot_file;
   let png_filename = "hierarchy_graph.png" in
   let png_path = Filename.concat output_dir png_filename in
@@ -243,18 +243,31 @@ let generate_hierarchy_graph xref_table output_dir dot_file =
   |> Graphviz.generate_file png_path map_path;
   let map = read_file map_path in
   (*TODO: ↓ The map id (#Hierarchy) should be taken from dot file *)
-  Printf.sprintf {|<h2>Mathematical Structures</h2><img src="%s" usemap="#Hierarchy"/>
-%s|} png_filename map
+  Printf.sprintf {|<h2>Mathematical Structures (%s only)</h2><img src="%s" title usemap="#Hierarchy"/>
+%s|} title png_filename map
+
+let generate_dependency_graph xref_table output_dir dot_file =
+  let png_filename = "dependency_graph.png" in
+  let png_path = Filename.concat output_dir png_filename in
+  let map_path = Filename.concat output_dir "dependency_graph.map" in
+  Graphviz.from_file dot_file
+  |> Graphviz.generate_file png_path map_path;
+  let map = read_file map_path in
+  Printf.sprintf {|<h2>Clickable Dependency Graph of Files</h2><img src="%s" usemap="#depend"/>%s|} png_filename map
 
 (*
  * generate index.html
  *)
-let generate_topfile output_dir all_files xrefs title xref_table hierarchy_graph_dot_file =
-  let body =
-    if hierarchy_graph_dot_file = "" then table xrefs
-    else
-      table xrefs ^ generate_hierarchy_graph xref_table output_dir hierarchy_graph_dot_file
+let generate_topfile output_dir all_files xrefs title xref_table hierarchy_graph_dot_file dependency_dot_file =
+  let hierarchy_graph =
+    if hierarchy_graph_dot_file = "" then "" else
+      generate_hierarchy_graph title xref_table output_dir hierarchy_graph_dot_file
+  in
+  let dependency_graph =
+    if dependency_dot_file = "" then "" else
+      generate_dependency_graph xref_table output_dir dependency_dot_file
   in
+  let body = table xrefs ^ hierarchy_graph ^ dependency_graph in
   write_html_file all_files body (Filename.concat output_dir "index.html") title
 
 let is_initial c s =
@@ -289,7 +302,7 @@ let all_files xref_modules =
   |> List.map (String.split_on_char '.')
   |> iter
 
-let generate output_dir (xref_table:XrefTable.t) xref_modules title hierarchy_dot_file =
+let generate output_dir (xref_table:XrefTable.t) xref_modules title hierarchy_dot_file dependency_dot_file =
   let indexed_items =
     List.map (fun c ->
         let items =
@@ -321,4 +334,4 @@ let generate output_dir (xref_table:XrefTable.t) xref_modules title hierarchy_do
   List.iter (fun kind ->
       List.iter (generate_with_capital output_dir (table indexed_items) all_files kind) indexed_items)
     kinds;
-  generate_topfile output_dir all_files indexed_items title xref_table hierarchy_dot_file
+  generate_topfile output_dir all_files indexed_items title xref_table hierarchy_dot_file dependency_dot_file

generate_index.mli

@@ -20,4 +20,4 @@ type file_path
 val all_files : (string, unit) Hashtbl.t -> file_path list
 val sidebar_files : file_path list -> string
 
-val generate : string -> XrefTable.t -> (string, unit) Hashtbl.t -> string -> string -> unit
+val generate : string -> XrefTable.t -> (string, unit) Hashtbl.t -> string -> string -> string -> unit

ocamldot/LICENSE

@@ -0,0 +1,2 @@
+Ocamldot was written by Trevor Jim.  It is in the public domain; use
+it however you like, at your own risk.

ocamldot/Makefile

@@ -0,0 +1,23 @@
+# Try to automatically guess whether we are running under Windows.
+# Set WIN32=true manually if this doesn't work.
+#
+ifeq (${OSTYPE},cygwin32) # Cygwin Beta 19
+  WIN32=true
+else
+ifeq (${OSTYPE},cygwin)	  # Cygwin Beta 20
+  WIN32=true
+endif
+endif
+
+ifdef WIN32
+EXE=.exe
+else # UNIX
+EXE=
+endif
+
+ocamldot$(EXE): ocamldot.mll
+	ocamllex ocamldot.mll
+	ocamlc -annot -o $@ ocamldot.ml
+
+clean:
+	$(RM) ocamldot$(EXE) ocamldot.ml *.cmi *.cmo *.o *.obj

ocamldot/README

@@ -0,0 +1,34 @@
+Ocamldot generates program dependency graphs for ocaml programs.
+
+The dependency graph output by ocamldot can be rendered by a separate
+program, dot.  Dot is freely available from
+
+  http://www.research.att.com/sw/tools/graphviz/
+
+Ocamldot is designed to process the output of ocamldep.  A typical use
+would be
+
+  ocamldep *.ml | ocamldot > dep.dot
+
+or
+
+  ocamldep *.ml > .depend
+  ocamldot .depend > dep.dot
+
+This will output a dot graph into the file dep.dot.  You can then use
+the program dotty to view, edit, and print the graph.
+
+Ocamldot has the following options:
+
+  -fullgraph   draw the full graph (default is to draw only the kernel)
+  -landscape   output in landscape format (default is portrait)
+  -lr          draw graph from left to right (default is top to bottom)
+  -r <r>       use <r> as a root in the graph; nodes reachable from <r>
+               will be shown
+
+(The transitive kernel of a dag is the smallest subset of the dag
+whose transitive closure is the same as the transitive closure of the
+dag.  For example, the kernel of A->B, A->C, B->C is just the two
+edges A->B, B->C.)
+
+-Trevor Jim

ocamldot/ocamldot.1

@@ -0,0 +1,52 @@
+.TH OCAMLDOT 1
+.SH NAME
+ocamldot \- generate dependency graphs of ocaml programs
+.SH SYNOPSIS
+.B ocamldot
+.I 
+.RI "[options] <dependency-file>"
+.SH "DESCRIPTION"
+This manual page documents briefly the
+.BR ocamldot
+command.
+.PP
+.B ocamldot
+generates program dependency graphs for ocaml programs.  The
+dependency graph output by ocamldot can be rendered by a separate
+program, \fIdot\fR.
+.P
+Ocamldot is designed to process the output of ocamldep. A typical use would be 
+.P
+	ocamldep *.ml | ocamldot > dep.dot 
+.P
+or 
+.P
+	ocamldep *.ml > .depend
+.br
+	ocamldot .depend > dep.dot 
+.SH OPTIONS
+.TP
+.B \-fullgraph 
+Draw the full graph (default is to draw only the kernel) 
+.TP
+.B \-landscape 
+Output in landscape format (default is portrait) 
+.TP
+.B \-lr 
+Draw graph from left to right (default is top to bottom) 
+.TP
+.B \-r <r>
+Use \fI<r>\fR as a root in the graph; nodes reachable from \fI<r>\fR
+will be shown.
+.P
+The transitive kernel of a dag is the smallest subset of the dag whose transitive closure is the same as the transitive closure of the dag.
+For example, the kernel of A->B, A->C, B->C is just the two edges A->B, B->C.
+
+.SH SEE ALSO
+.BR ocamldep (1),
+.BR dot(1)
+.P
+\fIhttp://www.research.att.com/~trevor/ocamldot\fR.
+
+.SH AUTHOR
+Trevor Jim <[email protected]>