(PR for dev branch tests)

.github/workflows/scala.yml

@@ -12,14 +12,21 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-    - uses: actions/checkout@v2
+    - name: Checkout repository (with submodules)
+      uses: actions/checkout@v2
+      with:
+        submodules: true
+        fetch-depth: 0
+
     - name: Set up JDK 11
       uses: actions/setup-java@v2
       with:
         java-version: '11'
         distribution: 'adopt'
     - name: Set up sbt
       uses: sbt/setup-sbt@v1
+    - name: Patch build.sbt files of submodules
+      run: ./patch-builds.sh
     - name: Build
       run: sbt nativeImage
     - name: Test

.gitmodules

@@ -0,0 +1,9 @@
+[submodule "eldarica"]
+	path = eldarica
+	url = https://github.com/uuverifiers/eldarica
+[submodule "horn-concurrency"]
+	path = horn-concurrency
+	url = https://github.com/uuverifiers/horn-concurrency
+[submodule "princess"]
+	path = princess
+	url = https://github.com/uuverifiers/princess

build.sbt

@@ -3,11 +3,13 @@ import java.nio.file.{Files, Paths}
 import java.nio.file.attribute.PosixFilePermissions
 import scala.language.postfixOps
 import scala.util.Try
+import sbt._
+import Keys._
 
 lazy val commonSettings = Seq(
     name                 := "TriCera",
     organization         := "uuverifiers",
-    version              := "0.4",
+    version              := "0.4-DEV",
     homepage             := Some(url("https://github.com/uuverifiers/tricera")),
     licenses             := Seq("BSD-3-Clause" -> url("https://opensource.org/licenses/BSD-3-Clause")),
     description          := "TriCera is a model checker for C programs.",
@@ -90,32 +92,29 @@ ppWithErrorHandling := {
 }
   (compile in Compile) := ((compile in Compile) dependsOn ppWithErrorHandling).value
 
-// Actual project
-lazy val root = (project in file(".")).
-  aggregate(ccParser).
-  dependsOn(ccParser).
-  aggregate(acslParser).
-  dependsOn(acslParser).
-  settings(commonSettings: _*).
+lazy val princess = ProjectRef(file("princess"), "root")
+lazy val eldarica = ProjectRef(file("eldarica"), "root")
+lazy val hornConcurrency = ProjectRef(file("horn-concurrency"), "root")
 
-//
-settings(
-  mainClass in Compile := Some("tricera.Main"),
-  //
-  scalacOptions in Compile ++=
-    List("-feature",
-         "-language:implicitConversions,postfixOps,reflectiveCalls"),
-  scalacOptions += "-opt:_",
-  resolvers += "uuverifiers" at "https://eldarica.org/maven/",
-  libraryDependencies += "uuverifiers" %% "eldarica" % "2.2.1",
-  libraryDependencies += "uuverifiers" %% "horn-concurrency" % "2.2.1",
-  libraryDependencies += "net.jcazevedo" %% "moultingyaml" % "0.4.2",
-  libraryDependencies += "org.scalactic" %% "scalactic" % "3.2.19",
-  libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.19" % "test",
-  excludeDependencies ++= Seq(
-    // exclude java-cup from transitive dependencies, ccParser includes newer version
-    ExclusionRule("net.sf.squirrel-sql.thirdparty-non-maven", "java-cup")),
+// Actual project
 
+lazy val root = (project in file("."))
+  .settings(commonSettings)
+  .settings(
+    mainClass in Compile := Some("tricera.Main"),
+    scalacOptions in Compile ++=
+    List("-feature", "-language:implicitConversions,postfixOps,reflectiveCalls",
+         "-encoding", "UTF-8"),
+    scalacOptions += "-opt:_",
+    //resolvers += "uuverifiers" at "https://eldarica.org/maven/",
+    libraryDependencies ++= Seq(
+      "net.jcazevedo" %% "moultingyaml" % "0.4.2",
+      "org.scalactic" %% "scalactic" % "3.2.19",
+      "org.scalatest" %% "scalatest" % "3.2.19" % Test
+      ),
+    excludeDependencies ++= Seq(
+      ExclusionRule("net.sf.squirrel-sql.thirdparty-non-maven", "java-cup")),
+
     nativeImageInstalled := false,
     nativeImageVersion := "21.1.0",
     nativeImageJvm := "graalvm-java11",
@@ -130,11 +129,48 @@ settings(
 
     nativeImageAgentMerge := true
   )
- .enablePlugins(NativeImagePlugin)
-
-// project can also be built by providing dependencies under the lib directory
-// and uncommenting below code to discard clashing transitive dependencies
-//assemblyMergeStrategy in assembly := {
-//  case PathList("META-INF", xs @ _*) => MergeStrategy.discard
-//  case x => MergeStrategy.last
-//}
+  .dependsOn(ccParser, acslParser, eldarica, hornConcurrency)
+  .aggregate(ccParser, acslParser)
+  .enablePlugins(NativeImagePlugin)
+
+// Remove java-cup-11a jars from unmanagedJars in subprojects
+ccParser / Compile / unmanagedJars :=
+(ccParser / Compile / unmanagedJars).value.filterNot(
+  _.data.getName.contains("java-cup-11a"))
+
+lazy val settingsAlreadyOverridden = settingKey[Boolean](
+  "Has overrideSettings command already run?")
+settingsAlreadyOverridden := false
+
+commands += Command.command("overrideSettings") { state =>
+  val extracted = Project.extract(state)
+  if (extracted.get(settingsAlreadyOverridden)) state
+  else {
+    Project.extract(state).appendWithSession(
+      Seq(
+        settingsAlreadyOverridden := true,
+        eldarica / organization        := "uuverifiers-dev",
+        eldarica / version             := "0.0.0-dev",
+        hornConcurrency / organization := "uuverifiers-dev",
+        hornConcurrency / version      := "0.0.0-dev",
+        princess / organization        := "uuverifiers-dev",
+        princess / version             := "0.0.0-dev",
+
+        eldarica / libraryDependencies := (eldarica / libraryDependencies).value.filterNot(_.organization.startsWith("uuverifiers")),
+        hornConcurrency / libraryDependencies := (hornConcurrency / libraryDependencies).value.filterNot(_.organization.startsWith("uuverifiers")),
+        ),
+      state
+      )
+  }
+}
+
+onLoad in Global := {
+  ((s: State) => "overrideSettings" :: s) compose (onLoad in Global).value
+}
+
+assembly / assemblyMergeStrategy := {
+  case PathList("java_cup", "runtime", _ @ _*) => MergeStrategy.first
+  case PathList("META-INF", _ @ _*) => MergeStrategy.discard
+  case x => MergeStrategy.first
+}
+

patch-builds.sh

@@ -0,0 +1,56 @@
+#!/usr/bin/env bash
+set -e
+
+ROOT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+
+echo "Patching local submodules under $ROOT_DIR ..."
+
+############################################
+# Patch eldarica build.sbt
+############################################
+ELDARICA_BUILD="$ROOT_DIR/eldarica/build.sbt"
+
+if [[ -f "$ELDARICA_BUILD" ]]; then
+  if ! grep -q 'ProjectRef(file("../princess"), "root")' "$ELDARICA_BUILD"; then
+    echo "  -> Patching eldarica/build.sbt"
+
+    # Insert the line between dependsOn(...) and .settings(...)
+    awk '
+      /dependsOn\(tplspecParser\)\./ {
+        print "    dependsOn(ProjectRef(file(\"../princess\"), \"root\"))."
+      }
+      { print }
+    ' "$ELDARICA_BUILD" > "$ELDARICA_BUILD.tmp" && mv "$ELDARICA_BUILD.tmp" "$ELDARICA_BUILD"
+  else
+    echo "  -> eldarica/build.sbt already patched"
+  fi
+else
+  echo "  !! eldarica/build.sbt not found"
+fi
+
+
+############################################
+# Patch horn-concurrency build.sbt
+############################################
+HORN_BUILD="$ROOT_DIR/horn-concurrency/build.sbt"
+
+if [[ -f "$HORN_BUILD" ]]; then
+  if ! grep -q 'ProjectRef(file("../eldarica"), "root")' "$HORN_BUILD"; then
+    echo "  -> Patching horn-concurrency/build.sbt"
+
+    # Append after the main project definition
+    awk '
+      /lazy val root = \(project in file\("\."\)\)\./ {
+        print $0 "\n  dependsOn(ProjectRef(file(\"../eldarica\"), \"root\"))."
+        next
+      }
+      { print }
+    ' "$HORN_BUILD" > "$HORN_BUILD.tmp" && mv "$HORN_BUILD.tmp" "$HORN_BUILD"
+  else
+    echo "  -> horn-concurrency/build.sbt already patched"
+  fi
+else
+  echo "  !! horn-concurrency/build.sbt not found"
+fi
+
+echo "Done."