Quelle bench-render.sh Sprache: Shell

#!/usr/bin/env bash

set -ex
set -o pipefail

export COQBIN=$BIN
export PATH="$COQBIN:$PATH"
export LC_ALL=C

diff() {
command diff -a -u --strip-trailing-cr "$1" "$2"
}

cd misc/bench-render

rocq timelog2html foo.v foo.v.time1 foo.v.time2 > result.html.real

diff result.html result.html.real

if rocq timelog2html foo.v foo.v.time1 foo.v.time3 > bad1v3.html.real 2>stderr1v3.real
then >&2 echo "Should have failed!"; exit 1
fi

diff /dev/null bad1v3.html.real
diff stderr1v3 stderr1v3.real

if rocq timelog2html foo.v foo.v.time1 foo.v.time4 > bad1v4.html.real 2>stderr1v4.real
then >&2 echo "Should have failed!"; exit 1
fi

diff /dev/null bad1v4.html.real
diff stderr1v4 stderr1v4.real

quality98%

¤ Dauer der Verarbeitung: 0.3 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.