<commit_before><?xml version="1.0" encoding="UTF-8"?>
<project name="TLA+ Tools" default="default" xmlns:jacoco="antlib:org.jacoco.ant">

	<!-- load property file -->
	<loadproperties srcfile="project.properties" />

	<!-- linking with system properties -->
	<property environment="env" />

	<!-- setup classpath -->
	<path id="project.classpath">

	</path>

	<!-- timestamp -->
	<tstamp>
		<format property="TODAY" pattern="yyyy-MM-dd" locale="en,US" />
	</tstamp>

	<!-- JaCoCo code coverage -->
	<taskdef uri="antlib:org.jacoco.ant" resource="org/jacoco/ant/antlib.xml">
		<classpath path="lib/jacocoant.jar"/>
	</taskdef>

	<taskdef resource="org/aspectj/tools/ant/taskdefs/aspectjTaskdefs.properties">
		<classpath>
			<pathelement location="lib/aspectjtools-1.8.5.jar" />
		</classpath>
	</taskdef>
	
	<condition property="test.skip">
		<istrue value="${maven.test.skip}"/>
	</condition>

	<condition property="test.halt">
		<istrue value="${maven.test.halt}"/>
	</condition>

	<!-- https://github.com/alx3apps/jgit-buildnumber -->
	<target name="git-revision">
	    <taskdef name="jgit-buildnumber" classname="ru.concerteza.util.buildnumber.JGitBuildNumberAntTask">
			<classpath>
				<pathelement location="lib/org.eclipse.jgit-2.3.1.201302201838-r.jar"/>
				<pathelement location="lib/jgit-buildnumber-ant-task-1.2.10.jar" />
			</classpath>
	    </taskdef>
	    <jgit-buildnumber/>
	</target>
	
	<target name="info" description="Prints information" depends="git-revision">
		<echo message="ANT_HOME     : ${env.ANT_HOME}" />
		<echo message="Ant Version  : ${ant.version}" />
		<echo message="Java Version : ${ant.java.version}" />
		<echo message="Skipping Tests : ${test.skip}" />
		<echo message="With AspectJ: ${withaj}" />
		<echo message="Git BuildNumber: ${git.branch}_${git.tag}_${git.shortRevision}" />
	</target>

	<target name="default" depends="info" description="Default">
		<antcall target="compile" inheritall="true" inheritrefs="true" />
		<antcall target="compile-aj" inheritall="true" inheritrefs="true" />
		<antcall target="compile-test" inheritall="true" inheritrefs="true" />
		<antcall target="test" inheritall="true" inheritrefs="true" />
		<antcall target="git-revision" inheritall="true" inheritrefs="true" />
		<antcall target="dist" inheritall="true" inheritrefs="true" />
		<antcall target="test-dist" inheritall="true" inheritrefs="true" />
	</target>

	<target name="default-release" depends="info" description="Produces a release">
		<antcall target="compile" inheritall="true" inheritrefs="true" />
		<antcall target="dist-mixed-zip" inheritall="true" inheritrefs="true" />
	</target>

	<!-- Compiles and runs the short-running tests. -->
	<target name="shorttests" depends="info" description="Run tests">
		<antcall target="default" inheritall="true" inheritrefs="true" />
		<antcall target="test-verify" inheritall="true" inheritrefs="true" />
	</target>

	<!-- Compiles and runs *only* the long-running tests. Not the ones. -->
	<target name="longtests" depends="info" description="Run long-running tests">
		<antcall target="compile" inheritall="true" inheritrefs="true" />
		<antcall target="compile-aj" inheritall="true" inheritrefs="true">
			<!-- long tests require AspjectJ -->
	        <param name="withaj" value="true"/>
	    </antcall>
		<antcall target="compile-test" inheritall="true" inheritrefs="true" />
		<antcall target="dist" inheritall="true" inheritrefs="true" />
		<antcall target="test-dist-long" inheritall="true" inheritrefs="true" />
	</target>
	
	<!-- ===========================================================-->
	<!-- Don't call any of the targets below, use the umbrella      -->
	<!-- targets above which correctly call a target's dependencies -->
	<!-- ===========================================================-->

	<!-- Cleans the compilation output directory -->
	<target name="clean" unless="noclean">
		<delete includeemptydirs="true" failonerror="false">
			<fileset dir="${class.dir}" includes="*/**" />
			<fileset dir="${test.class.dir}" includes="*/**" />
		</delete>
		<!-- Delete leftovers from previous junit invocation -->
		<delete includeemptydirs="true" failonerror="false">
			<fileset dir="states/" includes="*/**" />
		</delete>
	</target>

	<!-- Compiles the TLA+ tools code -->
	<target name="compile" depends="clean">
		<echo>
			================================================================
			= The following warnings about sun.misc.Unsafe can be ignored. = 
			= OffHeapDiskFPSet has been written using Unsafe to best use   =
			= a computer's memory. If Unsafe is removed from the JVM,      =
			= OffHeapDiskFPSet won't work anymore.                         =
			================================================================
		</echo>
		<!-- compile -->
		<mkdir dir="${class.dir}" />
		<javac includeantruntime="false" srcdir="${src.dir}" destdir="${class.dir}" debug="true" verbose="false" source="1.8" target="1.8">
			<!-- compilerarg value="-Xlint:deprecation"/-->
			<classpath refid="project.classpath" />
			<classpath>
				<pathelement location="lib/javax.mail.jar" />
			</classpath>
		</javac>

		<!-- copy the resource files -->
		<copy todir="${class.dir}">
			<fileset dir="${src.dir}">
				<include name="**/*.*" />
				<exclude name="**/*.java" />
				<exclude name="**/*.~*" />
				<exclude name="**/*##*" />
			</fileset>
		</copy>
	</target>

	<!-- Compiles AspectJ auxiliary code -->
	<target name="compile-aj" if="withaj">
		<echo>
			====================================================================
			= The following warnings (Xlint:adviceDidNotMatch) can be ignored. =
			= We are doing load time weaving that kicks in when TLC gets       = 
			= started, not when it is compiled.                                =
			====================================================================
		</echo>
		<!-- compile aspectj related class files -->
		<iajc destdir="${class.dir}" sourceRoots="${src-aj.dir}" debug="true" source="1.8" target="1.8">
			<classpath refid="project.classpath" />
			<classpath>
				<pathelement location="lib/aspectjrt-1.8.5.jar" />
				<pathelement location="lib/aspectjtools-1.8.5.jar" />
				<pathelement path="${class.dir}" />
			</classpath>
		</iajc>
		<!-- copy the resource files -->
		<copy todir="${class.dir}">
			<fileset dir="${src-aj.dir}">
				<include name="**/*.*" />
				<exclude name="**/*.aj" />
				<exclude name="**/*.java" />
				<exclude name="**/*.~*" />
				<exclude name="**/*##*" />
			</fileset>
		</copy>
		<!-- These files are requried for load time weaving and during runtime -->
		<copy todir="${class.dir}/lib">
			<fileset dir="lib/">
				<include name="aspectjrt-1.8.5.jar" />
				<include name="aspectjweaver-1.8.5.jar" />
			</fileset>
		</copy>
	</target>

	<!-- Creates a distribution out of compiled code -->
	<target name="dist">
		<!-- Extract javax.mail jar into class directory to be packaged into tla2tools.jar -->
		<!-- javax.mail is used by the MailSender functionality, that mails the output -->
		<!-- of TLC to a given email address. -->
		<!-- The javax.mail dependency as well as javax.activation is also depended upon -->
		<!-- by the tla2tools OSGi bundle and is expected to be the same version. -->
		<unzip src="lib/javax.mail.jar" dest="${class.dir}"/>

		<!-- Extract javax.mail to maven classes folder. This script is triggered by -->
		<!-- maven. However, maven compiles the code again to target/classes from -->
		<!-- where it creates the plugin -->
		<unzip src="lib/javax.mail.jar" dest="target/classes"/>

		<!-- TODO: add javax.activation to lib/ and extract it here too. Otherwise we have a -->
		<!-- runtime dependency on Java 6. -->

		<!-- create a JAR file for the users -->
		<mkdir dir="${dist.dir}" />
		<jar destfile="${dist.file}">
			<fileset dir="${class.dir}" includes="**/*" />
			<manifest>
				<attribute name="Built-By" value="${user.name}" />
				<attribute name="Build-Tag" value="${env.BUILD_TAG}" />
				<attribute name="Build-Rev" value="${Build-Rev}" />
				<attribute name="Implementation-Title" value="TLA+ Tools" />
				<attribute name="Implementation-Version" value="${version} ${TODAY}" />
				<attribute name="Implementation-Vendor" value="Microsoft Corp." />
				<!-- Git revision -->
				<attribute name="X-Git-Branch" value="${git.branch}" />
				<attribute name="X-Git-Tag" value="${git.tag}" />
				<attribute name="X-Git-Revision" value="${git.revision}" />
				<attribute name="X-Git-ShortRevision" value="${git.shortRevision}" />
				<attribute name="X-Git-BuildNumber" value="${git.branch}_${git.tag}_${git.shortRevision}" />
				<attribute name="X-Git-Commits-Count" value="${git.commitsCount}" />
				<!-- App-Name and Permissions is required by Java Webstart used by distributed TLC -->
				<!-- Depending on security level, the user will see a warning otherwise. -->
				<!-- http://docs.oracle.com/javase/7/docs/technotes/guides/jweb/security/manifest.html -->
				<attribute name="Application-Name" value="TLC" /><commit_msg>Exclude bogus content from jar file creation to reduce size of tla2tools.jar<commit_after><?xml version="1.0" encoding="UTF-8"?>
