{"action":"created","issue":{"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/236","labels_url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/236/labels{/name}","comments_url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/236/comments","events_url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/236/events","html_url":"https://github.com/HOL-Theorem-Prover/HOL/pull/236","id":57882453,"number":236,"title":"HolyHammer","user":{"login":"barakeel","id":4567783,"avatar_url":"https://avatars.githubusercontent.com/u/4567783?v=3","gravatar_id":"","url":"https://api.github.com/users/barakeel","html_url":"https://github.com/barakeel","followers_url":"https://api.github.com/users/barakeel/followers","following_url":"https://api.github.com/users/barakeel/following{/other_user}","gists_url":"https://api.github.com/users/barakeel/gists{/gist_id}","starred_url":"https://api.github.com/users/barakeel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/barakeel/subscriptions","organizations_url":"https://api.github.com/users/barakeel/orgs","repos_url":"https://api.github.com/users/barakeel/repos","events_url":"https://api.github.com/users/barakeel/events{/privacy}","received_events_url":"https://api.github.com/users/barakeel/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":15,"created_at":"2015-02-17T04:33:43Z","updated_at":"2015-03-13T20:25:49Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/pulls/236","html_url":"https://github.com/HOL-Theorem-Prover/HOL/pull/236","diff_url":"https://github.com/HOL-Theorem-Prover/HOL/pull/236.diff","patch_url":"https://github.com/HOL-Theorem-Prover/HOL/pull/236.patch"},"body":"Need to run make in src/holyhammer to create holyhammer executables. \r\nIt should not be included directly in the HOL4 build as it requires ocaml \r\nand a recent version of g++ installed."},"comment":{"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/comments/79348414","html_url":"https://github.com/HOL-Theorem-Prover/HOL/pull/236#issuecomment-79348414","issue_url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/236","id":79348414,"user":{"login":"konrad-slind","id":1105935,"avatar_url":"https://avatars.githubusercontent.com/u/1105935?v=3","gravatar_id":"","url":"https://api.github.com/users/konrad-slind","html_url":"https://github.com/konrad-slind","followers_url":"https://api.github.com/users/konrad-slind/followers","following_url":"https://api.github.com/users/konrad-slind/following{/other_user}","gists_url":"https://api.github.com/users/konrad-slind/gists{/gist_id}","starred_url":"https://api.github.com/users/konrad-slind/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/konrad-slind/subscriptions","organizations_url":"https://api.github.com/users/konrad-slind/orgs","repos_url":"https://api.github.com/users/konrad-slind/repos","events_url":"https://api.github.com/users/konrad-slind/events{/privacy}","received_events_url":"https://api.github.com/users/konrad-slind/received_events","type":"User","site_admin":false},"created_at":"2015-03-13T20:25:49Z","updated_at":"2015-03-13T20:25:49Z","body":"OK, I see. One of the goals of the tagging system was to allow such\nextralogical work (and data) to get passed along and altered as inference\nproceeds.\n\n  I was never very happy with the tag system since it is too inflexible.\nHaving to modify the kernel for such things as OpenTheory and HolyHammer\nshows that.\n\nI would favour a solution that could apply to all these kinds of primitive\ninference\nadd-ons. Probably having a universal datatype for tags would work, although\nthere\nis a requirement that tags need to be writable/readable from disk.\n\nKonrad.\n\n\nOn Fri, Mar 13, 2015 at 2:06 PM, Ramana Kumar <notifications@github.com>\nwrote:\n\n> The kernel alterations are for the \"recording dependencies\" that barakeel\n> mentioned. HolyHammer adds extra metadata (like the current tags) to\n> theorems to record what theorems they depend on.\n>\n> —\n> Reply to this email directly or view it on GitHub\n> <https://github.com/HOL-Theorem-Prover/HOL/pull/236#issuecomment-79260589>\n> .\n>\n"}}