search

ocaml / opam

opam is a source-based package manager. It supports multiple simultaneous compiler installations, flexible package constraints, and a Git-friendly development workflow.
https://opam.ocaml.org
Other
1.21k stars 348 forks source link

Always use aspcudf instead of custom solver heuristics #685

Closed darioteixeira closed 10 years ago

darioteixeira commented 10 years ago

After the latest "opam update" I'm getting the folllowing message:

The brute-force exploration algorithm timed-out [97 states, 5s].
You might need to add explicit version constraints to your request to get a better answer.

0 to install | 38 to reinstall | 0 to upgrade | 21 to downgrade | 0 to remove
You can now run 'opam upgrade' to upgrade your system.

I don't think I'm doing anything out of the ordinary with my OPAM installation. I do have a local repository with some packages (Blahcaml, Camlhighlight, Bookaml) which I have not yet uploaded to the main OPAM repository, but that's it. (I'm attaching my list of installed packages)

Is this a known issue? Also, isn't 5 seconds a bit on the low side for a time-out? Given that there is a huge performance difference in the systems OPAM may be running on (e.g. the latest Core i7 vs a Raspberry Pi), shouldn't this time-out be at least configurable?

darioteixeira commented 10 years ago

Here is the package list (compiler version is 4.00.1):

base-bigarray           base
base-threads            base
base-unix               base
batteries               2.0.0
bin_prot                109.30.00
biniou                  1.0.6
bitcoin                 1.1.1
blahcaml                2.1
bookaml                 1.0
calendar                2.03.2
camlhighlight           3.0
camlzip                 1.05
ccss                    1.4
comparelib              109.27.00
core                    109.32.00
core_extended           109.31.00
core_kernel             109.33.00
cppo                    0.9.3
cryptokit               1.7
csv                     1.3.0
custom_printf           109.27.00
dbm                     1.0
deriving-ocsigen        0.3c
easy-format             1.0.1
eliom                   3.0.3
fieldslib               109.20.00
fileutils               0.4.4
herelib                 109.15.00
js_of_ocaml             1.3.2
litiom                  2.0
lwt                     2.4.3
lwt-zmq                 1.0-beta3
menhir                  20130116
oasis                   0.3.0
ocaml-data-notation     0.0.10
ocaml-zmq               0
ocamlfind               1.3.3
ocamlify                0.0.1
ocamlmod                0.0.4
ocamlnet                3.6.0
ocsigenserver           2.2.0
optcomp                 1.4
ospec                   0.3.1
ounit                   1.1.2
pa_ounit                109.27.00
patdiff                 109.30.00
pcre-ocaml              7.0.2
pipebang                109.28.00
pxp                     1.2.3
react                   0.9.4
res                     4.0.3
safepass                1.2
sexplib                 109.20.00
sqlite3-ocaml           2.0.4
ssl                     0.4.6
textutils               109.24.00
type_conv               109.28.00
tyxml                   2.2.0
uint                    1.1.0
ulex                    1.1
variantslib             109.15.00
xstrp4                  1.8
yojson                  1.1.6
avsm commented 10 years ago

Which version of OPAM? (--git-version)

On 15 Jul 2013, at 11:25, darioteixeira notifications@github.com wrote:

Here is the package list (compiler version is 4.00.1):

base-bigarray base base-threads base base-unix base batteries 2.0.0 bin_prot 109.30.00 biniou 1.0.6 bitcoin 1.1.1 blahcaml 2.1 bookaml 1.0 calendar 2.03.2 camlhighlight 3.0 camlzip 1.05 ccss 1.4 comparelib 109.27.00 core 109.32.00 core_extended 109.31.00 core_kernel 109.33.00 cppo 0.9.3 cryptokit 1.7 csv 1.3.0 custom_printf 109.27.00 dbm 1.0 deriving-ocsigen 0.3c easy-format 1.0.1 eliom 3.0.3 fieldslib 109.20.00 fileutils 0.4.4 herelib 109.15.00 js_of_ocaml 1.3.2 litiom 2.0 lwt 2.4.3 lwt-zmq 1.0-beta3 menhir 20130116 oasis 0.3.0 ocaml-data-notation 0.0.10 ocaml-zmq 0 ocamlfind 1.3.3 ocamlify 0.0.1 ocamlmod 0.0.4 ocamlnet 3.6.0 ocsigenserver 2.2.0 optcomp 1.4 ospec 0.3.1 ounit 1.1.2 pa_ounit 109.27.00 patdiff 109.30.00 pcre-ocaml 7.0.2 pipebang 109.28.00 pxp 1.2.3 react 0.9.4 res 4.0.3 safepass 1.2 sexplib 109.20.00 sqlite3-ocaml 2.0.4 ssl 0.4.6 textutils 109.24.00 type_conv 109.28.00 tyxml 2.2.0 uint 1.1.0 ulex 1.1 variantslib 109.15.00 xstrp4 1.8 yojson 1.1.6 — Reply to this email directly or view it on GitHub.

