coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Tadeusz Litak <tadeusz.litak AT gmail.com>
- To: coqdev AT inria.fr, coq-club AT inria.fr
- Subject: [Coq-Club] Coq-HOTT via OPAM
- Date: Sat, 13 May 2017 13:18:30 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tadeusz.litak AT gmail.com; spf=Pass smtp.mailfrom=tadeusz.litak AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f48.google.com
- Ironport-phdr: 9a23:nEDO0BQujWRPs847QsP+eQ0Bk9psv+yvbD5Q0YIujvd0So/mwa6ybRKN2/xhgRfzUJnB7Loc0qyN4vymATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSijewZbx/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/n/XhMJtj6xVrhyuqBNjzIDbe4yVKPlzc7nBcd8GS2dMXMBcXDFBDIOmaIsPCvIMM/hCoIbguVQOsAC+BAixD+3pyz9ImmX53a4n2OkmDQHJxhEvEMwTsHTPrdT5LqMSUeGpzKbSzjXOdPxW2TLn54jJdhAtu+2DXbV1ccfIz0QkCg3LjlKVqYP/PjOV0PwAs2ea7+p8VeKvlnUopxttrTiow8chjJTCiIENyl3c9yh0z5w5KcCmREN7e9KpE4VcuzuVOoZ1Ws8uXX1ktDo0x7ADupO2fS0HxZUmyhPfaPGKdoiF7g//WOqNJDp0mnFodK+hixu38EWv0fDwWdSx3VtOoCdJjsXDu3UT2xPO9MSHRP1w9Vq71zmVzQDc8ORELFg0laXFL54hxaY9lp8JvkTCGi/6gUv3jKqKekk99Oil5Ofqbq/ppp+bMI90hQX+Pbo0lsOjBuQ4NxACX2md+euiyL3u5U/0TbpQgvErjKXUsIrWKMcFqqKjDAJY0Z4v6xOlADen1NQYk2MHLFVAeB+fk4jmIUzBL+7lDfekglWgijNrx/HaPrL7AZXANXfDkLL7crZ8705Q0hY8zdda555MELEOPOrzWlPttNzfFhI2Lwu0w//+BNph0oMeRHmAD7SCMKLStF+I/vggL/ONZI8Tojb9KuIq6+TgjX8jgVUdZ7Wm3YMLaHCkGfRrO1mWYX31gtgcD2gKoBEzTPfqiV2HST5cfWy+X6M65jEhCYKpF53PRo63gO/J4CDuFZpPam1YIlGKC3bhMYueH78HbzvXKct8mBQFU6KgQskvz0KArgj/noZuIufJ4T9QkZP/3ds9s/HamRwv7i4yC8WB2mKlQGR9n2dOTDgzivMs6Xdhw0uOhPAry8dTEsZesqtE
Dear all,
is $SUBJECT$ an intended or viable installation route? At the moment at least, it is not even possible. Have other users had the same experience as I did?
The following actions will be performed:
∗ install coq-hott 8.6.dev
=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
🐫
[coq-hott] https://github.com/HoTT/HoTT.git#master already up-to-date
=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
🐫
#=== ERROR while installing coq-hott.8.6.dev
==================================#
These patches didn't apply at
/Users/litak/ocamlbrew/ocaml-4.02.3/.opam/system/build/coq-hott.8.6.dev:
- emilio.diff
=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
🐫
The following actions failed
∗ install coq-hott 8.6.dev
No changes have been performed
Best,
t.
- [Coq-Club] Coq-HOTT via OPAM, Tadeusz Litak, 05/13/2017
Archive powered by MHonArc 2.6.18.