Link constants to corresponding docgen

.github/workflows/build_book.yml

@@ -49,7 +49,7 @@ jobs:
 
       - name: Build book
         run: |
-          ~/.elan/bin/lake exe analysis-book
+          ~/.elan/bin/lake exe analysis-book --docgen-url "https://teorth.github.io/analysis/docs/"
       - name: Copy docs to analysis-book
         run: |
           cp -r ../analysis/.lake/build/doc _site/docs

CONTRIBUTING.md

@@ -13,7 +13,7 @@ lake exe Analysis:docs
 Change the working directory to `./book/`
 Build:
 ```
-lake exe analysis-book
+lake exe analysis-book --docgen-url "http://localhost:8000/analysis/docs/"
 ```
 
 View the book:

README.md

@@ -107,8 +107,9 @@ To build the project's web page after [installing Lean](https://www.lean-lang.or
 % lake build
 % cd ../
 % cd book/
-% lake exe analysis-book
+% lake exe analysis-book --docgen-url="<url>"
 % cd ../
 ```
+where `<url>` is `http://localhost:8000/analysis/docs` for the local setup. 
 
 After this, `book/_site/` contains the project's web page.

book/lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "56d79b34f49586d95ac0a7c3d71f1342469d025d",
+   "rev": "36c5e5f804a3e3af661f550380628b037dcd5b08",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "analysis",