Weird filenames and doc4-gen

Stream: lean4

[Moritz Firsching]

When trying to get doc-gen4 to work with a project, I got a failure when trying to build a module/filename containing characters that need french quoting. Perhaps this is expected and just not supported by doc-gen4. I made a minimal working example here:
https://github.com/mo271/TestProject
This project contains a file TestProject/Erdős.lean. When running

DOCGEN_SRC="vscode" lake -R -Kenv=dev build TestProject:docs

I get an error:

[155/159] Documenting module: TestProject.«Erdős»
error: no such file or directory (error code: 2)
  file: ./.lake/build/doc/TestProject/Erdős.html

and indeed this file is not present:

ls ./.lake/build/doc/TestProject
Basic.html  Basic.html.hash  Basic.html.trace  «Erdős».html  Erdős.html.trace

However, «Erdős».html is there. I think the name of the missing file comes from this line:
https://github.com/leanprover/doc-gen4/blob/a34d3c1f7b72654c08abe5741d94794db40dbb2e/lakefile.lean#L139
while the file that is present is written here: https://github.com/leanprover/doc-gen4/blob/a34d3c1f7b72654c08abe5741d94794db40dbb2e/DocGen4/Output/Base.lean#L125

Is there an easy fix for that or is the solution to use more conventional names?

[Eric Wieser]

Is mod.filePath set incorrectly there?

[Moritz Firsching]

not sure which one it incorrect, but this one is set to the name without the french quotes : ./.lake/build/doc/TestProject/Erdős.html
https://github.com/leanprover/lean4/blob/62cdb51ed5b9d8487877d5a4adbcd4659d81fc6a/src/lake/Lake/Config/Module.lean#L65-L66

[Moritz Firsching]

bumping this: Has anyone been able to use doc4-gen together with filenames that work only with french quotes?

[Bulhwi Cha]

doc-gen4 failed to build Lean files with names containing a hyphen: https://paste.sr.ht/~chabulhwi/e2acec95483a00bc442afc376a2cf9ab6320da2d.

Some required builds logged failures:
- TPIL.Chapter02.«Question01-10»:docs
- TPIL.Chapter02.«Question13-14»:docs
- TPIL.Chapter02.«Question19-20»:docs
- TPIL.Chapter02.«Question22-25»:docs
- TPIL.Chapter02.«Question34-38»:docs
- TPIL.Chapter03.«Question03-08»:docs
- TPIL.Chapter03.«Question10-14»:docs
- TPIL.Chapter04.«Question04-05»:docs
error: build failed

[Eric Wieser]

Possible fix in https://github.com/leanprover/doc-gen4/pull/267

[Eric Wieser]

@Bulhwi Cha, @Moritz Firsching, this is now merged: can you check if it works for you?

[Bulhwi Cha]

I'll test it tomorrow. Thanks!

[Bulhwi Cha]

@Eric Wieser It works great!

[Bulhwi Cha]

I found another problem: doc-gen4 creates duplicate web pages for a Lean file containing a hyphen.

20250227_10h32m57s_doc-gen4.png

▼ TPIL (file)
  ▶ Chapter02
  ▼ Chapter03
      Question03-08
      Question10-14
      «Question03-08»
      «Question10-14»
  ▶ Chapter04
  ▶ Exam

[Eric Wieser]

Do both pages exist?

[Bulhwi Cha]

Yes, they do.

[Eric Wieser]

Or do half of these links not work? (if so, which half?)

[Eric Wieser]

Can you try rm -rf .lake and rebuilding, just to be sure?

[Eric Wieser]

I wonder if you have a mixture of outputs from old and new doc-gen somehow

[Bulhwi Cha]

Let me try removing the .lake subdirectory and rebuilding it.

[Eric Wieser]

If you have a live url you can share it would be much easier to debug

[Bulhwi Cha]

Rebuilding docs fixed the problem!

[Bulhwi Cha]

Now, there's no page whose name contains French double quotation marks.

▼ TPIL (file)
  ▶ Chapter02
  ▼ Chapter03
      Question03-08
      Question10-14
  ▶ Chapter04
  ▶ Exam

[Moritz Firsching]

Thanks @Eric Wieser , the fix also works for me!

[Moritz Firsching]

Just for the record, while the fixed worked for some weird filenames, it didn't fix the problem for filenames which contain "." (except of coure, the last "." in ".lean"). Example repo here: https://github.com/mo271/DocgenTest.

The error is something like:

rc3/lib ././../.lake/packages/doc-gen4/.lake/build/bin/doc-gen4 single --build ././.lake/build DocgenTest.«File.with.dots» file:///home/firsching/DocgenTest/DocgenTest/«File.with.dots».lean
error: no such file or directory (error code: 2)
  file: ././.lake/build/doc/DocgenTest/File.with.dots.html
Some required builds logged failures:
- DocgenTest.«File.with.dots»:docs

[Eric Wieser]

https://github.com/leanprover/doc-gen4/pull/275