diff --git a/.github/workflows/deploy_static_site.yml b/.github/workflows/deploy_static_site.yml index cba42256..6cb6b55a 100644 --- a/.github/workflows/deploy_static_site.yml +++ b/.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 \ No newline at end of file + uses: actions/deploy-pages@v4 diff --git a/Makefile b/Makefile index 2b59c39c..94ef8cd5 100644 --- a/Makefile +++ b/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 diff --git a/coq2html.mll b/coq2html.mll index 38c408d0..865d685f 100644 --- a/coq2html.mll +++ b/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 on the index.html" + " Show the hierarchy graph of on the index.html"; + "-dependency-graph", Arg.Set_string dependency_graph_dot_file, + " Show the dependency graph of 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") diff --git a/generate_index.ml b/generate_index.ml index ea296d36..d2e53e2c 100644 --- a/generate_index.ml +++ b/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 {|

Mathematical Structures

-%s|} png_filename map + Printf.sprintf {|

Mathematical Structures (%s only)

+%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 {|

Clickable Dependency Graph of Files

%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 diff --git a/generate_index.mli b/generate_index.mli index ce7efd49..f8afdc65 100644 --- a/generate_index.mli +++ b/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 diff --git a/ocamldot/LICENSE b/ocamldot/LICENSE new file mode 100644 index 00000000..30021ab3 --- /dev/null +++ b/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. diff --git a/ocamldot/Makefile b/ocamldot/Makefile new file mode 100644 index 00000000..1e1620b8 --- /dev/null +++ b/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 diff --git a/ocamldot/README b/ocamldot/README new file mode 100644 index 00000000..8ac23d09 --- /dev/null +++ b/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 use as a root in the graph; nodes reachable from + 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 diff --git a/ocamldot/ocamldot.1 b/ocamldot/ocamldot.1 new file mode 100644 index 00000000..770397d7 --- /dev/null +++ b/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] " +.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 +Use \fI\fR as a root in the graph; nodes reachable from \fI\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 diff --git a/ocamldot/ocamldot.mll b/ocamldot/ocamldot.mll new file mode 100644 index 00000000..311a9fe7 --- /dev/null +++ b/ocamldot/ocamldot.mll @@ -0,0 +1,365 @@ +(* ocamldot.mll, July 1999, Trevor Jim *) +(* partly based on https://github.com/math-comp/Coq-Combi/ *) + +{ +module StringSet = + Set.Make(struct type t = string let compare = compare end) + +let dependencies = ref [] +let nodes = ref StringSet.empty +let currentSources = ref StringSet.empty +let addDepend1 s t = + if s<>t + then dependencies := (s,t)::(!dependencies) +let addDepend t = + StringSet.iter (fun s -> addDepend1 s t) !currentSources +let addSources source = + currentSources := StringSet.add source !currentSources +let clearSources () = + currentSources := StringSet.empty + +} + +rule processSources = parse + | ':' + { processTargets lexbuf } + | ['.' '-' '/' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' + '\248'-'\255' '\'' '0'-'9' ]+ '.' ['A'-'Z' 'a'-'z']+ + [' ' '\009']* + { let s = Lexing.lexeme lexbuf in + let i = String.index s '.' in + let s = String.sub s 0 i in + let s = String.capitalize_ascii s in + addSources s; + nodes := StringSet.add s (!nodes); + processSources lexbuf } + | eof + { () } + | _ + { processSources lexbuf } + +and processTargets = parse + [' ' '\009']+ + { processTargets lexbuf } + | '\\' [' ' '\009']* ['\010' '\013']+ [' ' '\009']+ + { processTargets lexbuf } + | ['.' '/' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' + '\248'-'\255' '\'' '0'-'9' ]+ '.' ['A'-'Z' 'a'-'z']+ + { let t = Lexing.lexeme lexbuf in + let i = String.index t '.' in + let t = String.sub t 0 i in + let t = String.capitalize_ascii t in + addDepend t; + processTargets lexbuf } + | eof + { () } + | _ + { clearSources (); + processSources lexbuf } + +{ + + (********************************) + (* Utility functions for graphs *) + (********************************) + + +(**********************************************************************) +(* A graph is represented by a (string * StringSet) list, *) +(* that is, a list of (source,targets) pairs. *) +(**********************************************************************) + +let emptyGraph = [] + +(**********************************************************************) +(* divideGraph graph source = (sourceTargets, graphWithoutSource) *) +(* *) +(* Return the targets of a source in a graph and the graph with the *) +(* source substracted from the sources. GraphWithoutSources may *) +(* still contain source as a target. *) +(**********************************************************************) +let divideGraph graph source = + let rec aux l = + match l with + [] -> (StringSet.empty,[]) + | (s,ts)::tl -> + if s=source then (ts,tl) + else + let (sourceTargets,tlWithoutSource) = aux tl in + (sourceTargets,(s,ts)::tlWithoutSource) in + aux graph + +(*********************************************) +(* Add the edge (source,target) to the graph *) +(*********************************************) +let addEdge graph source target = + let (sourceTargets,graphWithoutSource) = divideGraph graph source in + (source,StringSet.add target sourceTargets)::graphWithoutSource + +(************************************************************) +(* Add the edges { (source,t) | t in targets } to the graph *) +(************************************************************) +let addEdges graph source targets = + let (sourceTargets,graphWithoutSource) = divideGraph graph source in + (source,StringSet.union targets sourceTargets)::graphWithoutSource + +(**************************************************) +(* Remove the edge (source,target) from the graph *) +(**************************************************) +let removeEdge graph source target = + let rec loop l = + match l with + [] -> [] + | (s,ts)::tl -> + if s=source + then (s,StringSet.remove target ts)::tl + else (s,ts)::(loop tl) + in loop graph + +(*****************************************************************) +(* Remove the edges { (source,t) | t in targets } from the graph *) +(*****************************************************************) +let removeEdges graph source targets = + let rec loop l = + match l with + [] -> [] + | (s,ts)::tl -> + if s=source + then (s,StringSet.diff ts targets)::tl + else (s,ts)::(loop tl) + in loop graph + +(**********************************************************************) +(* Convert between an edge-list representation of graphs and our *) +(* representation. *) +(**********************************************************************) +let edgesOfGraph graph = + List.concat + (List.map + (fun (s,ts) -> + List.map (fun t -> (s,t)) (StringSet.elements ts)) + graph) + +let graphOfEdges edges = + List.fold_left + (fun g (s,t) -> addEdge g s t) + emptyGraph + edges + +(****************************) +(* Is an edge in the graph? *) +(****************************) +let isEdge graph source target = + try + let sourceTargets = List.assoc source graph in + StringSet.mem target sourceTargets + with Not_found -> false + +(*****************) +(* Print a graph *) +(*****************) +let printGraph graph = + let printEdges(source,targets) = + StringSet.iter + (fun t -> Printf.printf " \"%s\" -> \"%s\" ;\n" + (Filename.basename t) (Filename.basename source)) + targets + in + StringSet.iter + (fun t -> Printf.printf " \"%s\" [URL=\"%s.html\"];\n" (Filename.basename t) t) + !nodes; + List.iter printEdges graph + + +(********************************) +(* Targets of a node in a graph *) +(********************************) +let targetsOf graph node = (* A set of nodes *) + try List.assoc node graph + with Not_found -> StringSet.empty + +(*****************************************) +(* Sources that target a node in a graph *) +(*****************************************) +let sourcesOf graph node = (* A list of nodes *) + let rec aux l = + match l with + [] -> [] + | (s,ts)::tl -> + if StringSet.mem node ts then s::(aux tl) + else aux tl in + aux graph + +(******************************************************************) +(* Add an edge to a transitively closed graph, and return the new *) +(* transitive closure. *) +(******************************************************************) +let addEdgeTc graph source target = + let targetTargets = targetsOf graph target in + let (sourceTargets,graphWithoutSource) = divideGraph graph source in + let sourceSources = sourcesOf graphWithoutSource source in + let newSourceTargets = + StringSet.add target + (StringSet.union sourceTargets targetTargets) in + (source,newSourceTargets):: + (List.fold_right + (fun s g -> addEdges g s newSourceTargets) + sourceSources + graphWithoutSource) + +(**********************************************************) +(* Compute the transitive closure of a graph from scratch *) +(**********************************************************) +let tc graph = + let loop graph (source,targets) = + let reachableFromSource = + List.fold_left + (fun r (s,ts) -> + if StringSet.mem s r then StringSet.union r ts + else r) + targets + graph in + (source,reachableFromSource):: + (List.map + (fun (s,ts) -> + if StringSet.mem source ts + then (s,StringSet.union ts reachableFromSource) + else (s,ts)) + graph) in + List.fold_left loop [] graph + +(************************************************************************) +(* The transitive kernel (tk) of a dag is a subset of the dag whose *) +(* transitive closure is the same as the transitive closure of the dag. *) +(* *) +(* IF THE GRAPH IS NOT A DAG, THIS CODE WON'T WORK PROPERLY!!! *) +(************************************************************************) + +(************************************************************************) +(* Add an edge to a kernel dag and return the new kernel and transitive *) +(* closure of the new kernel. Requires the transitive closure of the *) +(* old kernel. *) +(************************************************************************) +let addEdgeTk kernel tcKernel source target = + if isEdge tcKernel source target + then (kernel,tcKernel) + else if source=target + then (addEdge kernel source target,tcKernel) + else + begin + let (sourceTargets,kernelWithoutSource) = divideGraph kernel source in + let targetTargets = StringSet.add target (targetsOf tcKernel target) in + let sourceSources = sourcesOf tcKernel source in + let kernelWithoutSource = + List.fold_left + (fun kws s -> removeEdges kws s targetTargets) + kernelWithoutSource + sourceSources in + ((source, + StringSet.add target + (StringSet.diff sourceTargets targetTargets)) + ::kernelWithoutSource, + addEdgeTc tcKernel source target) + end + +(**********************************) +(* The transitive kernel of a dag *) +(**********************************) +let tk dag = + let edges = edgesOfGraph dag in + let (kernel,tcKernel) = + List.fold_left + (fun (k,tck) (s,t) -> addEdgeTk k tck s t) + (emptyGraph,emptyGraph) + edges in + kernel + +(**************************) +(* Print the dependencies *) +(**************************) +let doKernel = ref true +let printDepend graph = + if (!doKernel) then printGraph (tk graph) + else printGraph graph + +let calledOnFile = ref false +let getDependFromFile file = + calledOnFile := true; + try + let ic = open_in file in + let lexbuf = Lexing.from_channel ic in + processSources lexbuf; + close_in ic + with Sys_error msg -> () + | Exit -> () +let getDependFromStdin () = + try + let lexbuf = Lexing.from_channel stdin in + processSources lexbuf + with Sys_error msg -> () + | Exit -> () + + (***************) + (* Entry point *) + (***************) + +let usage = "Usage: ocamldot [options] " + +let leftToRight = ref false +let roots = ref [] +;; + +Arg.parse + [ + ("-fullgraph", + Arg.Clear doKernel, + " draw the full graph (default is to draw only the kernel)"); + ("-lr", + Arg.Set leftToRight, + " draw graph from left to right (default is top to bottom)"); + ("-r", + Arg.String(fun s -> roots := s::!roots), + " use as a root in the graph; nodes reachable from \n will be shown") + ] + getDependFromFile usage; +if not(!calledOnFile) then getDependFromStdin(); +print_string "digraph depend {\n"; +print_string " dpi = 48;\n"; +if (!leftToRight) then print_string " rankdir = LR ;\n" +else print_string " rankdir = TB ;\n"; +print_string "bgcolor=transparent;\n splines=true;\n nodesep=1;\n node [fontsize=18, shape=rect, color=\"#dbc3b6\", style=filled];\n"; +let graph = graphOfEdges(!dependencies) in +begin + match !roots with + [] -> printDepend graph + | roots -> + (* Set up the graph so that the roots are printed at the same level *) + print_string " { rank=same ;\n"; + List.iter + (fun r -> + print_string " "; + print_string r; + print_string " ;\n") + roots; + print_string " };\n"; + (* Find the graph reachable from the roots *) + let tcGraph = tc graph in + let reachable node = + (List.exists (fun r -> r=node) roots) + || + (List.exists (fun r -> isEdge tcGraph r node) roots) in + let reachableFromRoots = + List.concat + (List.map + (fun (source,targets) -> + if reachable source + then [(source,targets)] + else []) + graph) in + printDepend reachableFromRoots +end; +print_string "}\n"; +exit 0 +;; + +} diff --git a/tools/generate-mathcomp-analysis.sh b/tools/generate-mathcomp-analysis.sh index 9f59b0a5..e11bc6e5 100755 --- a/tools/generate-mathcomp-analysis.sh +++ b/tools/generate-mathcomp-analysis.sh @@ -1,6 +1,7 @@ #!/bin/sh set -eux MATHCOMP_ANALYSIS=./analysis +COMMIT_HASH=$1 DIR=$(pwd `dirname .`) OUTDIR=$DIR/html @@ -11,13 +12,27 @@ cd $MATHCOMP_ANALYSIS ls -l -FILES=$(find classical/ theories/ -name "*.v" -or -name "*.glob") +FILES=$(find classical/ theories/ reals/ reals_stdlib experimental_reals analysis_stdlib -name "*.v" -or -name "*.glob") + +coqdep -f _CoqProject > depend.d +cat -n depend.d >&2 +$DIR/ocamldot/ocamldot depend.d > depend.dot +sed -i 's/Classical/mathcomp\.classical/' depend.dot +sed -i 's/Theories/mathcomp\.analysis/' depend.dot +sed -i 's/Reals_stdlib/mathcomp\.reals_stdlib/' depend.dot +sed -i 's/Experimental_reals/mathcomp\.experimental_reals/' depend.dot +sed -i 's/Reals/mathcomp\.reals/' depend.dot +sed -i 's/Analysis_stdlib/mathcomp\.analysis_stdlib/' depend.dot +sed -i 's/\//\./g' depend.dot $DIR/tools/generate-hierarchy-graph.sh -$DIR/coq2html -title "MathComp-Analysis" -d $OUTDIR -base mathcomp \ +$DIR/coq2html -title "MathComp-Analysis($COMMIT_HASH)" -d $OUTDIR -base mathcomp \ -Q theories analysis -coqlib https://coq.inria.fr/doc/V8.18.0/stdlib/ \ -external https://math-comp.github.io/htmldoc_2_1_0/ mathcomp.ssreflect \ -external https://math-comp.github.io/htmldoc_2_1_0/ mathcomp.algebra \ -hierarchy-graph "hierarchy-graph.dot" \ + -dependency-graph "depend.dot" \ $FILES + +cp hierarchy-graph.dot depend.dot $OUTDIR/