isabelle: lib/Tools/makeall@7ba952481e29 (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	## global settings
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	8
15845 e84b1842a7a5 ALL_LOGICS: topological order; wenzelm parents: 14981 diff changeset	9	ALL_LOGICS="Pure FOL HOL ZF CCL CTT Cube FOLP HOLCF LCF Sequents"
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	10
dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	11
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	12	## diagnostics
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	13
10511 efb3428c9879 tuned; wenzelm parents: 9788 diff changeset	14	PRG="$(basename "$0")"
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	15
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	16	function usage()
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	17	{
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	18	echo
28650 a7ba12e0d3b7 tuned usage line; wenzelm parents: 28504 diff changeset	19	echo "Usage: isabelle $PRG [ARGS ...]"
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	20	echo
28504 7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle; wenzelm parents: 28500 diff changeset	21	echo " Apply isabelle make to all logics (passing ARGS)."
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	22	echo
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	23	exit 1
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	24	}
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	25
13229 a2b09d99e5cf fail early kleing parents: 10555 diff changeset	26	function fail()
a2b09d99e5cf fail early kleing parents: 10555 diff changeset	27	{
a2b09d99e5cf fail early kleing parents: 10555 diff changeset	28	echo "$1" >&2
a2b09d99e5cf fail early kleing parents: 10555 diff changeset	29	exit 2
a2b09d99e5cf fail early kleing parents: 10555 diff changeset	30	}
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	31
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	32	## main
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	33
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	34	[ "$1" = "-?" ] && usage
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	35
13235 c26fc3baeffc fail not so early, but produce correct exit code in the end kleing parents: 13229 diff changeset	36	FAIL=""
c26fc3baeffc fail not so early, but produce correct exit code in the end kleing parents: 13229 diff changeset	37
10511 efb3428c9879 tuned; wenzelm parents: 9788 diff changeset	38	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	39	. "$ISABELLE_HOME/lib/scripts/timestart.bash"
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	40
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	41	for L in $ALL_LOGICS
44e57a6d947d new version; wenzelm parents: 3957 diff changeset	42	do
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 18321 diff changeset	43	( cd "$ISABELLE_HOME/src/$L"; "$ISABELLE_TOOL" make "$@" ) \|\| FAIL="$FAIL$L "
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	44	done
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	45
4456 44e57a6d947d new version; wenzelm parents: 3957 diff changeset	46	echo -n "Finished at "; date
2502 dcf928805273 make all Isabelle systems afresh; wenzelm parents: diff changeset	47
18321 3414557c2dda replaced lib/scripts/showtime by more advanced lib/scripts/timestart\|stop.bash; wenzelm parents: 15845 diff changeset	48	. "$ISABELLE_HOME/lib/scripts/timestop.bash"
3414557c2dda replaced lib/scripts/showtime by more advanced lib/scripts/timestart\|stop.bash; wenzelm parents: 15845 diff changeset	49	echo "$TIMES_REPORT"
13235 c26fc3baeffc fail not so early, but produce correct exit code in the end kleing parents: 13229 diff changeset	50
13834 4d50cf8ea3d7 == -> = kleing parents: 13235 diff changeset	51	[ "$FAIL" = "" ] \|\| fail "Logics ${FAIL}FAILED!"

author	wenzelm
	Sat, 10 Jan 2009 13:10:07 +0100
changeset 29427	7ba952481e29
parent 29143	72c960b2b83e
child 32325	300b7d5d23d7
permissions	-rwxr-xr-x