Slash script is a universal (combined sh and batch) shell script using Windows’ .cmd file extension, where the actual script functionality is written in Slang. Similar to Slang script files, the Sireum IVE provides IDE support (e.g., Slang type checking) for Slash script files. Slash script uses the CRLF (Windows) newline separator and its header consists of sh and batch scripts that run the file using the Slang script runner. Note that sh part should end with a hash (#). Below is an example of a Slash file:


   ::/*#! 2> /dev/null                                           #
   @ 2>/dev/null # 2>nul & echo off & goto BOF                   #
   if [ -f "$0.com" ] && [ "$0.com" -nt "$0" ]; then             #
     exec "$0.com" "$@"                                          #
   fi                                                            #
   rm -f "$0.com"                                                #
   if [ -z ${SIREUM_HOME} ]; then                                #
     echo "Please set SIREUM_HOME env var"                       #
     exit -1                                                     #
   fi                                                            #
   exec ${SIREUM_HOME}/bin/sireum slang run -s -n "$0" "$@"      #
   :BOF
   if not defined SIREUM_HOME (
     echo Please set SIREUM_HOME env var
     exit /B -1
   )
   set NEWER=False
   if exist %~dpnx0.com for /f %%i in ('powershell -noprofile -executionpolicy bypass -command "(Get-Item %~dpnx0.com).LastWriteTime -gt (Get-Item %~dpnx0).LastWriteTime"') do @set NEWER=%%i
   if "%NEWER%" == "True" goto native
   del "%~dpnx0.com" > nul 2>&1
   %SIREUM_HOME%\bin\sireum.bat slang run -s -n "%0" %*
   exit /B %errorlevel%
   :native
   %~dpnx0.com %*
   exit /B %errorlevel%
   ::!#*/
   // #Sireum
   import org.sireum._
   
   println(s"Script home: ${Os.slashDir}")
   println(s"CLI args: ${Os.cliArgs}")
   println(s"Current working directory: ${Os.cwd}")
   
   if (Os.kind == Os.Kind.Win) {
     Os.proc(ISZ("cmd", "/c", "dir")).console.run()
   } else {
     Os.proc(ISZ("ls", "-lah")).console.run()
   }

Like Slang code, Slash script can be compiled to native code (.cmd.com) if Graal’s native-image is installed as part of the Sireum infrastructure (e.g., invoking $SIREUM_HOME/bin/install/grall.cmd in macOS/Linux or %SIREUM_HOME%\bin\install\graal.cmd in Windows).

The sh and batch script parts detect if it is already compiled to native and if the native executable is newer than this file (based on the files’ last modified time); if so, the native executable is called instead, thus offering no JVM boot up and no code compilation overhead on subsequent uses.

For more examples, see: