{"action":"created","issue":{"url":"https://api.github.com/repos/mattam82/Coq-Equations/issues/68","repository_url":"https://api.github.com/repos/mattam82/Coq-Equations","labels_url":"https://api.github.com/repos/mattam82/Coq-Equations/issues/68/labels{/name}","comments_url":"https://api.github.com/repos/mattam82/Coq-Equations/issues/68/comments","events_url":"https://api.github.com/repos/mattam82/Coq-Equations/issues/68/events","html_url":"https://github.com/mattam82/Coq-Equations/issues/68","id":313250961,"number":68,"title":"Problem with coq-equations installation","user":{"login":"paola-giannini","id":32738201,"avatar_url":"https://avatars1.githubusercontent.com/u/32738201?v=4","gravatar_id":"","url":"https://api.github.com/users/paola-giannini","html_url":"https://github.com/paola-giannini","followers_url":"https://api.github.com/users/paola-giannini/followers","following_url":"https://api.github.com/users/paola-giannini/following{/other_user}","gists_url":"https://api.github.com/users/paola-giannini/gists{/gist_id}","starred_url":"https://api.github.com/users/paola-giannini/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/paola-giannini/subscriptions","organizations_url":"https://api.github.com/users/paola-giannini/orgs","repos_url":"https://api.github.com/users/paola-giannini/repos","events_url":"https://api.github.com/users/paola-giannini/events{/privacy}","received_events_url":"https://api.github.com/users/paola-giannini/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2018-04-11T09:49:55Z","updated_at":"2018-04-11T12:57:16Z","closed_at":null,"author_association":"NONE","body":"I have very little knowledge about how to install packages, so I just followed the directions on how to install coq-equation on my mac (I have High Sierra), and I got the following problem:\r\n\r\nbash-3.2$ opam install coq-equations.1.0+8.7\r\nThe following actions will be performed:\r\n  ∗  install camlp5        7.05               [required by coq]\r\n  ∗  install conf-m4       1                  [required by ocamlfind]\r\n  ∗  install ocamlfind     1.7.3-1            [required by coq]\r\n  ∗  install num           1.1                [required by coq]\r\n  ∗  install coq           8.7.2              [required by coq-equations]\r\n  ∗  install coq-equations 1.0+8.7\r\n===== ∗  6 =====\r\nDo you want to continue ? [Y/n] Y\r\n\r\n=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 \r\n[coq-released] https://coq.inria.fr/opam/released/archives/coq-equations.1.0+8.7+opam.tar.gz downloaded\r\n[default] https://opam.ocaml.org/archives/num.1.1+opam.tar.gz downloaded\r\n[default] https://opam.ocaml.org/archives/camlp5.7.05+opam.tar.gz downloaded\r\n[default] https://opam.ocaml.org/archives/ocamlfind.1.7.3-1+opam.tar.gz downloaded\r\n[default] https://opam.ocaml.org/archives/coq.8.7.2+opam.tar.gz downloaded\r\n\r\n=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 \r\n∗  installed camlp5.7.05\r\n∗  installed conf-m4.1\r\n∗  installed ocamlfind.1.7.3-1\r\n∗  installed num.1.1\r\n∗  installed coq.8.7.2\r\n[ERROR] The compilation of coq-equations failed at \"make -j1\".\r\nProcessing  6/6: [coq-equations: rm]\r\n#=== ERROR while installing coq-equations.1.0+8.7 =============================#\r\n# opam-version 1.2.2\r\n# os           darwin\r\n# command      make -j1\r\n# path         /Users/giannini/.opam/4.06.1/build/coq-equations.1.0+8.7\r\n# compiler     4.06.1\r\n# exit-code    2\r\n# env-file     /Users/giannini/.opam/4.06.1/build/coq-equations.1.0+8.7/coq-equations-88650-5788a7.env\r\n# stdout-file  /Users/giannini/.opam/4.06.1/build/coq-equations.1.0+8.7/coq-equations-88650-5788a7.out\r\n# stderr-file  /Users/giannini/.opam/4.06.1/build/coq-equations.1.0+8.7/coq-equations-88650-5788a7.err\r\n### stdout ###\r\n# [...]\r\n# CAMLDEP src/principles_proofs.ml\r\n# CAMLDEP src/splitting.ml\r\n# CAMLDEP src/covering.ml\r\n# CAMLDEP src/syntax.ml\r\n# CAMLDEP src/depelim.ml\r\n# CAMLDEP src/eqdec.ml\r\n# CAMLDEP src/subterm.ml\r\n# CAMLDEP src/sigma_types.ml\r\n# CAMLDEP src/derive.ml\r\n# CAMLDEP src/equations_common.ml\r\n### stderr ###\r\n# [...]\r\n# /bin/sh: /opt/local/bin/ocamlfind: No such file or directory\r\n# /bin/sh: /opt/local/bin/ocamlfind: No such file or directory\r\n# /bin/sh: /opt/local/bin/ocamlfind: No such file or directory\r\n# /bin/sh: /opt/local/bin/ocamlfind: No such file or directory\r\n# /bin/sh: /opt/local/bin/ocamlfind: No such file or directory\r\n# /bin/sh: /opt/local/bin/ocamlfind: No such file or directory\r\n# /bin/sh: /opt/local/bin/ocamlfind: No such file or directory\r\n# /bin/sh: /opt/local/bin/ocamlfind: No such file or directory\r\n# /bin/sh: /opt/local/bin/ocamlfind: No such file or directory\r\n# Makefile:703: *** \"Cannot find the 'ocamlfind' binary used to build Coq (/opt/local/bin/ocamlfind). Pre-compiled binary packages of Coq do not support compiling plugins this way. Please download the sources of Coq and run the Windows build script.\".  Stop.\r\n\r\n\r\n\r\n=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫 \r\nThe following actions failed\r\n  ∗  install coq-equations 1.0+8.7\r\nThe following changes have been performed\r\n  ∗  install camlp5    7.05   \r\n  ∗  install conf-m4   1      \r\n  ∗  install coq       8.7.2  \r\n  ∗  install num       1.1    \r\n  ∗  install ocamlfind 1.7.3-1\r\n\r\nThe former state can be restored with:\r\n    opam switch import \"~/.opam/4.06.1/backup/state-20180311085727.export\"\r\nbash-3.2$ \r\n\r\ncan you tell me what to do?         Paola\r\n"},"comment":{"url":"https://api.github.com/repos/mattam82/Coq-Equations/issues/comments/380442105","html_url":"https://github.com/mattam82/Coq-Equations/issues/68#issuecomment-380442105","issue_url":"https://api.github.com/repos/mattam82/Coq-Equations/issues/68","id":380442105,"user":{"login":"mattam82","id":98373,"avatar_url":"https://avatars1.githubusercontent.com/u/98373?v=4","gravatar_id":"","url":"https://api.github.com/users/mattam82","html_url":"https://github.com/mattam82","followers_url":"https://api.github.com/users/mattam82/followers","following_url":"https://api.github.com/users/mattam82/following{/other_user}","gists_url":"https://api.github.com/users/mattam82/gists{/gist_id}","starred_url":"https://api.github.com/users/mattam82/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mattam82/subscriptions","organizations_url":"https://api.github.com/users/mattam82/orgs","repos_url":"https://api.github.com/users/mattam82/repos","events_url":"https://api.github.com/users/mattam82/events{/privacy}","received_events_url":"https://api.github.com/users/mattam82/received_events","type":"User","site_admin":false},"created_at":"2018-04-11T12:57:16Z","updated_at":"2018-04-11T12:57:16Z","author_association":"OWNER","body":"That's strange. What does \r\n``# which ocamlfind``\r\ngive you now? What about\r\n``# eval `opam config env` ``\r\n``# which ocamlfind``\r\n\r\nIf the path changes then maybe trying again \r\n``# opam install coq-equations.1.0+8.7``\r\nwill succeed.\r\n\r\nI'm trying to reproduce a fresh installation of the same set of packages on my computer to see."}}
{"actor":{"display_login":"mattam82"}}