Zulip Chat Archive
Stream: new members
Topic: Problem when generating html using Verso
Ilmārs Cīrulis (Dec 10 2025 at 01:04):
When trying to generate a HTML file from Lean file (using Verso) I get such error.
lake exe verso-html .lake/build/literate html
uncaught exception: no such file or directory (error code: 2)
file: html\-verso-search\../../../static-web/search\fuzzysort.d.ts
I'm following instructions from here. Everything else up to this point was okay.
Last updated: Dec 20 2025 at 21:32 UTC