iris-lean docs

Stream: iris-lean

[Oliver Soeser]

I made a documentation page for iris-lean: https://www.oliversoeser.com/iris-lean/

[Oliver Soeser]

At the moment I need to manually compile it with every new iris-lean version, but I'll look into automating that sometime soon

[Shreyas Srinivas]

I think you can add the doc-gen package and have CI do it for you

[Markus de Medeiros]

Much appreciated!

[Markus de Medeiros]

Shreyas Srinivas said:

I think you can add the doc-gen package and have CI do it for you

Ya, we got this working in SampCert Yes we got this running in SampCert here

[Shreyas Srinivas]

Oliver Soeser said:

I made a documentation page for iris-lean: https://www.oliversoeser.com/iris-lean/

Thanks btw. One thing that clearly emerges from this is that we don't have enough docstrings on our definitions and theorems. @Markus de Medeiros : this could be a good first contributor issue.

[Shreyas Srinivas]

I don't think even the original iris has def-by-def or theorem-by-theorem documentation.

[Oliver Soeser]

Yes definitely, there are hardly any docstrings and that makes it very difficult to understand