runtimeverification / plutus-core-semantics

BSD 3-Clause "New" or "Revised" License
27 stars 5 forks source link

Collecting execution time data #274

Open ChristianoBraga opened 2 years ago

ChristianoBraga commented 2 years ago
  1. IOG's uplc must be in your path.
  2. Save the script below in a file, say comp-time.sh, in the root directory of plutus-semantics, and run chmod +x comp-time.sh.
    
    #!/bin/bash

KPLC_CMD=".build/usr/bin/kplc run" TIMEFORMAT="%E;%U;%S" echo " ; kplc ; ; ; uplc ; ; ;" echo "Test file ; Real ; User ; System ; Real ; User ; System ;" echo " ; Elapsed real time ; CPU-seconds in user mode ; CPU-seconds in kernel mode ; Elapsed real time ; CPU-seconds in user mode ; CPU-seconds in kernel mode ;"

for i in $1/.uplc ; do OUT+="$(basename $i);" OUT+=$( { time $KPLC_CMD $i 1> /dev/null ; } 2>&1 ) OUT=${OUT/==.uplc/} OUT+=";" OUT+=$( { time uplc evaluate -i $i 1> /dev/null ; } 2>&1 ) echo $OUT OUT="" done


2. In the root directory of `plutus-semantics`, run `./comp-time.sh <dir> > comparison.csv` where `<dir>` = `tests/textual/simple`, for instance, or any directory with `uplc` files, with `.uplc` extensions. The file `comparison.csv` is a semicolon (";") separated file where the columns are the test file name followed by real, user and system times for `kplc` and `uplc`.

Note: Some (expected) error messages are not yet filtered by the script.