{"action":"created","issue":{"url":"https://api.github.com/repos/seL4/l4v/issues/12","repository_url":"https://api.github.com/repos/seL4/l4v","labels_url":"https://api.github.com/repos/seL4/l4v/issues/12/labels{/name}","comments_url":"https://api.github.com/repos/seL4/l4v/issues/12/comments","events_url":"https://api.github.com/repos/seL4/l4v/issues/12/events","html_url":"https://github.com/seL4/l4v/issues/12","id":169838805,"number":12,"title":"errors happen using proof  count","user":{"login":"ywzh","id":12252485,"avatar_url":"https://avatars.githubusercontent.com/u/12252485?v=3","gravatar_id":"","url":"https://api.github.com/users/ywzh","html_url":"https://github.com/ywzh","followers_url":"https://api.github.com/users/ywzh/followers","following_url":"https://api.github.com/users/ywzh/following{/other_user}","gists_url":"https://api.github.com/users/ywzh/gists{/gist_id}","starred_url":"https://api.github.com/users/ywzh/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ywzh/subscriptions","organizations_url":"https://api.github.com/users/ywzh/orgs","repos_url":"https://api.github.com/users/ywzh/repos","events_url":"https://api.github.com/users/ywzh/events{/privacy}","received_events_url":"https://api.github.com/users/ywzh/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2016-08-08T03:53:52Z","updated_at":"2016-08-08T07:58:22Z","closed_at":null,"body":"Hi, I am using proofcount with Isabelle 2016 in Ubuntu. Some errors occur as follows.\r\n\r\nCould you help to correct them? thanks.\r\n\r\n-------------------------------------------------------------------\r\nzhaoyw@zhaoyw-VirtualBox:~/research$ isabelle proofcount -x xkernel.xml -d xkernel -L XKernel -T SK_L2Spec\r\nStarting ProofCount...\r\nMaking new metric file at /home/zhaoyw/research/xkernel.xml. Running Isabelle...\r\nBuilding XKernel ...\r\nDocument at /home/zhaoyw/research/xkernel/output/document.pdf\r\nFinished XKernel (0:05:53 elapsed time, 0:06:38 cpu time, factor 1.12)\r\nRunning ProofCount_Exec ...\r\n\r\nProofCount_Exec FAILED\r\n(see also /home/zhaoyw/.isabelle/Isabelle2016/heaps/polyml-5.6_x86_64-linux/log/ProofCount_Exec)\r\n\r\n*** ML error (line 86 of \"~/software/proofcount/proof_count.ML\"):\r\n*** Type error in function application.\r\n***    Function: wrap_lthy' :\r\n***       Keyword.keywords ->\r\n***         (Token.T list -> ('a -> Proof.context -> Proof.context) * 'b) ->\r\n***           Token.T list -> ('a -> Proof.context -> Proof.context) * 'b\r\n***    Argument: \"lemmas\" : string\r\n***    Reason:\r\n***       Can't unify Keyword.keywords with string (*In Basis*)\r\n***          (Different type constructors)\r\n*** ML error (line 86 of \"~/software/proofcount/proof_count.ML\"):\r\n*** Value or constructor (lemmaK) has not been declared in structure Thm\r\n*** ML error (line 188 of \"~/software/proofcount/proof_count.ML\"):\r\n*** Type error in function application.\r\n***    Function: add_new_lemmas thy thy' pos pos : Keyword.keywords -> unit\r\n***    Argument: name : string\r\n***    Reason:\r\n***       Can't unify Keyword.keywords with string (*In Basis*)\r\n***          (Different type constructors)\r\n*** At command \"ML_file\" (line 15 of \"~/software/proofcount/ProofCount.thy\")\r\nUnfinished session(s): ProofCount_Exec\r\n0:06:34 elapsed time, 0:06:58 cpu time, factor 1.06\r\nisabelle processing proofcount failed\r\n"},"comment":{"url":"https://api.github.com/repos/seL4/l4v/issues/comments/238166625","html_url":"https://github.com/seL4/l4v/issues/12#issuecomment-238166625","issue_url":"https://api.github.com/repos/seL4/l4v/issues/12","id":238166625,"user":{"login":"lsf37","id":5506585,"avatar_url":"https://avatars.githubusercontent.com/u/5506585?v=3","gravatar_id":"","url":"https://api.github.com/users/lsf37","html_url":"https://github.com/lsf37","followers_url":"https://api.github.com/users/lsf37/followers","following_url":"https://api.github.com/users/lsf37/following{/other_user}","gists_url":"https://api.github.com/users/lsf37/gists{/gist_id}","starred_url":"https://api.github.com/users/lsf37/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/lsf37/subscriptions","organizations_url":"https://api.github.com/users/lsf37/orgs","repos_url":"https://api.github.com/users/lsf37/repos","events_url":"https://api.github.com/users/lsf37/events{/privacy}","received_events_url":"https://api.github.com/users/lsf37/received_events","type":"User","site_admin":false},"created_at":"2016-08-08T07:58:22Z","updated_at":"2016-08-08T07:58:22Z","body":"Proofcount is indeed currently broken for Isabelle2016 and its maintainer is on long-term leave on an internship, so it'll be a few months until we can fix this, sorry."}}
{"actor":{"display_login":"lsf37"}}