Allow both Dedukti v2.5 and Dedukti v2.6 as long as Sukerujo has the

same version

configure

@@ -10,7 +10,57 @@ print_to_stderr ()
     echo "$1" > /dev/stderr
 }
 
+version_min ()
+{
+    # Compare $1 and $2 as version numbers and return the smallest
+    ( echo "$1"; echo "$2" ) | sort -V | head -n 1
+}
+
+version_leq ()
+{
+    # Check that $1 <= $2 where <= is ordering between version numbers
+    if [ "$1" = $(version_min "$1" "$2") ]
+    then
+        return 0
+    else
+        print_to_stderr ""
+        print_to_stderr "ERROR: version constraint not satisfied: $1 <= $2"
+        return 1
+    fi
+}
+
+version_geq ()
+{
+    # Check that $1 >= $2 where >= is ordering between version numbers
+    version_leq "$2" "$1"
+}
+
+version_lt ()
+{
+    # Check that $1 < $2 where < is ordering between version numbers
+    if [ "$2" = $(version_min "$1" "$2") ]
+    then
+        print_to_stderr ""
+        print_to_stderr "ERROR: version constraint not satisfied: $1 < $2"
+        return 1
+    fi
+}
+
+version_eq ()
+{
+    # Check that $1 and $2 are equal version numbers
+    if [ "$1" = "$2" ]
+    then
+        return 0
+    else
+        print_to_stderr ""
+        print_to_stderr "ERROR: version constraint not satisfied: $1 = $2"
+        return 1
+    fi
+}
+
 declare -A VARS
