#!/usr/bin/env bash
# Copyright (c) 2019-2022 University of Exeter. 
#               2019 University of Paris-Saclay. 
#
# Redistribution and use in source and binary forms, with or without
# modification, are permitted provided that the following conditions
# are met:
# 1. Redistributions of source code must retain the above copyright
#    notice, this list of conditions and the following disclaimer.
# 2. Redistributions in binary form must reproduce the above copyright
#    notice, this list of conditions and the following disclaimer in
#    the documentation and/or other materials provided with the
#    distribution.
# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
# FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
# COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
# INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
# BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
# LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
# LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
# ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
# POSSIBILITY OF SUCH DAMAGE.
#
# SPDX-License-Identifier: BSD-2-Clause

set -e
shopt -s nocasematch


print_help()
{
    echo "Usage: mk_release [OPTION] "
    echo ""
    echo "       A tool for building an Isabelle/DOF release archive."
    echo ""
    echo "Run ..."
    echo ""
    echo "  --help, -h                display this help message"
    echo "  --sign, -s                sign release archive"
    echo "                            (default: $SIGN)"
    echo "  --isabelle, -i isabelle   isabelle command used for installation"
    echo "                            (default: $ISABELLE)"
    echo "  --tag tag, -t tag         use tag for release archive"
    echo "                            (default: use master branch)"
    echo "  --publish, -p             publish generated artefact"
    echo "                            (default: $PUBLISH)"
    echo "  --quick-and-dirty, -d     only build required artifacts, no complete test"
    echo "                            (default: $DIRTY)"
}

check_isabelle_version() {
    ACTUAL_ISABELLE_VERSION=`$ISABELLE version`
    echo "* Checking Isabelle version:"
    if [ "$ISABELLE_VERSION" != "$ACTUAL_ISABELLE_VERSION" ]; then
        echo "* Expecting $ISABELLE_VERSION, found $ACTUAL_ISABELLE_VERSION: ERROR"
        exit 1
    else
        echo "* Expecting $ISABELLE_VERSION, found $ACTUAL_ISABELLE_VERSION: success"
    fi
}

clone_repo()
{
    echo "* Cloning into $ISADOF_WORK_DIR"
    git clone . $ISADOF_WORK_DIR
    if [ "$USE_TAG" = "true" ]; then
        echo "  * Switching to tag $TAG"
        (cd $ISADOF_WORK_DIR && git checkout $TAG)
    else
        echo "  * No tag specified, using master branch"
    fi
    (cd $ISADOF_WORK_DIR && git show -s --format="COMMIT=%H%nDATE=%cd" --date=short | sed -e 's|-|/|g') >> $ISADOF_WORK_DIR/etc/settings
    
}

build_and_install_manuals()
{
    echo "* Building manual"

    if [ "$DIRTY" = "true" ]; then
        if [ -z ${ARTIFACT_DIR+x} ]; then
            echo "  * Quick and Dirty Mode (local build)"
            $ISABELLE build -d . Isabelle_DOF-Manual 2018-cicm-isabelle_dof-applications
            mkdir -p $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/
            cp examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/document.pdf \
               $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/
            mkdir -p $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/
            cp examples/technical_report/Isabelle_DOF-Manual/output/document.pdf \
               $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/;
        else
            echo "  * Quick and Dirty Mode (running on CI)"
            mkdir -p $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/
            cp $ARTIFACT_DIR/browser_info/Unsorted/2018-cicm-isabelle_dof-applications/document.pdf \
               $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/
 
            mkdir -p $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/
            cp $ARTIFACT_DIR/browser_info/Unsorted/Isabelle_DOF-Manual/document.pdf \
               $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/;
        fi
    else
        (cd $ISADOF_WORK_DIR && $ISABELLE env ./install-afp)
        (cd $ISADOF_WORK_DIR && $ISABELLE build -c -D . )
    fi
    mkdir -p $ISADOF_WORK_DIR/doc
    echo "Isabelle/DOF Manuals!" > $ISADOF_WORK_DIR/doc/Contents
    
    cp $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/document.pdf \
        $ISADOF_WORK_DIR/doc/Isabelle_DOF-Manual.pdf
    echo "  Isabelle_DOF-Manual                       User and Implementation Manual for Isabelle/DOF" >> $ISADOF_WORK_DIR/doc/Contents

    cp $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/document.pdf \
        $ISADOF_WORK_DIR/doc/2018-cicm-isabelle_dof-applications.pdf
    echo "  2018-cicm-isabelle_dof-applications       Example academic paper" >> $ISADOF_WORK_DIR/doc/Contents

    find $ISADOF_WORK_DIR -type d -name "output" -exec rm -rf {} \; &> /dev/null || true
    rm -rf $ISADOF_WORK_DIR/.git* $ISADOF_WORK_DIR/.woodpecker $ISADOF_WORK_DIR/.afp 
    
}