<project name="TLA+ Tools" default="default" xmlns:jacoco="antlib:org.jacoco.ant">

	<!-- load property file -->
	<loadproperties srcfile="project.properties" />

	<!-- linking with system properties -->
	<property environment="env" />

	<!-- setup classpath -->
	<path id="project.classpath">

	</path>

	<!-- timestamp -->
	<tstamp>
		<format property="TODAY" pattern="yyyy-MM-dd" locale="en,US" />
	</tstamp>

	<!-- JaCoCo code coverage -->
	<taskdef uri="antlib:org.jacoco.ant" resource="org/jacoco/ant/antlib.xml">
		<classpath path="lib/jacocoant.jar"/>
	</taskdef>

	<taskdef resource="org/aspectj/tools/ant/taskdefs/aspectjTaskdefs.properties">
		<classpath>
			<pathelement location="lib/aspectjtools-1.8.5.jar" />
		</classpath>
	</taskdef>
	
	<condition property="test.skip">
		<istrue value="${maven.test.skip}"/>
	</condition>

	<condition property="test.halt">
		<istrue value="${maven.test.halt}"/>
	</condition>

	<!-- https://github.com/alx3apps/jgit-buildnumber -->
	<target name="git-revision">
	    <taskdef name="jgit-buildnumber" classname="ru.concerteza.util.buildnumber.JGitBuildNumberAntTask">
			<classpath>
				<pathelement location="lib/org.eclipse.jgit-2.3.1.201302201838-r.jar"/>
				<pathelement location="lib/jgit-buildnumber-ant-task-1.2.10.jar" />
			</classpath>
	    </taskdef>
	    <jgit-buildnumber/>
	</target>
	
	<target name="info" description="Prints information" depends="git-revision">
		<echo message="ANT_HOME     : ${env.ANT_HOME}" />
		<echo message="Ant Version  : ${ant.version}" />
		<echo message="Java Version : ${ant.java.version}" />
		<echo message="Skipping Tests : ${test.skip}" />
		<echo message="With AspectJ: ${withaj}" />
		<echo message="Git BuildNumber: ${git.branch}_${git.tag}_${git.shortRevision}" />
	</target>

	<target name="default" depends="info" description="Default">
		<antcall target="compile" inheritall="true" inheritrefs="true" />
		<antcall target="compile-aj" inheritall="true" inheritrefs="true" />
		<antcall target="compile-test" inheritall="true" inheritrefs="true" />
		<antcall target="test" inheritall="true" inheritrefs="true" />
		<antcall target="git-revision" inheritall="true" inheritrefs="true" />
		<antcall target="dist" inheritall="true" inheritrefs="true" />
		<antcall target="test-dist" inheritall="true" inheritrefs="true" />
	</target>

	<target name="default-release" depends="info" description="Produces a release">
		<antcall target="compile" inheritall="true" inheritrefs="true" />
		<antcall target="dist-mixed-zip" inheritall="true" inheritrefs="true" />
	</target>

	<!-- Compiles and runs the short-running tests. -->
	<target name="shorttests" depends="info" description="Run tests">
		<antcall target="default" inheritall="true" inheritrefs="true" />
		<antcall target="test-verify" inheritall="true" inheritrefs="true" />
	</target>

	<!-- Compiles and runs *only* the long-running tests. Not the ones. -->
	<target name="longtests" depends="info" description="Run long-running tests">
		<antcall target="compile" inheritall="true" inheritrefs="true" />
		<antcall target="compile-aj" inheritall="true" inheritrefs="true">
			<!-- long tests require AspjectJ -->
	        <param name="withaj" value="true"/>
	    </antcall>
		<antcall target="compile-test" inheritall="true" inheritrefs="true" />
		<antcall target="dist" inheritall="true" inheritrefs="true" />
		<antcall target="test-dist-long" inheritall="true" inheritrefs="true" />
	</target>
	
	<!-- ===========================================================-->
	<!-- Don't call any of the targets below, use the umbrella      -->
	<!-- targets above which correctly call a target's dependencies -->
	<!-- ===========================================================-->

	<!-- Cleans the compilation output directory -->
	<target name="clean" unless="noclean">
		<delete includeemptydirs="true" failonerror="false">
			<fileset dir="${class.dir}" includes="*/**" />
			<fileset dir="${test.class.dir}" includes="*/**" />
		</delete>
		<!-- Delete leftovers from previous junit invocation -->
		<delete includeemptydirs="true" failonerror="false">
			<fileset dir="states/" includes="*/**" />
		</delete>
	</target>

	<!-- Compiles the TLA+ tools code -->
	<target name="compile" depends="clean">
		<echo>
			================================================================
			= The following warnings about sun.misc.Unsafe can be ignored. = 
			= OffHeapDiskFPSet has been written using Unsafe to best use   =
			= a computer's memory. If Unsafe is removed from the JVM,      =
			= OffHeapDiskFPSet won't work anymore.                         =
			================================================================
		</echo>
		<!-- compile -->
		<mkdir dir="${class.dir}" />
		<javac includeantruntime="false" srcdir="${src.dir}" destdir="${class.dir}" debug="true" verbose="false" source="1.8" target="1.8">
			<!-- compilerarg value="-Xlint:deprecation"/-->
			<classpath refid="project.classpath" />
			<classpath>
				<pathelement location="lib/javax.mail.jar" />
			</classpath>
		</javac>

		<!-- copy the resource files -->
		<copy todir="${class.dir}">
			<fileset dir="${src.dir}">
				<include name="**/*.*" />
				<exclude name="**/*.java" />
				<exclude name="**/*.~*" />
				<exclude name="**/*##*" />
			</fileset>
		</copy>
	</target>

	<!-- Compiles AspectJ auxiliary code -->
	<target name="compile-aj" if="withaj">
		<echo>
			====================================================================
			= The following warnings (Xlint:adviceDidNotMatch) can be ignored. =
			= We are doing load time weaving that kicks in when TLC gets       = 
			= started, not when it is compiled.                                =
			====================================================================
		</echo>
		<!-- compile aspectj related class files -->
		<iajc destdir="${class.dir}" sourceRoots="${src-aj.dir}" debug="true" source="1.8" target="1.8">
			<classpath refid="project.classpath" />
			<classpath>
				<pathelement location="lib/aspectjrt-1.8.5.jar" />
				<pathelement location="lib/aspectjtools-1.8.5.jar" />
				<pathelement path="${class.dir}" />
			</classpath>
		</iajc>
		<!-- copy the resource files -->
		<copy todir="${class.dir}">
			<fileset dir="${src-aj.dir}">
				<include name="**/*.*" />
				<exclude name="**/*.aj" />
				<exclude name="**/*.java" />
				<exclude name="**/*.~*" />
				<exclude name="**/*##*" />
			</fileset>
		</copy>
		<!-- These files are requried for load time weaving and during runtime -->
		<copy todir="${class.dir}/lib">
			<fileset dir="lib/">
				<include name="aspectjrt-1.8.5.jar" />
				<include name="aspectjweaver-1.8.5.jar" />
			</fileset>
		</copy>
	</target>

	<!-- Creates a distribution out of compiled code -->
	<target name="dist">
		<!-- Extract javax.mail jar into class directory to be packaged into tla2tools.jar -->
		<!-- javax.mail is used by the MailSender functionality, that mails the output -->
		<!-- of TLC to a given email address. -->
		<!-- The javax.mail dependency as well as javax.activation is also depended upon -->
		<!-- by the tla2tools OSGi bundle and is expected to be the same version. -->
		<unzip src="lib/javax.mail.jar" dest="${class.dir}"/>

		<!-- Extract javax.mail to maven classes folder. This script is triggered by -->
		<!-- maven. However, maven compiles the code again to target/classes from -->
		<!-- where it creates the plugin -->
		<unzip src="lib/javax.mail.jar" dest="target/classes"/>

		<!-- TODO: add javax.activation to lib/ and extract it here too. Otherwise we have a -->
		<!-- runtime dependency on Java 6. -->

		<!-- create a JAR file for the users -->
		<mkdir dir="${dist.dir}" />
		<jar destfile="${dist.file}" level="9">
			<fileset dir="${class.dir}" includes="**/*" excludes="
					**/*.jpg,
					tlc2/tool/fp/*.tla,
					pcal/*.tla,
					META-INF/maven/,
					src/tla2sany/parser/ParseException.09-09-07,
					src/tla2sany/parser/TLAplusParser.09-07-02,
					src/tla2sany/parser/TLAplusParser.11-02-10,
					src/tla2sany/parser/TLAplusParserConstants.09-07-02,
					src/tla2sany/parser/TLAplusParserConstants.09-09-07,
					src/tla2sany/parser/TLAplusParserConstants.11-02-10,
					src/tla2sany/parser/TLAplusParserTokenManager.09-07-02,
					src/tla2sany/parser/TLAplusParserTokenManager.09-09-07,
					src/tla2sany/parser/TLAplusParserTokenManager.11-02-10,
					src/tla2sany/parser/Token.09-09-07,
					src/tla2sany/parser/TokenMgrError.09-09-07"/>
			<manifest>
				<attribute name="Built-By" value="${user.name}" />
				<attribute name="Build-Tag" value="${env.BUILD_TAG}" />
				<attribute name="Build-Rev" value="${Build-Rev}" />
				<attribute name="Implementation-Title" value="TLA+ Tools" />
				<attribute name="Implementation-Version" value="${version} ${TODAY}" />
				<attribute name="Implementation-Vendor" value="Microsoft Corp." />
				<!-- Git revision -->
				<attribute name="X-Git-Branch" value="${git.branch}" />
				<attribute name="X-Git-Tag" value="${git.tag}" />
				<attribute name="X-Git-Revision" value="${git.revision}" />
				<attribute name="X-Git-ShortRevision" value="${git.shortRevision}" />
				<attribute name="X-Git-BuildNumber" value="${git.branch}_${git.tag}_${git.shortRevision}" />
				<attribute name="X-Git-Commits-Count" value="${git.commitsCount}" />
				<!-- App-Name and Permissions is required by Java Webstart used by distributed TLC -->
				<!-- Depending on security level, the user will see a warning otherwise. -->
				<!-- http://docs.oracle.com/javase/7/docs/technotes/guides/jweb/security/manifest.html -->
				<attribute name="Application-Name" value="TLC" />
{'fraction_non_alphanumeric': 0.22432446836859776, 'fraction_numerical': 0.00959334861162927, 'mean_word_length': 3.82985842985843, 'pattern_counts': {'":': 0, '<': 363, '<?xml version=': 2, '>': 363, 'https://': 2, 'lorem ipsum': 0, 'www.': 0, 'xml': 6}, 'pii_count': 2, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6854282', 'n_tokens_mistral': 6628, 'n_tokens_neox': 5793, 'n_words': 1304}