From 2a35c0f49bd97ef4c67a4caa03588dc80f4c09bd Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 23 Feb 2016 14:23:47 +0100
Subject: [PATCH] feat(script): add .md link checker script

---
 doc/make/split-stack.md  |  2 +-
 script/check_md_links.py | 71 ++++++++++++++++++++++++++++++++++++++++
 src/emacs/README.md      |  2 +-
 3 files changed, 73 insertions(+), 2 deletions(-)
 create mode 100755 script/check_md_links.py

diff --git a/doc/make/split-stack.md b/doc/make/split-stack.md
index 9ea85426e..e39b400bc 100644
--- a/doc/make/split-stack.md
+++ b/doc/make/split-stack.md
@@ -13,7 +13,7 @@ with libraries that do not. However, it did not work in our experiments.
 To be able to compile Lean with split-stacks, we also have to compile
 GMP, MPFR and Lua using split-stacks.
 
-We also had to use the [gold linker](http://en.wikipedia.org/wiki/Gold_(linker).
+We also had to use the [gold linker](<http://en.wikipedia.org/wiki/Gold_(linker)>).
 
 Gold linker
 -----------
diff --git a/script/check_md_links.py b/script/check_md_links.py
new file mode 100755
index 000000000..9172feeca
--- /dev/null
+++ b/script/check_md_links.py
@@ -0,0 +1,71 @@
+#!/usr/bin/env python
+
+import argparse
+import collections
+import os
+import sys
+import urllib.error
+import urllib.request
+try:
+    import mistune
+except ImportError:
+    print("Mistune package not found. Install e.g. via `pip install mistune`.")
+
+parser = argparse.ArgumentParser(description="Check all *.md files of the current directory's subtree for broken links.")
+parser.add_argument('--http', help="also check external links (can be slow)", action='store_true')
+parser.add_argument('--check-missing', help="also find unreferenced lean files", action='store_true')
+args = parser.parse_args()
+
+lean_root = os.path.join(os.path.dirname(__file__), os.path.pardir)
+lean_root = os.path.normpath(lean_root)
+result = {}
+
+def check_link(link, root):
+    if link.startswith('http'):
+        if not args.http:
+            return True
+        if link not in result:
+            try:
+                urllib.request.urlopen(link)
+                result[link] = True
+            except:
+                result[link] = False
+        return result[link]
+    else:
+        if link.startswith('/'):
+            # project root-relative link
+            path = lean_root + link
+        else:
+            path = os.path.join(root, link)
+
+        path = os.path.normpath(path) # should make it work on Windows
+
+        result[path] = os.path.exists(path)
+        return result[path]
+
+# check all .md files
+for root, _, files in os.walk('.'):
+    for f in files:
+        if not f.endswith('.md'):
+            continue
+
+        path = os.path.join(root, f)
+
+        class CheckLinks(mistune.Renderer):
+            def link(self, link, title, content):
+                if not check_link(link, root):
+                    print("Broken link", link, "in file", path)
+
+        mistune.Markdown(renderer=CheckLinks())(open(path).read())
+
+if args.check_missing:
+    # check all .(h)lean files
+    for root, _, files in os.walk('.'):
+        for f in files:
+            path = os.path.normpath(os.path.join(root, f))
+            if (path.endswith('.lean') or path.endswith('.hlean')) and path not in result:
+                result[path] = False
+                print("Missing file", path)
+
+if not all(result.values()):
+    sys.exit(1)
diff --git a/src/emacs/README.md b/src/emacs/README.md
index ecc5ac6b0..2d64902aa 100644
--- a/src/emacs/README.md
+++ b/src/emacs/README.md
@@ -33,7 +33,7 @@ automatically the first time you use ``lean-mode``, if you follow the
 installation instructions below.
 
 [company]: http://company-mode.github.io/
-[flycheck]: http://flycheck.readthedocs.org/en/latest
+[flycheck]: http://www.flycheck.org/manual/latest/index.html
 [fci]: https://github.com/alpaker/Fill-Column-Indicator
 [lua-mode]: http://immerrr.github.io/lua-mode/
 [mmm-mode]: https://github.com/purcell/mmm-mode