flyvy-verifier / flyvy

An experimental framework for temporal verification based on first-order linear-time temporal logic. Our goal is to express transition systems in first-order logic and verify temporal correctness properties, including safety and liveness.
BSD 2-Clause "Simplified" License
14 stars 1 forks source link

Add Windows support #62

Closed dranov closed 1 year ago

dranov commented 1 year ago

Here's a summary of the changes:

vmwclabot commented 1 year ago

@dranov, you must sign every commit in this pull request acknowledging our Developer Certificate of Origin before your changes are merged. This can be done by adding Signed-off-by: John Doe <john.doe@email.org> to the last line of each Git commit message. The e-mail address used to sign must match the e-mail address of the Git author. Click here to view the Developer Certificate of Origin agreement.

dranov commented 1 year ago

There was a merge commit I did using the GitHub interface, which didn't have the Signed-off-by line, so I force-pushed to remove it.

tchajed commented 1 year ago

Thanks for working on this!

None of us develop on Windows directly (though some do use WSL), so in order to support this I'd definitely want to test on Windows in CI. That would require porting tools/ci-checks.sh to Windows, and I'd rather not maintain a copy of that script. As a result if we do want to fully support Windows, I'd probably want to switch to something like cargo-xtask. Similarly this would easily avoid the duplication between tools/solver-versions.sh and tools/solver-versions.ps1 (the Rust code actually parses the shell script to avoid having those versions specified multiple times) by just porting download-solvers.sh to Rust.

Quick logistical note: I'd recommend rebasing rather than merging to update with the base branch - it tends to produce less conflicts in the end when we do a squash-merge.

tchajed commented 1 year ago

Oded and I discussed it and we don't think it's worth it for us to maintain Windows support, especially since WSL seems to work well for this use case.

That said, some of the changes in this PR are general improvements and should also make the code fairly compatible. If you remove the PowerShell scripts I'd be happy to merge everything else. If we (or you!) decide to implement cargo xtask, then I think adding (somewhat unofficial) Windows support would become easy.

dranov commented 1 year ago

Sure, I understand Windows is not a priority. That's okay. (I personally use WSL 2 myself.)

I don't have the bandwidth to look into cargo-xtask now, so I've removed the PowerShell scripts.

tchajed commented 1 year ago

Thanks for updating the PR!