testsuite_upgrade_prover

#!/bin/bash

if [ -z "$1" ]; then
    echo "Usage: $0 <UPGRADE> [path/to/test.coma]"
    echo "UPGRADE should be of the form: Alt-Ergo,2.4.3=Alt-Ergo,2.5.3"
    echo "If no path to a specific coma file is passed, tries to upgrade all tests in the testsuite"
    echo "If a path to a coma file is passed, tries to upgrade this test, and save the result even if it is a partial upgrade"
    exit 1
fi

eval $(cargo run --bin dev-env)

if [ -z "$2" ]; then
    # upgrade all
    failed=()

    shopt -s globstar
    for file in creusot/tests/**/*.coma; do
        # only try to upgrade if it looks like there is a session directory
        SESSION_DIR="$(dirname $file)/$(basename $file .coma)"
        if [ -d "$SESSION_DIR" ]; then
            echo "==> Upgrading $file"
            why3_tools upgrade -L. --upgrade=$1 "$file"
            if [ $? != 0 ]; then
                failed+=("$file")
            fi
        fi
    done
    if [ ${#failed[@]} != 0 ]; then
        echo ""
        echo "Failed to upgrade the following tests:"
        printf "%s\n" "${failed[@]}"
    fi
else
    # upgrade a specific test
    echo "==> Upgrading $2"
    why3_tools upgrade --allow-partial -L. --upgrade=$1 "$2"
fi