configure

#! /bin/bash
# Script to generate the configuration '.config' file for the framework.
# Copyright (C) 2008 Supercomputing Systems AG
# 
# Copying and distribution of this file, with or without modification,
# are permitted in any medium without royalty. This file is offered as-is,
# without any warranty.

set -e -o pipefail

print() { echo "$1" >&2; }
inform() { print "$0: $1"; }
warn() { print "Warning: $1"; }
error() { inform "Error: $1"; }
fail() { error "$1"; exit 1; }
status() { echo -n "$1" >&2; }

get_config() {
	# get_config $1 $2: load a configuration from a configuration file
	# $1: the name of the configuration file
	# $2: name of the configuration variable
	
	local CONFIG_FILE=$1 NAME=$2 EXPR="s/^#?$NAME[\t ]*=[\t ]*(.*)[\t ]*$/\1/p"
	[ -e "$CONFIG_FILE" ] && sed -rn "$EXPR" < "$CONFIG_FILE" | head -n 1 || true
}

ask() {
	# ask $1 $2: ask the user something and return the answer
	# $1: the default value
	# $2: the prompt
	
	read -e -p "$2 [$1]: " 
	[ "$REPLY" ] && echo $REPLY || echo $1
}

variable_read() {
	# variable_read $1: read the value of the variable with the given name
	# $1: the name of the variable
	
	eval echo \"\$"$1"\"
}

variable_write() {
	# variable_write $1 $2: write a value to the variable with the given name
	# $1: the name of the variable
	# $2: the value to write
	
	eval "$1"='$2'
}

SCRIPT_DIR=$(dirname "$BASH_SOURCE")
CONF_FILE=$(readlink -f "$SCRIPT_DIR/.config")

. "$SCRIPT_DIR/configure.in"

# Read the configurations set on the command line.
while [ "$1" ]; do
	echo "$1" | grep -qF "=" || "Unknown option: $$1"
	
	NAME=$(echo "$1" | cut -d "=" -f 1)
	VALUE=$(echo "$1" | cut -d "=" -f 2)
	
	echo "$NAME" | grep -xqF "$(echo "$CONFIGS" | tr ' ' '\n' | sed -r 's/^/CONFIG_/')" || fail "Unknown variable: $$NAME"
	variable_write "$NAME" "$VALUE"
	
	shift
done

# Ask the user about configurations.
for i_name in $CONFIGS; do
	NAME="CONFIG_$i_name"
	
	{
		VALUE_CLI=$(variable_read "$NAME")
		VALUE_FILE=$(get_config "$CONF_FILE" "$NAME")
		VALUE_DEFAULT=$("$NAME" default)
	} > /dev/null
	
	# Check if we should ask for the configuration.
	if "$NAME" enabled; then
		# Check if the configuration value has been given on the command line.
		if [ "$VALUE_CLI" ]; then
			VALUE_NEW=$VALUE_CLI
		else
			[ "$VALUE_FILE" ] && VALUE=$VALUE_FILE || VALUE=$VALUE_DEFAULT
			PROMPT=$("$NAME" prompt)
			
			while true; do
				VALUE_NEW=$(ask "$VALUE" "$PROMPT")
				
				echo "$VALUE_NEW" | "$NAME" check && break
				print "The configuration is not valid: $VALUE_NEW"
			done
			
		fi > /dev/null
		
		variable_write "$NAME" "$VALUE_NEW" > /dev/null
		echo "$NAME = $VALUE_NEW"
	else
		if [ "$VALUE_CLI" ]; then
			VALUE_NEW=$VALUE_CLI
		elif [ "$VALUE_FILE" ]; then
			VALUE_NEW=$VALUE_FILE
		else
			VALUE_NEW=
		fi > /dev/null
		
		[ "$VALUE_NEW" ] && echo "#$NAME = $VALUE_NEW"
	fi
done > "${CONF_FILE}~"

# Move the new configuration file in place.
mv -f "${CONF_FILE}~" "${CONF_FILE}"

# Call the makefile to update according to the new configuration.
make -C "$SCRIPT_DIR" --no-print-directory reconfigure