{"action":"created","issue":{"url":"https://api.github.com/repos/ProofGeneral/PG/issues/96","repository_url":"https://api.github.com/repos/ProofGeneral/PG","labels_url":"https://api.github.com/repos/ProofGeneral/PG/issues/96/labels{/name}","comments_url":"https://api.github.com/repos/ProofGeneral/PG/issues/96/comments","events_url":"https://api.github.com/repos/ProofGeneral/PG/issues/96/events","html_url":"https://github.com/ProofGeneral/PG/issues/96","id":168664971,"number":96,"title":"PG doesn't grok Coq's Add LoadPath","user":{"login":"jonleivent","id":7363878,"avatar_url":"https://avatars.githubusercontent.com/u/7363878?v=3","gravatar_id":"","url":"https://api.github.com/users/jonleivent","html_url":"https://github.com/jonleivent","followers_url":"https://api.github.com/users/jonleivent/followers","following_url":"https://api.github.com/users/jonleivent/following{/other_user}","gists_url":"https://api.github.com/users/jonleivent/gists{/gist_id}","starred_url":"https://api.github.com/users/jonleivent/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jonleivent/subscriptions","organizations_url":"https://api.github.com/users/jonleivent/orgs","repos_url":"https://api.github.com/users/jonleivent/repos","events_url":"https://api.github.com/users/jonleivent/events{/privacy}","received_events_url":"https://api.github.com/users/jonleivent/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":19,"created_at":"2016-08-01T14:51:31Z","updated_at":"2016-09-17T12:53:03Z","closed_at":null,"body":"I like the way PG is able to get info from _CoqProject.  But, in those cases where one is just experimenting with a script that isn't yet itself part of a project, it would be nice if PG didn't go bonkers when the script did an Add LoadPath,  Right now, if the current dir has no _CoqProject, and a script in that dir tries to do Add LoadPath to access an existing project (which works when the script is run in CoqIDE, by the way), not only does it fail, but PG pretty much becomes useless after that point - requiring one to kill Emacs and restart.\r\n \r\nThis is Emacs 24.4.1, Coq 8.5pl2, very recent PG build (462e3ef).\r\n"},"comment":{"url":"https://api.github.com/repos/ProofGeneral/PG/issues/comments/247767838","html_url":"https://github.com/ProofGeneral/PG/issues/96#issuecomment-247767838","issue_url":"https://api.github.com/repos/ProofGeneral/PG/issues/96","id":247767838,"user":{"login":"erikmd","id":10367254,"avatar_url":"https://avatars.githubusercontent.com/u/10367254?v=3","gravatar_id":"","url":"https://api.github.com/users/erikmd","html_url":"https://github.com/erikmd","followers_url":"https://api.github.com/users/erikmd/followers","following_url":"https://api.github.com/users/erikmd/following{/other_user}","gists_url":"https://api.github.com/users/erikmd/gists{/gist_id}","starred_url":"https://api.github.com/users/erikmd/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/erikmd/subscriptions","organizations_url":"https://api.github.com/users/erikmd/orgs","repos_url":"https://api.github.com/users/erikmd/repos","events_url":"https://api.github.com/users/erikmd/events{/privacy}","received_events_url":"https://api.github.com/users/erikmd/received_events","type":"User","site_admin":false},"created_at":"2016-09-17T12:53:03Z","updated_at":"2016-09-17T12:53:03Z","body":"Hi Jonathan,\n\nLe vendredi 16 septembre 2016 à 17:21 -0700, Jonathan Leivent a écrit :\n> When you say \"make install or so beforehand\", what are you\n> suggesting about their install paths, and how does the client code\n> pick up on those paths?\n> In my case, both client and library were being developed\n> simultaneously.\n\nIn my comment I was thinking of relying on the default install path\ngenerated by coq_makefile, namely:\n> COQLIBINSTALL=\"${COQLIB}user-contrib\"\n\nThe advantage of using this install path is that all \"client\" projects\nwill be able to use the libraries installed there without specifying\nany -R/-Q arguments for binding *absolute* paths to logical names.\n\nIn the use case you mention (concurrent development of two libraries),\nI think there are two possible cases:\n\nCase A: both libraries are hosted in the same repository, say in two\nsubfolders \"lib\" and \"client\", and \"client\" depends on \"lib\".\n\nIn this case we can just use a single _CoqProject file containing e.g.\n> -R lib FooLib\n> -R client FooClient\n> lib/lib.v\n> client/client.v\n\nso \"coq_makefile -f _CoqProject -o Makefile && make && make install\"\nwill compile everything and put the two libraries in\n$COQLIB/user-contrib/FooLib/ and $COQLIB/user-contrib/FooClient/\n\nCase B: the two libraries are hosted in different projects, each of\nthem containing a _CoqProject (and a Makefile generated similarly)\n\nIn this case I would follow the following workflow:\n\"cd .../lib && make && make install && cd .../client && make\"\n\nDoes this answer your question?\n\nKind regards,\nErik\n"}}
{"actor":{"display_login":"erikmd"}}