search

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint
https://apalache-mc.org/
Apache License 2.0
439 stars 40 forks source link

Bat file to run Apalache on Windows #2980

Closed bugarela closed 1 month ago

bugarela commented 2 months ago

Hello :octocat:

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 https://github.com/informalsystems/quint/issues/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.

lemmy commented 2 months ago

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.

bugarela commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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?