defxdoc :code-source definitional support

[bendyarm]

Adds the :code-source argument to defxdoc and defxdoc+.
There is an example of its use in ubi-doc.lisp.
Does not yet push the value into the doc entry and does not yet handle rendering.
See also a few inline comments in the code and in this PR.

[bendyarm]

The first rendering would just make this text into a link with the appropriate link target to github as the doc links currently do. If we want to allow lowercase :dir :system to mean the same thing when rendering, let me know, that would be easy.
Also, eventually I would like to be able to add a copy include-book form to clipboard button to the html xdoc rendering that follows the code-source link.

[acoglio]

I think it would be good to use lowercase :dir :system.

[bendyarm]

The proposal now is that if you say

  :code-source "ubi.lisp"

it would be a path relative to the current book, but if you say

  :code-source ("kestrel/utilities/ubi" :dir :system)

it would be relative to the community books.

[ericwhitmansmith]

Looks good. Would just :code-source "ubi" also work?

[ericwhitmansmith]

Oddly, the email github generated with my comment "Looks good" quoted the old example of the :code-source option! What I think actually looks good is Eric's "The proposal now ...".

[bendyarm]

@ericwhitmansmith Yes, :code-source "ubi" would also work, and because the defxdoc is under acl2/books, the code info would render as

  Code:  (include-book "kestrel/utilities/ubi" :dir :system)

[bendyarm]

I took this out for simplicity, since in my test it bloated only about 0.6%
However, once the downstream rendering is working I will put it back in later.

[MattKaufmann]

Just as for the related pull request #1454, I don't want to be involved in this project personally, so please remove me as a reviewer.

Please make sure that :DOC at the terminal or meta-x acl2-doc continue to work with these and subsequent xdoc changes.

[acoglio]

not currently not => currently not

[solswords]

I kind of think we ought to fix this before this enters widespread usage. It would seem strange to me to type in :code-from "my/book/path :DIR :SYSTEM" -- I suggest we allow both :code-from "path" and :code-from ("path" :dir :dirname), normalize both to full-book-names using ACL2 system functions (parse-book-name, or something like it) and then use xdoc's normalize-bookname to get it into the form we want.

[bendyarm]

Let's explore this a little bit. I like allowing ("path" :dir :system) with "path" relative to "acl2/books".

When you write ("path" :dir :dirname) do you really mean ("path" :dir <project-keyword>)?
If so, then I think we should interpret this "path" relative to the the project directory.
It would be confusing if "path" were relative to the current book containing the defxdoc.

Since the :code-source is supplied by the doc developer for doc purposes only, it is good to have clear rules on how the text is processed and what ends up in the rendered doc. I think if you say

  :code-source ("something" :dir :myproject)

then it would be most clear if the "something" is passed unchanged (*) to the sysfile-p (:myproject . "something"), and then rendered in the html doc as

  Code:  (include-book "something" :dir :myproject)

(*) There might be some minor modifications of adding and removing ".lisp", since full-book-names are supposed to have the ".lisp" extensions, but I am mainly referring to the directory of the "something" here.

I don't think that this makes code movement harder. If a doc file is referring to a source file with a path relative to the doc file that ought to remain in the same relative place upon movement, then specify it as the string form, not the list form.

For the string version with a relative path

  :code-source "subdir/file"

the developer story becomes slightly more complex. I think it is reasonable if we want this to be interpreted relative to the current book's path, since it saves the doc developer a lot of typing and makes it easier to move code. If the current book is under a project directory, subdirectory "currdir", then this could still be rendered in the html doc as something like

  Code:  (include-book "currdir/subdir/file" :dir :myproject)

@solswords @ericwhitmansmith What do you think?

[ericwhitmansmith]

This all seems good to me. I think we should make the :code-source as easy as possible to write and maintain (and so support relative paths there). When rendered, the include-book form should, whenever possible, be something that can be used from anywhere (and so should have a :dir option whenever possible).

[solswords]

That sounds good. I could go either way (in the :dir-relative, ("something" :dir :myproject) case) as to whether we do minimal processing and just produce a string directly from that object, or canonicalize using parse-book-name or something similar and then generate the string. I think the main differences would be that the former might allow 1) totally bogus paths, and 2) paths relative to include-book-dirs as well as project dirs, I think 1) is disadvantageous. 2) could be nice except that include-book-dirs aren't global, so potentially a user might have to determine what cert.acl2 file (or whatever) to load to get that include-book-dir. So I guess I'm leaning toward full processing and canonicalization with parse-book-name even for the :dir-relative case.

[solswords]

I guess my code comments here are mostly relative to planned work, not what's done here -- this PR seems pretty harmless in that it just adds the argument to defxdoc/defsection.

[solswords]

I kind of think we ought to fix this before this enters widespread usage. It would seem strange to me to type in :code-from "my/book/path :DIR :SYSTEM" -- I suggest we allow both :code-from "path" and :code-from ("path" :dir :dirname), normalize both to full-book-names using ACL2 system functions (parse-book-name, or something like it) and then use xdoc's normalize-bookname to get it into the form we want.

[solswords]

why is this still commented out? Shouldn't this change be tested with this uncommented?

[bendyarm]

Because if the xdoc table entry changes now, all the consumers will need to be OK with that, and I was probably missing one when I tried it before since I got errors that were hard to debug. I'm trying for a staged approach to make it easier.

[solswords]

see my other comment -- I think we should accept ("path" :dir :dirname) as well as just a string here

[acoglio]

Should we merge this?