Link to common lisp hyperspec?

_From [jared.c....@gmail.com](https://code.google.com/u/107361913114394030743/) on October 23, 2013 08:50:21_

The documentation for many ACL2 built-ins, for instance Append, say things like this:

"Append is a Common Lisp function. See any Common Lisp
documentation for more information."

We could perhaps link these to, e.g., the relevant pages from the Common Lisp HyperSpec.

This is straightforward to do with ordinary URLs. But it might be a better idea to add some kind of XDOC directive to support this. I'm imagining that the markup might look something like this:

```
"Append is a Common Lisp function. See any Common Lisp
documentation for more information. For instance, see
Function Append
in the
Common Lisp HyperSpec."
```

This directive might make it easy for us to change the URLs we generate.

That is, to begin we could have @(hyperspec ...) just link to Lispworks's web site. But we might eventually investigate distributing the hyperspec with the acl2-books. Its license is not very permissive, but does at least allow for redistribution under certain conditions. See: http://www.lispworks.com/documentation/HyperSpec/Front/Help.htm#Legal Some of these restrictions are pretty bad (e.g., you can't redistribute it for commercial advantage, whatever that means.) That sort of thing probably means we can't put a copy of it up on Centaur's web site. But perhaps it's acceptable to for us to bundle it with the "offline" version of the XDOC manual; we could ask the Lispworks folks for their blessing.

Instead of implementing @(hyperspec ...), it might suffice to have something like @(value _hyperspec_), which could be generally more useful.

_Original issue: http://code.google.com/p/acl2-books/issues/detail?id=112_