Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Bat file to run Apalache on Windows #2980

Merged
merged 6 commits into from
Sep 5, 2024
Merged

Bat file to run Apalache on Windows #2980

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
db26c3b
Add bat file to easily run Apalache on Windows
bugarela Sep 4, 2024
2048a73
Fix typo
bugarela Sep 4, 2024
cce9b89
Delete file that is not used in the distribution
bugarela Sep 5, 2024
2d4df36
Update installation instructions
bugarela Sep 5, 2024
585ced5
Fix typos
bugarela Sep 5, 2024
5c58646
Merge branch 'main' into gabriela/bat-file
bugarela Sep 5, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
39 changes: 39 additions & 0 deletions bin/apalache-mc.bat
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
@echo off
rem Run the APALACHE model checker
rem
rem NOTE: The primary intended use for this script is to be copied into the
rem packaged produced.
rem
rem Gabriela Moreira, 2024

rem Set the directory where the script is run from
set "DIR=%~dp0"

rem Set the path to the APALACHE JAR file
set "APALACHE_JAR=%DIR%\..\lib\apalache.jar"
Copy link
Collaborator

@thpani thpani Sep 4, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I believe this would fail to locate the jar when the script is located in ./bin

Are you including this script twice because there's no symlinks on Windows?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm I don't get why it would fail, and also I've tested it in Windows and it works (I've put it alongside the bash file in the bin folder, which is a sibling of lib).

I haven't noticed that one of the bash files was actually a symlink 🤦. I guess it should be fine if the bat is a symlink as well, since these get copied at the release. I'm looking at my apalache distribution downloaded by Quint and the bash in it is a proper file (not symlink), and that is what Windows will be using. So I'll fix this so this bat under comment is a symlink.

Copy link
Collaborator

@thpani thpani Sep 4, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

afaiu, the script in src/universal/bin is the one that's copied to the distribution?

The relative lookup via ../lib will only work relative to src/universal/bin

The reason it works in bash is that ${BASH_SOURCE[0]} gives you the path of the bash file that's executing (i.e., the target of the symlink)

So I would suggest to only keep one batch file, the one that's copied to the distribution. The other one (the symlink in ./bin) only exists to facilitate running a custom build from the source tree.

Copy link
Collaborator

@thpani thpani Sep 4, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also, last time I checked, Windows didn't understand symlinks (or at least not the one produced by ln on Linux)

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah I get what you mean. I think this is doing the same thing because of how DIR is defined 3 lines above this. See https://stackoverflow.com/questions/112055/what-does-d0-mean-in-a-windows-batch-file, this also will five the path of the bat file itself.

Unless you mean that this will only work if this file is a symlink to the one in src/universal/bin - of course, I'll fix that as I said above. Since the bash is a symlink, this should also be a symlink - I just failed to notice that this was the case before you brought it up.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also, last time I checked, Windows didn't understand symlinks (or at least not the one produced by ln on Linux)

What I meant before was: we only need the distribution to include the bat file in order to use it on Windows, and with the bash, this is currently a proper file, not a symlink. We don't need to be able to package Apalache on Windows, so I think it will be fine to only have the one in universal which I think is the one that gets distributed anyway.

I have to test this out, but I have to run right now, so I'll do it tomorrow and let you know if it works as I expect.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry, I was also only typing on my phone and had no way to confirm 😅

We don't need to be able to package Apalache on Windows, so I think it will be fine to only have the one in universal which I think is the one that gets distributed anyway.

Yeah, that's what I meant. There is no ..\lib relative to %DIR% for /bin/apalache-mc.bat.

The one included in the packaged distribution is taken from /src/universal/bin/, so I think we should just keep this one, and drop the duplicate in /bin.


rem Set JVM arguments
set "JVM_ARGS="

rem Check if the APALACHE JAR file exists
if not exist "%APALACHE_JAR%" (
echo ERROR: No file found at %APALACHE_JAR%
echo Ensure you have run 'make package' and are running the script from the
echo distribution package, or else set APALACHE_JAR to point to your custom
echo build jar.
exit /b 1
)

rem Check if the heap size is already set
echo %JVM_ARGS% | findstr /C:"-Xmx" >nul || echo %JVM_ARGS% | findstr /C:"-XX:MaxRAMPercentage" >nul || set "JVM_ARGS=-Xmx4096m"

rem Check whether the command-line arguments contain the debug flag
echo %* | find "--debug" >nul && (
echo # Tool home: %DIR%
echo # Package: %APALACHE_JAR%
echo # JVM args: %JVM_ARGS%
echo #
)

rem Run the Java command
java %JVM_ARGS% -jar "%APALACHE_JAR%" %*
2 changes: 1 addition & 1 deletion script/release-prepare.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ then
# Explicitly set the release version
sbt "setVersion ${RELEASE_VERSION}"
else
# Derive the relesae version by removing the -SNAPSHOT suffix
# Derive the release version by removing the -SNAPSHOT suffix
sbt removeVersionSnapshot
RELEASE_VERSION=$("$DIR"/get-version.sh)
fi
Expand Down
39 changes: 39 additions & 0 deletions src/universal/bin/apalache-mc.bat
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
@echo off
rem Run the APALACHE model checker
rem
rem NOTE: The primary intended use for this script is to be copied into the
rem packaged produced.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
rem packaged produced.
rem package produced.

rem
rem Gabriela Moreira, 2024

rem Set the directory where the script is run from
set "DIR=%~dp0"

rem Set the path to the APALACHE JAR file
set "APALACHE_JAR=%DIR%\..\lib\apalache.jar"

rem Set JVM arguments
set "JVM_ARGS="

rem Check if the APALACHE JAR file exists
if not exist "%APALACHE_JAR%" (
echo ERROR: No file found at %APALACHE_JAR%
echo Ensure you have run 'make package' and are running the script from the
echo distribution package, or else set APALACHE_JAR to point to your custom
echo build jar.
exit /b 1
)

rem Check if the heap size is already set
echo %JVM_ARGS% | findstr /C:"-Xmx" >nul || echo %JVM_ARGS% | findstr /C:"-XX:MaxRAMPercentage" >nul || set "JVM_ARGS=-Xmx4096m"

rem Check whether the command-line arguments contain the debug flag
echo %* | find "--debug" >nul && (
echo # Tool home: %DIR%
echo # Package: %APALACHE_JAR%
echo # JVM args: %JVM_ARGS%
echo #
)

rem Run the Java command
java %JVM_ARGS% -jar "%APALACHE_JAR%" %*
Loading