+declare -A VERSIONS
 
 find_binary () {
     # $1 is the name of the binary
@@ -18,83 +68,83 @@ find_binary () {
     # locate
 
     # Start by looking in path
-    print_to_stderr "Looking for program '$1' in PATH"
+    print_to_stderr "Looking for program '$1' in PATH."
     A=$(which "$1")
     if [ -n "$A" ]
     then
-        print_to_stderr "program '$1' found in PATH at \"$A\""
+        print_to_stderr "Program '$1' found in PATH at \"$A\"."
         echo "$A"
         return 0
     # else use locate
     else
-        print_to_stderr "program '$1' not found in PATH, trying with locate"
+        print_to_stderr "Program '$1' not found in PATH, trying with locate."
         A=$(locate "$1$2" | head -n 1)
         if [ -n "$A" ]
         then
-            print_to_stderr "program '$1$2' found using locate at \"$A\""
+            print_to_stderr "Program '$1$2' found using locate at \"$A\"."
             echo "$A"
             return 0
         else
             print_to_stderr ""
-            print_to_stderr "ERROR: program '$1$2' not found"
+            print_to_stderr "ERROR: Program '$1$2' not found."
             return 1
         fi
     fi
 }
 
-find_binary_no_check () {
-    # $1 and $2 are arguments to find_binary
-    # $3 is the variable name
-    A=$(find_binary $1 $2)
-    VARS[$3]="$A"
-    print_to_file "$3=\"$A\""
-    return 0
-}
-
-find_and_check_binary () {
+find_binary_and_version () {
     # $1 and $2 are arguments to find_binary
     # $3 is the variable name
     # $4 is the option to pass to the program to ask for its version
-    # $5 is the expected answer
     A=$(find_binary $1 $2)
     VARS[$3]="$A"
     VERSION_COMMAND="$A $4"
-    print_to_stderr "asking '$1' for its version number ($VERSION_COMMAND)"
+    print_to_stderr "Asking '$1' for its version number."
     B=$(eval $VERSION_COMMAND |& cat)
-    print_to_stderr "'$1' has version '$B'"
-    if [ "$B" = "$5" ]
-    then
-        print_to_stderr "'$1' has the expected version number"
-        print_to_file "$3=\"$A\""
-        return 0
-    else
-        print_to_stderr ""
-        print_to_stderr "ERROR: '$1' has version '$B' but version '$5' was expected"
-        return 1
-    fi
+    print_to_stderr "Program '$1' has version '$B'."
+    VERSIONS[$3]="$B"
+    print_to_file "$3=\"$A\""
 }
 
-echo > .config_vars &&
+echo -n > .config_vars &&
+
+# Core
+## Dedukti
+find_binary_and_version "dkcheck" ".native" "DKCHECK" "-version | cut -d ' ' -f 2" &&
+version_geq "${VERSIONS["DKCHECK"]}" "v2.5" &&
+find_binary_and_version "dkdep" ".native" "DKDEP" "" &&
+## Sukerujo
+find_binary_and_version "skcheck" ".native" "SKCHECK" "-version | cut -d ' ' -f 2" &&
+version_eq "${VERSIONS["SKCHECK"]}" "${VERSIONS["DKCHECK"]}" &&
+## FoCaLiZe
+find_binary_and_version "focalizec" "" "FOCALIZEC" "-v |& cut -d ' ' -f 5" &&
+version_eq "${VERSIONS["FOCALIZEC"]}" "0.9.2" &&
+find_binary_and_version "focalizedep" "" "FOCALIZEDEP" "" &&
 
-# Mandatory
-find_binary_no_check "dkdep" ".native" "DKDEP" &&
-find_and_check_binary "dkcheck" ".native" "DKCHECK" "-version" "Dedukti v2.5" &&
-find_and_check_binary "skcheck" ".native" "SKCHECK" "-version" "Sukerujo v2.5" &&
-find_and_check_binary "focalizec" "" "FOCALIZEC" "-v" "The FoCaLize compiler, version 0.9.2" &&
-find_binary_no_check "focalizedep" "" "FOCALIZEDEP" &&
-find_and_check_binary "coqc" "" "COQC" "-v | grep version | cut -d ' ' -f 6" "8.4pl6" &&
-find_and_check_binary "coqtop" "" "COQTOP" "-v | grep version | cut -d ' ' -f 6" "8.4pl6" &&
+# Interop
+## Coq
+find_binary_and_version "coqc" "" "COQC" "-v | grep version | cut -d ' ' -f 6" &&
+### Other Coq 8.4 versions probably work too but not >= 8.5
+version_eq "${VERSIONS["COQC"]}" "8.4pl6" &&
+find_binary_and_version "coqtop" "" "COQTOP" "-v | grep version | cut -d ' ' -f 6" &&
+version_eq "${VERSIONS["COQTOP"]}" "${VERSIONS["COQC"]}" &&
 
-# Check that Coqine is installed.  I do not know how to check the version
-if ( echo 'Require Coqine.' | ${VARS["COQTOP"]})
+## Check that Coqine is installed.  I do not know how to check the version
+if ( echo 'Require Coqine.' | ${VARS["COQTOP"]} &> /dev/null)
 then
-    print_to_stderr "Coqine found."
+    print_to_stderr "Program 'Coqine' found."
 else
-    print_to_stderr "Coqine not found."
+    print_to_stderr ""
+    print_to_stderr "ERROR: Program 'Coqine' not found."
     exit 1
 fi &&
 
-find_and_check_binary "opentheory" "" "OPENTHEORY" "-v" "opentheory 1.3 (release 20160204)" &&
-find_and_check_binary "holide" "" "HOLIDE" "--version" "Holide HOL to Dedukti translator, version 0.2.1 (Holala)" &&
+## OpenTheory tool
+find_binary_and_version "opentheory" "" "OPENTHEORY" "-v | cut -d ' ' -f 2" &&
+version_eq "${VERSIONS["OPENTHEORY"]}" "1.3" &&
+find_binary_and_version "holide" "" "HOLIDE" "--version" &&
+version_eq "${VERSIONS["HOLIDE"]}" \
+           "Holide HOL to Dedukti translator, version 0.2.1 (Holala)" &&
 print_to_stderr "" &&
-print_to_stderr "Configuration successful, please invoke make"
+print_to_stderr "Configuration successful, please invoke make" &&
+print_to_stderr ""