create_archive()
{    
    echo "* Creating archive"
    cp $ISADOF_WORK_DIR/doc/Isabelle_DOF-Manual.pdf  $ISADOF_TAR.pdf
    (mv $ISADOF_WORK_DIR $ISADOF_DIR)    
    (cd $BUILD_DIR && tar cf $ISADOF_TAR.tar $ISADOF_TAR && xz $ISADOF_DIR.tar)
    mv $BUILD_DIR/$ISADOF_TAR.tar.xz .
}

sign_archive()
{
    echo "* Signing archive"
    gpg --armor --output $ISADOF_TAR.tar.xz.asc --detach-sig $ISADOF_TAR.tar.xz
}

publish_archive()
{
    echo "* Publish archive"
    ssh 0x5f.org mkdir -p www/$DOF_ARTIFACT_HOST/htdocs/$DOF_ARTIFACT_DIR
    scp $ISADOF_TAR.* 0x5f.org:www/$DOF_ARTIFACT_HOST/htdocs/$DOF_ARTIFACT_DIR/
    ssh 0x5f.org chmod go+u-w -R www/$DOF_ARTIFACT_HOST/htdocs/$DOF_ARTIFACT_DIR
}


ISABELLE=`which isabelle`
USE_TAG="false"
SIGN="false"
PUBLISH="false"
DIRTY="false"
BUILD_DIR=`mktemp -d`
ISADOF_WORK_DIR="$BUILD_DIR/Isabelle_DOF"
while [ $# -gt 0 ]
do
    case "$1" in
        --isabelle|-i)
            ISABELLE="$2";
            shift;;
        --tag|-t)
            TAG="$2";
            USE_TAG="true"
            shift;;
        --sign|-s)
            SIGN="true";;
        --publish|-p)
            PUBLISH="true";;
        --quick-and-dirty|-d)
            DIRTY="true";;
        --help|-h)
            print_help
            exit 0;;
        *)  print_help
            exit 1;;
    esac
    shift
done


clone_repo

ISADOF_MAIN_DIR=`pwd`

if [ "$DIRTY" = "true" ]; then
    echo "Running in Quick and Dirty mode!"
    $ISABELLE components -u $ISADOF_MAIN_DIR
else
    $ISABELLE components -x $ISADOF_MAIN_DIR
    $ISABELLE components -u $ISADOF_WORK_DIR
fi

VARS=`$ISABELLE getenv ISABELLE_TOOL`
for i in $VARS; do
        export "$i"
done

ISABELLE_VERSION="Isabelle$($ISABELLE_TOOL options -g dof_isabelle)"
DOF_VERSION="$($ISABELLE_TOOL options -g dof_version)"

ISABELLE_SHORT_VERSION=`echo $ISABELLE_VERSION | sed -e 's/:.*$//'`
ISADOF_TAR="Isabelle_DOF-"$DOF_VERSION"_"$ISABELLE_SHORT_VERSION
ISADOF_DIR="$BUILD_DIR/$ISADOF_TAR"

check_isabelle_version
build_and_install_manuals

if [ "$DIRTY" != "true" ]; then
    $ISABELLE components -x $ISADOF_WORK_DIR
    $ISABELLE components -u $ISADOF_MAIN_DIR
fi

create_archive

if [ "$SIGN" = "true" ]; then
    sign_archive
fi

if [ "$PUBLISH" = "true" ]; then
    publish_archive
fi

rm -rf $BUILD_DIR

exit 0