isabelle: src/HOL/TPTP/lib/Tools/tptp_nitpick@735be7c77142 (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
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	27	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	28	do
46324 e4bccf5ec61e added problem importer blanchet parents: 46319 diff changeset	29	echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
47794 4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug) blanchet parents: 47670 diff changeset	30	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	31	> /tmp/$SCRATCH.thy
54434 e275d520f49d implemented 'tptp_translate' blanchet parents: 52124 diff changeset	32	"$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP \| grep --line-buffered -v "^###\\|^PROOF FAILED for depth\\|^Failure node\\|inferences so far. Searching to depth\\|^val \\|^Loading theory"
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	33	done

author	blanchet
	Tue, 09 Sep 2014 20:51:36 +0200
changeset 58264	735be7c77142
parent 54434	e275d520f49d
child 60544	3daf5eacec05
permissions	-rwxr-xr-x