{"action":"created","issue":{"url":"https://api.github.com/repos/GeoCoq/GeoCoq/issues/3","labels_url":"https://api.github.com/repos/GeoCoq/GeoCoq/issues/3/labels{/name}","comments_url":"https://api.github.com/repos/GeoCoq/GeoCoq/issues/3/comments","events_url":"https://api.github.com/repos/GeoCoq/GeoCoq/issues/3/events","html_url":"https://github.com/GeoCoq/GeoCoq/issues/3","id":121908405,"number":3,"title":"compilation error in coq8.4pl6 in ubuntu 12.04","user":{"login":"LovelyYanki","id":5094741,"avatar_url":"https://avatars.githubusercontent.com/u/5094741?v=3","gravatar_id":"","url":"https://api.github.com/users/LovelyYanki","html_url":"https://github.com/LovelyYanki","followers_url":"https://api.github.com/users/LovelyYanki/followers","following_url":"https://api.github.com/users/LovelyYanki/following{/other_user}","gists_url":"https://api.github.com/users/LovelyYanki/gists{/gist_id}","starred_url":"https://api.github.com/users/LovelyYanki/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/LovelyYanki/subscriptions","organizations_url":"https://api.github.com/users/LovelyYanki/orgs","repos_url":"https://api.github.com/users/LovelyYanki/repos","events_url":"https://api.github.com/users/LovelyYanki/events{/privacy}","received_events_url":"https://api.github.com/users/LovelyYanki/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":10,"created_at":"2015-12-13T08:54:21Z","updated_at":"2015-12-17T10:59:51Z","closed_at":"2015-12-17T08:05:20Z","body":"martin@ubuntu:~/geo$ cd GeoCoq/\r\nmartin@ubuntu:~/geo/GeoCoq$ ls\r\nAxioms     configure.sh  LICENSE  Makefile  Meta_theory  Tactics     Utils\r\nChangelog  Highschool    Make     Make.in   README.md    Tarski_dev\r\nmartin@ubuntu:~/geo/GeoCoq$ ./configure.sh \r\nmartin@ubuntu:~/geo/GeoCoq$ make\r\n\"coqc\"  -q  -R . GeoCoq   Tarski_dev/Ch02_cong\r\nFile \"/home/martin/geo/GeoCoq/Tarski_dev/Ch02_cong.v\", line 1, characters 0-43:\r\nError: File /home/martin/geo/GeoCoq/Axioms/tarski_axioms.vo has bad magic\r\nnumber. It is corrupted or was compiled with another version of Coq.\r\nmake: *** [Tarski_dev/Ch02_cong.vo] Error 1\r\nmartin@ubuntu:~/geo/GeoCoq$ coqc -v\r\nThe Coq Proof Assistant, version 8.4pl6 (December 2015)\r\ncompiled on Dec 13 2015 00:21:12 with OCaml 3.12.1\r\nmartin@ubuntu:~/geo/GeoCoq$ sudo make\r\n\"coqc\"  -q  -R . GeoCoq   Tarski_dev/Ch02_cong\r\nFile \"/home/martin/geo/GeoCoq/Tarski_dev/Ch02_cong.v\", line 1, characters 0-43:\r\nError: File /home/martin/geo/GeoCoq/Axioms/tarski_axioms.vo has bad magic\r\nnumber. It is corrupted or was compiled with another version of Coq.\r\nmake: *** [Tarski_dev/Ch02_cong.vo] Error 1\r\nmartin@ubuntu:~/geo/GeoCoq$ \r\n"},"comment":{"url":"https://api.github.com/repos/GeoCoq/GeoCoq/issues/comments/165422459","html_url":"https://github.com/GeoCoq/GeoCoq/issues/3#issuecomment-165422459","issue_url":"https://api.github.com/repos/GeoCoq/GeoCoq/issues/3","id":165422459,"user":{"login":"LovelyYanki","id":5094741,"avatar_url":"https://avatars.githubusercontent.com/u/5094741?v=3","gravatar_id":"","url":"https://api.github.com/users/LovelyYanki","html_url":"https://github.com/LovelyYanki","followers_url":"https://api.github.com/users/LovelyYanki/followers","following_url":"https://api.github.com/users/LovelyYanki/following{/other_user}","gists_url":"https://api.github.com/users/LovelyYanki/gists{/gist_id}","starred_url":"https://api.github.com/users/LovelyYanki/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/LovelyYanki/subscriptions","organizations_url":"https://api.github.com/users/LovelyYanki/orgs","repos_url":"https://api.github.com/users/LovelyYanki/repos","events_url":"https://api.github.com/users/LovelyYanki/events{/privacy}","received_events_url":"https://api.github.com/users/LovelyYanki/received_events","type":"User","site_admin":false},"created_at":"2015-12-17T10:59:51Z","updated_at":"2015-12-17T10:59:51Z","body":"thank you very much"}}