<div dir="ltr">Ah, that was my bad.  I didn't do `opam repo add coq-released <a href="https://coq.inria.fr/opam/released`">https://coq.inria.fr/opam/released`</a>.  Even without `aspcud`, Iris just works well.<div><br></div><div>Thank you,</div><div>Jeehoon</div></div><div class="gmail_extra"><br><div class="gmail_quote">2017-03-20 14:44 GMT+09:00 Jeehoon Kang <span dir="ltr"><<a href="mailto:jeehoon.kang@sf.snu.ac.kr" target="_blank">jeehoon.kang@sf.snu.ac.kr</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">I am on Fedora 25.  `aspcud` is not installed, and it seems Fedora 25's package manager doesn't have aspcud :\<div><br></div><div>Do you think the lack of `aspcud` is the cause of the build problem?  Then I will try to install it :)</div><div><br></div><div>Thank you,</div><div>Jeehoon</div></div><div class="gmail_extra"><div><div class="h5"><br><div class="gmail_quote">2017-03-17 17:58 GMT+09:00 Ralf Jung <span dir="ltr"><<a href="mailto:jung@mpi-sws.org" target="_blank">jung@mpi-sws.org</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Jehoon,<br>
<span><br>
> I am installing Iris in my laptop, but it fails with a strange error..<br>
> Is anybody aware of this build problem?<br>
><br>
> Thank you,<br>
> Jeehoon<br>
><br>
> PS. I'm experiencing the same problem for the sra-gps project.<br>
><br>
> ```<br>
> $ ~/Works/iris-coq   master  opam --version<br>
> 1.2.2<br>
<br>
</span>That's the same version as what I have.<br>
Which distribution do you use?  Could you please make sure you have<br>
aspcud installed?  That's a constraint solver that opam will use when<br>
available, and it's way better than the fallback it uses otherwise.<br>
<br>
Kind regards,<br>
Ralf<br>
<div><div class="m_7115917203381427210h5"><br>
><br>
> $ ~/Works/iris-coq   master  make build-dep<br>
><br>
> build/opam-pins.sh < opam.pins<br>
> [opam-pins] Recursing into<br>
> <a href="https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp" rel="noreferrer" target="_blank">https://gitlab.mpi-sws.org/rob<wbr>bertkrebbers/coq-stdpp</a><br>
> [opam-pins] coq-stdpp already at commit<br>
> 6ffa20c8f23797f81f1bb55ab27432<wbr>e897de71d5<br>
> opam upgrade  # it is not nice that we upgrade *all* packages here, but<br>
> I found no nice way to upgrade only those that we pinned<br>
> Already up-to-date.<br>
> opam pin add opam-builddep-temp "$(pwd)#HEAD" -k git -n -y<br>
> [NOTE] Package opam-builddep-temp is already git-pinned to<br>
> /home/jeehoon.kang/Works/iris-<wbr>coq#HEAD.<br>
>        This will erase any previous custom definition.<br>
> Proceed ? [Y/n] y<br>
><br>
> [opam-builddep-temp] /home/jeehoon.kang/Works/iris-<wbr>coq#HEAD updated<br>
> [opam-builddep-temp] Installing new package description from<br>
> /home/jeehoon.kang/Works/iris-<wbr>coq#HEAD<br>
><br>
> opam install opam-builddep-temp --deps-only<br>
><br>
> =-=- Synchronising pinned packages<br>
> =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-<wbr>=-=-=-=-=-=-=-=<br>
> [opam-builddep-temp] /home/jeehoon.kang/Works/iris-<wbr>coq#HEAD already<br>
> up-to-date<br>
> Your request can't be satisfied:<br>
>   - opam-builddep-temp is not available because the package is pinned to<br>
> /home/jeehoon.kang/Works/iris-<wbr>coq#HEAD, version dev.<br>
><br>
> No solution found, exiting<br>
> Makefile:25: recipe for target 'build-dep' failed<br>
> make: *** [build-dep] Error 3<br>
> ```<br>
><br>
><br>
> --<br>
</div></div>> Jeehoon Kang (Ph.D. student) <<a href="http://sf.snu.ac.kr/jeehoon.kang" rel="noreferrer" target="_blank">http://sf.snu.ac.kr/jeehoon.k<wbr>ang</a>><br>
> Software Foundations Laboratory <<a href="http://sf.snu.ac.kr" rel="noreferrer" target="_blank">http://sf.snu.ac.kr</a>><br>
> Seoul National University <<a href="http://www.snu.ac.kr" rel="noreferrer" target="_blank">http://www.snu.ac.kr</a>><br>
><br>
><br>
<span class="m_7115917203381427210HOEnZb"><font color="#888888"><br>
--<br>
<a href="mailto:iris-club@lists.mpi-sws.org" target="_blank">iris-club@lists.mpi-sws.org</a> - Mailing List for the Iris Logic<br>
Management: <a href="https://lists.mpi-sws.org/listinfo/iris-club" rel="noreferrer" target="_blank">https://lists.mpi-sws.org/list<wbr>info/iris-club</a><br>
Unsubscribe: <a href="mailto:iris-club-unsubscribe@lists.mpi-sws.org" target="_blank">iris-club-unsubscribe@lists.mp<wbr>i-sws.org</a><br>
</font></span></blockquote></div><br><br clear="all"><div><br></div>-- <br></div></div><div class="m_7115917203381427210gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><a href="http://sf.snu.ac.kr/jeehoon.kang" target="_blank">Jeehoon Kang (Ph.D. student)</a><span class=""><div><a href="http://sf.snu.ac.kr" target="_blank">Software Foundations Laboratory</a><div><a href="http://www.snu.ac.kr" target="_blank">Seoul National University</a></div></div></span></div></div>
</div>
</blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><a href="http://sf.snu.ac.kr/jeehoon.kang" target="_blank">Jeehoon Kang (Ph.D. student)</a><div><a href="http://sf.snu.ac.kr" target="_blank">Software Foundations Laboratory</a><div><a href="http://www.snu.ac.kr" target="_blank">Seoul National University</a></div></div></div></div>
</div>