{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/407","labels_url":"https://api.github.com/repos/leanprover/lean/issues/407/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/407/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/407/events","html_url":"https://github.com/leanprover/lean/issues/407","id":55305107,"number":407,"title":"make install does not configure emacs","user":{"login":"EgbertRijke","id":1252282,"avatar_url":"https://avatars.githubusercontent.com/u/1252282?v=3","gravatar_id":"","url":"https://api.github.com/users/EgbertRijke","html_url":"https://github.com/EgbertRijke","followers_url":"https://api.github.com/users/EgbertRijke/followers","following_url":"https://api.github.com/users/EgbertRijke/following{/other_user}","gists_url":"https://api.github.com/users/EgbertRijke/gists{/gist_id}","starred_url":"https://api.github.com/users/EgbertRijke/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/EgbertRijke/subscriptions","organizations_url":"https://api.github.com/users/EgbertRijke/orgs","repos_url":"https://api.github.com/users/EgbertRijke/repos","events_url":"https://api.github.com/users/EgbertRijke/events{/privacy}","received_events_url":"https://api.github.com/users/EgbertRijke/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/leanprover/lean/labels/emacs","name":"emacs","color":"eb6420"}],"state":"open","locked":false,"assignee":{"login":"soonhokong","id":403281,"avatar_url":"https://avatars.githubusercontent.com/u/403281?v=3","gravatar_id":"","url":"https://api.github.com/users/soonhokong","html_url":"https://github.com/soonhokong","followers_url":"https://api.github.com/users/soonhokong/followers","following_url":"https://api.github.com/users/soonhokong/following{/other_user}","gists_url":"https://api.github.com/users/soonhokong/gists{/gist_id}","starred_url":"https://api.github.com/users/soonhokong/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/soonhokong/subscriptions","organizations_url":"https://api.github.com/users/soonhokong/orgs","repos_url":"https://api.github.com/users/soonhokong/repos","events_url":"https://api.github.com/users/soonhokong/events{/privacy}","received_events_url":"https://api.github.com/users/soonhokong/received_events","type":"User","site_admin":false},"milestone":null,"comments":3,"created_at":"2015-01-23T16:58:13Z","updated_at":"2015-01-23T18:47:11Z","closed_at":null,"body":"emacs mode doesn't load after following the installation instructions. I'm on a ubuntu 14.10 machine."},"comment":{"url":"https://api.github.com/repos/leanprover/lean/issues/comments/71243126","html_url":"https://github.com/leanprover/lean/issues/407#issuecomment-71243126","issue_url":"https://api.github.com/repos/leanprover/lean/issues/407","id":71243126,"user":{"login":"soonhokong","id":403281,"avatar_url":"https://avatars.githubusercontent.com/u/403281?v=3","gravatar_id":"","url":"https://api.github.com/users/soonhokong","html_url":"https://github.com/soonhokong","followers_url":"https://api.github.com/users/soonhokong/followers","following_url":"https://api.github.com/users/soonhokong/following{/other_user}","gists_url":"https://api.github.com/users/soonhokong/gists{/gist_id}","starred_url":"https://api.github.com/users/soonhokong/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/soonhokong/subscriptions","organizations_url":"https://api.github.com/users/soonhokong/orgs","repos_url":"https://api.github.com/users/soonhokong/repos","events_url":"https://api.github.com/users/soonhokong/events{/privacy}","received_events_url":"https://api.github.com/users/soonhokong/received_events","type":"User","site_admin":false},"created_at":"2015-01-23T18:47:11Z","updated_at":"2015-01-23T18:47:11Z","body":"I guess you're attending Prof. @avigad's lecture today. If so, I am happy to help you set things up before/after the class. Please find me in the class room if that's the case.\r\n\r\nThat being said, I want to take this as an opportunity to make things better. First of all, it's not really easy to fully automate the emacs setup process because it's required to modify user's emacs configuration.\r\n\r\nFor now, we have two issues which makes things complicated:\r\n\r\n 1. lean-mode depends on other emacs packages such as comply, flycheck, etc\r\n 2. lean-mode requires the location of lean binaries such as `lean`, `linja`, and `leantags`.\r\n\r\nI think the best solution is to upload lean-mode to the [melpa](http://melpa.org) so that users can install it via `package-install`. This is nice in a sense that we can specify its dependencies and `package-install` will install all the required packages for lean-mode.\r\n\r\nFor the second issue, I think we can first assume that those binaries (`lean`, `linja`, `leantags`) are in the system's path. As an option, we can provide a customization variable to specify the location of them.\r\n\r\n@leodemoura, what do you think? Of course, another option is to package all the required packages in lean-mode to make it self-contained. However, I'm not sure that this is an elegant solution (should be easier than melpa one for users though)"}}