equal
deleted
inserted
replaced
1 #!/bin/bash |
1 #!/bin/bash |
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
|
4 # Author: Markus Wenzel, TU Muenchen |
|
5 # License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 # |
6 # |
5 # Poly/ML startup script. |
7 # Poly/ML startup script. |
6 # |
8 # |
7 # Global vars: INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP, |
9 # Global vars: INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP, |
8 # and from settings |
10 # and from settings |
26 } |
28 } |
27 |
29 |
28 |
30 |
29 ## Poly/ML programs |
31 ## Poly/ML programs |
30 |
32 |
31 POLY=$ML_HOME/poly |
33 POLY="$ML_HOME/poly" |
32 DISCGARB=$ML_HOME/discgarb |
34 DISCGARB="$ML_HOME/discgarb" |
33 |
35 |
34 check_mlhome_file "$POLY" |
36 check_mlhome_file "$POLY" |
35 check_mlhome_file "$DISCGARB" |
37 check_mlhome_file "$DISCGARB" |
36 |
38 |
37 |
39 |
66 cp "$INFILE" "$OUTFILE" || fail_out |
68 cp "$INFILE" "$OUTFILE" || fail_out |
67 chmod +w "$OUTFILE" || fail_out |
69 chmod +w "$OUTFILE" || fail_out |
68 DB="$OUTFILE" |
70 DB="$OUTFILE" |
69 else |
71 else |
70 [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; } |
72 [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; } |
71 echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | $POLY -r "$INFILE" |
73 echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | "$POLY" -r "$INFILE" |
72 [ -f "$OUTFILE" ] || fail_out |
74 [ -f "$OUTFILE" ] || fail_out |
73 DB="$OUTFILE" |
75 DB="$OUTFILE" |
74 fi |
76 fi |
75 |
77 |
76 |
78 |
82 FEEDER_OPTS="-q" |
84 FEEDER_OPTS="-q" |
83 fi |
85 fi |
84 |
86 |
85 DB_INFO=$(ls -l "$DB") |
87 DB_INFO=$(ls -l "$DB") |
86 |
88 |
87 $ISABELLE_HOME/lib/scripts/feeder -p -h "$MLTEXT" $FEEDER_OPTS | \ |
89 "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" $FEEDER_OPTS | \ |
88 { read FPID; $POLY $ML_OPTIONS "$DB"; RC=$?; kill -HUP $FPID; exit $RC; } |
90 { read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } |
89 RC=$? |
91 RC="$?" |
90 |
92 |
91 NEW_DB_INFO=$(ls -l "$DB") |
93 NEW_DB_INFO=$(ls -l "$DB") |
92 [ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB -c "$OUTFILE" |
94 [ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && "$DISCGARB" -c "$OUTFILE" |
93 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
95 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" |
94 |
96 |
95 exit $RC |
97 exit "$RC" |