search

acl2 / acl2

ACL2 System and Books as Maintained by the Community
http://www.cs.utexas.edu/users/moore/acl2
Other
364 stars 100 forks source link

cert.pl and add-include-book-dir! #159

Closed ragerdl closed 10 years ago

ragerdl commented 10 years ago

From shigoel on February 28, 2014 13:56:33

It would be nice if cert.pl accounted for add-include-book-dir! when doing dependency tracking.

For the record: I've pasted in a part of my email to the acl2 help list:

"I know that cert.pl supports add-include-book-dir (thanks a lot for that!), but is there some special something that has to be done so that add-include-book-dir! works as well? I get a bad path warning when I include a book with a :dir , where is a keyword I added using add-include-book-dir!.

My workaround for now is defining all such s using add-include-book-dir in cert.acl2 files of all my directories. However, it kind of defeats the purpose of add-include-book-dir!."

Original issue: http://code.google.com/p/acl2-books/issues/detail?id=158

ragerdl commented 10 years ago

From sswo...@gmail.com on February 28, 2014 12:56:24

At the moment, we're doing this even a bit more incorrectly than the bug suggests. In particular, the new port file loading stuff can propagate the effects add-include-book-dir in the portcullis between books without cert.pl being able to properly track it. That is, if your book has a book.acl2 or cert.acl2 that either has an add-include-book-dir or LDs some files that eventually contain one, cert.pl can track that, but if it includes a book that has such a .acl2 file, it can't, and if the book has an add-include-book-dir!, it can't either.

To do this correctly we need to store, for each book, a hash for its add-include-book-dir entries, and each time we include a book, copy that book's mappings into the current book's. Should be doable. However, to keep things simple, I propose that we ignore the following complicating factors:

  1. the presence or absence of an exclamation mark
  2. whether an include-book is local or not. Keeping track of either of these would be kind of a pain in that we'd need to maintain one mapping to figure out include-book directories for the current book and a separate mapping for the ones we'll export to other books. Furthermore, simple regex-based parsing of books doesn't give us a reliable way to know whether a given include-book is local or not.

If we ignore these complicating factors, we're basically assuming that if you have an add-include-book-dir(!) in some book/portcullis, then you want to be able to use it anywhere that book is included, and if you didn't put it in a place where it'll be exported and use it erroneously, ACL2 will catch your mistake, not the build system. Does that seem reasonable?

ragerdl commented 10 years ago

From sswo...@gmail.com on February 28, 2014 14:05:14

Owner: sswo...@gmail.com

ragerdl commented 10 years ago

From shigoel on February 28, 2014 16:18:05

Yes, I think it's reasonable for a build system to treat local and non-local include-books and add-include-book-dirs equally. Thanks, Sol.

ragerdl commented 10 years ago

From rage...@gmail.com on July 15, 2014 15:50:30

Something tells me this might be fixed. If so, please close it :). If not, given Shilpi and Sol sit near one another, maybe one of them would like to take care of this.

ragerdl commented 10 years ago

From sswo...@gmail.com on July 16, 2014 06:01:10

I guess my commit message had the wrong syntax.

Status: Fixed

ragerdl commented 10 years ago

From rage...@gmail.com on September 03, 2014 05:53:11

Labels: Type-Task