1
1
import sbt ._
2
- import Keys ._
2
+ import sbt . Keys ._
3
3
import org .eclipse .jgit .api ._
4
+ import scala .sys .process ._
4
5
5
- object ScalaZ3Build extends Build {
6
+ object ScalaZ3Build {
6
7
7
- lazy val PS = java.io.File .pathSeparator
8
- lazy val DS = java.io.File .separator
8
+ lazy val PS = java.io.File .pathSeparator
9
+ lazy val DS = java.io.File .separator
9
10
10
- lazy val soName = System .mapLibraryName(" scalaz3" )
11
+ lazy val soName = System .mapLibraryName(" scalaz3" )
11
12
12
- lazy val z3Name = if (isMac) " libz3.dylib" else if (isWindows) " libz3.dll" else System .mapLibraryName(" z3" )
13
- lazy val javaZ3Name = if (isMac) " libz3java.dylib" else if (isWindows) " libz3java.dll" else System .mapLibraryName(" z3java" )
13
+ lazy val z3Name = {
14
+ if (isMac) " libz3.dylib"
15
+ else if (isWindows) " libz3.dll"
16
+ else System .mapLibraryName(" z3" )
17
+ }
18
+
19
+ lazy val javaZ3Name = {
20
+ if (isMac) " libz3java.dylib"
21
+ else if (isWindows) " libz3java.dll"
22
+ else System .mapLibraryName(" z3java" )
23
+ }
14
24
15
25
lazy val libBinPath = file(" lib-bin" )
16
26
lazy val z3BinFilePath = z3BuildPath / z3Name
@@ -42,21 +52,20 @@ object ScalaZ3Build extends Build {
42
52
lazy val z3Path = file(" ." ) / " z3" / z3SourceTag
43
53
lazy val z3BuildPath = z3Path / " build"
44
54
lazy val z3BinaryFiles = Seq (z3BuildPath / z3Name, z3BuildPath / javaZ3Name)
45
- lazy val z3JarFile = z3BuildPath / " com.microsoft.z3.jar"
46
55
47
56
lazy val z3JavaDepsPrefixes = Seq (
48
57
" com.microsoft.z3.Native" ,
49
58
" com.microsoft.z3.Z3Exception" ,
50
- " com.microsoft.z3.enumerations"
59
+ " com.microsoft.z3.enumerations" ,
51
60
)
52
61
53
62
def exec (cmd : String , s : TaskStreams ): Int = {
54
- s.log.info(" $ " + cmd)
63
+ s.log.info(" $ " + cmd)
55
64
cmd ! s.log
56
65
}
57
66
58
67
def exec (cmd : String , dir : File , s : TaskStreams ): Int = {
59
- s.log.info(" $ cd " + dir + " && " + cmd)
68
+ s.log.info(" $ cd " + dir + " && " + cmd)
60
69
Process (cmd, dir) ! s.log
61
70
}
62
71
@@ -97,8 +106,10 @@ object ScalaZ3Build extends Build {
97
106
strBuf.toString
98
107
}
99
108
100
- val z3Task = (streams) map { case s =>
101
- s.log.info(" Compiling Z3 ..." )
109
+ lazy val z3JarFile = z3BuildPath / " com.microsoft.z3.jar"
110
+
111
+ val z3Task = Def .task {
112
+ val s = streams.value
102
113
103
114
if (! z3Path.asFile.exists) {
104
115
s.log.info(" Cloning Z3 source repository ..." )
@@ -114,19 +125,25 @@ object ScalaZ3Build extends Build {
114
125
.call()
115
126
116
127
val hashFile = z3Path / " .build-hash"
128
+
117
129
def computeHash (): String = {
118
- hashFiles(listAllFiles(z3Path.asFile).filter { f =>
119
- ! f.getName.endsWith(" .pyc" ) && ! f.isHidden && ! f.getName.startsWith(" ." ) && ! f.getName.endsWith(" .a" )
130
+ hashFiles(listAllFiles((z3Path / " src" ).asFile).filter { f =>
131
+ ! f.getName.endsWith(" .pyc" ) &&
132
+ ! f.isHidden &&
133
+ ! f.getName.startsWith(" ." ) &&
134
+ ! f.getName.endsWith(" .a" )
120
135
})
121
136
}
122
137
123
138
val initialHash = computeHash()
124
- s.log.info(" New checksum is : " + initialHash)
139
+ s.log.info(" Checksum of Z3 source file : " + initialHash)
125
140
126
- if (hashFile.exists && IO .read(hashFile) == initialHash) {
127
- s.log.info(" Checksum matched previous, skipping build..." )
141
+ if (hashFile.exists && IO .read(hashFile).trim == initialHash.trim ) {
142
+ s.log.info(" Checksum of Z3 source files matched previous, skipping build..." )
128
143
initialHash
129
144
} else {
145
+ s.log.info(" Compiling Z3..." )
146
+
130
147
val code = if (isUnix) {
131
148
val python = if ((" which python2.7" #> file(" /dev/null" )).! == 0 ) " python2.7" else " python"
132
149
@@ -140,7 +157,7 @@ object ScalaZ3Build extends Build {
140
157
val i1 = exec(" python scripts/mk_make.py --java" , z3Path, s)
141
158
if (i1 != 0 ) i1 else exec(" make" , z3Path / " build" , s)
142
159
} else {
143
- error(" Don't know how to compile Z3 on arch: " + osInf+ " - " + osArch)
160
+ sys. error(" Don't know how to compile Z3 on arch: " + osInf + " - " + osArch)
144
161
}
145
162
146
163
if (code == 0 ) {
@@ -150,50 +167,59 @@ object ScalaZ3Build extends Build {
150
167
s.log.info(" Wrote checksum " + finalHash + " for z3 build." )
151
168
finalHash
152
169
} else {
153
- error(" Compilation of Z3 failed... aborting" )
170
+ sys. error(" Compilation of Z3 failed... aborting" )
154
171
}
155
172
}
156
173
}
157
174
158
- val checksumTask = (streams, z3Key, sourceDirectory in Compile ) map {
159
- case (s, z3checksum, sd) =>
160
- val checksumFilePath = sd / " java" / " z3" / " LibraryChecksum.java"
175
+ val checksumTask = Def .task {
176
+ val s = streams.value
177
+ val z3checksum = z3Key.value
178
+ val sd = (Compile / sourceDirectory).value
161
179
162
- val extensions = Set ( " java" , " c " , " h " , " sbt " , " properties " )
180
+ val checksumFilePath = sd / " java" / " z3 " / " LibraryChecksum.java "
163
181
164
- val checksumSourcePaths = listAllFiles(sd.asFile).filter { file =>
165
- val pathParts = file.getPath.split(" ." )
166
- pathParts.size > 1 && extensions(pathParts.last)
167
- }
182
+ val extensions = Set (" java" , " c" , " h" , " sbt" , " properties" )
183
+
184
+ val checksumSourcePaths = listAllFiles(sd.asFile).filter { file =>
185
+ val pathParts = file.getPath.split(" ." )
186
+ pathParts.size > 1 && extensions(pathParts.last)
187
+ }
168
188
169
- s.log.info(" Generating library checksum" )
189
+ s.log.info(" Generating library checksum" )
170
190
171
- val md5String = hashFiles(checksumSourcePaths.map(_.asFile), z3checksum)
191
+ val md5String = hashFiles(checksumSourcePaths.map(_.asFile), z3checksum)
172
192
173
- val fw = new java.io.FileWriter (checksumFilePath.asFile)
174
- val nl = System .getProperty(" line.separator" )
175
- fw.write(" // THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT" + nl)
176
- fw.write(" package z3;" + nl)
177
- fw.write(nl)
178
- fw.write(" public final class LibraryChecksum {" + nl)
179
- fw.write(" public static final String value = \" " + md5String + " \" ;" + nl)
180
- fw.write(" }" + nl)
181
- fw.close
193
+ val fw = new java.io.FileWriter (checksumFilePath.asFile)
194
+ val nl = System .getProperty(" line.separator" )
195
+ fw.write(" // THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT" + nl)
196
+ fw.write(" package z3;" + nl)
197
+ fw.write(nl)
198
+ fw.write(" public final class LibraryChecksum {" + nl)
199
+ fw.write(" public static final String value = \" " + md5String + " \" ;" + nl)
200
+ fw.write(" }" + nl)
201
+ fw.close
182
202
183
- s.log.info(" Wrote checksum " + md5String + " as part of " + checksumFilePath.asFile + " ." )
203
+ s.log.info(" Wrote checksum " + md5String + " as part of " + checksumFilePath.asFile + " ." )
184
204
185
- md5String
205
+ md5String
186
206
}
187
207
188
- val gccTask = (streams, checksumKey, z3Key).map { case (s, cs, _) =>
208
+ val gccTask = Def .task {
209
+ val s = streams.value
210
+ val cs = checksumKey.value
211
+
189
212
s.log.info(" Compiling dummy C sources ..." )
190
213
191
214
def extractDir (checksum : String ): String = {
192
215
System .getProperty(" java.io.tmpdir" ) + DS + " SCALAZ3_" + checksum + DS + " lib-bin" + DS
193
216
}
194
217
195
218
// First, we look for z3
196
- for (file <- (z3BinaryFiles :+ z3JarFile) if ! file.exists) error(" Could not find Z3 : " + file.absolutePath)
219
+ for (file <- (z3BinaryFiles :+ z3JarFile) if ! file.exists) {
220
+ sys.error(" Could not find Z3 : " + file.absolutePath)
221
+ }
222
+
197
223
libBinFilePath.getParentFile.mkdirs()
198
224
199
225
if (isUnix) {
@@ -219,10 +245,10 @@ object ScalaZ3Build extends Build {
219
245
} else if (isMac) {
220
246
val frameworkPath = " /System/Library/Frameworks/JavaVM.framework/Versions/Current/Headers"
221
247
222
- exec(" install_name_tool -id @loader_path/" + z3Name+ " " + z3BinFilePath.absolutePath, s)
223
- exec(" install_name_tool -id @loader_path/" + javaZ3Name+ " " + javaZ3BinFilePath.absolutePath, s)
248
+ exec(" install_name_tool -id @loader_path/" + z3Name + " " + z3BinFilePath.absolutePath, s)
249
+ exec(" install_name_tool -id @loader_path/" + javaZ3Name + " " + javaZ3BinFilePath.absolutePath, s)
224
250
// make the dependency to z3 be relative to the caller's location
225
- exec(" install_name_tool -change " + z3Name+ " @loader_path/" + z3Name+ " " + javaZ3BinFilePath.absolutePath, s)
251
+ exec(" install_name_tool -change " + z3Name + " @loader_path/" + z3Name + " " + javaZ3BinFilePath.absolutePath, s)
226
252
227
253
exec(" gcc -std=gnu89 -o " + libBinFilePath.absolutePath + " " +
228
254
" -dynamiclib" + " " +
@@ -232,69 +258,59 @@ object ScalaZ3Build extends Build {
232
258
" -I" + frameworkPath + " " +
233
259
" -L" + z3BuildPath.absolutePath + " " +
234
260
" -g -lc " +
235
- " -Wl,-rpath," + extractDir(cs)+ " " +
261
+ " -Wl,-rpath," + extractDir(cs) + " " +
236
262
" -lz3 -fPIC -O2" , s)
237
263
238
264
} else {
239
- error(" Unknown arch: " + osInf+ " - " + osArch)
265
+ sys. error(" Unknown arch: " + osInf + " - " + osArch)
240
266
}
267
+
241
268
() // unit task!
242
269
}
243
270
244
- val packageTask = (Keys .`package` in Compile ).dependsOn(gccKey)
271
+ val packageTask = (Compile / Keys .`package`).dependsOn(gccKey)
245
272
246
- val newMappingsTask = mappings in ( Compile , packageBin) <<= (mappings in ( Compile , packageBin), streams) map {
247
- case (normalFiles, s) =>
248
- val newBinaryFiles = (libBinFilePath +: z3BinaryFiles).map { f => f.getAbsoluteFile -> ( " lib-bin " + DS + f.getName) }
273
+ val newMappingsTask = Def .task {
274
+ val s = streams.value
275
+ val normalFiles = (Compile / packageBin / mappings).value
249
276
250
- s.log.info(" Bundling binary files:" )
251
- for ((from, to) <- newBinaryFiles) {
252
- s.log.info(" - " + from+ " -> " + to)
253
- }
277
+ val newBinaryFiles = (libBinFilePath +: z3BinaryFiles).map { f =>
278
+ f.getAbsoluteFile -> (" lib-bin" + DS + f.getName)
279
+ }
254
280
255
- s.log.info(" Bunding relevant java-Z3 files:" )
256
- val outputDir = new File (System .getProperty(" java.io.tmpdir" ) + DS + " Z3JAR_jars" + DS )
257
- outputDir.delete
258
- outputDir.mkdirs
259
- IO .unzip(z3JarFile, outputDir)
260
-
261
- val z3JavaDepsMappings : Seq [(File , String )] = listAllFiles(outputDir).flatMap { f =>
262
- if (f.isDirectory) None else {
263
- import java .nio .file .Paths
264
- val path = Paths .get(outputDir.getAbsolutePath).relativize(Paths .get(f.getAbsolutePath)).toString
265
- val extensionSplit = path.split(" \\ ." )
266
- if (extensionSplit.length < 2 || extensionSplit(1 ) != " class" ) None else {
267
- val classPath = extensionSplit(0 ).replace(DS , " ." )
268
- if (z3JavaDepsPrefixes.exists(prefix => classPath.startsWith(prefix))) {
269
- s.log.info(" - " + classPath)
270
- Some (f.getAbsoluteFile -> path)
271
- } else {
272
- None
273
- }
281
+ s.log.info(" Bundling binary files:" )
282
+ for ((from, to) <- newBinaryFiles) {
283
+ s.log.info(" - " + from+ " -> " + to)
284
+ }
285
+
286
+ s.log.info(" Bundling relevant java-Z3 files:" )
287
+ val outputDir = new File (System .getProperty(" java.io.tmpdir" ) + DS + " Z3JAR_jars" + DS )
288
+ outputDir.delete
289
+ outputDir.mkdirs
290
+ IO .unzip(z3JarFile, outputDir)
291
+
292
+ val z3JavaDepsMappings : Seq [(File , String )] = listAllFiles(outputDir).flatMap { f =>
293
+ if (f.isDirectory) None else {
294
+ import java .nio .file .Paths
295
+ val path = Paths .get(outputDir.getAbsolutePath).relativize(Paths .get(f.getAbsolutePath)).toString
296
+ val extensionSplit = path.split(" \\ ." )
297
+ if (extensionSplit.length < 2 || extensionSplit(1 ) != " class" ) None else {
298
+ val classPath = extensionSplit(0 ).replace(DS , " ." )
299
+ if (z3JavaDepsPrefixes.exists(prefix => classPath.startsWith(prefix))) {
300
+ s.log.info(" - " + classPath)
301
+ Some (f.getAbsoluteFile -> path)
302
+ } else {
303
+ None
274
304
}
275
305
}
276
306
}
307
+ }
277
308
278
- newBinaryFiles ++ z3JavaDepsMappings ++ normalFiles
309
+ newBinaryFiles ++ z3JavaDepsMappings ++ normalFiles
279
310
}
280
311
281
- val testClasspath = internalDependencyClasspath in (Test ) <<= (artifactPath in (Compile , packageBin)) map {
282
- case jar => List (Attributed .blank(jar))
312
+ val testClasspath = Def .task {
313
+ val jar = (Compile / packageBin / artifactPath).value
314
+ Seq (Attributed .blank(jar))
283
315
}
284
-
285
- lazy val root = Project (
286
- id = " ScalaZ3" ,
287
- base = file(" ." ),
288
- settings = Project .defaultSettings ++ Seq (
289
- checksumKey <<= checksumTask,
290
- gccKey <<= gccTask,
291
- z3Key <<= z3Task,
292
- (Keys .`package` in Compile ) <<= packageTask,
293
- (unmanagedJars in Compile ) += Attributed .blank(z3JarFile),
294
- (compile in Compile ) <<= (compile in Compile ) dependsOn (checksumTask),
295
- (test in Test ) <<= (test in Test ) dependsOn (Keys .`package` in Compile ),
296
- testClasspath,
297
- newMappingsTask
298
- )
299
- )
300
316
}
0 commit comments