Verso template difficulties

Stream: general

[Marx]

Dear maintainers of Verso,

I recently tried to write documentation using verso and ran into a few difficulties that took a while to untangle. I thought it might be helpful to report them, since they seem likely to affect new users.

1. Version mismatch between verso and verso-templates

The README of the verso repository links to verso-templates, but that repository currently appears to use older Lean / Verso versions. When I tried to import (an older version of) mathlib and use something like `Mathlib.Data.Set.Basic, I ran into “unreachable code” errors. I am not sure if it is because of the version mismatch, but this was quite confusing.
Once I updated the verisons, I had the same issue as described in 2.

2. Example projects are not safe to copy verbatim

After realizing that the main verso repository itself contains example projects, I cloned those instead. However, copying the examples verbatim requires renaming DemoTextbook. Otherwise, the build fails with errors like:

 [298/309] Running DemoTextbook
error: DemoTextbook.lean: could not disambiguate the module `DemoTextbook.Meta.Lean`; multiple packages provide distinct definitions:
  textbook (hash: 825556ba2f7f673b)
  verso (hash: 1bea9ae421a13634)

This happens because multiple packages define modules under the DemoTextbook namespace, but this is not obvious from the error message or from the documentation.

Possible improvements

• Keep example projects out of the main verso repository and have the verso-templates for the examples.
• Clearly document that the directories and / or files must be renamed before reuse.

Note: Everything I described happened while trying to set up a textbook/ Manual. I did not try the others.

Thanks for all the work on Verso — once things are set up, it’s a great tool. If i can do anything to assist you, just let me know. I would be happy to help.

[David Thrane Christiansen]

Thanks for the feedback!

I'll get that templates repo updated to this week's Lean release right away, and find a way to make this an automatic part of new Lean version processes.

The contents of test-projects are intended for testing parts of Verso itself while working on it, and I don't think we can take them out of the repository. What would have indicated to you that they weren't intended to be copied and used? In any case, I'll add a README to that effect to the test-projects directory.

I'm glad you got up and going despite the difficulties!

[Marx]

@David Thrane Christiansen Thank you for the answer!
Oh okay, I see! This explains quite a bit. I think i was confusing, that the DemoTextbookfrom the templates looked quite similar and the sentence "To base your own book on it, copy the contents of this directory and add the following files:" in the README of the test-projects/textbookled me to thinking, it was intended to serve as "base" from my own project.

[David Thrane Christiansen]

Once upon a time, they were. Leaving that README was an oversight when I created the verso-templates repository. I'm sorry to have not noticed it - but they are now deleted, the templates repository is up to date, and the other README is added.

Thank you once again for the helpful feedback!

[Marx]

Thank you very much!