coqdocjs icon indicating copy to clipboard operation
coqdocjs copied to clipboard

Using with dune

Open dlesbre opened this issue 1 year ago • 0 comments

Thanks for this nice addition which renders some very nice documentation.

I've been trying to use it with the dune build system since its gradually becoming more popular among the community. Here are the tricks I had to do to get it working:

  • Add the following to any coq-theory stanza to run coqdocjs
     (coqdoc_flags 
        :standard --toc --toc-depth 2 --interpolate --index indexpage --no-lib-name
        --with-header ../../../../../coqdocjs/header.html
        --with-footer ../../../../../coqdocjs/footer.html)
    
  • Add the following stanza in any dune file
    (copy_files
     (files ../coqdocjs/resources/*)
     (alias doc))
    
  • modify the header.html file by prepending ../../coqdocjs/ to all links to ressources files.

Obviously this solution is quite brittle since it hard-codes paths in dune files so it won't work with different number of sub-directories, but its the best I can do with my limited knowledge of dune. One good point is that building the doc dune build @doc will raise errors if the paths are invalid so its easy to get them right by trial and error (well, except for the links in the header.html file)

Note that this is designed for browsing the documentation directly in _build/default/theories/<name>.html/. For deploying the documentation though, I'd advise only doing the first of the above steps and copying the resource files manually.

For reference, my repository looks like this:

.
├── coqdocjs
│   ├── resources
│   │   ├── config.js
│   │   ├── coqdoc.css
│   │   ├── coqdocjs.css
│   │   └── coqdocjs.js
│   ├── footer.html
│   └── header.html
├── theories
│   ├── a bunch of .v files
│   └── dune
└── dune-project

dlesbre avatar Aug 06 '24 15:08 dlesbre