From 6995461742bc01431103f9efe54b6d81eaf87a7b Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 6 Apr 2019 10:04:44 +0100 Subject: [PATCH 1/3] Improved error handling during patch installation. --- install | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/install b/install index 31b1b2c..a120571 100755 --- a/install +++ b/install @@ -129,13 +129,16 @@ check_isa_dof_patch() { command -v md5sum >/dev/null 2>&1 || echo " Warning: md5sum not available, cannot check if patch is already applied." echo " Warning: Isabelle/DOF patch is not available or outdated." echo " Trying to patch system ...." - if (cp $dst $dst.backup-by-isadof-installer && cp -f $src $dst) &> /dev/null; then + if [ ! -f "$dst.backup-by-isadof-installer" ]; then + cp -f "$dst" "$dst.backup-by-isadof-installer" || true; + fi + if (cp -f $src $dst) &> /dev/null; then echo " Applied patch successfully, Isabelle/HOL will be rebuilt during" echo " the next start of Isabelle." else echo " FAILURE: Could not apply Isabelle/DOF patch." - echo " Please copy patches/thy_output.ML to $ISABELLE_HOME/src/Pure/Thy/:" - echo " cp patches/thy_output.ML $ISABELLE_HOME/src/Pure/Thy/" + echo " Please copy $src to $dst, e.g.:" + echo " cp -f $src $dst" echo " and rebuild Isabelle/HOL." exit_error fi From d5e295c7f318393587c0819bc3f6c775e0da57c1 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 6 Apr 2019 10:22:40 +0100 Subject: [PATCH 2/3] Use cmp instead of md5sum for checking if files are identical. --- install | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/install b/install index a120571..e0e241f 100755 --- a/install +++ b/install @@ -118,7 +118,7 @@ check_isa_dof_patch() { src="patches/thy_output.ML" dst="$ISABELLE_HOME/src/Pure/Thy/thy_output.ML" - if command -v md5sum > /dev/null 2>&1 && [[ $(md5sum "$src" | cut -d' ' -f1) = $(md5sum "$dst" | cut -d' ' -f1) ]]; then + if command -v cmp > /dev/null 2>&1 && cmp -s "$src" "$dst" ; then echo " Success: latest Isabelle/DOF patch already applied" if isabelle process -e 'Thy_Output.set_meta_args_parser' &> /dev/null ; then true @@ -126,7 +126,7 @@ check_isa_dof_patch() { echo " Warning: Isabelle/HOL needs to be rebuild to activate patch." fi else - command -v md5sum >/dev/null 2>&1 || echo " Warning: md5sum not available, cannot check if patch is already applied." + command -v cmp >/dev/null 2>&1 || echo " Warning: cmp not available, cannot check if patch is already applied." echo " Warning: Isabelle/DOF patch is not available or outdated." echo " Trying to patch system ...." if [ ! -f "$dst.backup-by-isadof-installer" ]; then From e4c1356a798fc282d78e6ff68deac32bb9d5b3cd Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 6 Apr 2019 10:23:30 +0100 Subject: [PATCH 3/3] Fixed spelling in info/warning/error messages. --- install | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/install b/install index e0e241f..4c24817 100755 --- a/install +++ b/install @@ -114,7 +114,7 @@ check_afp_entries() { } check_isa_dof_patch() { - echo "* Check availabilty of Isabelle/DOF patch:" + echo "* Check availability of Isabelle/DOF patch:" src="patches/thy_output.ML" dst="$ISABELLE_HOME/src/Pure/Thy/thy_output.ML" @@ -152,7 +152,7 @@ check_old_installation(){ rm -rf "$ISABELLE_HOME_USER/DOF.bak" mv "$ISABELLE_HOME_USER/DOF" "$ISABELLE_HOME_USER/DOF.bak" else - echo " No old instllation found." + echo " No old installation found." fi }