Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

merge
HOL-OCL/Isabelle_DOF/master This commit looks good Details

This commit is contained in:
Burkhart Wolff 2019-04-06 12:16:36 +02:00
parent e362286c32 e4c1356a79
commit 4a61b55763
1 changed files with 18 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

42
install
View File

@ -114,11 +114,11 @@ 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"
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,28 +126,22 @@ check_isa_dof_patch() {
echo " Warning: Isabelle/HOL needs to be rebuild to activate patch."
fi
else
if command -v md5 > /dev/null 2>&1 && [[ $(md5 "$src" | cut -d' ' -f1) = $(md5 "$dst" | cut -d' ' -f1) ]]; then
echo " Success: latest Isabelle/DOF patch already applied"
if isabelle process -e 'Thy_Output.set_meta_args_parser' &> /dev/null ; then
true
else
echo " Warning: Isabelle/HOL needs to be rebuild to activate patch."
fi
else
ommand -v md5sum >/dev/null 2>&1 || command -v md5 >/dev/null 2>&1 || echo " Warning: neither md5sum inor md5 were 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
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 " and rebuild Isabelle/HOL."
exit_error
fi
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
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 $src to $dst, e.g.:"
echo " cp -f $src $dst"
echo " and rebuild Isabelle/HOL."
exit_error
fi
fi
}
@ -158,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
}