search

pysathq / pysat

A toolkit for SAT-based prototyping in Python
https://pysathq.github.io/
MIT License
385 stars 69 forks source link

Setup failing due to broken links #48

Closed MiguelTerraNeves closed 4 years ago

MiguelTerraNeves commented 4 years ago

Hi Alexey,

I have had an issue a few times with broken links for the SAT solvers during the pysat installation. This is particularly severe in my case because pysat is part of a testing pipeline that is run for each PR, which requires installing pysat in a VM every time. Because of this, from time to time, all our tests start failing because of a broken link in pysat, even if the code being pushed does not use pysat.

This problem would be fixed if the SAT solvers were part of pysat itself instead of automatically downloaded at setup time. Is there any particularly strong reason why you opted for the latter solution?

alexeyignatiev commented 4 years ago

Hi Miguel,

That was a decision made by all the authors of the paper - not just mine. The reason was that we did not want PySAT to have third-party source code. Hence all the headaches with solver installation now. Do you know what exactly is failing? Is it always the same solver?

MiguelTerraNeves commented 4 years ago

It happened a few weeks ago with the Maple solvers (I fixed this by commenting those solvers from the installation process in my fork since I'm not using those). Last week it was with Glucose 3, but in the meantime that one fixed itself. Nonetheless, it's something that is bound to happen again in the future.

alexeyignatiev commented 4 years ago

It would be great to understand why it fails to download some of the solvers on your machine and does so randomly as far as I understand... A number of people complained about this issue before. It never happens for me and so I can't see where the problem resides. I will need to do some googling. :)

MiguelTerraNeves commented 4 years ago

It's not something specific to someone's machine. The problem is the links in the sources variable (line 30 of solvers/prepare.py) being down. Basically, I pasted the link of one of the Maple solvers into a web browser and got a 404, thus why the download was failing. It's not something you can control with the current solution

alexeyignatiev commented 4 years ago

Well, if there was a reliable server (or even a few servers), we could just upload the archives there and use it as a mirror. For that, we could simply use the current functionality of solvers/prepare.py.

MiguelTerraNeves commented 4 years ago

Sounds good to me. You could also have a caching system in place in that server that maintains the most recently downloaded solver sources, and this way if you fail to download the source you just return the cached source instead. Another option could be to have a background process that periodically downloads the most recent versions of the solver sources

alexeyignatiev commented 4 years ago

OK, I need to think if there is such a server that could be a mirror. :) Regarding "most recent versions", PySAT can only handle one specific version of each supported solver because of the current patch mechanism. I mean even if there is another version available, patch would most likely fail anyway.

MiguelTerraNeves commented 4 years ago

Ok, in that case it makes sense for the mirror server to be managed manually instead :)

alexeyignatiev commented 4 years ago

Hi @MiguelTerraNeves. I hope that 2822e9c should solve most if not all installation-related issues.

MiguelTerraNeves commented 4 years ago

You can't really test without breaking the links but I don't see why that shouldn't fix it :) Feel free to close this. Thanks for fixing this

alexeyignatiev commented 4 years ago

OK, closing it. :)