documentation search failure

Stream: lean4

[Floris van Doorn]

Does anyone know why carleson#ProofData doesn't find https://florisvandoorn.com/carleson/docs/Carleson/Defs.html#ProofData ?

This is the CI file responsible for creating the documentation. Are we doing anything wrong there?

cc @Henrik Böving

[Henrik Böving]

For one I'm a little confused with your setup, you got

name = "docbuild"
version = "0.1.0"
defaultTargets = ["docbuild"]

[[require]]
name = "carleson"
path = "../"

[[require]]
scope = "leanprover"
name = "doc-gen4"
# Use revision v4.x if you are developing against a stable Lean version.
rev = "main"

which doesn't contain the

packagesDir = "../.lake/packages"

line from the documentation that makes sure you share build artefacts, so building your documentation currently recompiles mathlib? Where are the CI jobs that build the documentation for your project? They should certainly be timing out or just straight up taking hours

[Pietro Monticone]

We are still using the previous setup with the symlinks. I'll update it as soon as I find the time.

[Pietro Monticone]

Done.