check-yaml exception: unknown module prefix 'Archive'

Stream: mathlib4

[Maja Kądziołka]

I'm trying to run check-yaml locally, and I'm getting the following issue:

~/dev/mathlib4$ lake exe check-yaml
uncaught exception: unknown module prefix 'Archive'

No directory 'Archive' or file 'Archive.olean' in the search path entries:
././.lake/packages/Cli/.lake/build/lib/lean
././.lake/packages/batteries/.lake/build/lib/lean
././.lake/packages/Qq/.lake/build/lib/lean
././.lake/packages/aesop/.lake/build/lib/lean
././.lake/packages/proofwidgets/.lake/build/lib/lean
././.lake/packages/importGraph/.lake/build/lib/lean
././.lake/packages/LeanSearchClient/.lake/build/lib/lean
././.lake/packages/plausible/.lake/build/lib/lean
././.lake/build/lib/lean
/home/mei/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean
/home/mei/.elan/toolchains/leanprover--lean4---v4.19.0-rc2/lib/lean

moreover, when I try running lake exe cache get, this happens:

~/dev/mathlib4$ lean exe cache get
Expected exactly one file name
Lean (version 4.19.0-rc2, x86_64-unknown-linux-gnu, commit fafd381c9059, Release)
Miscellaneous:
  -h, --help             display this message
      --features         display features compiler provides (eg. LLVM support)
[etcetc]

what gives?

[Kevin Buzzard]

For the latter question: lake exe... not lean exe....

[Maja Kądziołka]

oh, right, typo on that front >.<

[Maja Kądziołka]

my mental hash function of "first letter of name + length + vague purpose" got a collision i think

[Maja Kądziołka]

now cache get completes successfully and check-yaml fails just as before

[Kevin Buzzard]

For the former, I can confirm that I get the same error as you running lake exe check-yaml in mathlib, so perhaps that's not what you're supposed to do (I know nothing about check-yaml)

[Maja Kądziołka]

the CI gives a different error that isn't very descriptive either: https://github.com/leanprover-community/mathlib4/actions/runs/14317787908/job/40127784545?pr=23801

[Maja Kądziołka]

I guess I'll poke at the Python...

[Maja Kądziołka]

not sure where I got lake exe check-yaml into my mind because apparently that's not supposed to work without first having a Python script convert the yaml to json

[Bryan Gin-ge Chen]

The CI run is probably hitting this check. I'd have to do some more digging to be sure, but I suspect that the check is there since our website can't render a YAML file with nesting > 3.

[Maja Kądziołka]

It can, undergrad.yaml uses that possibility

[Maja Kądziołka]

for example here:
image.png

[Maja Kądziołka]

pretty sure they're rendered by the same template

[Maja Kądziołka]

the thing I want to do is have it list "computable function ([in terms of general recursive functions], [in terms of Turing machines])"

[Bryan Gin-ge Chen]

They're different templates: here's the one for the overview and here's the one for the undergrad page.

[Bryan Gin-ge Chen]

If you'd like to PR a corresponding change to the overview template to support what you want, I'd be happy to review it!

[Maja Kądziołka]

WIP at https://github.com/leanprover-community/leanprover-community.github.io/pull/616, any idea/hints on how to test this with the data from my mathlib PR?

[Maja Kądziołka]

gah why is it not doing CI

[Kevin Buzzard]

I don't know about that repo but for mathlib CI only functions correctly if the PR is from a branch (rather than a fork).

[Maja Kądziołka]

should I have repo access for that repo as well?

[Ruben Van de Velde]

No, the website repo uses forks

[Ruben Van de Velde]

But I also don't know if many people look at it

[Maja Kądziołka]

okay, i think i got it to build locally

[Maja Kądziołka]

Bryan Gin-ge Chen said:

If you'd like to PR a corresponding change to the overview template to support what you want, I'd be happy to review it!

It was a bit cumbersome due to the sluggish build process, but I managed to test my changes and they're ready for review: https://github.com/leanprover-community/leanprover-community.github.io/pull/616

[Bryan Gin-ge Chen]

Thanks! I'll try to take a look this week.