408 lines
25 KiB
HTML
408 lines
25 KiB
HTML
<!DOCTYPE html>
|
||
<html lang="en"><head>
|
||
<meta charset="utf-8">
|
||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||
<meta name="viewport" content="width=device-width, initial-scale=1">
|
||
<title>Getting Started | Programming Language Foundations in Agda
|
||
</title><!-- Begin Jekyll SEO tag v2.6.1 -->
|
||
<meta name="generator" content="Jekyll v3.9.0" />
|
||
<meta property="og:title" content="Getting Started" />
|
||
<meta property="og:locale" content="en_US" />
|
||
<meta name="description" content="Programming Language Foundations in Agda" />
|
||
<meta property="og:description" content="Programming Language Foundations in Agda" />
|
||
<link rel="canonical" href="https://plfa.github.io/20.07/GettingStarted/" />
|
||
<meta property="og:url" content="https://plfa.github.io/20.07/GettingStarted/" />
|
||
<meta property="og:site_name" content="Programming Language Foundations in Agda" />
|
||
<script type="application/ld+json">
|
||
{"url":"https://plfa.github.io/20.07/GettingStarted/","headline":"Getting Started","description":"Programming Language Foundations in Agda","@type":"WebPage","@context":"https://schema.org"}</script>
|
||
<!-- End Jekyll SEO tag -->
|
||
<link rel="stylesheet" href="/20.07/assets/main.css"></head>
|
||
<body><header class="site-header" role="banner">
|
||
|
||
<div class="wrapper">
|
||
|
||
<a class="site-title" href="/20.07/">Programming Language Foundations in Agda
|
||
</a>
|
||
|
||
<nav class="site-nav">
|
||
<span class="menu-icon">
|
||
<svg viewBox="0 0 18 15" width="18px" height="15px">
|
||
<path fill="#424242" d="M18,1.484c0,0.82-0.665,1.484-1.484,1.484H1.484C0.665,2.969,0,2.304,0,1.484l0,0C0,0.665,0.665,0,1.484,0 h15.031C17.335,0,18,0.665,18,1.484L18,1.484z"/>
|
||
<path fill="#424242" d="M18,7.516C18,8.335,17.335,9,16.516,9H1.484C0.665,9,0,8.335,0,7.516l0,0c0-0.82,0.665-1.484,1.484-1.484 h15.031C17.335,6.031,18,6.696,18,7.516L18,7.516z"/>
|
||
<path fill="#424242" d="M18,13.516C18,14.335,17.335,15,16.516,15H1.484C0.665,15,0,14.335,0,13.516l0,0 c0-0.82,0.665-1.484,1.484-1.484h15.031C17.335,12.031,18,12.696,18,13.516L18,13.516z"/>
|
||
</svg>
|
||
</span>
|
||
|
||
<div class="trigger">
|
||
<a class="page-link" href="/20.07/">The Book</a>
|
||
<a class="page-link" href="/20.07/Announcements/">Announcements</a>
|
||
<a class="page-link" href="/20.07/GettingStarted/">Getting Started</a>
|
||
<a class="page-link" href="/20.07/Citing/">Citing</a>
|
||
<a class="page-link" href="https://agda-zh.github.io/PLFA-zh/">中文</a>
|
||
</div>
|
||
</nav>
|
||
|
||
</div>
|
||
|
||
</header>
|
||
<main class="page-content" aria-label="Content">
|
||
<div class="wrapper">
|
||
<article class="post">
|
||
|
||
<header class="post-header">
|
||
<h1 class="post-title">Getting Started</h1>
|
||
</header>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
|
||
|
||
|
||
|
||
</p>
|
||
|
||
|
||
<div class="post-content">
|
||
<!-- Links -->
|
||
|
||
<!-- Status & Version Badges -->
|
||
|
||
<p><a href="https://travis-ci.org/plfa/plfa.github.io"><img src="https://travis-ci.org/plfa/plfa.github.io.svg?branch=dev" alt="Build Status" /></a>
|
||
<a href="https://github.com/agda/agda/releases/tag/v2.6.0.1"><img src="https://img.shields.io/badge/agda-v2.6.0.1-blue.svg" alt="Agda" /></a>
|
||
<a href="https://github.com/agda/agda-stdlib/releases/tag/v1.1"><img src="https://img.shields.io/badge/agda--stdlib-v1.1-blue.svg" alt="agda-stdlib" /></a></p>
|
||
|
||
<h1 id="getting-started-with-plfa">Getting Started with PLFA</h1>
|
||
|
||
<h2 id="dependencies-for-users">Dependencies for users</h2>
|
||
|
||
<p>You can read PLFA <a href="http://plfa.inf.ed.ac.uk">online</a> without installing anything.
|
||
However, if you wish to interact with the code or complete the exercises, you need several things:</p>
|
||
|
||
<ul>
|
||
<li><a href="https://github.com/agda/agda/releases/tag/v2.6.0.1">Agda</a></li>
|
||
<li><a href="https://github.com/agda/agda-stdlib/releases/tag/v1.1">Agda standard library</a></li>
|
||
<li><a href="https://github.com/plfa/plfa.github.io/archive/dev.zip">PLFA</a></li>
|
||
</ul>
|
||
|
||
<p>PLFA is tested against specific versions of Agda and the standard library, which are shown in the badges above. Agda and the standard library change rapidly, and these changes often break PLFA, so using older or newer versions usually causes problems.</p>
|
||
|
||
<h3 id="installing-agda-using-stack">Installing Agda using Stack</h3>
|
||
|
||
<p>The easiest way to install any specific version of Agda is using <a href="https://docs.haskellstack.org/en/stable/README/">Stack</a>. You can get the required version of Agda from GitHub, either by cloning the repository and switching to the correct branch, or by downloading <a href="https://github.com/agda/agda/releases/tag/v2.6.0.1">the zip archive</a>:</p>
|
||
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>git clone https://github.com/agda/agda.git
|
||
<span class="nb">cd </span>agda
|
||
git checkout v2.6.0.1
|
||
</code></pre></div></div>
|
||
<p>To install Agda, run Stack from the Agda source directory:</p>
|
||
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>stack <span class="nb">install</span> <span class="nt">--stack-yaml</span> stack-8.6.5.yaml
|
||
</code></pre></div></div>
|
||
<p>If you want Stack to use you system installation of GHC, you can pass the <code class="language-plaintext highlighter-rouge">--system-ghc</code> flag and select the appropriate <code class="language-plaintext highlighter-rouge">stack-*.yaml</code> file. For instance, if you have GHC 8.2.2 installed, run:</p>
|
||
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>stack <span class="nb">install</span> <span class="nt">--system-ghc</span> <span class="nt">--stack-yaml</span> stack-8.2.2.yaml
|
||
</code></pre></div></div>
|
||
|
||
<h3 id="installing-the-standard-library-and-plfa">Installing the Standard Library and PLFA</h3>
|
||
|
||
<p>You can get the required version of the Agda standard library from GitHub, either by cloning the repository and switching to the correct branch, or by downloading <a href="https://github.com/agda/agda-stdlib/releases/tag/v1.1">the zip archive</a>:</p>
|
||
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>git clone https://github.com/agda/agda-stdlib.git
|
||
<span class="nb">cd </span>agda-stdlib
|
||
git checkout v1.1
|
||
</code></pre></div></div>
|
||
<p>You can get the latest version of Programming Language Foundations in Agda from GitHub, either by cloning the repository, or by downloading <a href="https://github.com/plfa/plfa.github.io/archive/dev.zip">the zip archive</a>:</p>
|
||
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>git clone https://github.com/plfa/plfa.github.io
|
||
</code></pre></div></div>
|
||
<p>Finally, we need to let Agda know where to find the standard library. For this, you can follow the instructions <a href="https://agda.readthedocs.io/en/v2.6.0.1/tools/package-system.html#example-using-the-standard-library">here</a>.</p>
|
||
|
||
<p>It is possible to set up PLFA as an Agda library as well. If you want to complete the exercises found in the <code class="language-plaintext highlighter-rouge">courses</code> folder, or to import modules from the book, you need to do this. To do so, add the path to <code class="language-plaintext highlighter-rouge">plfa.agda-lib</code> to <code class="language-plaintext highlighter-rouge">~/.agda/libraries</code> and add <code class="language-plaintext highlighter-rouge">plfa</code> to <code class="language-plaintext highlighter-rouge">~/.agda/defaults</code>, both on lines of their own.</p>
|
||
|
||
<h2 id="setting-up-and-using-emacs">Setting up and using Emacs</h2>
|
||
|
||
<p>The recommended editor for Agda is Emacs with <code class="language-plaintext highlighter-rouge">agda-mode</code>. Agda ships with <code class="language-plaintext highlighter-rouge">agda-mode</code>, so if you’ve installed Agda, all you have to do to configure <code class="language-plaintext highlighter-rouge">agda-mode</code> is run:</p>
|
||
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>agda-mode setup
|
||
</code></pre></div></div>
|
||
|
||
<p>To load and type-check the file, use <a href="https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html#notation-for-key-combinations"><code class="language-plaintext highlighter-rouge">C-c C-l</code></a>.</p>
|
||
|
||
<p>Agda is edited “interactively, which means that one can type check code which is not yet complete: if a question mark (?) is used as a placeholder for an expression, and the buffer is then checked, Agda will replace the question mark with a “hole” which can be filled in later. One can also do various other things in the context of a hole: listing the context, inferring the type of an expression, and even evaluating an open term which mentions variables bound in the surrounding context.”</p>
|
||
|
||
<p>Agda is edited interactively, using “holes”, which are bits of the program that are not yet filled in. If you use a question mark as an expression, and load the buffer using <code class="language-plaintext highlighter-rouge">C-c C-l</code>, Agda replaces the question mark with a hole. There are several things you can to while the cursor is in a hole:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>C-c C-c x split on variable x
|
||
C-c C-space fill in hole
|
||
C-c C-r refine with constructor
|
||
C-c C-a automatically fill in hole
|
||
C-c C-, goal type and context
|
||
C-c C-. goal type, context, and inferred type
|
||
</code></pre></div></div>
|
||
|
||
<p>See <a href="https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html">the emacs-mode docs</a> for more details.</p>
|
||
|
||
<p>If you want to see messages beside rather than below your Agda code, you can do the following:</p>
|
||
|
||
<ul>
|
||
<li>Open your Agda file, and load it using <code class="language-plaintext highlighter-rouge">C-c C-l</code>;</li>
|
||
<li>type <code class="language-plaintext highlighter-rouge">C-x 1</code> to get only your Agda file showing;</li>
|
||
<li>type <code class="language-plaintext highlighter-rouge">C-x 3</code> to split the window horizontally;</li>
|
||
<li>move your cursor to the right-hand half of your frame;</li>
|
||
<li>type <code class="language-plaintext highlighter-rouge">C-x b</code> and switch to the buffer called “Agda information”.</li>
|
||
</ul>
|
||
|
||
<p>Now, error messages from Agda will appear next to your file, rather than squished beneath it.</p>
|
||
|
||
<h3 id="auto-loading-agda-mode-in-emacs">Auto-loading <code class="language-plaintext highlighter-rouge">agda-mode</code> in Emacs</h3>
|
||
|
||
<p>Since version 2.6.0, Agda has support for literate editing with Markdown, using the <code class="language-plaintext highlighter-rouge">.lagda.md</code> extension. One side-effect of this extension is that most editors default to Markdown editing mode, whereas
|
||
In order to have <code class="language-plaintext highlighter-rouge">agda-mode</code> automatically loaded whenever you open a file ending with <code class="language-plaintext highlighter-rouge">.agda</code> or <code class="language-plaintext highlighter-rouge">.lagda.md</code>, put the following on your Emacs configuration file:</p>
|
||
<div class="language-elisp highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="p">(</span><span class="k">setq</span> <span class="nv">auto-mode-alist</span>
|
||
<span class="p">(</span><span class="nb">append</span>
|
||
<span class="o">'</span><span class="p">((</span><span class="s">"\\.agda\\'"</span> <span class="o">.</span> <span class="nv">agda2-mode</span><span class="p">)</span>
|
||
<span class="p">(</span><span class="s">"\\.lagda.md\\'"</span> <span class="o">.</span> <span class="nv">agda2-mode</span><span class="p">))</span>
|
||
<span class="nv">auto-mode-alist</span><span class="p">))</span>
|
||
</code></pre></div></div>
|
||
|
||
<p>The configuration file for Emacs is normally located in <code class="language-plaintext highlighter-rouge">~/.emacs</code> or <code class="language-plaintext highlighter-rouge">~/.emacs.d/init.el</code>, but Aquamacs users might need to move their startup settings to the <code class="language-plaintext highlighter-rouge">Preferences.el</code> file in <code class="language-plaintext highlighter-rouge">~/Library/Preferences/Aquamacs Emacs/Preferences</code>.</p>
|
||
|
||
<h3 id="using-mononoki-in-emacs">Using mononoki in Emacs</h3>
|
||
|
||
<p>It is recommended that you install the font <a href="https://madmalik.github.io/mononoki/">mononoki</a>, and add the following to the end of your emacs configuration file at <code class="language-plaintext highlighter-rouge">~/.emacs</code>:</p>
|
||
|
||
<div class="language-elisp highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="c1">;; default to mononoki</span>
|
||
<span class="p">(</span><span class="nv">set-face-attribute</span> <span class="ss">'default</span> <span class="no">nil</span>
|
||
<span class="ss">:family</span> <span class="s">"mononoki"</span>
|
||
<span class="ss">:height</span> <span class="mi">120</span>
|
||
<span class="ss">:weight</span> <span class="ss">'normal</span>
|
||
<span class="ss">:width</span> <span class="ss">'normal</span><span class="p">)</span>
|
||
</code></pre></div></div>
|
||
|
||
<h3 id="unicode-characters">Unicode characters</h3>
|
||
|
||
<p>If you’re having trouble typing the Unicode characters into Emacs, the end of each chapter should provide a list of the unicode characters introduced in that chapter.</p>
|
||
|
||
<p><code class="language-plaintext highlighter-rouge">agda-mode</code> and emacs have a number of useful commands. Two of them are especially useful when you solve exercises.</p>
|
||
|
||
<p>For a full list of supported characters, use <code class="language-plaintext highlighter-rouge">agda-input-show-translations</code> with:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>M-x agda-input-show-translations
|
||
</code></pre></div></div>
|
||
|
||
<p>All the supported characters in <code class="language-plaintext highlighter-rouge">agda-mode</code> are shown.</p>
|
||
|
||
<p>If you want to know how you input a specific Unicode character in agda file, move the cursor onto the character and type the following command:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>M-x quail-show-key
|
||
</code></pre></div></div>
|
||
|
||
<p>You’ll see the key sequence of the character in mini buffer.</p>
|
||
|
||
<h2 id="dependencies-for-developers">Dependencies for developers</h2>
|
||
|
||
<p>PLFA is available as both a website and an EPUB e-book,
|
||
both of which can be built on Linux and macOS.
|
||
PLFA is written in literate Agda with <a href="https://kramdown.gettalong.org/syntax.html">Kramdown Markdown</a>.</p>
|
||
|
||
<h3 id="building-the-website">Building the website</h3>
|
||
|
||
<p>The website version of the book is built in three stages:</p>
|
||
|
||
<ol>
|
||
<li>
|
||
<p>The <code class="language-plaintext highlighter-rouge">.lagda.md</code> files are compiled to Markdown using Agda’s highlighter.
|
||
(This requires several POSIX tools, such as <code class="language-plaintext highlighter-rouge">bash</code>, <code class="language-plaintext highlighter-rouge">sed</code>, and <code class="language-plaintext highlighter-rouge">grep</code>.)</p>
|
||
</li>
|
||
<li>
|
||
<p>The Markdown files are converted to HTML using <a href="https://jekyllrb.com/">Jekyll</a>, a widely-used static site builder.
|
||
(This requires <a href="https://www.ruby-lang.org/en/documentation/installation/">Ruby</a> and <a href="https://jekyllrb.com/">Jekyll</a>.)</p>
|
||
</li>
|
||
<li>
|
||
<p>The HTML is checked using <a href="https://github.com/gjtorikian/html-proofer">html-proofer</a>.
|
||
(This requires <a href="https://www.ruby-lang.org/en/documentation/installation/">Ruby</a> and <a href="https://github.com/gjtorikian/html-proofer">html-proofer</a>.)</p>
|
||
</li>
|
||
</ol>
|
||
|
||
<p>Most recent versions of <a href="https://www.ruby-lang.org/en/documentation/installation/">Ruby</a> should work. The easiest way to install <a href="https://jekyllrb.com/">Jekyll</a> and <a href="https://github.com/gjtorikian/html-proofer">html-proofer</a> is using <a href="https://bundler.io/#getting-started">Bundler</a>. You can install <a href="https://bundler.io/#getting-started">Bundler</a> by running:</p>
|
||
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>gem <span class="nb">install </span>bundler
|
||
</code></pre></div></div>
|
||
<p>You can install the remainder of the dependencies—<a href="https://jekyllrb.com/">Jekyll</a>, <a href="https://github.com/gjtorikian/html-proofer">html-proofer</a>, <em>etc.</em>—by running:</p>
|
||
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>bundle <span class="nb">install</span>
|
||
</code></pre></div></div>
|
||
<p>Once you have installed all of the dependencies, you can build a copy of the book, and host it locally, by running:</p>
|
||
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>make build
|
||
make serve
|
||
</code></pre></div></div>
|
||
<p>The Makefile offers more than just these options:</p>
|
||
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>make <span class="c"># see make test</span>
|
||
make build <span class="c"># builds lagda->markdown and the website</span>
|
||
make build-incremental <span class="c"># builds lagda->markdown and the website incrementally</span>
|
||
make <span class="nb">test</span> <span class="c"># checks all links are valid</span>
|
||
make test-offline <span class="c"># checks all links are valid offline</span>
|
||
make serve <span class="c"># starts the server</span>
|
||
make server-start <span class="c"># starts the server in detached mode</span>
|
||
make server-stop <span class="c"># stops the server, uses pkill</span>
|
||
make clean <span class="c"># removes all ~unnecessary~ generated files</span>
|
||
make clobber <span class="c"># removes all generated files</span>
|
||
</code></pre></div></div>
|
||
<p>If you simply wish to have a local copy of the book, e.g. for offline reading, but don’t care about editing and rebuilding the book, you can grab a copy of the <a href="https://github.com/plfa/plfa.github.io/archive/master.zip">master branch</a>, which is automatically built using Travis. You will still need <a href="https://jekyllrb.com/">Jekyll</a> and preferably <a href="https://bundler.io/#getting-started">Bundler</a> to host the book (see above). To host the book this way, download a copy of the <a href="https://github.com/plfa/plfa.github.io/archive/master.zip">master branch</a>, unzip, and from within the directory run</p>
|
||
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>bundle <span class="nb">install
|
||
</span>bundle <span class="nb">exec </span>jekyll serve
|
||
</code></pre></div></div>
|
||
|
||
<h3 id="building-the-epub">Building the EPUB</h3>
|
||
|
||
<p>The EPUB version of the book is built using Pandoc. Here’s how to build the EPUB:</p>
|
||
|
||
<ol>
|
||
<li>
|
||
<p>Install a recent version of Pandoc, <a href="https://pandoc.org/installing.html">available here</a>.
|
||
We recommend their official installer (on the linked page),
|
||
which is much faster than compiling Pandoc from source with Haskell Stack.</p>
|
||
</li>
|
||
<li>
|
||
<p>Build the EPUB by running:</p>
|
||
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>make epub
|
||
</code></pre></div> </div>
|
||
<p>The EPUB is written to <code class="language-plaintext highlighter-rouge">out/epub/plfa.epub</code>.</p>
|
||
</li>
|
||
</ol>
|
||
|
||
</div>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
|
||
|
||
|
||
|
||
</p>
|
||
|
||
|
||
</article>
|
||
|
||
</div>
|
||
</main><footer class="site-footer h-card">
|
||
<data class="u-url" href="/20.07/"></data>
|
||
|
||
<div class="wrapper">
|
||
|
||
<h2 class="footer-heading">Programming Language Foundations in Agda
|
||
</h2><div class="footer-col-wrapper">
|
||
<div class="footer-col footer-col-1">
|
||
<ul class="contact-list">
|
||
<li class="p-name">Philip Wadler</li>
|
||
<li><a class="u-email" href="mailto:wadler@inf.ed.ac.uk">wadler@inf.ed.ac.uk</a></li>
|
||
</ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wadler"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wadler</span></a></li></ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-3"></div>
|
||
</div><div class="footer-col-wrapper">
|
||
<div class="footer-col footer-col-1">
|
||
<ul class="contact-list">
|
||
<li class="p-name">Wen Kokke</li>
|
||
<li><a class="u-email" href="mailto:wen.kokke@ed.ac.uk">wen.kokke@ed.ac.uk</a></li>
|
||
</ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wenkokke"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wenkokke</span></a></li><li><a href="https://www.twitter.com/wenkokke"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">wenkokke</span></a></li></ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-3"></div>
|
||
</div><div class="footer-col-wrapper">
|
||
<div class="footer-col footer-col-1">
|
||
<ul class="contact-list">
|
||
<li class="p-name">Jeremy G. Siek</li>
|
||
<li><a class="u-email" href="mailto:jsiek@indiana.edu">jsiek@indiana.edu</a></li>
|
||
</ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/jsiek"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">jsiek</span></a></li><li><a href="https://www.twitter.com/jeremysiek"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">jeremysiek</span></a></li></ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-3"></div>
|
||
</div>This work is licensed under a <a rel="license" href="https://creativecommons.org/licenses/by/4.0/">Creative Commons Attribution 4.0 International License</a>
|
||
</div>
|
||
</footer>
|
||
<!-- Import jQuery -->
|
||
<script type="text/javascript" src="/20.07/assets/jquery.js"></script>
|
||
|
||
<script src="https://cdnjs.cloudflare.com/ajax/libs/anchor-js/4.2.2/anchor.min.js" integrity="sha256-E4RlfxwyJVmkkk0szw7LYJxuPlp6evtPSBDlWHsYYL8=" crossorigin="anonymous"></script>
|
||
<script type="text/javascript">
|
||
anchors.add();
|
||
</script>
|
||
|
||
<script type="text/javascript">
|
||
|
||
// Makes sandwhich menu works
|
||
$('.menu-icon').click(function(){
|
||
$('.trigger').toggle();
|
||
});
|
||
|
||
// Script which allows for foldable code blocks
|
||
$('div.foldable pre').each(function(){
|
||
var autoHeight = $(this).height();
|
||
var lineHeight = parseFloat($(this).css('line-height'));
|
||
|
||
var plus = $("<div></div>");
|
||
var horLine = $("<div></div>");
|
||
var verLine = $("<div></div>");
|
||
$(this).prepend(plus);
|
||
plus.css({
|
||
'position' : 'relative',
|
||
'float' : 'right',
|
||
'right' : '-' + (0.5 * lineHeight - 1.5) + 'px',
|
||
'width' : lineHeight,
|
||
'height' : lineHeight});
|
||
verLine.css({
|
||
'position' : 'relative',
|
||
'height' : lineHeight,
|
||
'width' : '3px',
|
||
'background-color' : '#C1E0FF'});
|
||
horLine.css({
|
||
'position' : 'relative',
|
||
'top' : '-' + (0.5 * lineHeight + 1.5) + 'px',
|
||
'left' : '-' + (0.5 * lineHeight - 1.5) + 'px',
|
||
'height' : '3px',
|
||
'width' : lineHeight,
|
||
'background-color' : '#C1E0FF'});
|
||
plus.append(verLine);
|
||
plus.append(horLine);
|
||
|
||
$(this).height(2.0 * lineHeight);
|
||
$(this).css('overflow','hidden');
|
||
|
||
$(this).click(function(){
|
||
if ($(this).height() == autoHeight) {
|
||
$(this).height(2.0 * lineHeight);
|
||
plus.show();
|
||
}
|
||
else {
|
||
$(this).height('auto');
|
||
plus.hide();
|
||
}
|
||
});
|
||
});
|
||
</script>
|
||
|
||
<!-- Import KaTeX -->
|
||
<script type="text/javascript" src="/20.07/assets/katex.js"></script>
|
||
|
||
<!-- Script which renders TeX using KaTeX -->
|
||
<script type="text/javascript">
|
||
$("script[type='math/tex']").replaceWith(
|
||
function(){
|
||
var tex = $(this).text();
|
||
return "<span class=\"inline-equation\">" +
|
||
katex.renderToString(tex) +
|
||
"</span>";
|
||
});
|
||
$("script[type='math/tex; mode=display']").replaceWith(
|
||
function(){
|
||
var tex = $(this).text().replace(/%.*?(\n|$)/g,"");
|
||
return "<div class=\"equation\">" +
|
||
katex.renderToString("\\displaystyle "+tex) +
|
||
"</div>";
|
||
});
|
||
</script>
|
||
</body>
|
||
|
||
</html>
|