question: can we use verso by simply adding require verso to the lakefile?

[Seasawher]

I would like to ask a question about how users can use verso to write documents.

1A. When a user tries to write a document using the verso, do they need to clone the verso code and add their articles to a specific directory ?

2A. Can the verso syntax and commands for outputting HTML be made available simply by adding a dependency on verso to the lakefile?

2A would be more user-friendly; if not 2A, is it possible to make it like 2A?

I apologise if I have been careless and have missed the written explanation.

[david-christiansen]

No, there's no explanation yet to miss :-)

One difference between Verso and most documentation tools is that Verso isn't really a tool per se - it's a library for building a documentation tool that closely integrates with Lean. This is because different kinds of documents have different needs, and no single tool will serve them all well - mdbook would be a poor fit for blogging, for instance.

The way you'll use Verso, once it makes a bit more progress, is to pick one of the tools implemented with it and then follow that tool's instructions. For now, there's an examples directory that you can refer to, but things are still in flux and not quite ready for general use.