src/HOL/IMP/export.sh
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 53498 05313b45a5ae
permissions -rwxr-xr-x
Lots of new material for multivariate analysis
wenzelm@53498
     1
#!/usr/bin/env bash
kleing@45254
     2
#
kleing@45254
     3
# Author: Gerwin Klein
kleing@45254
     4
#
kleing@45254
     5
#  make a copy of IMP with isaverbatimwrite lines in thy files removed
kleing@45254
     6
kleing@45254
     7
## diagnostics
kleing@45254
     8
kleing@45254
     9
function fail()
kleing@45254
    10
{
kleing@45254
    11
  echo "$1" >&2
kleing@45254
    12
  exit 2
kleing@45254
    13
}
kleing@45254
    14
kleing@45254
    15
## main
kleing@45254
    16
kleing@45254
    17
EXPORT=IMP
kleing@45254
    18
kleing@45254
    19
rm -rf "$EXPORT"
kleing@45254
    20
kleing@45254
    21
# make directories
kleing@45254
    22
kleing@45254
    23
DIRS=$(find . -type d)
kleing@45254
    24
for D in $DIRS; do
kleing@45254
    25
    mkdir -p "$EXPORT/$D" || fail "could not create directory $EXPORT/$D"
kleing@45254
    26
done
kleing@45254
    27
kleing@45254
    28
# filter thy files
kleing@45254
    29
kleing@45254
    30
FILES=$(find . -name "*.thy")
kleing@45254
    31
for F in $FILES; do
kleing@45254
    32
    grep -v isaverbatimwrite "$F" > "$EXPORT/$F"
kleing@45254
    33
done
kleing@45254
    34
kleing@45254
    35
# copy rest
kleing@45254
    36
kleing@45254
    37
cp ROOT.ML "$EXPORT"
kleing@45254
    38
cp -r document "$EXPORT"
kleing@45254
    39
kleing@45254
    40
# tar and clean up
kleing@45254
    41
tar cvzf "$EXPORT.tar.gz" "$EXPORT"
kleing@45254
    42
rm -r "$EXPORT"