{"action":"created","issue":{"url":"https://api.github.com/repos/acl2/acl2/issues/477","labels_url":"https://api.github.com/repos/acl2/acl2/issues/477/labels{/name}","comments_url":"https://api.github.com/repos/acl2/acl2/issues/477/comments","events_url":"https://api.github.com/repos/acl2/acl2/issues/477/events","html_url":"https://github.com/acl2/acl2/pull/477","id":99796829,"number":477,"title":"Restore rtl/rel11/masc arrays. Use rtl/rel11 in workshop. Remove trai…","user":{"login":"nadezhin","id":1213537,"avatar_url":"https://avatars.githubusercontent.com/u/1213537?v=3","gravatar_id":"","url":"https://api.github.com/users/nadezhin","html_url":"https://github.com/nadezhin","followers_url":"https://api.github.com/users/nadezhin/followers","following_url":"https://api.github.com/users/nadezhin/following{/other_user}","gists_url":"https://api.github.com/users/nadezhin/gists{/gist_id}","starred_url":"https://api.github.com/users/nadezhin/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nadezhin/subscriptions","organizations_url":"https://api.github.com/users/nadezhin/orgs","repos_url":"https://api.github.com/users/nadezhin/repos","events_url":"https://api.github.com/users/nadezhin/events{/privacy}","received_events_url":"https://api.github.com/users/nadezhin/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":24,"created_at":"2015-08-08T11:53:50Z","updated_at":"2015-08-13T16:57:25Z","closed_at":"2015-08-09T17:06:00Z","pull_request":{"url":"https://api.github.com/repos/acl2/acl2/pulls/477","html_url":"https://github.com/acl2/acl2/pull/477","diff_url":"https://github.com/acl2/acl2/pull/477.diff","patch_url":"https://github.com/acl2/acl2/pull/477.patch"},"body":"…ling spaces.\r\n\r\n@ragerdl , is this simple cert.acl2 enough to support package-aware certification ?"},"comment":{"url":"https://api.github.com/repos/acl2/acl2/issues/comments/130760148","html_url":"https://github.com/acl2/acl2/pull/477#issuecomment-130760148","issue_url":"https://api.github.com/repos/acl2/acl2/issues/477","id":130760148,"user":{"login":"ragerdl","id":2245886,"avatar_url":"https://avatars.githubusercontent.com/u/2245886?v=3","gravatar_id":"","url":"https://api.github.com/users/ragerdl","html_url":"https://github.com/ragerdl","followers_url":"https://api.github.com/users/ragerdl/followers","following_url":"https://api.github.com/users/ragerdl/following{/other_user}","gists_url":"https://api.github.com/users/ragerdl/gists{/gist_id}","starred_url":"https://api.github.com/users/ragerdl/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ragerdl/subscriptions","organizations_url":"https://api.github.com/users/ragerdl/orgs","repos_url":"https://api.github.com/users/ragerdl/repos","events_url":"https://api.github.com/users/ragerdl/events{/privacy}","received_events_url":"https://api.github.com/users/ragerdl/received_events","type":"User","site_admin":false},"created_at":"2015-08-13T16:57:25Z","updated_at":"2015-08-13T16:57:25Z","body":"Hi David,\n\nIf it's the typing of \"10\" that you're concerned about, you should be able\nto use \"?\" instead.\n\nDavid\n\nOn Thu, Aug 13, 2015 at 11:55 AM, russinoff <notifications@github.com>\nwrote:\n\n> Thanks. In the end, I guess to certify a book interactively, I can't do\n> any better than what I've been doing:\n>\n> (include-book \"rtl/rel11/lib/top\" :dir :system)\n>\n> (certify-book \"foo\" 1)\n>\n> If I do this consistently, then I won't have to think about how a book was\n> certified.\n>\n> If I try to certify a book after\n>\n> (ld \"rtl/rel11/lib/top.port\")\n>\n> then it wants\n>\n> (certify-book \"foo\" 10)\n>\n> which is a little scary.\n>\n>\n> On Wed, Aug 12, 2015 at 2:37 PM, solswords <notifications@github.com>\n> wrote:\n>\n> > Personally speaking, I rarely certify a book from inside an interactive\n> > ACL2 session. I use the Makefile from the books directory or else use \"\n> > cert.pl bookname\" to do it from the command line. (Cert.pl is located in\n> > books/build and I would suggest symlinking it into your path, or adding\n> > books/build to your path.)\n> >\n> > If you want to certify a book from an interactive session, you can\n> manually\n> > replicate what cert.pl automates by\n> > - certifying all the books that your book includes, using cert.pl or the\n> > Makefile\n> > - in your interactive session, LDing the .port files of all those books\n> > before certifying your book. Each of these contains the portcullis\n> > commands of the corresponding book, which in particular will define all\n> of\n> > the packages used by those books.\n> >\n> > E.g. if your book includes rtl/rel11/lib/top, then do\n> > (ld \"rtl/rel11/lib/top.port\" :dir :system)\n> > before your certify-book command.\n> >\n> > I would suggest just using cert.pl instead, though -- if only so that\n> once\n> > you succeed in certifying a book, you can be sure of repeating that\n> > success, without having to look through your session to figure out\n> exactly\n> > what you had to do before certifying it.\n> >\n> > - Sol\n> >\n> >\n> >\n> > On Wed, Aug 12, 2015 at 11:45 AM, russinoff <notifications@github.com>\n> > wrote:\n> >\n> > > OK, I think I just created a pull request. I would note once again that\n> > > the instructions in the on-line documentation are badly broken. I had\n> to\n> > > guess about a few things.\n> > >\n> > > I have another pull request that I'd like to make, to add\n> > > books/projects/masc, but first I have a question, which I think was\n> once\n> > > answered, but I didn't understand the answer.\n> > >\n> > > What is the recommended way to certify a book that begins with\n> > (in-package\n> > > \"RTL\")? If I try (certify-book \"foo\") immediately after loading acl2,\n> > thrn\n> > > of course I get the complaint that the RTL package is unknown. So\n> instead\n> > > I do this:\n> > >\n> > > (include-book \"rtl/rel11/lib/top\" :dir :system) ;or some such\n> > > (certify-book \"foo\" 1)\n> > >\n> > > This works, but it seems clumsy.\n> > >\n> > >\n> > >\n> > > On Tue, Aug 11, 2015 at 11:30 PM, David L. Rager <\n> > notifications@github.com\n> > > >\n> > >\n> > > wrote:\n> > >\n> > > > Hi David,\n> > > >\n> > > > You should now be able to do a \"git pull\" from within your version of\n> > the\n> > > > master branch and obtain Dmitry's changes from the other day.\n> > > >\n> > > > David\n> > > >\n> > > > On Tue, Aug 11, 2015 at 10:21 PM, russinoff <\n> notifications@github.com>\n> > > > wrote:\n> > > >\n> > > > > I abandoned my proposal when I started trying to prove the analogs\n> of\n> > > the\n> > > > > lemmas in misc/records. For example, the analog of\n> > > > >\n> > > > > (defthm s-same-g\n> > > > > (equal (s a (g a r) r)\n> > > > > r))\n> > > > >\n> > > > > is not true.\n> > > > >\n> > > > > I'd like to settle on a solution soon, because I have a project\n> that\n> > > > > depends on it.\n> > > > >\n> > > > > Meanwhile, I think I'll go ahead and issue a pull request for my\n> > other\n> > > > > stuff.\n> > > > >\n> > > > >\n> > > > > On Tue, Aug 11, 2015 at 9:56 PM, nadezhin <\n> notifications@github.com>\n> > > > > wrote:\n> > > > >\n> > > > > > David @russinoff <https://github.com/russinoff>,\n> > > > > >\n> > > > > > I agree that keeping multiple variances of records in ACL2 books\n> is\n> > > > > > inelegant.\n> > > > > > By the way, there are yet more records with default 0\n> > > > > > in projects/x86isa/utils/records-0.\n> > > > > > I would like to search for a better solution.\n> > > > > >\n> > > > > > Why did you retract your solution with r (a x) ?\n> > > > > >\n> > > > > > I thought about one more solution - a limited support of\n> > > > > > default value in misc/records.\n> > > > > > Now (implies (rcdp r) (true-listp r)).\n> > > > > > We could relax this to (implies (rcdp r) (listp r))\n> > > > > > and consider the atom (final-cdr r) as the default value.\n> > > > > > However, default value is limited to an atom in this case.\n> > > > > > Another drawback that it could break some of misc/records\n> clients.\n> > > > > >\n> > > > > > —\n> > > > > > Reply to this email directly or view it on GitHub\n> > > > > > <https://github.com/acl2/acl2/pull/477#issuecomment-130141820>.\n> > > > >\n> > > > > >\n> > > > >\n> > > > > —\n> > > > > Reply to this email directly or view it on GitHub\n> > > > > <https://github.com/acl2/acl2/pull/477#issuecomment-130145582>.\n> > > > >\n> > > >\n> > > > —\n> > > > Reply to this email directly or view it on GitHub\n> > > > <https://github.com/acl2/acl2/pull/477#issuecomment-130156664>.\n> > >\n> > > >\n> > >\n> > > —\n> > > Reply to this email directly or view it on GitHub\n> > > <https://github.com/acl2/acl2/pull/477#issuecomment-130366389>.\n> > >\n> >\n> > —\n> > Reply to this email directly or view it on GitHub\n> > <https://github.com/acl2/acl2/pull/477#issuecomment-130422003>.\n>\n> >\n>\n> —\n> Reply to this email directly or view it on GitHub\n> <https://github.com/acl2/acl2/pull/477#issuecomment-130759512>.\n>\n"}}