{"action":"created","issue":{"url":"https://api.github.com/repos/psteckler/ProofGeneral/issues/74","repository_url":"https://api.github.com/repos/psteckler/ProofGeneral","labels_url":"https://api.github.com/repos/psteckler/ProofGeneral/issues/74/labels{/name}","comments_url":"https://api.github.com/repos/psteckler/ProofGeneral/issues/74/comments","events_url":"https://api.github.com/repos/psteckler/ProofGeneral/issues/74/events","html_url":"https://github.com/psteckler/ProofGeneral/issues/74","id":203867637,"number":74,"title":"Cannot enter interactive mode: Symbol's function definition is void: some","user":{"login":"RalfJung","id":330628,"avatar_url":"https://avatars.githubusercontent.com/u/330628?v=3","gravatar_id":"","url":"https://api.github.com/users/RalfJung","html_url":"https://github.com/RalfJung","followers_url":"https://api.github.com/users/RalfJung/followers","following_url":"https://api.github.com/users/RalfJung/following{/other_user}","gists_url":"https://api.github.com/users/RalfJung/gists{/gist_id}","starred_url":"https://api.github.com/users/RalfJung/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/RalfJung/subscriptions","organizations_url":"https://api.github.com/users/RalfJung/orgs","repos_url":"https://api.github.com/users/RalfJung/repos","events_url":"https://api.github.com/users/RalfJung/events{/privacy}","received_events_url":"https://api.github.com/users/RalfJung/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":5,"created_at":"2017-01-29T12:43:50Z","updated_at":"2017-01-30T20:19:00Z","closed_at":null,"body":"Entering interactive mode (C-c C-RET) fails with PG c6704da3bdfce424df33867cf04ae5f45682ec70:\r\n```\r\nunexpected error during parallel compilation: (void-function some)\r\nbyte-code: Symbol's function definition is void: some\r\n```\r\nI tried this with `algebra/ofe.v` and `heap_lang/lib/barrier/proof.v` of Iris (https://gitlab.mpi-sws.org/FP/iris-coq.git) eda69d4f36efbfe48fc70955244ffb4ccfa925c7.\r\n\r\nThe strange point is, even going back to PG a8f6e0d0, the error remains -- and that commit used to work. Seems like something else must have changed on my side, but I can't figure out what, and the error is not exactly helpful.\r\n\r\nPG master works fine."},"comment":{"url":"https://api.github.com/repos/psteckler/ProofGeneral/issues/comments/276178093","html_url":"https://github.com/psteckler/ProofGeneral/issues/74#issuecomment-276178093","issue_url":"https://api.github.com/repos/psteckler/ProofGeneral/issues/74","id":276178093,"user":{"login":"psteckler","id":2244648,"avatar_url":"https://avatars.githubusercontent.com/u/2244648?v=3","gravatar_id":"","url":"https://api.github.com/users/psteckler","html_url":"https://github.com/psteckler","followers_url":"https://api.github.com/users/psteckler/followers","following_url":"https://api.github.com/users/psteckler/following{/other_user}","gists_url":"https://api.github.com/users/psteckler/gists{/gist_id}","starred_url":"https://api.github.com/users/psteckler/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/psteckler/subscriptions","organizations_url":"https://api.github.com/users/psteckler/orgs","repos_url":"https://api.github.com/users/psteckler/repos","events_url":"https://api.github.com/users/psteckler/events{/privacy}","received_events_url":"https://api.github.com/users/psteckler/received_events","type":"User","site_admin":false},"created_at":"2017-01-30T20:19:00Z","updated_at":"2017-01-30T20:19:00Z","body":"I removed several `(require 'cl)` in my PG files, because it's now deprecated. The cl definitions might have been getting imported into the compilation code.\r\n\r\nPerhaps there's an equivalent in `cl-lib` that I can use. "}}
{"actor":{"display_login":"psteckler"}}