rdicosmo commented 10 years ago

Hi Dario, whenever one encounters such an issue, it is extremely useful to run opam with the option --cudf=foo and attach the resulting file(s) foo-1.cudf, ... foo-XXX.cudf to the bug a report; this allows to reproduce the issue completely, and see what went wrong.

On my side, I use opam with the aspcud external solver on quite complex configurations with no real issues found up to now.

Roberto

On Mon, Jul 15, 2013 at 03:20:35AM -0700, darioteixeira wrote:

After the latest "opam update" I'm getting the folllowing message:

The brute-force exploration algorithm timed-out [97 states, 5s]. You might need to add explicit version constraints to your request to get a better answer.

0 to install | 38 to reinstall | 0 to upgrade | 21 to downgrade | 0 to remove You can now run 'opam upgrade' to upgrade your system.

I don't think I'm doing anything out of the ordinary with my OPAM installation. I do have a local repository with some packages (Blahcaml, Camlhighlight, Bookaml) which I have not yet uploaded to the main OPAM repository, but that's it. (I'm attaching my list of installed packages)

Is this a known issue? Also, isn't 5 seconds a bit on the low side for a time-out? Given that there is a huge performance difference in the systems OPAM may be running on (e.g. the latest Core i7 vs a Raspberry Pi), shouldn't this time-out be at least configurable?

— Reply to this email directly or view it on GitHub.*

Roberto Di Cosmo

Professeur En delegation a l'INRIA PPS E-mail: roberto@dicosmo.org Universite Paris Diderot WWW : http://www.dicosmo.org Case 7014 Tel : ++33-(0)1-57 27 92 20 5, Rue Thomas Mann
F-75205 Paris Cedex 13 Identica: http://identi.ca/rdicosmo

FRANCE. Twitter: http://twitter.com/rdicosmo

Attachments: MIME accepted, Word deprecated

http://www.gnu.org/philosophy/no-word-attachments.html

Office location:

Bureau 3020 (3rd floor) Batiment Sophie Germain Avenue de France

Metro Bibliotheque Francois Mitterrand, ligne 14/RER C

GPG fingerprint 2931 20CE 3A5A 5390 98EC 8BFC FCCA C3BE 39CB 12D3

darioteixeira commented 10 years ago

@avsm:

dario@dual:~$ opam --git-version
dario@dual:~$ opam --version
1.0.1
darioteixeira commented 10 years ago

@rdicosmo:

timeout-1.cudf: http://pastebin.com/K8VqBpL9 timeout-2.cudf: http://pastebin.com/7mAFs0bN

Let me know if further info is necessary.

rdicosmo commented 10 years ago

Hi Dario, you hit a limitation of the opam internal solver.

Using the aspcud external solver, a solution is found in 1/10th of a second (see attached solution file... to get the actual package version you need to lookup the sourceversion value in the original timeout-1.cudf file).

Hence, I do recommend always using the aspcud external solver. It is available on stock Debian machines by installing apt-cudf and aspcud, but not packaged yet for OS X or Windows.

If anybody is interested in adding support for executing a remote solver, and setting up a simple solver farm to help friend Opamers/OCamlers out there in case they are not on Linux machines, let me know, and we can set up a task force for doing this.

For future reference, here are the commands I used to test your report

