<commit_before>#!/usr/bin/env bash

set -e

PADIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"

SYNC="rsync --exclude '.*' --chmod=ug=rwX --chmod=o=rX --recursive"
WEB_MACH="uwplse.org"
WEB_PATH="/var/www/verdi/dash/"
RDASH="${WEB_MACH}:${WEB_PATH}"
LDASH="${PADIR}/dash/"
NONCE=$(printf "PA-%s-%s-%s-%s" \
               $(date "+%y%m%d") \
               $(date "+%H%M%S") \
               $(hostname -s) \
               $(git rev-parse --abbrev-ref HEAD))
REPDIR="${LDASH}${NONCE}"

function main {
  echo "SYNC remote -> local"
  $SYNC "$RDASH" "$LDASH"

  mkdir "$REPDIR"
  cp index.html *.csv "$REPDIR"

  mkindex > "${LDASH}index.html"

  echo "SYNC local  -> remote"
  $SYNC "$LDASH" "$RDASH"
}

function mkindex {
  pushd "$LDASH" > /dev/null

  cat <<EOF
<!DOCTYPE html>
<html>
<head>
  <meta charset="UTF-8">
  <title>Verdi Proofalytics</title>
  <style>
    html {
      font-family: sans-serif;
    }
    body {
      margin: 30px;
    }
    h1 {
      font-size: 28pt;
      color: #4b2e83;
    }
    h2 {
      font-size: 18pt;
      color: #4b2e83;
    }
    p {
      font-size: 14pt;
    }
    .it {
      font-style: italic;
    }
    .bf {
      font-weight: bold;
    }
    ul {
      list-style-type: square;
    }
    li {
      padding-bottom: 10px;
    }
  </style>
</head>
<body>
  <h1>Verdi Proofalytics</h1>
  <ul>
EOF
  for d in PA-*; do
    printf "<li><a href='%s'>%s</a></li>" "$d" "$d"
  done
  cat <<EOF
  </ul>
</body>
</html>
EOF
  popd > /dev/null
}

main<commit_msg>add summary statistics to dash index<commit_after>#!/usr/bin/env bash

set -e

PADIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"

SYNC="rsync --exclude '.*' --chmod=ug=rwX --chmod=o=rX --recursive"
WEB_MACH="uwplse.org"
WEB_PATH="/var/www/verdi/dash/"
RDASH="${WEB_MACH}:${WEB_PATH}"
LDASH="${PADIR}/dash/"
NONCE=$(printf "PA-%s-%s-%s-%s" \
               $(date "+%y%m%d") \
               $(date "+%H%M%S") \
               $(hostname -s) \
               $(git rev-parse --abbrev-ref HEAD))
REPDIR="${LDASH}${NONCE}"

function main {
  echo "SYNC remote -> local"
  $SYNC "$RDASH" "$LDASH"

  mkdir "$REPDIR"
  cp index.html *.csv "$REPDIR"

  mkindex > "${LDASH}index.html"

  echo "SYNC local  -> remote"
  $SYNC "$LDASH" "$RDASH"
}

function mkindex {
  pushd "$LDASH" > /dev/null

  cat <<EOF
<!DOCTYPE html>
<html>
<head>
  <meta charset="UTF-8">
  <title>Verdi Proofalytics</title>
  <style>
    html {
      font-family: sans-serif;
    }
    body {
      margin: 30px;
    }
    h1 {
      font-size: 28pt;
      color: #4b2e83;
    }
    h2 {
      font-size: 18pt;
      color: #4b2e83;
    }
    p {
      font-size: 14pt;
    }
    .it {
      font-style: italic;
    }
    .bf {
      font-weight: bold;
    }
    ul {
      list-style-type: square;
    }
    li {
      padding-bottom: 10px;
      line-height: 150%;
    }
  </style>
</head>
<body>
  <h1>Verdi Proofalytics</h1>
  <ul>
EOF
  for rep in $(ls -r | grep 'PA-*'); do
    echo "<li>"

    printf "<a href='%s'>%s</a>\n" "$rep" "$rep"

    echo "<br> &nbsp;"
    echo "<span class='it'>max ltac:</span> &nbsp;"
    cat "${rep}/proof-times.csv" \
      | awk -v key=2 -f "${PADIR}/csv-sort.awk" \
      | awk -F "," 'NR == 2 {print $1 " (" $2 " ms)"}'

    echo "<br> &nbsp;"
    echo "<span class='it'>max qed:</span> &nbsp;"
    cat "${rep}/proof-times.csv" \
      | awk -v key=3 -f "${PADIR}/csv-sort.awk" \
      | awk -F "," 'NR == 2 {print $1 " (" $2 " ms)"}'

    echo "<br> &nbsp;"
    echo "<span class='it'>build time:</span> &nbsp;"
    awk 'BEGIN { FS = ","; tot = 0 }  \
         { tot += $2 }      \
         END { print tot " s"}' \
        "${rep}/build-times.csv"

    # TODO
    # echo "<br> &nbsp;"
    # echo "<span class='it'>admits:</span> &nbsp;"

    echo "</li>"
  done
  cat <<EOF
  </ul>
</body>
</html>
EOF
  popd > /dev/null
}

main
{'fraction_non_alphanumeric': 0.21630745260971176, 'fraction_numerical': 0.015840041547649963, 'mean_word_length': 2.103948428686543, 'pattern_counts': {'":': 0, '<': 63, '<?xml version=': 0, '>': 65, 'https://': 0, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7213263', 'n_tokens_mistral': 1657, 'n_tokens_neox': 1577, 'n_words': 343}