isabelle: lib/Tools/makeall@d74dc1b54930 (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	#
9788 df671fa2562a GPLed; wenzelm parents: 7277 diff changeset	3	# Author: Markus Wenzel, TU Muenchen
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	4	#
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	5	# DESCRIPTION: apply make utility to all logics
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	6
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	7	## diagnostics
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	8
10511 efb3428c9879 tuned; wenzelm parents: 9788 diff changeset	9	PRG="$(basename "$0")"
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	10
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	11	function usage()
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	12	{
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	13	echo
28650 a7ba12e0d3b7 tuned usage line; wenzelm parents: 28504 diff changeset	14	echo "Usage: isabelle $PRG [ARGS ...]"
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	15	echo
32325 300b7d5d23d7 turned object-logics into components; wenzelm parents: 29143 diff changeset	16	echo " Apply isabelle make to all components with IsaMakefile (passing ARGS)."
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	17	echo
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	18	exit 1
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	19	}
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	20
13229 a2b09d99e5cf fail early kleing parents: 10555 diff changeset	21	function fail()
a2b09d99e5cf fail early kleing parents: 10555 diff changeset	22	{
a2b09d99e5cf fail early kleing parents: 10555 diff changeset	23	echo "$1" >&2
a2b09d99e5cf fail early kleing parents: 10555 diff changeset	24	exit 2
a2b09d99e5cf fail early kleing parents: 10555 diff changeset	25	}
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	26
32325 300b7d5d23d7 turned object-logics into components; wenzelm parents: 29143 diff changeset	27
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	28	## main
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	29
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	30	[ "$1" = "-?" ] && usage
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	31
13235 c26fc3baeffc fail not so early, but produce correct exit code in the end kleing parents: 13229 diff changeset	32	FAIL=""
c26fc3baeffc fail not so early, but produce correct exit code in the end kleing parents: 13229 diff changeset	33
10511 efb3428c9879 tuned; wenzelm parents: 9788 diff changeset	34	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	35	. "$ISABELLE_HOME/lib/scripts/timestart.bash"
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	36
32390 468eff174a77 function splitarray: splightly more abstract version that accomodates older bashes; wenzelm parents: 32325 diff changeset	37	splitarray ":" "$ISABELLE_COMPONENTS"; COMPONENTS=("${SPLITARRAY[@]}")
32325 300b7d5d23d7 turned object-logics into components; wenzelm parents: 29143 diff changeset	38
300b7d5d23d7 turned object-logics into components; wenzelm parents: 29143 diff changeset	39	for DIR in "${COMPONENTS[@]}"
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	40	do
32325 300b7d5d23d7 turned object-logics into components; wenzelm parents: 29143 diff changeset	41	if [ -f "$DIR/IsaMakefile" ]; then
300b7d5d23d7 turned object-logics into components; wenzelm parents: 29143 diff changeset	42	NAME="$(basename "$DIR")"
300b7d5d23d7 turned object-logics into components; wenzelm parents: 29143 diff changeset	43	( cd "$DIR"; "$ISABELLE_TOOL" make "$@" ) \|\| FAIL="$FAIL$NAME "
300b7d5d23d7 turned object-logics into components; wenzelm parents: 29143 diff changeset	44	fi
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, 01 Nov 2009 20:55:14 +0100
changeset 33371	d74dc1b54930
parent 32390	468eff174a77
permissions	-rwxr-xr-x