1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465 |
- #!/bin/bash
- if [ $# -ne 2 ]; then
- cat<<EOF
- Usage: $0 <module> <output file>
- Runs various benchmarks for the Agda file <module>.
- EOF
- exit 1
- else
- MODULE="$1"
- OUTPUT="$2"
- fi
- printf "Benchmarks for $MODULE\n\n" > "$OUTPUT"
- printf "Configuration:\n" >> "$OUTPUT"
- if [[ `uname` == 'Darwin' ]]; then
- uname -ms >> "$OUTPUT"
- else
- uname -io >> "$OUTPUT"
- fi
- agda --version >> "$OUTPUT"
- ghc --version >> "$OUTPUT"
- emacs --version | head -1 >> "$OUTPUT"
- printf "Byte-compiled files:\n" >> "$OUTPUT"
- ELDIR=$(dirname `agda-mode locate`)
- for FILE in "$ELDIR"/*.el; do
- ELCFILE=$(basename "$FILE" .el).elc
- if [ -r "$ELDIR"/"$ELCFILE" ]; then
- printf " %s\n" "$ELCFILE" >> "$OUTPUT"
- fi
- done
- printf "\n" >> "$OUTPUT"
- printf "Batch-mode:\n" >> "$OUTPUT"
- rm -f "$MODULE"i
- 'time' -p agda -v0 "$MODULE" 2>>"$OUTPUT"
- for MODE in None NonInteractive Interactive; do
- printf "\nHaskell only, %s:\n" $MODE >> "$OUTPUT"
- rm -f "$MODULE"i
- printf '\nioTCM "%s" %s (cmd_load "%s" [])\n' "$MODULE" $MODE "$MODULE" | \
- time -p agda --ghci-interaction > /dev/null 2>>"$OUTPUT"
- done
- # for MODE in none non-interactive interactive; do
- # printf "\nIn Emacs, %s: " $MODE >> "$OUTPUT"
- # emacs -Q \
- # --eval "(load-file (let ((coding-system-for-read 'utf-8))
- # (shell-command-to-string \"agda-mode locate\")))" \
- # "$MODULE" \
- # --eval "(progn
- # (defun test nil
- # (agda2-measure-load-time '$MODE nil
- # (lambda (time)
- # (with-temp-buffer
- # (insert time)
- # (append-to-file (point-min) (point-max) \"$OUTPUT\"))
- # (kill-emacs))))
- # (run-with-idle-timer 1 nil 'test))" \
- # 2>/dev/null
- # printf "\n" >> "$OUTPUT"
- # done
|