-> remove the comment line in timeout-1.cudf (# comments are not allowed in CUDF) -> issue

  aspcud timeout-1.cudf solution.cudf "trendy"

or any optimization criteria allowed in the MISC 2012 competition, like 

  aspcud timeout-1.cudf solution.cudf "-count(removed),-notuptodate(solution),-count(new)"

-> read the results in the solution.cudf file

Roberto

On Mon, Jul 15, 2013 at 05:47:48AM -0700, darioteixeira wrote:

@rdicosmo:

timeout-1.cudf: http://pastebin.com/K8VqBpL9 timeout-2.cudf: http://pastebin.com/7mAFs0bN

Let me know if further info is necessary.

— Reply to this email directly or view it on GitHub.*

Roberto Di Cosmo

Professeur En delegation a l'INRIA PPS E-mail: roberto@dicosmo.org Universite Paris Diderot WWW : http://www.dicosmo.org Case 7014 Tel : ++33-(0)1-57 27 92 20 5, Rue Thomas Mann
F-75205 Paris Cedex 13 Identica: http://identi.ca/rdicosmo

FRANCE. Twitter: http://twitter.com/rdicosmo

Attachments: MIME accepted, Word deprecated

http://www.gnu.org/philosophy/no-word-attachments.html

Office location:

Bureau 3020 (3rd floor) Batiment Sophie Germain Avenue de France

Metro Bibliotheque Francois Mitterrand, ligne 14/RER C

GPG fingerprint 2931 20CE 3A5A 5390 98EC 8BFC FCCA C3BE 39CB 12D3

darioteixeira commented 10 years ago

Hi Roberto,

Thanks for your assistance -- it is much appreciated. One immediate question, though: I must be missing something obvious, because I cannot find documentation on how to run OPAM with an external solver. Neither the man pages nor the "Advanced Usage" mention this possibility.

Another not-so-immediate question: it is disappointing that OPAM cannot handle a fairly small use case. Is this issue solely related to the parameterisation of OPAM's built-in solver, and thus easily fixed? (Timing out after only 5 seconds does strike me as a bit premature).

rdicosmo commented 10 years ago

Hi Dario, there is nothing special to do for using the aspcud external solver: opam detects the presence of aspcud in the path, and uses it if it is available.

You can tweak the optimization criteria by setting the environment variable OPAMCRITERIA... the default value is

 -removed,-notuptodate,-new

I agree that the documentation should mention this, I'll have a look

Roberto

On Mon, Jul 15, 2013 at 11:07:30AM -0700, darioteixeira wrote:

Hi Roberto,

Thanks for your assistance -- it is much appreciated. One immediate question, though: I must be missing something obvious, because I cannot find documentation on how to run OPAM with an external solver. Neither the man pages nor the "Advanced Usage" mention this possibility.

Another not-so-immediate question: it is disappointing that OPAM cannot handle a fairly small use case. Is this issue solely related to the parameterisation of OPAM's built-in solver, and thus easily fixed? (Timing out after only 5 seconds does strike me as a bit premature).

— Reply to this email directly or view it on GitHub.*

Roberto Di Cosmo

Professeur En delegation a l'INRIA PPS E-mail: roberto@dicosmo.org Universite Paris Diderot WWW : http://www.dicosmo.org Case 7014 Tel : ++33-(0)1-57 27 92 20 5, Rue Thomas Mann
F-75205 Paris Cedex 13 Identica: http://identi.ca/rdicosmo

FRANCE. Twitter: http://twitter.com/rdicosmo

Attachments: MIME accepted, Word deprecated

http://www.gnu.org/philosophy/no-word-attachments.html

Office location:

Bureau 3020 (3rd floor) Batiment Sophie Germain Avenue de France

Metro Bibliotheque Francois Mitterrand, ligne 14/RER C

GPG fingerprint 2931 20CE 3A5A 5390 98EC 8BFC FCCA C3BE 39CB 12D3

samoht commented 10 years ago

I'm a bit reluctant to mention the external solver as the "recommended" way to go, as it is only packaged for debian for now on. On the long term, I think that's indeed a better solution than the custom-made heuristic used in OPAM, but we definitely need some help to make it nicely available on all possible platforms (including windows :p).

btw, I'm not able to reproduce your issue easily, as you have blahcaml which is not in the main repository. Regarding your " fairly small use case", don't forget it's a combinatorial problem, so what is important is the size of the universe of packages, not your request -- but I'm interested to understand what went wrong with.

darioteixeira commented 10 years ago

Since I run a Debian-based system, installing the external solver was a quick and easy way to make the problem go away. But I agree that this is not a particularly user-friendly solution in the general case...

Anyway, I'll soon upload blahcaml and my other local packages to the main OPAM repository. This should give you a chance to replicate the problem. But before that, I'll compile the current git snapshot of OPAM, and check whether the configurable timeout is a good stop-gap option.

darioteixeira commented 10 years ago

Good news! After uninstalling apt-cudf and aspcud, I ran opam update, which again produced the time-out error after the default 5 seconds. However, setting OPAMSOLVERTIMEOUT=7 is enough for opam update to succeed!

rdicosmo commented 10 years ago

Following up on the brainstorming, I see a few lines of progress here, and I'd love to hear feedback/suggestions/ and finding volunteers :-)

What we recommend in http://dx.doi.org/10.1016/j.infsof.2012.09.002 is to use an external solver (for several reasons detailed in the paper).

To do that, here are the possibilities I see

Any thoughts on this?

On Tue, Jul 16, 2013 at 03:40:16AM -0700, darioteixeira wrote:

Since I run a Debian-based system, installing the external solver was a quick and easy way to make the problem go away. But I agree that this is not a particularly user-friendly solution in the general case...

Anyway, I'll soon upload blahcaml and my other local packages to the main OPAM repository. This should give you a chance to replicate the problem. But before that, I'll compile the current git snapshot of OPAM, and check whether the configurable timeout is a good stop-gap option.

— Reply to this email directly or view it on GitHub.*

Roberto Di Cosmo

Professeur En delegation a l'INRIA PPS E-mail: roberto@dicosmo.org Universite Paris Diderot WWW : http://www.dicosmo.org Case 7014 Tel : ++33-(0)1-57 27 92 20 5, Rue Thomas Mann
F-75205 Paris Cedex 13 Identica: http://identi.ca/rdicosmo

FRANCE. Twitter: http://twitter.com/rdicosmo

Attachments: MIME accepted, Word deprecated

http://www.gnu.org/philosophy/no-word-attachments.html

Office location:

Bureau 3020 (3rd floor) Batiment Sophie Germain Avenue de France

Metro Bibliotheque Francois Mitterrand, ligne 14/RER C

GPG fingerprint 2931 20CE 3A5A 5390 98EC 8BFC FCCA C3BE 39CB 12D3

avsm commented 10 years ago

On 16 Jul 2013, at 12:00, Roberto Di Cosmo notifications@github.com wrote:

  • take an existing solver (aspcud) and package it for all common platforms (*nix, OS X, Windows...): it is possible to do it (the source of aspcud is basically C++ plus some scripts), but requires manpower skilled on the various platforms

This is my preferred solution. The source for ASPCUD is remarkably hard to find online though. Is it available on a public repository?

-anil

rdicosmo commented 10 years ago

Of course it is, and is distributed under an Open Source licence.

You can find it here:

http://www.cs.uni-potsdam.de/wv/aspcud/

and that's the first result I see when googling "aspcud", but of course, Google result may vary :-)

On Tue, Jul 16, 2013 at 05:18:44AM -0700, Anil Madhavapeddy wrote:

On 16 Jul 2013, at 12:00, Roberto Di Cosmo notifications@github.com wrote:

  • take an existing solver (aspcud) and package it for all common platforms (*nix, OS X, Windows...): it is possible to do it (the source of aspcud is basically C++ plus some scripts), but requires manpower skilled on the various platforms

This is my preferred solution. The source for ASPCUD is remarkably hard to find online though. Is it available on a public repository?

-anil

— Reply to this email directly or view it on GitHub.*

Roberto Di Cosmo

Professeur En delegation a l'INRIA PPS E-mail: roberto@dicosmo.org Universite Paris Diderot WWW : http://www.dicosmo.org Case 7014 Tel : ++33-(0)1-57 27 92 20 5, Rue Thomas Mann
F-75205 Paris Cedex 13 Identica: http://identi.ca/rdicosmo

FRANCE. Twitter: http://twitter.com/rdicosmo

Attachments: MIME accepted, Word deprecated

http://www.gnu.org/philosophy/no-word-attachments.html

Office location:

Bureau 3020 (3rd floor) Batiment Sophie Germain Avenue de France

Metro Bibliotheque Francois Mitterrand, ligne 14/RER C

GPG fingerprint 2931 20CE 3A5A 5390 98EC 8BFC FCCA C3BE 39CB 12D3

avsm commented 10 years ago

I found that of course, but not a repository URL that didn't need a password (on inria gforge)

On 16 Jul 2013, at 13:30, Roberto Di Cosmo notifications@github.com wrote:

Of course it is, and is distributed under an Open Source licence.

You can find it here:

http://www.cs.uni-potsdam.de/wv/aspcud/

and that's the first result I see when googling "aspcud", but of course, Google result may vary :-)

On Tue, Jul 16, 2013 at 05:18:44AM -0700, Anil Madhavapeddy wrote:

On 16 Jul 2013, at 12:00, Roberto Di Cosmo notifications@github.com wrote:

  • take an existing solver (aspcud) and package it for all common platforms (*nix, OS X, Windows...): it is possible to do it (the source of aspcud is basically C++ plus some scripts), but requires manpower skilled on the various platforms

This is my preferred solution. The source for ASPCUD is remarkably hard to find online though. Is it available on a public repository?

-anil

— Reply to this email directly or view it on GitHub.*

Roberto Di Cosmo

Professeur En delegation a l'INRIA PPS E-mail: roberto@dicosmo.org Universite Paris Diderot WWW : http://www.dicosmo.org Case 7014 Tel : ++33-(0)1-57 27 92 20 5, Rue Thomas Mann F-75205 Paris Cedex 13 Identica: http://identi.ca/rdicosmo

FRANCE. Twitter: http://twitter.com/rdicosmo

Attachments: MIME accepted, Word deprecated

http://www.gnu.org/philosophy/no-word-attachments.html

Office location:

Bureau 3020 (3rd floor) Batiment Sophie Germain Avenue de France

Metro Bibliotheque Francois Mitterrand, ligne 14/RER C

GPG fingerprint 2931 20CE 3A5A 5390 98EC 8BFC FCCA C3BE 39CB 12D3 — Reply to this email directly or view it on GitHub.

rdicosmo commented 10 years ago

Hi Anil, the aspcud code is developed by the Potassco team, which is in Potsdam, not in Paris, and is not hosted on the Inria gforge; maybe you got confused following links.

The code you want (pointed at from the aspcud page) is

http://www.cs.uni-potsdam.de/wv/aspcud/files/aspcud-full-1.7.tar

that needs also the solver engine composed of the four projects

Preprocessor/Wrapper Sources (tar.xz) http://www.cs.uni-potsdam.de/wv/aspcud/files/aspcud-r5904.tar.xz
Grounder Sources http://sourceforge.net/projects/potassco/files/gringo/3.0.4/
Solver(clasp) Sources http://sourceforge.net/p/potassco/code/5807/tree/trunk/clasp/
Solver(unclasp) Sources http://sourceforge.net/p/potassco/code/5873/tree/branches/unclasp-oll/

Ralf Treinen treinen@debian.org already did the packaging work for Debian, so it may be easier to just do

apt-get source aspcud

on a Debian machine and have a look at how it has been compiled... and even better would be to get in touch with the Potassco people who are surely interested in having their tools compiled/packaged for other system.

Let me know if you are looking into this packaging work, and I will put you in touch!

All the best

Roberto

On Tue, Jul 16, 2013 at 06:29:44AM -0700, Anil Madhavapeddy wrote:

I found that of course, but not a repository URL that didn't need a password (on inria gforge)

On 16 Jul 2013, at 13:30, Roberto Di Cosmo notifications@github.com wrote:

Of course it is, and is distributed under an Open Source licence.

You can find it here:

http://www.cs.uni-potsdam.de/wv/aspcud/

and that's the first result I see when googling "aspcud", but of course, Google result may vary :-)

On Tue, Jul 16, 2013 at 05:18:44AM -0700, Anil Madhavapeddy wrote:

On 16 Jul 2013, at 12:00, Roberto Di Cosmo notifications@github.com wrote:

  • take an existing solver (aspcud) and package it for all common platforms (*nix, OS X, Windows...): it is possible to do it (the source of aspcud is basically C++ plus some scripts), but requires manpower skilled on the various platforms

This is my preferred solution. The source for ASPCUD is remarkably hard to find online though. Is it available on a public repository?

-anil

— Reply to this email directly or view it on GitHub.*

Roberto Di Cosmo

Professeur En delegation a l'INRIA PPS E-mail: roberto@dicosmo.org Universite Paris Diderot WWW : http://www.dicosmo.org Case 7014 Tel : ++33-(0)1-57 27 92 20 5, Rue Thomas Mann F-75205 Paris Cedex 13 Identica: http://identi.ca/rdicosmo

FRANCE. Twitter: http://twitter.com/rdicosmo

Attachments: MIME accepted, Word deprecated

http://www.gnu.org/philosophy/no-word-attachments.html

Office location:

Bureau 3020 (3rd floor) Batiment Sophie Germain Avenue de France

Metro Bibliotheque Francois Mitterrand, ligne 14/RER C

GPG fingerprint 2931 20CE 3A5A 5390 98EC 8BFC FCCA C3BE 39CB 12D3 — Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub.*

Roberto Di Cosmo

Professeur En delegation a l'INRIA PPS E-mail: roberto@dicosmo.org Universite Paris Diderot WWW : http://www.dicosmo.org Case 7014 Tel : ++33-(0)1-57 27 92 20 5, Rue Thomas Mann
F-75205 Paris Cedex 13 Identica: http://identi.ca/rdicosmo

FRANCE. Twitter: http://twitter.com/rdicosmo

Attachments: MIME accepted, Word deprecated

http://www.gnu.org/philosophy/no-word-attachments.html

Office location:

Bureau 3020 (3rd floor) Batiment Sophie Germain Avenue de France

Metro Bibliotheque Francois Mitterrand, ligne 14/RER C

GPG fingerprint 2931 20CE 3A5A 5390 98EC 8BFC FCCA C3BE 39CB 12D3

darioteixeira commented 10 years ago

And for those who don't know this already: the source code for all Debian packages can be browsed online, thanks to the very neat http://sources.debian.net/ site. It's even syntax highlighted! Here's a direct link to aspcud: http://sources.debian.net/src/aspcud

rdicosmo commented 10 years ago

Thanks Dario for the advertisement : that's beautiful work sponsored by Irill (and actually performed in the office next to mine by Zack and Matthieu) :-)

Nevetheless, it's better to get in touch with upstream in this cas

On Tue, Jul 16, 2013 at 07:35:51AM -0700, darioteixeira wrote:

And for those who don't know this already: the source code for all Debian packages can be browsed online, thanks to the very neat http:// sources.debian.net/ site. It's even syntax highlighted! Here's a direct link to aspcud: http://sources.debian.net/src/aspcud

— Reply to this email directly or view it on GitHub.*

Roberto Di Cosmo

Professeur En delegation a l'INRIA PPS E-mail: roberto@dicosmo.org Universite Paris Diderot WWW : http://www.dicosmo.org Case 7014 Tel : ++33-(0)1-57 27 92 20 5, Rue Thomas Mann
F-75205 Paris Cedex 13 Identica: http://identi.ca/rdicosmo

FRANCE. Twitter: http://twitter.com/rdicosmo

Attachments: MIME accepted, Word deprecated

http://www.gnu.org/philosophy/no-word-attachments.html

Office location:

Bureau 3020 (3rd floor) Batiment Sophie Germain Avenue de France

Metro Bibliotheque Francois Mitterrand, ligne 14/RER C

GPG fingerprint 2931 20CE 3A5A 5390 98EC 8BFC FCCA C3BE 39CB 12D3

AltGr commented 10 years ago

Superseded by #1267