Changed to use Proyek instead of mill build tasks.

.gitignore

@@ -3,6 +3,7 @@
 /out
 target
 /versions.properties
+/bin/install
 /bin/mill.bat
 /bin/prelude.sh
 /bin/platform.sh

bin/build.cmd

@@ -63,14 +63,12 @@ if (Os.cliArgs.isEmpty) {
 
 
 val homeBin = Os.slashDir
-val home = homeBin.up
+val home = homeBin.up.canon
 val sireumJar = homeBin / "sireum.jar"
-val mill = homeBin / "mill.bat"
 var didTipe = F
 var didCompile = F
 val versions = (home / "versions.properties").properties
-val cache = Os.home / "Downloads" / "sireum"
-
+val projectStandalone = home / "bin" / "project-standalone.cmd"
 
 def platformKind(kind: Os.Kind.Type): String = {
   kind match {
@@ -83,16 +81,6 @@ def platformKind(kind: Os.Kind.Type): String = {
 }
 
 
-def downloadMill(): Unit = {
-  if (!mill.exists) {
-    println("Downloading mill ...")
-    mill.downloadFrom("https://github.com/sireum/rolling/releases/download/mill/standalone")
-    mill.chmod("+x")
-    println()
-  }
-}
-
-
 def installZ3(kind: Os.Kind.Type): Unit = {
   Init(home, kind, versions).installZ3()
 }
@@ -140,7 +128,7 @@ def compile(): Unit = {
     didCompile = T
     tipe()
     println("Compiling ...")
-    Os.proc(ISZ(mill.string, "all", "logika.shared.tests.compile")).at(home).console.runCheck()
+    proc"java -Xss2M -jar $sireumJar proyek compile --project $projectStandalone $home".console.echo.runCheck()
     println()
   }
 }
@@ -149,20 +137,11 @@ def compile(): Unit = {
 def test(): Unit = {
   compile()
   println("Running shared tests ...")
-  Os.proc(ISZ(mill.string, "logika.jvm.tests")).at(home).console.runCheck()
+  proc"java -Xss2M -jar $sireumJar proyek test --project $projectStandalone --packages org.sireum $home org.sireum.logika".
+    env(ISZ("JAVA_OPTS" ~> "-Xss2M")).console.echo.runCheck()
   println()
 }
 
-
-def testJs(): Unit = {
-  compile()
-  println("Running js tests ...")
-  Os.proc(ISZ(mill.string, "logika.js.tests")).at(home).console.runCheck()
-  println()
-}
-
-
-downloadMill()
 installZ3(Os.kind)
 installCVC(Os.kind)
 
@@ -174,7 +153,6 @@ for (i <- 0 until Os.cliArgs.size) {
   Os.cliArgs(i) match {
     case string"compile" => compile()
     case string"test" => test()
-    case string"test-js" => testJs()
     case cmd =>
       usage()
       eprintln(s"Unrecognized command: $cmd")

bin/project-standalone.cmd

@@ -0,0 +1,60 @@
+::/*#! 2> /dev/null                                 #
+@ 2>/dev/null # 2>nul & echo off & goto BOF         #
+if [ -z ${SIREUM_HOME} ]; then                      #
+  echo "Please set SIREUM_HOME env var"             #
+  exit -1                                           #
+fi                                                  #
+exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@"  #
+:BOF
+setlocal
+if not defined SIREUM_HOME (
+  echo Please set SIREUM_HOME env var
+  exit /B -1
+)
+%SIREUM_HOME%\bin\sireum.bat slang run -n "%0" %*
+exit /B %errorlevel%
+::!#*/
+// #Sireum
+
+import org.sireum._
+import org.sireum.project.ProjectUtil._
+import org.sireum.project.JSON
+
+
+def usage(): Unit = {
+  println("Usage: [ json ]")
+}
+
+var isDot = T
+
+Os.cliArgs match {
+  case ISZ(string"json") => isDot = F
+  case ISZ(string"-h") =>
+    usage()
+    Os.exit(0)
+  case ISZ() =>
+  case _ =>
+    usage()
+    Os.exit(-1)
+}
+
+val homeDir = Os.slashDir.up.canon
+
+val projects = ISZ(
+  homeDir,
+  homeDir / "runtime",
+  homeDir / "slang"
+)
+
+loadFromBaseDirs(projects) match {
+  case Some(project) =>
+    if (isDot) {
+      val projectDot = homeDir / "project.dot"
+      projectDot.writeOver(toDot(project))
+      println(s"Wrote $projectDot")
+    } else {
+      println(JSON.fromProject(project, T))
+    }
+  case _ =>
+    Os.exit(-1)
+}

jvm/src/test/scala/org/sireum/logika/LogikaRcTest.scala

@@ -51,7 +51,6 @@ class LogikaRcTest extends SireumRcSpec {
     name match {
     case "opsem.sc" | "opsem-alt.sc" => Os.isMac && isInGithubAction
     case "conformance-swap.sc" => isSimplified
-    case "list.sc" => isInGithubAction && Os.env("MILL_VERSION").nonEmpty
     case "strictpure.sc" => Os.isWin && isInGithubAction && !isSimplified
     case _ => false
   }