https://github.com/gapt/gapt
Tip revision: 2f9ab4b9865f0e3e4b8b04b71d2f0fbf3d1b8623 authored by Jannik Vierling on 21 July 2022, 07:37:48 UTC
release 2.16.0
release 2.16.0
Tip revision: 2f9ab4b
build.sbt
import java.io.ByteArrayOutputStream
import org.apache.commons.compress.archivers.tar.{ TarArchiveEntry, TarArchiveOutputStream }
import scalariform.formatter.preferences._
import sys.process._
val Version = "2.16.0"
lazy val commonSettings = Seq(
organization := "at.logic.gapt",
homepage := Some( url( "https://logic.at/gapt/" ) ),
organizationHomepage := homepage.value,
licenses += ( "GPL-3.0" -> url( "http://www.gnu.org/licenses/gpl-3.0.html" ) ),
startYear := Some( 2008 ),
version := Version,
autoAPIMappings := true,
publishMavenStyle := true,
publishTo := Some(
if ( isSnapshot.value )
Opts.resolver.sonatypeSnapshots
else
Opts.resolver.sonatypeStaging ),
scmInfo := Some( ScmInfo(
browseUrl = url( "https://github.com/gapt/gapt" ),
connection = "scm:git:https://github.com/gapt/gapt.git",
devConnection = Some( "scm:git:git@github.com:gapt/gapt.git" ) ) ),
scalaVersion := "2.13.8",
developers := List(
Developer(
id = "jvierling",
name = "Jannik Vierling",
email = "jannik.vierling@gmail.com",
url = url( "https://jvierling.github.io/" ) ),
Developer(
id = "shetzl",
name = "Stefan Hetzl",
email = "stefan.hetzl@tuwien.ac.at",
url = url( "http://dmg.tuwien.ac.at/hetzl/" ) ),
Developer(
id = "gebner",
name = "Gabriel Ebner",
email = "gebner@gebner.org",
url = url( "https://gebner.org/" ) ) ),
scalacOptions in Compile ++= Seq(
"-deprecation",
"-language:postfixOps",
"-language:implicitConversions",
"-feature",
"-unchecked" ),
javaOptions ++= Seq( "-Xss40m", "-Xmx1g" ),
fork := true,
baseDirectory in run := file( "." ),
sourcesInBase := false // people like to keep scripts lying around
) ++ scalariformSettings
lazy val scalariformSettings =
Seq( scalariformPreferences := scalariformPreferences.value
.setPreference( AlignParameters, true )
.setPreference( AlignSingleLineCaseStatements, true )
.setPreference( DoubleIndentConstructorArguments, true )
.setPreference( SpaceInsideParentheses, true ) )
val specs2Version = "4.16.0"
lazy val testSettings = Seq(
testOptions in Test += Tests.Argument( TestFrameworks.Specs2, "junitxml", "console" ),
javaOptions in Test += "-Xmx2g",
libraryDependencies ++= Seq(
"org.specs2" %% "specs2-core" % specs2Version,
"org.specs2" %% "specs2-junit" % specs2Version, // needed for junitxml output
"org.specs2" %% "specs2-matcher" % specs2Version ) map ( _ % Test ) )
lazy val BuildSbtConfig = config( "buildsbt" ) extend Compile
lazy val root = project.in( file( "." ) ).
aggregate( core, examples, tests, userManual, cli, testing ).
dependsOn( core, examples, cli ).
settings( commonSettings: _* ).
enablePlugins( ScalaUnidocPlugin ).
settings(
fork in console := true,
initialCommands in console := IO.read( resourceDirectory.in( cli, Compile ).value / "gapt-cli-prelude.scala" ),
publish / skip := true,
packagedArtifacts := Map(),
inConfig( BuildSbtConfig )( SbtScalariform.configScalariformSettings ++ scalariformSettings ),
sourceDirectories in ( BuildSbtConfig, scalariformFormat ) := Seq( baseDirectory.value ),
includeFilter in ( BuildSbtConfig, scalariformFormat ) := ( "*.sbt": FileFilter ),
apiURL := Some( url( "https://logic.at/gapt/api/" ) ),
scalacOptions in ( ScalaUnidoc, unidoc ) ++= Seq(
"-doc-title", "gapt",
"-doc-version", version.value,
"-doc-source-url", s"https://github.com/gapt/gapt/blob/${"git rev-parse HEAD" !!}/€{FILE_PATH}.scala",
"-doc-root-content", ( baseDirectory.value / "doc" / "rootdoc.txt" ).getAbsolutePath,
"-sourcepath", baseDirectory.value.getAbsolutePath,
"-skip-packages", "ammonite:ammonite.ops",
"-diagrams",
"-implicits", "-implicits-show-all",
"-skip-packages", "scala" ),
scripts := {
val runJVMOptions = javaOptions.value ++ Seq( "-cp", Path.makeString(
Attributed.data( fullClasspath.in( cli, Compile ).value ++ fullClasspath.in( testing, Compile ).value distinct ) ) )
def mkScript( file: File, extraArgs: String* ) = {
IO.write(
file,
s"#!/bin/sh\njava ${( runJVMOptions ++ extraArgs ).mkString( " " )} ${"\"$@\""}\n" )
file.setExecutable( true )
}
(
mkScript( target.value / "run" ),
mkScript( target.value / "test-cut-intro", "gapt.testing.testCutIntro" ),
mkScript( target.value / "test-pi2-cut-intro", "gapt.testing.testPi2CutIntro" ),
mkScript( target.value / "test-induction", "gapt.testing.testInduction" ),
mkScript( target.value / "viper", "gapt.provers.viper.Viper" ),
mkScript( target.value / "escargot", "gapt.provers.escargot.Escargot" ),
mkScript( target.value / "slakje", "gapt.provers.slakje.Slakje" ),
mkScript( target.value / "cli", "gapt.cli.CLIMain" ) )
},
// Release stuff
mainClass in assembly := Some( "gapt.cli.CLIMain" ),
aggregate in assembly := false,
releaseDist := {
val baseDir = file( "." )
val version = Keys.version.value
val apidocs = doc.in( ScalaUnidoc, unidoc ).value
val archiveFile = file( "." ) / "target" / s"gapt-$version.tar.gz"
Process( List( "latexmk", "-pdf", "-silent", "user_manual.tex" ), baseDir / "doc" ) !
val filesToIncludeAsIs = List(
"COPYING", "gapt.sh", "slakje.sh", "escargot.sh", "viper.sh", "include.sh", "examples" )
val entries = List( ( assembly.value, s"gapt-$version.jar" ) ) ++
filesToIncludeAsIs.flatMap { fn => recursiveListFiles( baseDir / fn ) }
.map { f => ( f, baseDir.toPath.relativize( f.toPath ) ) } ++
List(
( baseDir / "doc/README.dist", "README" ),
( baseDir / "doc/user_manual.pdf", "user_manual.pdf" ) ) ++
recursiveListFiles( apidocs ).map { f => f -> s"apidocs/${apidocs.toPath.relativize( f.toPath )}" }
val archiveStem = s"gapt-$version"
IO.gzipFileOut( archiveFile ) { gzipOut =>
val tarOut = new TarArchiveOutputStream( gzipOut )
tarOut.setLongFileMode( TarArchiveOutputStream.LONGFILE_POSIX )
entries.foreach {
case ( file, pathInArchive ) =>
val tarEntry = new TarArchiveEntry( file, s"$archiveStem/$pathInArchive" )
if ( file.canExecute ) tarEntry.setMode( BigInt( "755", 8 ).toInt )
tarOut.putArchiveEntry( tarEntry )
IO.transfer( file, tarOut )
tarOut.closeArchiveEntry()
}
tarOut.close()
}
archiveFile
},
evalUserManual := {
val userManFn = "doc/user_manual.tex"
val out = new ByteArrayOutputStream
val exitVal = new Fork( "java", Some( "gapt.doc.evalCodeSnippets" ) ).fork(
ForkOptions(
javaHome = javaHome.value,
outputStrategy = Some( CustomOutput( out ) ),
bootJars = Vector(),
workingDirectory = Some( new java.io.File( "." ) ),
runJVMOptions = Vector() ++ javaOptions.value ++ Seq( "-cp", Path.makeString(
Attributed.data( fullClasspath.in( userManual, Compile ).value ) ) ),
connectInput = false,
envVars = envVars.value ),
Seq( userManFn ) ).exitValue()
if ( exitVal == 0 ) IO.write( file( userManFn ), out.toByteArray )
} )
lazy val core = project.in( file( "core" ) ).
settings( commonSettings: _* ).
settings(
name := "gapt",
description := "General Architecture for Proof Theory",
scalacOptions in Compile += "-Xfatal-warnings",
libraryDependencies ++= Seq(
"org.scala-lang.modules" %% "scala-parallel-collections" % "1.0.4",
"org.scala-lang.modules" %% "scala-parser-combinators" % "2.1.1",
"org.scala-lang" % "scala-reflect" % scalaVersion.value,
"org.parboiled" %% "parboiled" % "2.4.0",
"com.lihaoyi" %% "fastparse" % "2.3.3",
"com.lihaoyi" %% "sourcecode" % "0.2.8",
"org.typelevel" %% "cats-free" % "2.7.0",
"org.scala-lang.modules" %% "scala-xml" % "2.1.0",
"org.apache.commons" % "commons-lang3" % "3.12.0",
"com.lihaoyi" %% "ammonite-ops" % "2.4.1",
"de.uni-freiburg.informatik.ultimate" % "smtinterpol" % "2.5",
"com.github.scopt" %% "scopt" % "4.0.1",
"org.ow2.sat4j" % "org.ow2.sat4j.core" % "2.3.6",
"org.ow2.sat4j" % "org.ow2.sat4j.maxsat" % "2.3.6" ),
// UI
libraryDependencies ++= Seq(
"org.scala-lang.modules" %% "scala-swing" % "3.0.0",
"com.itextpdf" % "itextpdf" % "5.5.13.3",
"org.scilab.forge" % "jlatexmath" % "1.0.7" ),
// JSON serialization
libraryDependencies += "org.json4s" %% "json4s-native" % "4.0.5",
libraryDependencies ++= Seq(
"io.circe" %% "circe-core",
"io.circe" %% "circe-generic",
"io.circe" %% "circe-parser",
"io.circe" %% "circe-generic-extras" ).map( _ % "0.14.2" ) )
lazy val examples = project.in( file( "examples" ) ).
dependsOn( core ).
settings( commonSettings: _* ).
settings(
name := "gapt-examples",
unmanagedSourceDirectories in Compile := Seq( baseDirectory.value ),
resourceDirectory in Compile := baseDirectory.value,
excludeFilter in ( Compile, unmanagedResources ) := {
val target = ( baseDirectory.value / "target" ).getCanonicalPath
new SimpleFileFilter( _.getCanonicalPath startsWith target )
} || "*.scala" )
lazy val tests = project.in( file( "tests" ) ).
dependsOn( core, examples ).
settings( commonSettings: _* ).
settings( testSettings: _* ).
disablePlugins( JUnitXmlReportPlugin ).
settings(
testForkedParallel := true,
publish / skip := true,
packagedArtifacts := Map() )
lazy val userManual = project.in( file( "doc" ) ).
dependsOn( cli ).
settings( commonSettings: _* ).
settings(
unmanagedSourceDirectories in Compile := Seq( baseDirectory.value ),
publish / skip := true,
packagedArtifacts := Map() )
lazy val cli = project.in( file( "cli" ) ).
dependsOn( core, examples ).
settings( commonSettings: _* ).
settings(
mainClass := Some( "gapt.cli.CLIMain" ),
scalacOptions in Compile += "-Xfatal-warnings",
libraryDependencies ++= Seq(
"org.scala-lang" % "scala-compiler" % scalaVersion.value ),
publish / skip := true,
packagedArtifacts := Map() )
addCommandAlias( "format", "; scalariformFormat ; buildsbt:scalariformFormat" )
lazy val testing = project.in( file( "testing" ) ).
dependsOn( core, examples ).
settings( commonSettings: _* ).
settings(
name := "gapt-testing",
description := "gapt extended regression tests",
scalacOptions in Compile += "-Xfatal-warnings",
publish / skip := true,
packagedArtifacts := Map() )
lazy val releaseDist = TaskKey[File]( "release-dist", "Creates the release tar ball." )
lazy val evalUserManual = TaskKey[Unit]( "eval-user-manual", "Evaluates the snippets in the user manual." )
lazy val scripts = TaskKey[Unit]( "scripts", "Creates scripts in target/" )
def recursiveListFiles( f: File ): Seq[File] =
if ( f.getName == "target" )
Seq()
else if ( f.isDirectory )
IO.listFiles( f ).flatMap( recursiveListFiles )
else
Seq( f )