Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Collision between generated HTML filenames #14

Open
palmskog opened this issue Dec 16, 2020 · 3 comments · May be fixed by #25
Open

Collision between generated HTML filenames #14

palmskog opened this issue Dec 16, 2020 · 3 comments · May be fixed by #25

Comments

@palmskog
Copy link
Collaborator

palmskog commented Dec 16, 2020

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
Copy link
Owner

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
Copy link
Collaborator Author

palmskog commented Dec 19, 2020

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
Copy link
Contributor

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.

@JasonGross JasonGross linked a pull request Apr 13, 2021 that will close this issue
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants