Skip to content

Commit c5e9e65

Browse files
kjain14kjain14
committed
mCoq release 1.0
0 parents  commit c5e9e65

File tree

291 files changed

+41724
-0
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

291 files changed

+41724
-0
lines changed

‎README.txt

+39
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
Installing and using the mCoq public release
2+
--------------------------------------------
3+
4+
Note for ICSE Reviewers: We recently cleaned the code and improved our scripts for running the tool, so the steps shown in paper may differ from the ones below. Additionally, the directory structures may differ from the ones shown in the demo video.
5+
6+
0. Download and unpack the mCoq archive, and enter the directory:
7+
8+
```
9+
$ wget https://cozy.ece.utexas.edu/mcoq/mcoq.tgz
10+
$ tar xfz mcoq.tgz
11+
$ cd mcoq
12+
```
13+
14+
1. Make sure OPAM 2.0.5 is installed (https://opam.ocaml.org)
15+
16+
2. Make sure to use OCaml 4.07.1 via OPAM, for example:
17+
18+
```
19+
$ opam switch create 4.07.1
20+
$ opam switch 4.07.1
21+
$ eval $(opam env)
22+
```
23+
24+
3. Install Coq 8.10.2 and SerAPI 0.7.0 (pinning for convenience):
25+
26+
```
27+
$ opam update
28+
$ opam upgrade
29+
$ opam pin add coq 8.10.2
30+
$ opam pin add coq-serapi 8.10.0+0.7.0
31+
```
32+
33+
4. For example, here is how to apply mCoq to StructTact revision b95f041cb83986fb0fe1f9689d7196e2f09a4839 (https://github.com/uwplse/StructTact):
34+
35+
```
36+
$ ./mcoq.py --project StructTact --sha 82a85b7ec07e71fa6b30cfc05f6a7bfb09ef2510 --url https://github.com/uwplse/StructTact.git --buildcmd "./configure && make -j4" --qdir ".,StructTact"
37+
```
38+
39+
This command should generate a HTML report in the reports directory.

‎downloads/README.txt

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
Downloaded Coq projects and serialized files will appear here

‎jsexp/.gitignore

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
/.gradle

‎jsexp/build.gradle

+35
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
2+
apply plugin: 'java'
3+
apply plugin: 'maven'
4+
5+
group = 'de.tu-dresden.inf.lat.jsexp'
6+
version = '0.3.0-SNAPSHOT'
7+
8+
description = """jsexp"""
9+
10+
sourceCompatibility = 1.8
11+
targetCompatibility = 1.8
12+
13+
buildDir = 'target'
14+
libsDirName = '.'
15+
16+
17+
18+
repositories {
19+
mavenCentral()
20+
}
21+
22+
23+
dependencies {
24+
testCompile group: 'junit', name: 'junit', version: '4.12'
25+
}
26+
27+
28+
jar {
29+
manifest {
30+
attributes 'Implementation-Title': 'de.tu-dresden.inf.lat.jsexp' ,
31+
'Implementation-Version': version
32+
}
33+
}
34+
35+

‎jsexp/build.xml

+55
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<project name="jsexp" default="dist" basedir=".">
3+
4+
<!--
5+
*
6+
* Copyright (C) 2009, 2012, 2015 Julian Mendez
7+
*
8+
*
9+
* This file is part of jsexp.
10+
*
11+
* jsexp is free software: you can redistribute it and/or modify
12+
* it under the terms of the GNU Lesser General Public License as published by
13+
* the Free Software Foundation, either version 3 of the License, or
14+
* (at your option) any later version.
15+
*
16+
* jsexp is distributed in the hope that it will be useful,
17+
* but WITHOUT ANY WARRANTY; without even the implied warranty of
18+
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
19+
* GNU Lesser General Public License for more details.
20+
*
21+
* You should have received a copy of the GNU Lesser General Public License
22+
* along with jsexp. If not, see <http://www.gnu.org/licenses/>.
23+
*
24+
*
25+
-->
26+
27+
<!-- For more information about this file, see https://ant.apache.org -->
28+
29+
<!-- Imports 'project.groupId', 'project.artifactId', and 'project.version' properties. -->
30+
<xmlproperty file="pom.xml" />
31+
32+
<!-- Project-specific properties. -->
33+
<fail unless="project.groupId">Error: 'project.groupId' is undefined. This property is the group identifier.</fail>
34+
<fail unless="project.artifactId">Error: 'project.artifactId' is undefined. This property is the artifact identifier.</fail>
35+
<fail unless="project.version">Error: 'project.version' is undefined. This property is the version number in the form major.minor.patch.</fail>
36+
37+
<property name="project.build.directory" value="${basedir}/target" />
38+
<property name="project.build.outputDirectory" value="${project.build.directory}/classes" />
39+
40+
<!-- Cleans compiled files. -->
41+
<target name="clean">
42+
<delete dir="${project.build.directory}" />
43+
</target>
44+
45+
<!-- Compiles this module. -->
46+
<target name="dist">
47+
<subant genericantfile="genericantfile.xml" buildpath=".">
48+
<property name="project.groupId" value="${project.groupId}" />
49+
<property name="project.artifactId" value="${project.artifactId}" />
50+
<property name="project.version" value="${project.version}" />
51+
</subant>
52+
</target>
53+
54+
</project>
55+

‎jsexp/genericantfile.xml

+224
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,224 @@
1+
<?xml version="1.0" encoding="UTF-8" ?>
2+
<project xmlns:ivy="antlib:org.apache.ivy.ant" name="parent" default="dist" basedir=".">
3+
4+
<!--
5+
*
6+
* Copyright 2009-2015 Julian Mendez
7+
*
8+
*
9+
* This file is part of GenericAntFile [https://github.com/julianmendez/genericantfile]
10+
* and formerly was part of jcel [https://github.com/julianmendez/jcel].
11+
*
12+
*
13+
* The contents of this file are subject to the GNU Lesser General Public License
14+
* version 3
15+
*
16+
*
17+
* This program is free software: you can redistribute it and/or modify
18+
* it under the terms of the GNU Lesser General Public License as published by
19+
* the Free Software Foundation, either version 3 of the License, or
20+
* (at your option) any later version.
21+
*
22+
* This program is distributed in the hope that it will be useful,
23+
* but WITHOUT ANY WARRANTY; without even the implied warranty of
24+
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
25+
* GNU Lesser General Public License for more details.
26+
*
27+
* You should have received a copy of the GNU Lesser General Public License
28+
* along with this program. If not, see <http://www.gnu.org/licenses/>.
29+
*
30+
*
31+
* Alternatively, the contents of this file may be used under the terms
32+
* of the Apache License, Version 2.0, in which case the
33+
* provisions of the Apache License, Version 2.0 are applicable instead of those
34+
* above.
35+
*
36+
*
37+
* Licensed under the Apache License, Version 2.0 (the "License");
38+
* you may not use this file except in compliance with the License.
39+
* You may obtain a copy of the License at
40+
*
41+
* http://www.apache.org/licenses/LICENSE-2.0
42+
*
43+
* Unless required by applicable law or agreed to in writing, software
44+
* distributed under the License is distributed on an "AS IS" BASIS,
45+
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
46+
* See the License for the specific language governing permissions and
47+
* limitations under the License.
48+
*
49+
-->
50+
51+
<!-- For more information about this file, see https://ant.apache.org -->
52+
53+
<!-- Project-specific properties. -->
54+
<fail unless="project.groupId">Error: 'project.groupId' is undefined. This property is the group identifier.</fail>
55+
<fail unless="project.artifactId">Error: 'project.artifactId' is undefined. This property is the artifact identifier.</fail>
56+
<fail unless="project.version">Error: 'project.version' is undefined. This property is the version number in the form major.minor.patch.</fail>
57+
58+
<!-- Default value for Javadoc source path. -->
59+
<property name="javadoc.sourcepath" value="src/main/java:src/main/javadoc" />
60+
61+
<!-- Default value for project directory. -->
62+
<property name="project.directory" value="${basedir}" />
63+
64+
<!-- General properties. -->
65+
<property name="project.build.directory" value="${project.directory}/target" />
66+
<property name="_src.subdirectory" value="src" />
67+
<property name="_src.directory" value="${project.directory}/${_src.subdirectory}" />
68+
<property name="_src.javadoc.directory" value="${_src.directory}/main/javadoc" />
69+
<property name="project.build.sourceDirectory" value="${_src.directory}/main/java" />
70+
<property name="project.build.testSourceDirectory" value="${_src.directory}/test/java" />
71+
<property name="_project.build.resourcesDirectory" value="${_src.directory}/main/resources" />
72+
<property name="_javadoc.destDir" value="${project.build.directory}/apidocs" />
73+
<property name="_javadoc.show" value="protected" />
74+
<property name="project.build.outputDirectory" value="${project.build.directory}/classes" />
75+
<property name="project.build.testOutputDirectory" value="${project.build.directory}/test-classes" />
76+
<property name="project.reporting.outputDirectory" value="${project.build.directory}/test-reports" />
77+
<property name="_debuglevel" value="lines,vars,source" />
78+
79+
<!-- Beginning of snippet for Ivy. -->
80+
81+
<!-- Properties for Ivy. -->
82+
<property name="project.build.ivyReportDirectory" location="${project.build.directory}/ivy-reports" />
83+
<property name="maven.repository" value="https://repo.maven.apache.org/maven2" />
84+
<property name="ivy.install.version" value="2.3.0" />
85+
<condition property="ivy.home" value="${env.IVY_HOME}">
86+
<isset property="env.IVY_HOME" />
87+
</condition>
88+
<property name="ivy.home" value="${user.home}/.ant" />
89+
<property name="ivy.jar.directory" value="${ivy.home}/lib/org/apache/ivy/ivy/${ivy.install.version}" />
90+
<property name="ivy.jar.file" value="${ivy.jar.directory}/ivy-${ivy.install.version}.jar" />
91+
92+
<!-- Default value for directory of dependency jars. -->
93+
<property name="jars.directory" value="${ivy.settings.dir}/target/jars/lib" />
94+
95+
<!-- Downloads Ivy. -->
96+
<target name="downloadivy" unless="offline">
97+
<mkdir dir="${ivy.jar.directory}" />
98+
<get src="${maven.repository}/org/apache/ivy/ivy/${ivy.install.version}/ivy-${ivy.install.version}.jar" dest="${ivy.jar.file}" usetimestamp="true" />
99+
</target>
100+
101+
<!-- Initializes Ivy. -->
102+
<target name="initializeivy" depends="downloadivy">
103+
<path id="ivy.lib.path">
104+
<fileset dir="${ivy.jar.directory}" includes="*.jar" />
105+
</path>
106+
<taskdef resource="org/apache/ivy/ant/antlib.xml" uri="antlib:org.apache.ivy.ant" classpathref="ivy.lib.path" />
107+
</target>
108+
109+
<!-- Initializes Ivy paths. -->
110+
<target name="initialize" depends="initializeivy">
111+
<ivy:resolve />
112+
<ivy:report todir='${project.build.ivyReportDirectory}' graph='false' xml='false' />
113+
<ivy:cachepath pathid="compile.path" conf="compile" />
114+
<ivy:cachepath pathid="runtime.path" conf="runtime" />
115+
<ivy:cachepath pathid="test.path" conf="test" />
116+
</target>
117+
118+
<!-- Retrieves dependencies with Ivy. -->
119+
<target name="retrieve" depends="initialize">
120+
<ivy:retrieve pattern="${jars.directory}/[orgPath]/[module]/[revision]/[artifact]-[revision].[ext]" type="jar,bundle" />
121+
<ivy:retrieve pattern="${jars.directory}/[orgPath]/[module]/[revision]/[artifact]-[revision]-sources.[ext]" type="source" />
122+
<ivy:retrieve pattern="${jars.directory}/[orgPath]/[module]/[revision]/[artifact]-[revision]-[type].[ext]" type="javadoc" />
123+
</target>
124+
125+
<!-- End of snippet for Ivy. -->
126+
127+
<!-- Cleans compiled files. -->
128+
<target name="clean">
129+
<delete dir="${project.build.directory}" />
130+
</target>
131+
132+
<!-- Creates a jar with the source code. -->
133+
<target name="source" depends="clean">
134+
<mkdir dir="${project.build.directory}" />
135+
<jar destfile="${project.build.directory}/${project.artifactId}-${project.version}-sources.jar">
136+
<fileset dir="${project.build.sourceDirectory}" />
137+
<fileset dir="${_project.build.resourcesDirectory}" erroronmissingdir="false" />
138+
<manifest>
139+
<attribute name="Implementation-Title" value="${project.groupId}-${project.artifactId}" />
140+
<attribute name="Implementation-Version" value="${project.version}" />
141+
</manifest>
142+
</jar>
143+
</target>
144+
145+
<!-- Compiles the project. -->
146+
<target name="compile">
147+
<mkdir dir="${project.build.outputDirectory}" />
148+
<javac srcdir="${project.build.sourceDirectory}" destdir="${project.build.outputDirectory}" debug="true" debuglevel="${_debuglevel}" includeantruntime="false" createMissingPackageInfoClass="false">
149+
<classpath>
150+
<path refid="compile.path" />
151+
</classpath>
152+
</javac>
153+
</target>
154+
155+
<!-- Checks availability of unit tests. -->
156+
<target name="checktestsources">
157+
<available file="${project.build.testSourceDirectory}" property="testSourceDirectory.available" />
158+
</target>
159+
160+
<!-- Compiles the tests. -->
161+
<target name="compiletests" depends="compile, checktestsources" if="testSourceDirectory.available">
162+
<mkdir dir="${project.build.testOutputDirectory}" />
163+
<javac srcdir="${project.build.testSourceDirectory}" destdir="${project.build.testOutputDirectory}" classpath="${project.build.outputDirectory}" debug="true" debuglevel="${_debuglevel}" includeantruntime="false" createMissingPackageInfoClass="false">
164+
<classpath>
165+
<path refid="test.path" />
166+
<pathelement path="${project.build.directory}" />
167+
</classpath>
168+
</javac>
169+
</target>
170+
171+
<!-- Performs the unit tests. -->
172+
<target name="test" depends="compiletests" if="testSourceDirectory.available" unless="skipTests">
173+
<mkdir dir="${project.reporting.outputDirectory}" />
174+
<junit printsummary="on" haltonfailure="yes" fork="yes" dir="${project.directory}">
175+
<classpath>
176+
<path refid="test.path" />
177+
<pathelement path="${project.build.outputDirectory}" />
178+
<pathelement path="${project.build.testOutputDirectory}" />
179+
</classpath>
180+
<formatter type="plain" usefile="on" />
181+
<batchtest fork="yes" todir="${project.reporting.outputDirectory}">
182+
<fileset dir="${project.build.testSourceDirectory}" erroronmissingdir="false">
183+
<include name="**/*Test*.java" />
184+
</fileset>
185+
</batchtest>
186+
</junit>
187+
</target>
188+
189+
<!-- Creates a jar with the binaries. -->
190+
<target name="jar" depends="compile">
191+
<mkdir dir="${project.build.directory}" />
192+
<jar destfile="${project.build.directory}/${project.artifactId}-${project.version}.jar">
193+
<fileset dir="${project.build.outputDirectory}" />
194+
<fileset dir="${_project.build.resourcesDirectory}" erroronmissingdir="false" />
195+
<manifest>
196+
<attribute name="Implementation-Title" value="${project.groupId}-${project.artifactId}" />
197+
<attribute name="Implementation-Version" value="${project.version}" />
198+
</manifest>
199+
</jar>
200+
</target>
201+
202+
<!-- Creates the Javadoc. -->
203+
<target name="javadoc">
204+
<mkdir dir="${_javadoc.destDir}" />
205+
<javadoc packagenames="*" sourcepath="${javadoc.sourcepath}" destdir="${_javadoc.destDir}" version="true" use="true" windowtitle="${project.groupId}-${project.artifactId}" overview="${_src.javadoc.directory}/overview.html" access="${_javadoc.show}" useexternalfile="true" />
206+
</target>
207+
208+
<!-- Creates a jar with the Javadoc. -->
209+
<target name="javadocjar" depends="javadoc">
210+
<mkdir dir="${project.build.directory}" />
211+
<jar destfile="${project.build.directory}/${project.artifactId}-${project.version}-javadoc.jar">
212+
<fileset dir="${_javadoc.destDir}" />
213+
<manifest>
214+
<attribute name="Implementation-Title" value="${project.groupId}-${project.artifactId}" />
215+
<attribute name="Implementation-Version" value="${project.version}" />
216+
</manifest>
217+
</jar>
218+
</target>
219+
220+
<!-- Executes all the tasks. -->
221+
<target name="dist" depends="clean, source, retrieve, compile, checktestsources, compiletests, test, jar, javadoc, javadocjar" />
222+
223+
</project>
224+

‎jsexp/ivy.xml

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<ivy-module version="2.0">
3+
4+
<info organisation="de.tu-dresden.inf.lat.jsexp" module="jsexp" />
5+
6+
<configurations defaultconfmapping="compile->default;sources;javadoc">
7+
<conf name="compile" />
8+
<conf name="runtime" extends="compile" />
9+
<conf name="test" extends="runtime" />
10+
<conf name="sources" />
11+
<conf name="javadoc" />
12+
</configurations>
13+
14+
<dependencies>
15+
<dependency org="junit" name="junit" rev="4.12" />
16+
</dependencies>
17+
18+
</ivy-module>
19+

‎jsexp/ivysettings.xml

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<ivysettings>
3+
<settings defaultResolver="chain" />
4+
<resolvers>
5+
<chain name="chain" returnFirst="true">
6+
<filesystem name="local">
7+
<!-- <artifact pattern="${ivy.settings.dir}/target/jars/lib/[orgPath]/[module]/[revision]/[artifact]-[revision].[ext]" /> -->
8+
<artifact pattern="${ivy.settings.dir}/../[artifact]/target/[artifact]-[revision].[ext]" />
9+
</filesystem>
10+
<ibiblio name="central" m2compatible="true" />
11+
</chain>
12+
</resolvers>
13+
</ivysettings>
14+

0 commit comments

Comments
 (0)