Skip to content

Commit

Permalink
Bug fix: clusters' names are now unique integers.
Browse files Browse the repository at this point in the history
With the previous implementation, all the files in the
subdirectory [XXX] where gathered in a cluster named
[clusterXXX].

In coqtail we have the directory [src/Reals/] as well as
[src/Fresh/Reals] and we ended up producing a dot file
with two distinct clusters named [clusterReals].
And this was confusing for dot.

Now that each name is unique, we won't have this kind of
problem anymore.

** Special thanks **
Bug fixed thanks to marapet's diagnostic on stackoverflow:
http://stackoverflow.com/questions/11584771/cryptic-dot-error-message-for-graph-with-big-subclusters/



git-svn-id: svn+ssh://svn.code.sf.net/p/coqtail/code@401 7194d10d-a3ed-4628-aea2-7b4a0dfde000
  • Loading branch information
gallais committed Jul 24, 2012
1 parent 163ff20 commit 9376144
Show file tree
Hide file tree
Showing 2 changed files with 13 additions and 11 deletions.
6 changes: 3 additions & 3 deletions depend/README
Expand Up @@ -12,7 +12,7 @@ II. How to get a nice graph?

1. Run [coqdep -dumpgraph] or [coqdep -dumpgraph boxes]
2. Use tred (graphviz) to get rid of redundant edges
3. To get coqtail's dependencies graph, go to coqtail's
src/ directory, run [./generate_makedep.sh] which will
followed by [./Dependencies]. The result is in [graph.pdf]
3. To get coqtail's dependencies' graph, go to coqtail's
src/ directory, run [./generate_makedep.sh] followed by
[./dependencies]. The result is in [graph.pdf]

18 changes: 10 additions & 8 deletions depend/coqdep_common.ml
Expand Up @@ -404,7 +404,7 @@ let coq_dependencies () =
(fun (name,_) ->
let ename = escape name in
let glob = if !option_noglob then "" else " "^ename^".glob" in
printf "%s%s%s: %s.v" ename !suffixe glob ename;
printf "%s%s%s %s.v.beautified: %s.v" ename !suffixe glob ename ename;
traite_fichier_Coq true (name ^ ".v");
printf "\n";
flush stdout)
Expand Down Expand Up @@ -591,14 +591,16 @@ let rec insert_graph name path graphs = match path, graphs with
| _, hd :: tl -> hd :: (insert_graph name path tl)
| (box :: boxes), [] -> [ Subgraph (box, insert_graph name boxes []) ]

let rec print_graphs = function
| [] -> ()
| (Element str) :: tl -> printf "%s\n" str; print_graphs tl
let print_graphs graph =
let rec print_aux name = function
| [] -> name
| (Element str) :: tl -> printf "%s\n" str; print_aux name tl
| Subgraph (box, names) :: tl ->
printf "subgraph cluster%s {\n label=\"%s\"" box box;
print_graphs names;
printf "}\n";
print_graphs tl
printf "subgraph cluster%n {\n label=\"%s\"" name box;
let name = print_aux (name + 1) names in
printf "}\n"; print_aux name tl
in
let _ = print_aux 0 graph in ()

let rec pop_common_prefix = function
| [Subgraph (_, graphs)] -> pop_common_prefix graphs
Expand Down

0 comments on commit 9376144

Please sign in to comment.