isabelle: src/HOL/TPTP/lib/Tools/tptp_nitpick@050104f01bf9 (annotated)

42064 f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter blanchet parents: diff changeset	1	#!/usr/bin/env bash
f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter blanchet parents: diff changeset	2	#
f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter blanchet parents: diff changeset	3	# Author: Jasmin Blanchette
f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter blanchet parents: diff changeset	4	#
46319 c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: 46318 diff changeset	5	# DESCRIPTION: Nitpick for TPTP
42064 f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter blanchet parents: diff changeset	6
f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter blanchet parents: diff changeset	7
f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter blanchet parents: diff changeset	8	PRG="$(basename "$0")"
f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter blanchet parents: diff changeset	9
f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter blanchet parents: diff changeset	10	function usage() {
f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter blanchet parents: diff changeset	11	echo
47670 24babc4b1925 added timeout argument to TPTP tools blanchet parents: 46324 diff changeset	12	echo "Usage: isabelle $PRG TIMEOUT FILES"
42064 f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter blanchet parents: diff changeset	13	echo
46319 c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: 46318 diff changeset	14	echo " Runs Nitpick on TPTP problems."
47670 24babc4b1925 added timeout argument to TPTP tools blanchet parents: 46324 diff changeset	15	echo " Each problem is allocated at most TIMEOUT seconds."
42064 f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter blanchet parents: diff changeset	16	echo
f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter blanchet parents: diff changeset	17	exit 1
f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter blanchet parents: diff changeset	18	}
f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter blanchet parents: diff changeset	19
42108 f55562e77d5c add "-?" to "nitrox" tool blanchet parents: 42064 diff changeset	20	[ "$#" -eq 0 -o "$1" = "-?" ] && usage
f55562e77d5c add "-?" to "nitrox" tool blanchet parents: 42064 diff changeset	21
43811 402e1a0d93d9 better temp name creation for Nitrox -- still very hackish though, but should get us through CASC-23 and CASC-J6 blanchet parents: 43808 diff changeset	22	SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
402e1a0d93d9 better temp name creation for Nitrox -- still very hackish though, but should get us through CASC-23 and CASC-J6 blanchet parents: 43808 diff changeset	23
47670 24babc4b1925 added timeout argument to TPTP tools blanchet parents: 46324 diff changeset	24	TIMEOUT=$1
24babc4b1925 added timeout argument to TPTP tools blanchet parents: 46324 diff changeset	25	shift
24babc4b1925 added timeout argument to TPTP tools blanchet parents: 46324 diff changeset	26
64561 a7664ca9ffc5 updated CASC instructions + tuning blanchet parents: 62634 diff changeset	27	isabelle build -b HOL-TPTP 2>&1 \| grep --line-buffered -v "elapsed time$"
60546 dcb0b9b42fcb automatically build image blanchet parents: 60545 diff changeset	28
42064 f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter blanchet parents: diff changeset	29	for FILE in "$@"
f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter blanchet parents: diff changeset	30	do
46324 e4bccf5ec61e added problem importer blanchet parents: 46319 diff changeset	31	echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
60544 3daf5eacec05 removed (now illegal) semicolons in generated theory files blanchet parents: 54434 diff changeset	32	ML {* ATP_Problem_Import.nitpick_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
43811 402e1a0d93d9 better temp name creation for Nitrox -- still very hackish though, but should get us through CASC-23 and CASC-J6 blanchet parents: 43808 diff changeset	33	> /tmp/$SCRATCH.thy
64561 a7664ca9ffc5 updated CASC instructions + tuning blanchet parents: 62634 diff changeset	34	isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" -l HOL-TPTP \| grep --line-buffered -v "^###\\|^PROOF FAILED for depth\\|^Failure node\\|inferences so far. Searching to depth\\|^val \\|^Loading theory\\|^poly.*warning: The type of\\|^ monotype.$"
42064 f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter blanchet parents: diff changeset	35	done

author	haftmann
	Fri, 14 Jun 2019 08:34:27 +0000
changeset 70344	050104f01bf9
parent 64561	a7664ca9ffc5
child 81527	4f4159c2cad3
permissions	-rwxr-xr-x