Stricter xdoc checking
2 views
Skip to first unread message
Eric Smith
Mar 2, 2026, 7:05:28 PM (2 days ago) Mar 2
to acl2-...@googlegroups.com, Matt Kaufmann
Hi acl2-books,
Some of us would like to make more xdoc issues into errors, not merely warnings,
to catch issues earlier and to avoid having to deal with them all before a
release. Please let us know if you have any objections to this.
A relevant PR, to disallow non-existent xdoc parents, is:
https://github.com/acl2/acl2/pull/1909
Other things that probably should be errors:
- topics with no parents
- links to topics that don't exist
- subtopic ordering declarations that mention things that are not subtopics
- shadowed topics
For some of these, there are deliberate instances used for testing
and/or known instances that will be whitelisted. But it would be good
to ensure that more of these issues are not introduced by accident.
Thoughts? One thing to think about would be the impact on custom
manuals and/or the "ACL2 only" manual (without the books). (I suppose we could
do something like adding a strictp flag that is nil for manuals other than the
main one.)
Thanks,
-Eric
Some of us would like to make more xdoc issues into errors, not merely warnings,
to catch issues earlier and to avoid having to deal with them all before a
release. Please let us know if you have any objections to this.
A relevant PR, to disallow non-existent xdoc parents, is:
https://github.com/acl2/acl2/pull/1909
Other things that probably should be errors:
- topics with no parents
- links to topics that don't exist
- subtopic ordering declarations that mention things that are not subtopics
- shadowed topics
For some of these, there are deliberate instances used for testing
and/or known instances that will be whitelisted. But it would be good
to ensure that more of these issues are not introduced by accident.
Thoughts? One thing to think about would be the impact on custom
manuals and/or the "ACL2 only" manual (without the books). (I suppose we could
do something like adding a strictp flag that is nil for manuals other than the
main one.)
Thanks,
-Eric
Matt Kaufmann
Mar 2, 2026, 7:12:51 PM (2 days ago) Mar 2
to Eric Smith, acl2-...@googlegroups.com
Hi Eric,
You've got my vote. I'm pretty sure that building the acl2-only manual
isn't generating any such warnings (I just checked my copy of
books/system/doc/render-doc.cert.out).
Maybe there's no loss in removing the tests that deliberately
exercise the current warnings, as an easy way to prevent them
from turning into errors.
But I think your concern about custom manuals is valid. You
could document the use of set-warnings-as-errors (which is
documented) to avoid errors -- I think.
-- Matt
Sol Swords
Mar 3, 2026, 12:37:44 PM (2 days ago) Mar 3
to acl2-...@googlegroups.com, Eric Smith
I think this makes sense, but I would like there to be an easy way to turn off the strictness. Sometimes I just want to build a small manual to see what a topic looks like and I don't care if there are problems in other topics or connectivity or whatever.
-Sol
--
--
ACL2-books help:
To post new messages: acl2-...@googlegroups.com
To unsubscribe: acl2-books-...@googlegroups.com
More options: http://groups.google.com/group/acl2-books?hl=en
---
You received this message because you are subscribed to the Google Groups "acl2-books" group.
To unsubscribe from this group and stop receiving emails from it, send an email to acl2-books+...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/acl2-books/CAOQvmW%2BjeBTtJdZFfPyyjPjBS5EXwrgw_zg6idFmgOyO2sz07Q%40mail.gmail.com.
Eric Smith
Mar 3, 2026, 1:35:16 PM (2 days ago) Mar 3
to Sol Swords, acl2-...@googlegroups.com
Sol,
What command do you use to build these small manuals? xdoc::save or some
variant of that?
Thanks,
-Eric
> https://github.com/acl2/acl2/pull/1909 <https://github.com/acl2/acl2/
> pull/1909>
> bo...@googlegroups.com>
> To unsubscribe: acl2-books-...@googlegroups.com <mailto:acl2-books-
> unsub...@googlegroups.com>
> More options: http://groups.google.com/group/acl2-books?hl=en <http://
> groups.google.com/group/acl2-books?hl=en>
> books+un...@googlegroups.com>.
> CAOQvmW%2BjeBTtJdZFfPyyjPjBS5EXwrgw_zg6idFmgOyO2sz07Q%40mail.gmail.com?
> utm_medium=email&utm_source=footer>.
>
What command do you use to build these small manuals? xdoc::save or some
variant of that?
Thanks,
-Eric
> pull/1909>
>
> Other things that probably should be errors:
> - topics with no parents
> - links to topics that don't exist
> - subtopic ordering declarations that mention things that are not subtopics
> - shadowed topics
>
> For some of these, there are deliberate instances used for testing
> and/or known instances that will be whitelisted. But it would be good
> to ensure that more of these issues are not introduced by accident.
>
> Thoughts? One thing to think about would be the impact on custom
> manuals and/or the "ACL2 only" manual (without the books). (I suppose
> we could
> do something like adding a strictp flag that is nil for manuals other
> than the
> main one.)
>
> Thanks,
> -Eric
>
> --
> --
> ACL2-books help:
> To post new messages: acl2-...@googlegroups.com <mailto:acl2-
> Other things that probably should be errors:
> - topics with no parents
> - links to topics that don't exist
> - subtopic ordering declarations that mention things that are not subtopics
> - shadowed topics
>
> For some of these, there are deliberate instances used for testing
> and/or known instances that will be whitelisted. But it would be good
> to ensure that more of these issues are not introduced by accident.
>
> Thoughts? One thing to think about would be the impact on custom
> manuals and/or the "ACL2 only" manual (without the books). (I suppose
> we could
> do something like adding a strictp flag that is nil for manuals other
> than the
> main one.)
>
> Thanks,
> -Eric
>
> --
> --
> ACL2-books help:
> bo...@googlegroups.com>
> To unsubscribe: acl2-books-...@googlegroups.com <mailto:acl2-books-
> unsub...@googlegroups.com>
> More options: http://groups.google.com/group/acl2-books?hl=en <http://
> groups.google.com/group/acl2-books?hl=en>
>
> ---
> You received this message because you are subscribed to the Google Groups
> "acl2-books" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to acl2-books+...@googlegroups.com <mailto:acl2-
> ---
> You received this message because you are subscribed to the Google Groups
> "acl2-books" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> books+un...@googlegroups.com>.
> To view this discussion visit https://groups.google.com/d/msgid/acl2-books/
> CAOQvmW%2BjeBTtJdZFfPyyjPjBS5EXwrgw_zg6idFmgOyO2sz07Q%40mail.gmail.com
> <https://groups.google.com/d/msgid/acl2-books/
> CAOQvmW%2BjeBTtJdZFfPyyjPjBS5EXwrgw_zg6idFmgOyO2sz07Q%40mail.gmail.com
> CAOQvmW%2BjeBTtJdZFfPyyjPjBS5EXwrgw_zg6idFmgOyO2sz07Q%40mail.gmail.com?
> utm_medium=email&utm_source=footer>.
>
Sol Swords
Mar 3, 2026, 1:45:08 PM (2 days ago) Mar 3
to Eric Smith, acl2-...@googlegroups.com
Yes, xdoc::save.
Eric Smith
Mar 3, 2026, 5:27:33 PM (2 days ago) Mar 3
to Sol Swords, acl2-...@googlegroups.com
Ok, great. xdoc::save already has some arguments controlling strictness (see
below). So I propose adding more such options. Probably we should make the
defaults be non-strict (like :the current defaults of error nil and
:broken-links-limit nil) but transition to using the strict options when
building the main manual. Sound ok?
Here is the current usage:
(save <target-dir>
[:redef-okp bool] ;; default is nil
[:zip-p bool] ;; default is t
[:logo-image path] ;; default is nil
[:error bool] ;; default is nil
[:broken-links-limit nil-or-nat] ;; default is nil
)
I'm working on adding a new option, :error-on-non-existent-parents, in my PR #1909.
Thanks,
-Eric
On 3/3/26 10:44 AM, Sol Swords wrote:
> Yes, xdoc::save.
>
> On Tue, Mar 3, 2026 at 12:35 PM Eric Smith <eric....@kestrel.edu
> <mailto:eric....@kestrel.edu>> wrote:
>
> Sol,
>
> What command do you use to build these small manuals? xdoc::save or some
> variant of that?
>
> Thanks,
> -Eric
>
> On 3/3/26 9:37 AM, Sol Swords wrote:
> > I think this makes sense, but I would like there to be an easy way to
> turn off
> > the strictness. Sometimes I just want to build a small manual to see what a
> > topic looks like and I don't care if there are problems in other topics or
> > connectivity or whatever.
> > -Sol
> >
> > On Mon, Mar 2, 2026 at 6:12 PM Matt Kaufmann
> <matthew.j...@gmail.com <mailto:matthew.j...@gmail.com>
> > <mailto:matthew.j...@gmail.com
> > bo...@googlegroups.com <mailto:bo...@googlegroups.com>>
> books-un...@googlegroups.com> <mailto:acl2-books- <mailto:acl2-books->
> > unsub...@googlegroups.com <mailto:unsub...@googlegroups.com>>
> > More options: http://groups.google.com/group/acl2-books?hl=en
> <http://groups.google.com/group/acl2-books?hl=en> <http://
> > books+un...@googlegroups.com
> <mailto:books%2Bunsu...@googlegroups.com>>.
> >
> CAOQvmW%2BjeBTtJdZFfPyyjPjBS5EXwrgw_zg6idFmgOyO2sz07Q%40mail.gmail.com
> <http://40mail.gmail.com>
> > <https://groups.google.com/d/msgid/acl2-books/ <https://
> groups.google.com/d/msgid/acl2-books/>
> >
> CAOQvmW%2BjeBTtJdZFfPyyjPjBS5EXwrgw_zg6idFmgOyO2sz07Q%40mail.gmail.com
> <http://40mail.gmail.com>?
> > utm_medium=email&utm_source=footer>.
> >
>
below). So I propose adding more such options. Probably we should make the
defaults be non-strict (like :the current defaults of error nil and
:broken-links-limit nil) but transition to using the strict options when
building the main manual. Sound ok?
Here is the current usage:
(save <target-dir>
[:redef-okp bool] ;; default is nil
[:zip-p bool] ;; default is t
[:logo-image path] ;; default is nil
[:error bool] ;; default is nil
[:broken-links-limit nil-or-nat] ;; default is nil
)
I'm working on adding a new option, :error-on-non-existent-parents, in my PR #1909.
Thanks,
-Eric
On 3/3/26 10:44 AM, Sol Swords wrote:
> Yes, xdoc::save.
>
> On Tue, Mar 3, 2026 at 12:35 PM Eric Smith <eric....@kestrel.edu
> <mailto:eric....@kestrel.edu>> wrote:
>
> Sol,
>
> What command do you use to build these small manuals? xdoc::save or some
> variant of that?
>
> Thanks,
> -Eric
>
> On 3/3/26 9:37 AM, Sol Swords wrote:
> > I think this makes sense, but I would like there to be an easy way to
> turn off
> > the strictness. Sometimes I just want to build a small manual to see what a
> > topic looks like and I don't care if there are problems in other topics or
> > connectivity or whatever.
> > -Sol
> >
> > On Mon, Mar 2, 2026 at 6:12 PM Matt Kaufmann
> <matthew.j...@gmail.com <mailto:matthew.j...@gmail.com>
> <mailto:matthew.j...@gmail.com>>> wrote:
> >
> > Hi Eric,
> >
> > You've got my vote. I'm pretty sure that building the acl2-only manual
> > isn't generating any such warnings (I just checked my copy of
> > books/system/doc/render-doc.cert.out).
> >
> > Maybe there's no loss in removing the tests that deliberately
> > exercise the current warnings, as an easy way to prevent them
> > from turning into errors.
> >
> > But I think your concern about custom manuals is valid. You
> > could document the use of set-warnings-as-errors (which is
> > documented) to avoid errors -- I think.
> >
> > -- Matt
> >
> > On Mon, Mar 2, 2026 at 4:05 PM Eric Smith <eric....@kestrel.edu
> <mailto:eric....@kestrel.edu>
> >
> > Hi Eric,
> >
> > You've got my vote. I'm pretty sure that building the acl2-only manual
> > isn't generating any such warnings (I just checked my copy of
> > books/system/doc/render-doc.cert.out).
> >
> > Maybe there's no loss in removing the tests that deliberately
> > exercise the current warnings, as an easy way to prevent them
> > from turning into errors.
> >
> > But I think your concern about custom manuals is valid. You
> > could document the use of set-warnings-as-errors (which is
> > documented) to avoid errors -- I think.
> >
> > -- Matt
> >
> > On Mon, Mar 2, 2026 at 4:05 PM Eric Smith <eric....@kestrel.edu
> <mailto:eric....@kestrel.edu>
> > <mailto:eric....@kestrel.edu <mailto:eric....@kestrel.edu>>> wrote:
> >
> > Hi acl2-books,
> >
> > Some of us would like to make more xdoc issues into errors, not
> merely
> > warnings,
> > to catch issues earlier and to avoid having to deal with them all
> before a
> > release. Please let us know if you have any objections to this.
> >
> > A relevant PR, to disallow non-existent xdoc parents, is:
> >
> > https://github.com/acl2/acl2/pull/1909 <https://github.com/acl2/acl2/
> pull/1909> <https://github.com/acl2/acl2/ <https://github.com/acl2/acl2/>
> >
> > Hi acl2-books,
> >
> > Some of us would like to make more xdoc issues into errors, not
> merely
> > warnings,
> > to catch issues earlier and to avoid having to deal with them all
> before a
> > release. Please let us know if you have any objections to this.
> >
> > A relevant PR, to disallow non-existent xdoc parents, is:
> >
> > https://github.com/acl2/acl2/pull/1909 <https://github.com/acl2/acl2/
> > pull/1909>
> >
> > Other things that probably should be errors:
> > - topics with no parents
> > - links to topics that don't exist
> > - subtopic ordering declarations that mention things that are not
> subtopics
> > - shadowed topics
> >
> > For some of these, there are deliberate instances used for testing
> > and/or known instances that will be whitelisted. But it would be
> good
> > to ensure that more of these issues are not introduced by accident.
> >
> > Thoughts? One thing to think about would be the impact on custom
> > manuals and/or the "ACL2 only" manual (without the books). (I
> suppose
> > we could
> > do something like adding a strictp flag that is nil for manuals other
> > than the
> > main one.)
> >
> > Thanks,
> > -Eric
> >
> > --
> > --
> > ACL2-books help:
> > To post new messages: acl2-...@googlegroups.com <mailto:acl2-
> bo...@googlegroups.com> <mailto:acl2- <mailto:acl2->
> >
> > Other things that probably should be errors:
> > - topics with no parents
> > - links to topics that don't exist
> > - subtopic ordering declarations that mention things that are not
> subtopics
> > - shadowed topics
> >
> > For some of these, there are deliberate instances used for testing
> > and/or known instances that will be whitelisted. But it would be
> good
> > to ensure that more of these issues are not introduced by accident.
> >
> > Thoughts? One thing to think about would be the impact on custom
> > manuals and/or the "ACL2 only" manual (without the books). (I
> suppose
> > we could
> > do something like adding a strictp flag that is nil for manuals other
> > than the
> > main one.)
> >
> > Thanks,
> > -Eric
> >
> > --
> > --
> > ACL2-books help:
> > To post new messages: acl2-...@googlegroups.com <mailto:acl2-
> > bo...@googlegroups.com <mailto:bo...@googlegroups.com>>
> books-un...@googlegroups.com> <mailto:acl2-books- <mailto:acl2-books->
> > unsub...@googlegroups.com <mailto:unsub...@googlegroups.com>>
> > More options: http://groups.google.com/group/acl2-books?hl=en
> <http://groups.google.com/group/acl2-books?hl=en> <http://
> > groups.google.com/group/acl2-books?hl=en <http://groups.google.com/group/
> acl2-books?hl=en>>
> >
> > ---
> > You received this message because you are subscribed to the Google Groups
> > "acl2-books" group.
> > To unsubscribe from this group and stop receiving emails from it, send an
> > email to acl2-books+...@googlegroups.com <mailto:acl2-
> books%2Bunsu...@googlegroups.com> <mailto:acl2- <mailto:acl2->
> acl2-books?hl=en>>
> >
> > ---
> > You received this message because you are subscribed to the Google Groups
> > "acl2-books" group.
> > To unsubscribe from this group and stop receiving emails from it, send an
> > email to acl2-books+...@googlegroups.com <mailto:acl2-
> > books+un...@googlegroups.com
> <mailto:books%2Bunsu...@googlegroups.com>>.
> > To view this discussion visit https://groups.google.com/d/msgid/acl2-
> books/ <https://groups.google.com/d/msgid/acl2-books/>
> >
> CAOQvmW%2BjeBTtJdZFfPyyjPjBS5EXwrgw_zg6idFmgOyO2sz07Q%40mail.gmail.com
> <http://40mail.gmail.com>
> > <https://groups.google.com/d/msgid/acl2-books/ <https://
> groups.google.com/d/msgid/acl2-books/>
> >
> CAOQvmW%2BjeBTtJdZFfPyyjPjBS5EXwrgw_zg6idFmgOyO2sz07Q%40mail.gmail.com
> <http://40mail.gmail.com>?
> > utm_medium=email&utm_source=footer>.
> >
>
Sol Swords
Mar 3, 2026, 6:12:04 PM (2 days ago) Mar 3
to Eric Smith, acl2-...@googlegroups.com
Sounds good. I don't mind particularly what the default is (keeping it backward-compatible is fine though).
Reply all
Reply to author
Forward
0 new messages