All of the Agda files are now .lagda.md so can be converted to HTML via Agda's formatter and a Markdown processor. The script in the repo under nix/plutus-metatheory-site.nix has a working processes to do this.
We would like this to be run as part of the commit/CI process and present the resulting HTML somewhere static that can be referenced from the general Plutus documentation.
Describe the feature you'd like
All of the Agda files are now
.lagda.mdso can be converted to HTML via Agda's formatter and a Markdown processor. The script in the repo undernix/plutus-metatheory-site.nixhas a working processes to do this.We would like this to be run as part of the commit/CI process and present the resulting HTML somewhere static that can be referenced from the general Plutus documentation.
Describe alternatives you've considered
No response