agda-web.github.io/index.html at master · agda-web/agda-web.github.io · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
<!DOCTYPE html>
<head>
  <meta charset="utf-8">
  <meta name="color-scheme" content="light dark">
  <meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes">
  <title>Agda Web</title>
  <link rel="stylesheet" href="/github-markdown.css">
  <style>
    body, html {
      box-sizing: border-box;
    }

    *, *:before, *:after {
      box-sizing: inherit;
    }

    .markdown-body {
      box-sizing: border-box;
      line-height: 1.5;
      min-width: 200px;
      max-width: 80ex;
      padding: 45px;
      margin-top: 56px;
      margin-left: auto;
      margin-right: auto;
    }
  </style>
</head>

<div class="markdown-body">
  <h1>agda-web</h1>

  <p>A stub page for the <a href="https://github.com/agda-web">Agda Web</a> project. Our aim is to be able to run an interactive session of Agda the proof assistant in a browser, powered by GHC's <a href="https://gitlab.haskell.org/haskell-wasm/ghc-wasm-meta">WebAssembly backend</a>.</p>

  <p>Useful links:</p>

  <ul>
    <li>An experimental <a href="https://agda-web.github.io/als-demo/">PoC on Agda Language Server</a>.
    <li><a href="https://github.com/agda-web/agda-wasm-dist">Distributions</a> of Agda executable compiled into WebAssembly, for Agda version 2.6.4.3 through 2.8.0. It includes an alternative setup script, written in Python, to the GHC-WASM backend. See <a href="https://github.com/agda-web/agda">what patch looks like</a>.
    <li>A <a href="https://github.com/agda-web/plfa.github.io">fork</a> of PLFA that can be evaluated in a browser page via <a href="https://vscode.dev/github/agda-web/plfa.github.io" rel="nofollow">vscode.dev</a> or <a href="https://github.dev/agda-web/plfa.github.io" rel="nofollow">github.dev</a>. Self-hosted version is work in progress.
    <li>A <a href="https://agda-web.github.io/lsp-spec/">dark-theme-friendly version of LSP Spec</a> generated via Pandoc.
  </ul>
</div>