Collision between generated HTML filenames

[palmskog]

Consider a Coq project organized like this (assume -Q theories Test):

theories/
├── A
│   └── A.v
└── B
    └── A.v

If I call Alectryon as a coqdoc substitute on each these files with --output-directory X, I only get a single file X/A.html in the end. In contrast, coqdoc will generate the files X/Test.A.A.html and X/Test.B.A.html. A more detailed discussion of the coqdoc naming scheme can be found in the coq2html documentation.

Is there a reasonable way of changing the current naming approach to work with the coqdoc scheme?

[cpitclaudel]

Is there a reasonable way of changing the current naming approach to work with the coqdoc scheme?

Probably — either by directly emulating that naming scheme, or by replicating the directory structure, which might be a touch nicer than stuffing everything in one directory?

We'd have to modify write_output, and also adjust paths to CSS and JS files when we generate HTML. What I've done in the past is to compile each file individually using a makefile, respecting the original folder structure.

[palmskog]

I assume you mean that the output directory should mirror the Coq file directory structure, e.g.,

alectryon/A/A.html
alectryon/B/A.html

This unfortunately makes it impossible to have the coqdoc output from Alectryon be compatible with pure coqdoc and coq2html for linking purposes. As Xavier says in the coq2html README, cross-referencing external files can only work if all tools follow the same file naming conventions. I also think it's more convenient to have all HTML files in a flat structure (for table of contents, etc.).

[JasonGross]

Note also that mirroring is incompatible with Alectryon's own linking via alectryon.docutils.COQ_IDENT_DB_URLS. I agree with @palmskog , when there are any -Q or -R directives present which capture the given filename, the longest prefix match should be chosen to transform the file name into a module path and that should be used as the output name.