{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/862","labels_url":"https://api.github.com/repos/leanprover/lean/issues/862/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/862/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/862/events","html_url":"https://github.com/leanprover/lean/issues/862","id":114933655,"number":862,"title":"unknown annotation kind 'notation_info' from lean.js (emscripten build)","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},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":16,"created_at":"2015-11-03T23:23:02Z","updated_at":"2015-11-04T18:21:25Z","closed_at":"2015-11-04T17:06:05Z","body":"Dear @leodemoura,\r\n\r\nI was updating Lean.js and found this problem. An minimal example is the following line:\r\n\r\n```lean\r\nimport data.set\r\n```\r\n\r\nand it generates the message \"unknown annotation kind 'notation_info'\". Do you have any clue where it comes from? I tried to reproduce the problem without using emscripten (i.e. `DMULTI_THREAD=OFF`) but couldn't find a way.\r\n\r\nBTW, I had another problem building the latest version of it and had to make a patch: https://github.com/soonhokong/lean/commit/a25b43f1e80fecaf8d00f08e75926d6fc13de0d0\r\n\r\n"},"comment":{"url":"https://api.github.com/repos/leanprover/lean/issues/comments/153817983","html_url":"https://github.com/leanprover/lean/issues/862#issuecomment-153817983","issue_url":"https://api.github.com/repos/leanprover/lean/issues/862","id":153817983,"user":{"login":"avigad","id":2783534,"avatar_url":"https://avatars.githubusercontent.com/u/2783534?v=3","gravatar_id":"","url":"https://api.github.com/users/avigad","html_url":"https://github.com/avigad","followers_url":"https://api.github.com/users/avigad/followers","following_url":"https://api.github.com/users/avigad/following{/other_user}","gists_url":"https://api.github.com/users/avigad/gists{/gist_id}","starred_url":"https://api.github.com/users/avigad/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/avigad/subscriptions","organizations_url":"https://api.github.com/users/avigad/orgs","repos_url":"https://api.github.com/users/avigad/repos","events_url":"https://api.github.com/users/avigad/events{/privacy}","received_events_url":"https://api.github.com/users/avigad/received_events","type":"User","site_admin":false},"created_at":"2015-11-04T18:21:25Z","updated_at":"2015-11-04T18:21:25Z","body":"@soonhokong Thanks for catching these errors; they are fixed now. Thanks even more for getting the online version of Lean working again."}}