diff --git a/extras/depgraph/leandeps.sh b/extras/depgraph/leandeps.sh new file mode 100755 index 0000000000..4337ad7e11 --- /dev/null +++ b/extras/depgraph/leandeps.sh @@ -0,0 +1,21 @@ +#!/usr/bin/env bash +set -e + +sanitizer="s,\\.o\?lean,,g" +for dir in $(lean -p | tr : ' '); do + if [[ -d $dir ]]; then + dir=$(readlink -f $dir) + sanitizer="$sanitizer;s,$dir/,,g" + fi +done + +echo 'digraph {' + +for lean_fn in $(find $@ -name \*.lean -not -name .\*); do + lean_fn=$(readlink -f $lean_fn) + for dep_lean_fn in $(lean --deps $lean_fn); do + echo "\"$lean_fn\" -> \"$dep_lean_fn\"" + done +done | sed "$sanitizer" + +echo '}'