Bat file to run Apalache on Windows

[bugarela]

Hello

I've written this file months ago and gave it to my students that use windows. I'd like to add it to the released Apalache files mainly in order to call this bat from Quint when in Windows, and therefore have the same seamless integration on quint verify as we have on Linux and Mac OS. See informalsystems/quint#1414. WDYT?

PS: I'm not familiar with bat at all. I've asked ChatGPT to convert the bash version into bat and inspected the results to make sure nothing weird was added. One thing I noticed is that killing the bat doesn't kill Apalache, which would be ideal. I looked at this template as basis (as the bash refers to this set of templates) but couldn't find how to set that up.

• Tests added for any new code
• Ran make fmt-fix (or had formatting run automatically on all files edited)
• Documentation added for any new functionality
• Entries added to ./unreleased/ for any new functionality

[konnov]

That's a good addition, though I am not sure whether Windows users are using WSL these days. Perhaps, @lemmy could give us a hint.

Shall we add at least one CI test to check, whether this file is actually executable on Windows?

[konnov]

Suggested change

	rem packaged produced.
	rem package produced.

[lemmy]

That's a good addition, though I am not sure whether Windows users are using WSL these days. Perhaps, @lemmy could give us a hint.

Shall we add at least one CI test to check, whether this file is actually executable on Windows?

I'm not a Windows user, but WSL (Windows Subsystem for Linux) is quite popular among Windows developers. Interestingly, a few years ago, TLC ran faster virtualized on WSL than it did when running natively.

[thpani]

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?

[bugarela]

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.

[thpani]

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.

[thpani]

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

[bugarela]

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.

[bugarela]

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.

[thpani]

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.

[bugarela]

I removed the extra file per @thpani explanation and found some documentation to update.

I'm trying to come up with a way to test this, but I can't think of a simple way. I think we need a windows machine with an up-to-date version of the .jar file so the bat calls it. It should be up-to-date, because otherwise there's no reason to run the test as a CI check. But also, I don't think we can compile Apalache on Windows at the moment (?) I can try that maybe.

So my best idea so far would be to set up a windows machine that uses docker to build the .jar and then we call the .bat outside of docker.

@konnov @thpani do you have a better idea?

[konnov]

I removed the extra file per @thpani explanation and found some documentation to update.

I'm trying to come up with a way to test this, but I can't think of a simple way. I think we need a windows machine with an up-to-date version of the .jar file so the bat calls it. It should be up-to-date, because otherwise there's no reason to run the test as a CI check. But also, I don't think we can compile Apalache on Windows at the moment (?) I can try that maybe.

So my best idea so far would be to set up a windows machine that uses docker to build the .jar and then we call the .bat outside of docker.

@konnov @thpani do you have a better idea?

That sounds complicated. Can we maybe just get the jar from the latest release somehow?

[bugarela]

That sounds complicated. Can we maybe just get the jar from the latest release somehow?

Agreed. We can, but then it's kind of a silly CI check, since it will run for every commit but it will be testing the same thing (last released jar). I thought about maybe adding this as a check while releasing, but then, do we really want to have that fail the whole release pipeline?

[thpani]

I'm okay merging this — if it doesn't work for someone, hopefully we'd get a bug report