Merge pull request #408 from Michael-F-Bryan/book-linkcheck

Enabled the link checker

Author: nikomatsakis

.github/workflows/ci.yml

@@ -35,6 +35,13 @@ jobs:
       - name: Install mdbook
         run: cd book && curl -L https://github.com/rust-lang/mdBook/releases/download/v0.3.5/mdbook-v0.3.5-x86_64-unknown-linux-gnu.tar.gz | tar xz
 
+      - name: Install mdbook-linkcheck
+        run: |
+          cd book
+          curl -L https://github.com/Michael-F-Bryan/mdbook-linkcheck/releases/download/v0.5.0/mdbook-linkcheck-v0.5.0-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          # Add the book directory to the $PATH
+          echo "::add-path::$GITHUB_WORKSPACE/book"
+
       - name: Execute tests for Chalk book
         run: cd book && ./mdbook test
 

book/book.toml

@@ -3,3 +3,8 @@ authors = []
 language = "en"
 multilingual = false
 src = "src"
+
+[output.html]
+
+[output.linkcheck]
+follow-web-links = true

book/src/engine/logic/coinduction.md

@@ -95,13 +95,6 @@ This is true for all `A, B`
 * When all subgoals have been tested, and there are remaining delayed co-inductive subgoals, this is propogated up, marking the current `Strand` as co-inductive
 * When the co-inductive `Strand`s reach the root table, we only then pursue an answer
 
-### Failing tests
-
-* Tests were added for the tricky cases above:
-    * [First](https://github.com/rust-lang/chalk/pull/272/commits/7be2d42c6ea36dd4416774d6872c43e3988f05bd#diff-721709466568566f24fc2e8634c40dcbR140)
-    * [Second](https://github.com/rust-lang/chalk/pull/272/commits/7be2d42c6ea36dd4416774d6872c43e3988f05bd#diff-721709466568566f24fc2e8634c40dcbR171)
-* Both *are* provable to have no solutions, but are returned as ambiguous
-
 ## Niko's proposed solution
 
 ### High-level idea