diff --git a/.gitignore b/.gitignore index 1d5c327d..b2cb58e0 100644 --- a/.gitignore +++ b/.gitignore @@ -3,6 +3,7 @@ /out target /versions.properties +/bin/install /bin/mill.bat /bin/prelude.sh /bin/platform.sh diff --git a/bin/build.cmd b/bin/build.cmd index 0da952be..0b097732 100755 --- a/bin/build.cmd +++ b/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") diff --git a/bin/project-standalone.cmd b/bin/project-standalone.cmd new file mode 100755 index 00000000..ba0d8b76 --- /dev/null +++ b/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) +} \ No newline at end of file diff --git a/jvm/src/test/scala/org/sireum/logika/LogikaRcTest.scala b/jvm/src/test/scala/org/sireum/logika/LogikaRcTest.scala index 054d7c01..c9a7e634 100644 --- a/jvm/src/test/scala/org/sireum/logika/LogikaRcTest.scala +++ b/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 }