src/HOL/IMP/export.sh
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45254 e41c679c9d82
child 53498 05313b45a5ae
permissions -rwxr-xr-x
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45254
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
     1
#!/bin/bash
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
     2
#
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
     3
# Author: Gerwin Klein
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
     4
#
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
     5
#  make a copy of IMP with isaverbatimwrite lines in thy files removed
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
     6
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
     7
## diagnostics
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
     8
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
     9
function fail()
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    10
{
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    11
  echo "$1" >&2
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    12
  exit 2
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    13
}
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    14
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    15
## main
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    16
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    17
EXPORT=IMP
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    18
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    19
rm -rf "$EXPORT"
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    20
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    21
# make directories
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    22
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    23
DIRS=$(find . -type d)
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    24
for D in $DIRS; do
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    25
    mkdir -p "$EXPORT/$D" || fail "could not create directory $EXPORT/$D"
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    26
done
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    27
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    28
# filter thy files
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    29
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    30
FILES=$(find . -name "*.thy")
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    31
for F in $FILES; do
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    32
    grep -v isaverbatimwrite "$F" > "$EXPORT/$F"
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    33
done
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    34
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    35
# copy rest
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    36
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    37
cp ROOT.ML "$EXPORT"
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    38
cp -r document "$EXPORT"
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    39
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    40
# tar and clean up
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    41
tar cvzf "$EXPORT.tar.gz" "$EXPORT"
e41c679c9d82 script for exporting filtered IMP files as tar.gz
kleing
parents:
diff changeset
    42
rm -r "$EXPORT"