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;

#!/bin/bash
#
# Author: Gerwin Klein
#
#  make a copy of IMP with isaverbatimwrite lines in thy files removed

## diagnostics

function fail()
{
  echo "$1" >&2
  exit 2
}

## main

EXPORT=IMP

rm -rf "$EXPORT"

# make directories

DIRS=$(find . -type d)
for D in $DIRS; do
    mkdir -p "$EXPORT/$D" || fail "could not create directory $EXPORT/$D"
done

# filter thy files

FILES=$(find . -name "*.thy")
for F in $FILES; do
    grep -v isaverbatimwrite "$F" > "$EXPORT/$F"
done

# copy rest

cp ROOT.ML "$EXPORT"
cp -r document "$EXPORT"

# tar and clean up
tar cvzf "$EXPORT.tar.gz" "$EXPORT"
rm -r "$EXPORT"