search

arminbiere / kissat

MIT License
459 stars 85 forks source link

Make binaries available for common platforms #33

Open danielleberre opened 1 year ago

danielleberre commented 1 year ago

In addition to source code, provide pre-compiled binaries for common platform (windows, macOS, linux) to allow students or researchers to simply download them to give a try to kissat.

If compiling kissat is easy for any computer scientist, when giving a tutorial about SAT, one would prefer to allow the audience to simply download a binary.

I am happy to contribute macOS binaries (M2 and Intel binaries).

arminbiere commented 1 year ago

Sounds very intriguing indeed. I am just worried about legal issues (of distribution in binary form) and security (making sure the binary does not have any backdoor etc.) Do you have examples of other automated reasoning tools providing binaries (except for the web-assembly of Z3 which might have more resources to figure out what to release or not).

danielleberre commented 1 year ago

I see.

In Sat4j, you can download binaries from the continuous integration (or release). https://gitlab.ow2.org/sat4j/sat4j/-/releases

Most tools I know are provided in binary form with Linux distro or homebrew, i.e. third parties.

Just checked clasp, the github repository only contains source code: https://potassco.org/clasp/

Not sure how to deal with that.

a1880 commented 1 year ago

I have ported and compiled most of the Biere family solvers for Windows. Would be happy to provide them here. But I am also not aware of potential legal issues.

a1880 commented 1 year ago

The Potassco team does provide Clasp binaries.

For Windows there are packages for conda. A clasp executable is part of the clingo package:

https://anaconda.org/potassco/clingo
https://anaconda.org/conda-forge/clingo
sfiruch commented 1 year ago

Mate Soos releases CryptoMiniSat binaries as well.

(I don't think there are any legal angles to consider.)

arminbiere commented 1 year ago

I have added linux (amd64) and apple binaries (arm64 and amd64) to the 3.0.0 release. And will work on Windows next.

danielleberre commented 1 year ago

I confirm that I can run kissat arm64 binaries on my mac.

However, I had to allow the unsigned executable to be executed using the following procedure: https://github.molgen.mpg.de/pages/bs/macOSnotes/mac/mac_procs_unsigned.html

a1880 commented 1 year ago

Windows executables can/should also be signed to ensure integrity. I am using this c# class to sign my executables.

danielleberre commented 1 year ago

Just noticed that windows 64 binaries are available through a third party: #7

arminbiere commented 1 year ago

Right, but as I wrote before, I had been working on porting some other code to windows. This for instance applies to dualiza which cross-compiles on linux to windows with mingw. The general problem with supporting different platforms is that it takes time to set-up the port and worse to maintain it or tweak and pay the platforms on which this is done automatically - for instance I just removed Travis for continous testing completely after it failed for Apple already some time ago. Getting the binaries out on top of porting it is an additional hurdle. I am looking into a solution where I can perform and test the occassional release build for MacOS and Windows as easily as possible. For MacOS it is pretty simple by having access to Apple HW directly. This is anyhow a must for us to have as we are teaching courses where students have programming tasks and only have Apple HW. For Windows it is different as WSL (with Ubuintu) really works the same way as native Linux (Ubuntu) for our type software. Only for Windows users who do not want to install WSL we still need a solution (for both porting and generating binaries).

krobelus commented 1 year ago

Yeah travis is dead but Github Actions or Cirrus CI provide MacOS runners.