isabelle: lib/Tools/makeall@68ff03c069a0 (annotated)

10555 2323ec838401 /usr/bin/env bash; wenzelm parents: 10511 diff changeset	1	#!/usr/bin/env bash
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	2	#
dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	3	# $Id$
9788 df671fa2562a GPLed; wenzelm parents: 7277 diff changeset	4	# Author: Markus Wenzel, TU Muenchen
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	5	#
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	6	# DESCRIPTION: apply make utility to all logics
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	7
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	8	## global settings
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	9
15845 e84b1842a7a5 ALL_LOGICS: topological order; wenzelm parents: 14981 diff changeset	10	ALL_LOGICS="Pure FOL HOL ZF CCL CTT Cube FOLP HOLCF LCF Sequents"
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	11
dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	12
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	13	## diagnostics
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	14
10511 efb3428c9879 tuned; wenzelm parents: 9788 diff changeset	15	PRG="$(basename "$0")"
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	16
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	17	function usage()
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	18	{
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	19	echo
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	20	echo "Usage: $PRG [ARGS ...]"
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	21	echo
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	22	echo " Apply isatool make to all logics (passing ARGS)."
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	23	echo
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	24	exit 1
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	25	}
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	26
13229 a2b09d99e5cf fail early kleing parents: 10555 diff changeset	27	function fail()
a2b09d99e5cf fail early kleing parents: 10555 diff changeset	28	{
a2b09d99e5cf fail early kleing parents: 10555 diff changeset	29	echo "$1" >&2
a2b09d99e5cf fail early kleing parents: 10555 diff changeset	30	exit 2
a2b09d99e5cf fail early kleing parents: 10555 diff changeset	31	}
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	32
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	33	## main
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	34
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	35	[ "$1" = "-?" ] && usage
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	36
13235 c26fc3baeffc fail not so early, but produce correct exit code in the end kleing parents: 13229 diff changeset	37	FAIL=""
c26fc3baeffc fail not so early, but produce correct exit code in the end kleing parents: 13229 diff changeset	38
10511 efb3428c9879 tuned; wenzelm parents: 9788 diff changeset	39	echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
18321 3414557c2dda replaced lib/scripts/showtime by more advanced lib/scripts/timestart\|stop.bash; wenzelm parents: 15845 diff changeset	40	. "$ISABELLE_HOME/lib/scripts/timestart.bash"
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	41
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	42	for L in $ALL_LOGICS
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	43	do
13235 c26fc3baeffc fail not so early, but produce correct exit code in the end kleing parents: 13229 diff changeset	44	( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make "$@" ) \|\| FAIL="$FAIL$L "
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	45	done
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	46
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	47	echo -n "Finished at "; date
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	48
18321 3414557c2dda replaced lib/scripts/showtime by more advanced lib/scripts/timestart\|stop.bash; wenzelm parents: 15845 diff changeset	49	. "$ISABELLE_HOME/lib/scripts/timestop.bash"
3414557c2dda replaced lib/scripts/showtime by more advanced lib/scripts/timestart\|stop.bash; wenzelm parents: 15845 diff changeset	50	echo "$TIMES_REPORT"
13235 c26fc3baeffc fail not so early, but produce correct exit code in the end kleing parents: 13229 diff changeset	51
13834 4d50cf8ea3d7 == -> = kleing parents: 13235 diff changeset	52	[ "$FAIL" = "" ] \|\| fail "Logics ${FAIL}FAILED!"

author	wenzelm
	Sun, 07 Oct 2007 13:41:31 +0200
changeset 24888	68ff03c069a0
parent 18321	3414557c2dda
child 28500	4b79e5d3d0aa
permissions	-rwxr-xr-x