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
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Gerwin Klein
     4 #
     5 #  make a copy of IMP with isaverbatimwrite lines in thy files removed
     6 
     7 ## diagnostics
     8 
     9 function fail()
    10 {
    11   echo "$1" >&2
    12   exit 2
    13 }
    14 
    15 ## main
    16 
    17 EXPORT=IMP
    18 
    19 rm -rf "$EXPORT"
    20 
    21 # make directories
    22 
    23 DIRS=$(find . -type d)
    24 for D in $DIRS; do
    25     mkdir -p "$EXPORT/$D" || fail "could not create directory $EXPORT/$D"
    26 done
    27 
    28 # filter thy files
    29 
    30 FILES=$(find . -name "*.thy")
    31 for F in $FILES; do
    32     grep -v isaverbatimwrite "$F" > "$EXPORT/$F"
    33 done
    34 
    35 # copy rest
    36 
    37 cp ROOT.ML "$EXPORT"
    38 cp -r document "$EXPORT"
    39 
    40 # tar and clean up
    41 tar cvzf "$EXPORT.tar.gz" "$EXPORT"
    42 rm -r "$EXPORT"