doc: add instructions to build documentation (#1645)

Closes #1642

docs/src/.vitepress/config.mts

@@ -132,8 +132,8 @@ export default defineConfig({
               text: 'Developer',
               collapsed: true,
               items: [
-                { text: 'Macros', link: 'manual/developer/macros'},
                 { text: 'Tests', link: 'manual/developer/test'},
+                { text: 'Documentation', link: 'manual/developer/documentation'},
               ]
             }
           ]

docs/src/manual/developer/documentation.md

@@ -0,0 +1,27 @@
+# Documentation
+
+The files for the documentation are located in the
+`docs/src/manual/` directory.
+
+## Adding files to the documentation
+
+To add files to the documentation edit directly the file
+`docs/src/.vitepress/config.mts`.
+
+## Building the documentation
+
+1. Run julia and execute (with Hecke developed in your current environment)
+```julia-repl
+julia> using Hecke
+
+julia> Hecke.build_doc() # or Hecke.build_doc(;doctest = false) to speed things up
+```
+
+2. In the terminal, navigate to `docs/` and run
+```bash
+Hecke/docs> npm run docs:build
+```
+(This step takes place outside of julia.)
+
+!!! note
+    To speed up the development process, step 1 can be repeated within the same julia session.

src/Hecke.jl

@@ -787,11 +787,10 @@ function build_doc(; doctest=false, strict=false, format=:vitepress)
   if format == :html
     open_doc()
   elseif format == :vitepress
-    println("""Run `mkdocs serve` inside `../Hecke/docs/` to view the documentation.
-
-            Use `format = :html` for a simplified version of the docs which does
-            not require `mkdocs`.
+    println("""Run `npm run docs:dev` inside `../Hecke/docs/` to view the documentation.
             """)
+  else
+    error("format :$(format) not recognized")
   end
 end