linduf
1
When I try to install any package with Opam, i.e.
$ opam install why3
I receive the following message:
[ERROR] Solver failed: “/usr/bin/aspcud
/home/jfd/.opam/log/solver-in-22974-5f1023
/home/jfd/.opam/log/solver-out-22974-58c514
-count(removed),-sum(request,version-lag),-count(down),-sum(solution,version-lag),-count(changed)”
exited with code 1 “ERROR: grounder returned with non-zero exit status”
Somebody can help?
Thank you
njb
2
I just tried a:
$ ls -al /usr/bin/aspcud
ls: cannot access '/usr/bin/aspcud': No such file or directory
and then I did:
$ opam install why3
The following actions will be performed:
∗ install why3 1.2.1
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[why3.1.2.1] downloaded from cache at https://opam.ocaml.org/cache
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
∗ installed why3.1.2.1
Done.
So, all I can say is that I have coq 8.10.2 installed - probably best to contact the why3 group
PatJ
3
This looks like a solver failure, this might be an opam bug. What version of opam and aspcud are you using and on what system/distribution?
Try opam --solver=mcss install why3
to see if this is an aspcud issue.
linduf
4
The problem has been solved by reinstallation of the last versions of apscud and opam. Many thanks.
rjbou
5
Great! Since opam 2.0, the solver is embedded, you should no more need an external aspcud (unless you choose to use an external solver).