{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/835","labels_url":"https://api.github.com/repos/leanprover/lean/issues/835/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/835/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/835/events","html_url":"https://github.com/leanprover/lean/issues/835","id":108486903,"number":835,"title":"Installing Lean on Windows 10","user":{"login":"fpvandoorn","id":7376012,"avatar_url":"https://avatars.githubusercontent.com/u/7376012?v=3","gravatar_id":"","url":"https://api.github.com/users/fpvandoorn","html_url":"https://github.com/fpvandoorn","followers_url":"https://api.github.com/users/fpvandoorn/followers","following_url":"https://api.github.com/users/fpvandoorn/following{/other_user}","gists_url":"https://api.github.com/users/fpvandoorn/gists{/gist_id}","starred_url":"https://api.github.com/users/fpvandoorn/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/fpvandoorn/subscriptions","organizations_url":"https://api.github.com/users/fpvandoorn/orgs","repos_url":"https://api.github.com/users/fpvandoorn/repos","events_url":"https://api.github.com/users/fpvandoorn/events{/privacy}","received_events_url":"https://api.github.com/users/fpvandoorn/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":7,"created_at":"2015-09-26T18:59:51Z","updated_at":"2015-09-30T07:35:50Z","closed_at":null,"body":"I installed Windows 10 on my laptop, and I tried if the installation instructions for Windows 8 worked for me.\r\n\r\nHowever, when I open a Lean file, Emacs freezes after ~10 seconds (even when doing nothing), and Flycheck displays \"FlyC*\". \r\n\r\nEmacs and Python are in my path.\r\n\r\nCan I send more information which could be helpful? The only thing which looked strange is that the `cmd` screen opened when running `leanemacs.bat` displays paths which have `\\/` in them:\r\n\r\n```\r\nD:\\Programs\\Lean\\lean-0.2.0-windows\\bin>SET MY_PATH=D:\\Programs\\Lean\\lean-0.2.0-windows\\bin\\\r\n\r\nD:\\Programs\\Lean\\lean-0.2.0-windows\\bin>SET LEAN_ROOTDIR=D:\\Programs\\Lean\\lean-0.2.0-windows\\bin\\/..\r\n\r\nD:\\Programs\\Lean\\lean-0.2.0-windows\\bin>SET LEAN_EMACS_PATH=D:\\Programs\\Lean\\lean-0.2.0-windows\\bin\\/../share/emacs/site-lisp/lean\r\n\r\nD:\\Programs\\Lean\\lean-0.2.0-windows\\bin>emacs -load D:\\Programs\\Lean\\lean-0.2.0-windows\\bin\\/../share/emacs/site-lisp/lean/load-lean.el\r\n```"},"comment":{"url":"https://api.github.com/repos/leanprover/lean/issues/comments/144314084","html_url":"https://github.com/leanprover/lean/issues/835#issuecomment-144314084","issue_url":"https://api.github.com/repos/leanprover/lean/issues/835","id":144314084,"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-09-30T07:35:49Z","updated_at":"2015-09-30T07:35:49Z","body":"@fpvandoorn, I'm testing it on a Windows7 machine and it works without adding `lean/bin` to `PATH` env variable.\r\n\r\nCould you test the following things on your Windows 10 machine?\r\n\r\n - remove `.../lean/bin` from your `PATH` env variable (to reproduce the problem)\r\n - launch `leanemacs`, open a `.lean` file, make sure that you have the problem.\r\n - press <kbd>C-h v</kbd>`lean-rootdir`. It will show the current value of `lean-rootdir` variable. Please copy/paste it here.\r\n\r\nFYI, it works in the following ways (at least in Windows7):\r\n\r\n - `LEAN_ROOTDIR` is set up in https://github.com/leanprover/lean/blob/master/bin/leanemacs.in#L5\r\n - and it's loaded into emacs at https://github.com/leanprover/lean/blob/master/src/emacs/load-lean.el#L3-L5\r\n\r\nIt's possible that the above is not working in Windows 10 anymore (because of some reasons).\r\n\r\nYou also told me that the effect of `setx` seemed to be temporary (not permanent). I looked up some references but [a link](https://technet.microsoft.com/en-us/library/cc755104.aspx) says that it's effect is permanent. Could you double-check it (it might be difficult)? Note that it seems the effect of `set` is limited to the current session."}}