{"action":"created","issue":{"url":"https://api.github.com/repos/Karmaki/coq-dpdgraph/issues/1","labels_url":"https://api.github.com/repos/Karmaki/coq-dpdgraph/issues/1/labels{/name}","comments_url":"https://api.github.com/repos/Karmaki/coq-dpdgraph/issues/1/comments","events_url":"https://api.github.com/repos/Karmaki/coq-dpdgraph/issues/1/events","html_url":"https://github.com/Karmaki/coq-dpdgraph/pull/1","id":108653312,"number":1,"title":"Introduce a configure file + compute also dependencies that come from the type","user":{"login":"ybertot","id":3407333,"avatar_url":"https://avatars.githubusercontent.com/u/3407333?v=3","gravatar_id":"","url":"https://api.github.com/users/ybertot","html_url":"https://github.com/ybertot","followers_url":"https://api.github.com/users/ybertot/followers","following_url":"https://api.github.com/users/ybertot/following{/other_user}","gists_url":"https://api.github.com/users/ybertot/gists{/gist_id}","starred_url":"https://api.github.com/users/ybertot/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ybertot/subscriptions","organizations_url":"https://api.github.com/users/ybertot/orgs","repos_url":"https://api.github.com/users/ybertot/repos","events_url":"https://api.github.com/users/ybertot/events{/privacy}","received_events_url":"https://api.github.com/users/ybertot/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-09-28T13:00:42Z","updated_at":"2015-09-28T14:54:23Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/Karmaki/coq-dpdgraph/pulls/1","html_url":"https://github.com/Karmaki/coq-dpdgraph/pull/1","diff_url":"https://github.com/Karmaki/coq-dpdgraph/pull/1.diff","patch_url":"https://github.com/Karmaki/coq-dpdgraph/pull/1.patch"},"body":"Il y a encore un petit problème avec le calcul de dépendance des fichiers ml4, qui n'est pas bien fait.\r\n\r\nSinon, la modification dans searchdepend.ml4 doit permettre d'assurer que le type des constantes est aussi utilisé pour calculer les dépendances, même pour des axiomes.\r\n\r\n"},"comment":{"url":"https://api.github.com/repos/Karmaki/coq-dpdgraph/issues/comments/143766332","html_url":"https://github.com/Karmaki/coq-dpdgraph/pull/1#issuecomment-143766332","issue_url":"https://api.github.com/repos/Karmaki/coq-dpdgraph/issues/1","id":143766332,"user":{"login":"ybertot","id":3407333,"avatar_url":"https://avatars.githubusercontent.com/u/3407333?v=3","gravatar_id":"","url":"https://api.github.com/users/ybertot","html_url":"https://github.com/ybertot","followers_url":"https://api.github.com/users/ybertot/followers","following_url":"https://api.github.com/users/ybertot/following{/other_user}","gists_url":"https://api.github.com/users/ybertot/gists{/gist_id}","starred_url":"https://api.github.com/users/ybertot/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ybertot/subscriptions","organizations_url":"https://api.github.com/users/ybertot/orgs","repos_url":"https://api.github.com/users/ybertot/repos","events_url":"https://api.github.com/users/ybertot/events{/privacy}","received_events_url":"https://api.github.com/users/ybertot/received_events","type":"User","site_admin":false},"created_at":"2015-09-28T14:54:23Z","updated_at":"2015-09-28T14:54:23Z","body":"No, ocamlfind is not used here.  To use ocamlfind, I would need to add a check for its presence in the configure file, which was not the case yet.  I expected ocamlgraph to be installed inside the ocaml library.  You example shows that opam installs it on the side.\r\n\r\nThe wrong lines in configure.in are lines 159-162:\r\n\r\nAC_CHECK_FILE($OCAMLLIB/ocamlgraph/graph.cmxa,\r\n  OCAMLGRAPH=yes,\r\n  OCAMLGRAPH=no)\r\n\r\ninstead of calling ocamlfind.  But I have yet to understand what ocamlfind does, really.\r\n\r\n"}}