chore(*): warning box about Lean2

01_Introduction.org

@@ -3,6 +3,12 @@
 
 * Introduction
 
+#+begin_warning
+Please note that this is the tutorial for [[https://github.com/leanprover/lean2][Lean2]], which allows the use of
+homotopy type theory (HoTT). It is /not/ the [[https://leanprover.github.io/introduction_to_lean][tutorial]] for the
+[[https://github.com/leanprover/lean][current version of Lean]].
+#+end_warning
+
 ** Computers and Theorem Proving
 
 /Formal verification/ involves the use of logical and computational
@@ -84,12 +90,6 @@ is more flexible in other ways, too. It comes with an Emacs mode that
 offers powerful support for writing and debugging proofs, and is much
 better suited for serious use.
 
-At this moment, the active development branch for Lean does not support
-homotopy type theory. The tutorial you are reading now is for the Lean
-snapshot which has been preserved for working in homotopy type theory.
-The tutorial for the active development branch can be found at
-[[https://leanprover.github.io/theorem_proving_in_lean/]].
-
 ** About this Book
 
 This book is designed to teach you to develop and verify proofs in

README.md

@@ -6,7 +6,7 @@ Lean Tutorial
  - Web : https://leanprover.github.io/tutorial
  - PDF : https://leanprover.github.io/tutorial/tutorial.pdf
 
-Please note that this is the tutorial for the snapshot of Lean which allows the use of homotopy type theory. It is /not/ the [[https://github.com/leanprover/introduction_to_lean][tutorial]] for the [[https://github.com/leanprover/lean][active development branch]].
+Please note that this is the tutorial for [Lean2](https://github.com/leanprover/lean2), which allows the use of homotopy type theory (HoTT). It is /not/ the [tutorial](https://leanprover.github.io/introduction_to_lean) for the [current version of Lean](https://github.com/leanprover/lean).
 
 How to Build
 ------------

css/tutorial.css

@@ -289,6 +289,18 @@ button::-moz-focus-inner {
   padding: 0;
   border: 0;
 }
+.warning {
+  padding: 15px;
+  margin-bottom: 20px;
+  border: 1px solid transparent;
+  border-radius: 4px;
+  background-color: #fcf8e3;
+  border-color: #faebcc;
+  color: #8a6d3b;
+}
+.warning > p {
+    margin: 0;
+}
 
 .org-src-container {
     margin-bottom: 15px;
@@ -337,4 +349,4 @@ pre.src.src-text {
 }
 fieldset {
     border:0;
-}
+}

header/latex.tex

@@ -42,6 +42,14 @@
     citecolor=Periwinkle
 }
 
+% warning box
+\usepackage{mdframed}
+\definecolor{warningborder}{HTML}{FAEBCC}
+\definecolor{warning}{HTML}{FCF8E3}
+\newenvironment{warning}{%
+  \begin{mdframed}[backgroundcolor=warning,linecolor=warningborder]%
+}{\end{mdframed}}
+
 \usepackage[acronym,toc]{glossaries}
 \include{Glossary}
 \makeglossaries