Compare revisions

2d0ce50e · 2a40a0b1 · 2a40a0b1 · 2a40a0b1 · 2a40a0b1 · 2d0ce50e
--- a/frontend/node/src/my_fflate.ts
+++ b/frontend/node/src/my_fflate.ts
-import fs from 'fs';
-import path from 'path';
-import mkdirp from 'mkdirp';
-import { unzipSync } from 'fflate';
-
-
-
-export type UnzipSource = string | ArrayBuffer | Uint8Array;
-
-export type UnzipOptions = {
-    to?: {fs?: typeof fs, directory?: string}
-};
-
-
-export async function unzip(zipfile: UnzipSource, opts?: UnzipOptions | string) {
-    var {to: {directory: odir, fs: ofs}} = options(opts),
-        z = unzipSync(await open(zipfile));
-
-    for (let [relativePath, content] of Object.entries(z)) {
-        var outf = path.join(odir, relativePath);
-        mkdirp.sync(path.dirname(outf), {fs: ofs});
-        ofs.writeFileSync(outf, content);
-    }
-}
-
-async function open(zipfile: UnzipSource) {
-    if (typeof zipfile === 'string') {
-        return fs.readFileSync ? fs.readFileSync(zipfile)
-            : new Uint8Array(await (await fetch(zipfile)).arrayBuffer());
-    }
-    else if (zipfile instanceof ArrayBuffer) {
-        return new Uint8Array(zipfile);
-    }
-    else return zipfile;
-}
-
-function options(opts?: UnzipOptions | string): UnzipOptions {
-    if (opts) {
-        if (typeof opts === 'string') {
-            return {to: {directory: opts, fs}};
-        }
-        else if (opts.to) {
-            if (typeof opts.to === 'string')
-                return {to: {directory: opts.to, fs}};
-            else
-                return {to: {directory: opts.to.directory || '',
-                             fs: opts.to.fs || fs}};
-        }
-    }
-    return {to: {directory: '', fs}};
-}
--- a/index.html
+++ b/index.html
@@ -58,7 +58,7 @@
    </nav>
    <!------------------------------->
  
-  <div id="document">
+  <div id="document" data-filename="index.v">
  <div>
    <h3>Welcome to the <span class="jscoq-name">jsCoq</span> Interactive Online System!</h3>
    <p>
@@ -77,8 +77,8 @@

    <h4>A First Example: <code>rev</code> <code>∘</code> <code>rev = id</code></h4>
    <p>
-      The following is a simple proof that <code>rev</code>, the standard list
-      reversal function as commonly defined in ML and other languages of the
+      The following is a simple proof that <code class="coq-highlight">rev</code>, the standard list
+      reversal function as commonly <code class="cm-s-default coq-highlight">Definition x := 3.</code> defined in ML and other languages of the
      family, is an involution.
    </p>
    <p>
@@ -244,21 +244,19 @@ Qed.</textarea>
  <script type="module">
    import { JsCoq } from './jscoq.js';

-    var sp = new URLSearchParams(location.search);
+    var sp = new URLSearchParams(location.search),
+        ifHas = x => sp.has(x) ? x : undefined;

    if (!localStorage['scratchpad.last_filename'])
        setTimeout(() => document.body.classList.add('welcome'), 1500);

    var jscoq_ids  = ['.snippet'];
    var jscoq_opts = {
-        backend:   sp.get('backend'),
+        backend:   sp.get('backend') ?? ifHas('wa'),
        implicit_libs: false,
        focus: false,
        editor: { mode: { 'company-coq': true } },
-        all_pkgs: ['coq', 'mathcomp', 'equations', 'elpi',
-                   'quickchick', 'software-foundations',
-                   'hahn', 'paco', 'snu-sflib',
-                   'fcsl-pcm', 'htt', 'pnp', 'stdpp', 'iris']
+        all_pkgs: {'./coq-pkgs': ['coq'], './addons/teach/coq-pkgs': ['teach']}
    };

    JsCoq.start(jscoq_ids, jscoq_opts).then(res => {

--- a/jscoq.opam
+++ b/jscoq.opam
@@ -12,6 +12,7 @@ doc:          "https://github.com/jscoq/jscoq#readme"

 depends: [
  "ocaml"               { >= "4.12.0"           }
+  "result"              { >= "1.5"              }
  "dune"                { >= "3.5.0" & < "3.8"  }
  "js_of_ocaml"         { >= "4.0.0" & < "4.1"  }
  "js_of_ocaml-ppx"     { >= "4.0.0" & < "4.1"  }
@@ -22,9 +23,9 @@ depends: [
  "lwt_ppx"             { >= "2.0.1"            }
  # We should just rely on OPAM's serlib but this is still early
  "sexplib"             { >= "v0.14.0"          }
-  "ppx_sexp_conv"       { >= "v0.14.1" & < "v0.15" }
-  "ppx_hash"            { >= "v0.14.0" & < "v0.15" }
-  "ppx_compare"         { >= "v0.14.0" & < "v0.15" }
+  "ppx_sexp_conv"       { >= "v0.14.1" & < "v0.17" }
+  "ppx_hash"            { >= "v0.14.0" & < "v0.17" }
+  "ppx_compare"         { >= "v0.14.0" & < "v0.17" }
  # We build a local, patched Coq, but however it is still a dependency and
  # we could build from the opam-installed setup.
  # "coq"                 { >= "8.13.0" & < "8.14" }

--- a/package-lock.json
+++ b/package-lock.json
 {
  "name": "jscoq",
-  "version": "0.17.0",
+  "version": "0.17.1",
  "lockfileVersion": 2,
  "requires": true,
  "packages": {
    "": {
      "name": "jscoq",
-      "version": "0.17.0",
+      "version": "0.17.1",
      "license": "AGPL-3.0-or-later",
      "dependencies": {
+        "@octokit/core": "^4.2.1",
        "array-equal": "^1.0.0",
        "browser-or-node": "^2.0.0",
        "child-process-promise": "^2.2.1",
@@ -26,7 +27,7 @@
        "proper-lockfile": "^4.1.2",
        "vue": "^2.6.12",
        "vue-context-menu": "^2.0.6",
-        "wacoq-deps": "^0.1.0"
+        "wacoq-deps": "0.1.1"
      },
      "bin": {
        "jscoq": "dist-cli/cli.cjs",
@@ -40,7 +41,7 @@
        "@types/jquery": "^3.5.14",
        "@types/mkdirp": "^1.0.1",
        "@types/mocha": "^10.0.1",
-        "@types/node": "^13.11.1",
+        "@types/node": "^20.4.8",
        "@types/pako": "^2.0.0",
        "assert": "^2.0.0",
        "bootstrap": "^5.2.1",
@@ -703,9 +704,118 @@
      "integrity": "sha512-2lm/1xOg2jifiB0JMlJV7heR2lafy/R7JQ4a0aP36VsCl/w5E7Eck1Q9SI1opzJ1QinFdG5YAVfD2clLqRp8pQ=="
    },
    "node_modules/@ocaml-wasm/4.12--zarith": {
-      "version": "1.12.0-0",
-      "resolved": "https://registry.npmjs.org/@ocaml-wasm/4.12--zarith/-/4.12--zarith-1.12.0-0.tgz",
-      "integrity": "sha512-xTAAVR77m5UTMvfrXIKPpdgKyHLqJlRE6WsuEAu7W5+t5x34VPkyJauuXaRZEq3XG81dTVqIGBw0OKXmiXhXoA=="
+      "version": "1.13.0-0",
+      "resolved": "https://registry.npmjs.org/@ocaml-wasm/4.12--zarith/-/4.12--zarith-1.13.0-0.tgz",
+      "integrity": "sha512-JN/UOsZwR/JdSwGMrOCUfg1YM1yc8izAzKXhj0qnwy9ncwsk/jWv2zJP1zI/Mgj3hirnngc08MN1LHJeQkvreQ=="
+    },
+    "node_modules/@octokit/auth-token": {
+      "version": "3.0.4",
+      "resolved": "https://registry.npmjs.org/@octokit/auth-token/-/auth-token-3.0.4.tgz",
+      "integrity": "sha512-TWFX7cZF2LXoCvdmJWY7XVPi74aSY0+FfBZNSXEXFkMpjcqsQwDSYVv5FhRFaI0V1ECnwbz4j59T/G+rXNWaIQ==",
+      "engines": {
+        "node": ">= 14"
+      }
+    },
+    "node_modules/@octokit/core": {
+      "version": "4.2.4",
+      "resolved": "https://registry.npmjs.org/@octokit/core/-/core-4.2.4.tgz",
+      "integrity": "sha512-rYKilwgzQ7/imScn3M9/pFfUf4I1AZEH3KhyJmtPdE2zfaXAn2mFfUy4FbKewzc2We5y/LlKLj36fWJLKC2SIQ==",
+      "dependencies": {
+        "@octokit/auth-token": "^3.0.0",
+        "@octokit/graphql": "^5.0.0",
+        "@octokit/request": "^6.0.0",
+        "@octokit/request-error": "^3.0.0",
+        "@octokit/types": "^9.0.0",
+        "before-after-hook": "^2.2.0",
+        "universal-user-agent": "^6.0.0"
+      },
+      "engines": {
+        "node": ">= 14"
+      }
+    },
+    "node_modules/@octokit/endpoint": {
+      "version": "7.0.6",
+      "resolved": "https://registry.npmjs.org/@octokit/endpoint/-/endpoint-7.0.6.tgz",
+      "integrity": "sha512-5L4fseVRUsDFGR00tMWD/Trdeeihn999rTMGRMC1G/Ldi1uWlWJzI98H4Iak5DB/RVvQuyMYKqSK/R6mbSOQyg==",
+      "dependencies": {
+        "@octokit/types": "^9.0.0",
+        "is-plain-object": "^5.0.0",
+        "universal-user-agent": "^6.0.0"
+      },
+      "engines": {
+        "node": ">= 14"
+      }
+    },
+    "node_modules/@octokit/endpoint/node_modules/is-plain-object": {
+      "version": "5.0.0",
+      "resolved": "https://registry.npmjs.org/is-plain-object/-/is-plain-object-5.0.0.tgz",
+      "integrity": "sha512-VRSzKkbMm5jMDoKLbltAkFQ5Qr7VDiTFGXxYFXXowVj387GeGNOCsOH6Msy00SGZ3Fp84b1Naa1psqgcCIEP5Q==",
+      "engines": {
+        "node": ">=0.10.0"
+      }
+    },
+    "node_modules/@octokit/graphql": {
+      "version": "5.0.6",
+      "resolved": "https://registry.npmjs.org/@octokit/graphql/-/graphql-5.0.6.tgz",
+      "integrity": "sha512-Fxyxdy/JH0MnIB5h+UQ3yCoh1FG4kWXfFKkpWqjZHw/p+Kc8Y44Hu/kCgNBT6nU1shNumEchmW/sUO1JuQnPcw==",
+      "dependencies": {
+        "@octokit/request": "^6.0.0",
+        "@octokit/types": "^9.0.0",
+        "universal-user-agent": "^6.0.0"
+      },
+      "engines": {
+        "node": ">= 14"
+      }
+    },
+    "node_modules/@octokit/openapi-types": {
+      "version": "18.0.0",
+      "resolved": "https://registry.npmjs.org/@octokit/openapi-types/-/openapi-types-18.0.0.tgz",
+      "integrity": "sha512-V8GImKs3TeQRxRtXFpG2wl19V7444NIOTDF24AWuIbmNaNYOQMWRbjcGDXV5B+0n887fgDcuMNOmlul+k+oJtw=="
+    },
+    "node_modules/@octokit/request": {
+      "version": "6.2.8",
+      "resolved": "https://registry.npmjs.org/@octokit/request/-/request-6.2.8.tgz",
+      "integrity": "sha512-ow4+pkVQ+6XVVsekSYBzJC0VTVvh/FCTUUgTsboGq+DTeWdyIFV8WSCdo0RIxk6wSkBTHqIK1mYuY7nOBXOchw==",
+      "dependencies": {
+        "@octokit/endpoint": "^7.0.0",
+        "@octokit/request-error": "^3.0.0",
+        "@octokit/types": "^9.0.0",
+        "is-plain-object": "^5.0.0",
+        "node-fetch": "^2.6.7",
+        "universal-user-agent": "^6.0.0"
+      },
+      "engines": {
+        "node": ">= 14"
+      }
+    },
+    "node_modules/@octokit/request-error": {
+      "version": "3.0.3",
+      "resolved": "https://registry.npmjs.org/@octokit/request-error/-/request-error-3.0.3.tgz",
+      "integrity": "sha512-crqw3V5Iy2uOU5Np+8M/YexTlT8zxCfI+qu+LxUB7SZpje4Qmx3mub5DfEKSO8Ylyk0aogi6TYdf6kxzh2BguQ==",
+      "dependencies": {
+        "@octokit/types": "^9.0.0",
+        "deprecation": "^2.0.0",
+        "once": "^1.4.0"
+      },
+      "engines": {
+        "node": ">= 14"
+      }
+    },
+    "node_modules/@octokit/request/node_modules/is-plain-object": {
+      "version": "5.0.0",
+      "resolved": "https://registry.npmjs.org/is-plain-object/-/is-plain-object-5.0.0.tgz",
+      "integrity": "sha512-VRSzKkbMm5jMDoKLbltAkFQ5Qr7VDiTFGXxYFXXowVj387GeGNOCsOH6Msy00SGZ3Fp84b1Naa1psqgcCIEP5Q==",
+      "engines": {
+        "node": ">=0.10.0"
+      }
+    },
+    "node_modules/@octokit/types": {
+      "version": "9.3.2",
+      "resolved": "https://registry.npmjs.org/@octokit/types/-/types-9.3.2.tgz",
+      "integrity": "sha512-D4iHGTdAnEEVsB8fl95m1hiz7D5YiRdQ9b/OEb3BYRVwbLsGHcRVPz+u+BgRLNk0Q0/4iZCBqDN96j2XNxfXrA==",
+      "dependencies": {
+        "@octokit/openapi-types": "^18.0.0"
+      }
    },
    "node_modules/@popperjs/core": {
      "version": "2.11.6",
@@ -806,9 +916,9 @@
      "dev": true
    },
    "node_modules/@types/node": {
-      "version": "13.13.51",
-      "resolved": "https://registry.npmjs.org/@types/node/-/node-13.13.51.tgz",
-      "integrity": "sha512-66/xg5I5Te4oGi5Jws11PtNmKkZbOPZWyBZZ/l5AOrWj1Dyw+6Ge/JhYTq/2/Yvdqyhrue8RL+DGI298OJ0xcg==",
+      "version": "20.4.8",
+      "resolved": "https://registry.npmjs.org/@types/node/-/node-20.4.8.tgz",
+      "integrity": "sha512-0mHckf6D2DiIAzh8fM8f3HQCvMKDpK94YQ0DSVkfWTG9BZleYIWudw9cJxX8oCk9bM+vAkDyujDV6dmKHbvQpg==",
      "dev": true
    },
    "node_modules/@types/pako": {
@@ -1359,6 +1469,11 @@
        }
      ]
    },
+    "node_modules/before-after-hook": {
+      "version": "2.2.3",
+      "resolved": "https://registry.npmjs.org/before-after-hook/-/before-after-hook-2.2.3.tgz",
+      "integrity": "sha512-NzUnlZexiaH/46WDhANlyR2bXRopNg4F/zuSA3OpZnllCUgRaOF2znDioDWrmbNVsuZk6l9pMquQB38cfBZwkQ=="
+    },
    "node_modules/big.js": {
      "version": "5.2.2",
      "resolved": "https://registry.npmjs.org/big.js/-/big.js-5.2.2.tgz",
@@ -2221,6 +2336,11 @@
      "integrity": "sha512-bd2L678uiWATM6m5Z1VzNCErI3jiGzt6HGY8OVICs40JQq/HALfbyNJmp0UDakEY4pMMaN0Ly5om/B1VI/+xfQ==",
      "dev": true
    },
+    "node_modules/deprecation": {
+      "version": "2.3.1",
+      "resolved": "https://registry.npmjs.org/deprecation/-/deprecation-2.3.1.tgz",
+      "integrity": "sha512-xmHIy4F3scKVwMsQ4WnVaS8bHOx0DmVwRywosKhaILI0ywMDWPtBSku2HNxRvF7jtwDRsoEwYQSfbxj8b7RlJQ=="
+    },
    "node_modules/detect-libc": {
      "version": "2.0.1",
      "resolved": "https://registry.npmjs.org/detect-libc/-/detect-libc-2.0.1.tgz",
@@ -4508,7 +4628,6 @@
      "version": "2.6.7",
      "resolved": "https://registry.npmjs.org/node-fetch/-/node-fetch-2.6.7.tgz",
      "integrity": "sha512-ZjMPFEfVx5j+y2yF35Kzx5sF7kDzxuDj6ziH4FFbOp87zKDZNx8yExJIb05OGF4Nlt9IHFIMBkRl41VdvcNdbQ==",
-      "dev": true,
      "dependencies": {
        "whatwg-url": "^5.0.0"
      },
@@ -4589,9 +4708,9 @@
      }
    },
    "node_modules/normalize-package-data/node_modules/semver": {
-      "version": "5.7.1",
-      "resolved": "https://registry.npmjs.org/semver/-/semver-5.7.1.tgz",
-      "integrity": "sha512-sauaDf/PZdVgrLTNYHRtpXa1iRiKcaebiKQ1BJdpQlWH2lCvexQdX55snPFyK7QzpudqbCI0qXFfOasHdyNDGQ==",
+      "version": "5.7.2",
+      "resolved": "https://registry.npmjs.org/semver/-/semver-5.7.2.tgz",
+      "integrity": "sha512-cBznnQ9KjJqU67B52RMC65CMarK2600WFnbkcaiwWq3xy/5haFJlshgnpjovMVJ+Hff49d8GEn0b87C5pDQ10g==",
      "dev": true,
      "bin": {
        "semver": "bin/semver"
@@ -5629,9 +5748,9 @@
      }
    },
    "node_modules/semver": {
-      "version": "6.3.0",
-      "resolved": "https://registry.npmjs.org/semver/-/semver-6.3.0.tgz",
-      "integrity": "sha512-b39TBaTSfV6yBrapU89p5fKekE2m/NwnDocOVruQFS1/veMgdzuPcnOM34M6CwxW8jH/lxEa5rBoDeUwu5HHTw==",
+      "version": "6.3.1",
+      "resolved": "https://registry.npmjs.org/semver/-/semver-6.3.1.tgz",
+      "integrity": "sha512-BR7VvDCVHO+q2xBEWskxS6DJE1qRnb7DxzUrogb71CWoSficBxYsiAGd+Kl0mmq/MprG9yArRkyrQxTO6XjMzA==",
      "dev": true,
      "bin": {
        "semver": "bin/semver.js"
@@ -6455,8 +6574,7 @@
    "node_modules/tr46": {
      "version": "0.0.3",
      "resolved": "https://registry.npmjs.org/tr46/-/tr46-0.0.3.tgz",
-      "integrity": "sha512-N3WMsuqV66lT30CrXNbEjx4GEwlow3v6rr4mCcv6prnfwhS01rkgyFdjPNBYd9br7LpXV1+Emh01fHnq2Gdgrw==",
-      "dev": true
+      "integrity": "sha512-N3WMsuqV66lT30CrXNbEjx4GEwlow3v6rr4mCcv6prnfwhS01rkgyFdjPNBYd9br7LpXV1+Emh01fHnq2Gdgrw=="
    },
    "node_modules/traverse-chain": {
      "version": "0.1.0",
@@ -6566,6 +6684,11 @@
        "url": "https://github.com/sponsors/ljharb"
      }
    },
+    "node_modules/universal-user-agent": {
+      "version": "6.0.0",
+      "resolved": "https://registry.npmjs.org/universal-user-agent/-/universal-user-agent-6.0.0.tgz",
+      "integrity": "sha512-isyNax3wXoKaulPDZWHQqbmIx1k2tb9fb3GGDBRxCscfYV2Ch7WxPArBsFEG8s/safwXTT7H4QGhaIkTp9447w=="
+    },
    "node_modules/unordered-array-remove": {
      "version": "1.0.2",
      "resolved": "https://registry.npmjs.org/unordered-array-remove/-/unordered-array-remove-1.0.2.tgz",
@@ -6773,13 +6896,13 @@
      "dev": true
    },
    "node_modules/wacoq-deps": {
-      "version": "0.1.0",
-      "resolved": "https://registry.npmjs.org/wacoq-deps/-/wacoq-deps-0.1.0.tgz",
-      "integrity": "sha512-9QbdAAcGE7J8T5xHhkWqEZhAJnKvCMXBfmZBNh6eYp/6cUunxNa/gvl32te7kWDOfUYxWTe/sRY5CNW6dxa6Rg==",
+      "version": "0.1.1",
+      "resolved": "https://registry.npmjs.org/wacoq-deps/-/wacoq-deps-0.1.1.tgz",
+      "integrity": "sha512-PMSWk0zKEQrNNYDiyAJ/Eb1jcq1psn2Uk5jMbbTHnFP8H7hiNw1QjZvP3P4TblmYaccl1hlI2CrfOrjCzv3zMQ==",
      "dependencies": {
        "@ocaml-wasm/4.12--janestreet-base": "^0.16.0-0",
        "@ocaml-wasm/4.12--num": "^1.4.0-0",
-        "@ocaml-wasm/4.12--zarith": "^1.12.0-0",
+        "@ocaml-wasm/4.12--zarith": "^1.13.0-0",
        "ocaml-wasm": "^4.12.0-0",
        "wasi-kernel": "^0.1.6"
      }
@@ -6995,7 +7118,6 @@
      "version": "5.0.0",
      "resolved": "https://registry.npmjs.org/whatwg-url/-/whatwg-url-5.0.0.tgz",
      "integrity": "sha512-saE57nupxk6v3HY35+jzBwYa0rKSy0XR8JSxZPwgLr7ys0IBzhGviA1/TUGJLmSVqs8pb9AnvICXEuOHLprYTw==",
-      "dev": true,
      "dependencies": {
        "tr46": "~0.0.3",
        "webidl-conversions": "^3.0.0"
@@ -7004,8 +7126,7 @@
    "node_modules/whatwg-url/node_modules/webidl-conversions": {
      "version": "3.0.1",
      "resolved": "https://registry.npmjs.org/webidl-conversions/-/webidl-conversions-3.0.1.tgz",
-      "integrity": "sha512-2JAn3z8AR6rjK8Sm8orRC0h/bcl/DqL7tRPdGZ4I1CjdF+EaMLmYxBHyXuKL849eucPFhvBoxMsflfOb8kxaeQ==",
-      "dev": true
+      "integrity": "sha512-2JAn3z8AR6rjK8Sm8orRC0h/bcl/DqL7tRPdGZ4I1CjdF+EaMLmYxBHyXuKL849eucPFhvBoxMsflfOb8kxaeQ=="
    },
    "node_modules/which": {
      "version": "2.0.2",
@@ -7624,9 +7745,98 @@
      "integrity": "sha512-2lm/1xOg2jifiB0JMlJV7heR2lafy/R7JQ4a0aP36VsCl/w5E7Eck1Q9SI1opzJ1QinFdG5YAVfD2clLqRp8pQ=="
    },
    "@ocaml-wasm/4.12--zarith": {
-      "version": "1.12.0-0",
-      "resolved": "https://registry.npmjs.org/@ocaml-wasm/4.12--zarith/-/4.12--zarith-1.12.0-0.tgz",
-      "integrity": "sha512-xTAAVR77m5UTMvfrXIKPpdgKyHLqJlRE6WsuEAu7W5+t5x34VPkyJauuXaRZEq3XG81dTVqIGBw0OKXmiXhXoA=="
+      "version": "1.13.0-0",
+      "resolved": "https://registry.npmjs.org/@ocaml-wasm/4.12--zarith/-/4.12--zarith-1.13.0-0.tgz",
+      "integrity": "sha512-JN/UOsZwR/JdSwGMrOCUfg1YM1yc8izAzKXhj0qnwy9ncwsk/jWv2zJP1zI/Mgj3hirnngc08MN1LHJeQkvreQ=="
+    },
+    "@octokit/auth-token": {
+      "version": "3.0.4",
+      "resolved": "https://registry.npmjs.org/@octokit/auth-token/-/auth-token-3.0.4.tgz",
+      "integrity": "sha512-TWFX7cZF2LXoCvdmJWY7XVPi74aSY0+FfBZNSXEXFkMpjcqsQwDSYVv5FhRFaI0V1ECnwbz4j59T/G+rXNWaIQ=="
+    },
+    "@octokit/core": {
+      "version": "4.2.4",
+      "resolved": "https://registry.npmjs.org/@octokit/core/-/core-4.2.4.tgz",
+      "integrity": "sha512-rYKilwgzQ7/imScn3M9/pFfUf4I1AZEH3KhyJmtPdE2zfaXAn2mFfUy4FbKewzc2We5y/LlKLj36fWJLKC2SIQ==",
+      "requires": {
+        "@octokit/auth-token": "^3.0.0",
+        "@octokit/graphql": "^5.0.0",
+        "@octokit/request": "^6.0.0",
+        "@octokit/request-error": "^3.0.0",
+        "@octokit/types": "^9.0.0",
+        "before-after-hook": "^2.2.0",
+        "universal-user-agent": "^6.0.0"
+      }
+    },
+    "@octokit/endpoint": {
+      "version": "7.0.6",
+      "resolved": "https://registry.npmjs.org/@octokit/endpoint/-/endpoint-7.0.6.tgz",
+      "integrity": "sha512-5L4fseVRUsDFGR00tMWD/Trdeeihn999rTMGRMC1G/Ldi1uWlWJzI98H4Iak5DB/RVvQuyMYKqSK/R6mbSOQyg==",
+      "requires": {
+        "@octokit/types": "^9.0.0",
+        "is-plain-object": "^5.0.0",
+        "universal-user-agent": "^6.0.0"
+      },
+      "dependencies": {
+        "is-plain-object": {
+          "version": "5.0.0",
+          "resolved": "https://registry.npmjs.org/is-plain-object/-/is-plain-object-5.0.0.tgz",
+          "integrity": "sha512-VRSzKkbMm5jMDoKLbltAkFQ5Qr7VDiTFGXxYFXXowVj387GeGNOCsOH6Msy00SGZ3Fp84b1Naa1psqgcCIEP5Q=="
+        }
+      }
+    },
+    "@octokit/graphql": {
+      "version": "5.0.6",
+      "resolved": "https://registry.npmjs.org/@octokit/graphql/-/graphql-5.0.6.tgz",
+      "integrity": "sha512-Fxyxdy/JH0MnIB5h+UQ3yCoh1FG4kWXfFKkpWqjZHw/p+Kc8Y44Hu/kCgNBT6nU1shNumEchmW/sUO1JuQnPcw==",
+      "requires": {
+        "@octokit/request": "^6.0.0",
+        "@octokit/types": "^9.0.0",
+        "universal-user-agent": "^6.0.0"
+      }
+    },
+    "@octokit/openapi-types": {
+      "version": "18.0.0",
+      "resolved": "https://registry.npmjs.org/@octokit/openapi-types/-/openapi-types-18.0.0.tgz",
+      "integrity": "sha512-V8GImKs3TeQRxRtXFpG2wl19V7444NIOTDF24AWuIbmNaNYOQMWRbjcGDXV5B+0n887fgDcuMNOmlul+k+oJtw=="
+    },
+    "@octokit/request": {
+      "version": "6.2.8",
+      "resolved": "https://registry.npmjs.org/@octokit/request/-/request-6.2.8.tgz",
+      "integrity": "sha512-ow4+pkVQ+6XVVsekSYBzJC0VTVvh/FCTUUgTsboGq+DTeWdyIFV8WSCdo0RIxk6wSkBTHqIK1mYuY7nOBXOchw==",
+      "requires": {
+        "@octokit/endpoint": "^7.0.0",
+        "@octokit/request-error": "^3.0.0",
+        "@octokit/types": "^9.0.0",
+        "is-plain-object": "^5.0.0",
+        "node-fetch": "^2.6.7",
+        "universal-user-agent": "^6.0.0"
+      },
+      "dependencies": {
+        "is-plain-object": {
+          "version": "5.0.0",
+          "resolved": "https://registry.npmjs.org/is-plain-object/-/is-plain-object-5.0.0.tgz",
+          "integrity": "sha512-VRSzKkbMm5jMDoKLbltAkFQ5Qr7VDiTFGXxYFXXowVj387GeGNOCsOH6Msy00SGZ3Fp84b1Naa1psqgcCIEP5Q=="
+        }
+      }
+    },
+    "@octokit/request-error": {
+      "version": "3.0.3",
+      "resolved": "https://registry.npmjs.org/@octokit/request-error/-/request-error-3.0.3.tgz",
+      "integrity": "sha512-crqw3V5Iy2uOU5Np+8M/YexTlT8zxCfI+qu+LxUB7SZpje4Qmx3mub5DfEKSO8Ylyk0aogi6TYdf6kxzh2BguQ==",
+      "requires": {
+        "@octokit/types": "^9.0.0",
+        "deprecation": "^2.0.0",
+        "once": "^1.4.0"
+      }
+    },
+    "@octokit/types": {
+      "version": "9.3.2",
+      "resolved": "https://registry.npmjs.org/@octokit/types/-/types-9.3.2.tgz",
+      "integrity": "sha512-D4iHGTdAnEEVsB8fl95m1hiz7D5YiRdQ9b/OEb3BYRVwbLsGHcRVPz+u+BgRLNk0Q0/4iZCBqDN96j2XNxfXrA==",
+      "requires": {
+        "@octokit/openapi-types": "^18.0.0"
+      }
    },
    "@popperjs/core": {
      "version": "2.11.6",
@@ -7723,9 +7933,9 @@
      "dev": true
    },
    "@types/node": {
-      "version": "13.13.51",
-      "resolved": "https://registry.npmjs.org/@types/node/-/node-13.13.51.tgz",
-      "integrity": "sha512-66/xg5I5Te4oGi5Jws11PtNmKkZbOPZWyBZZ/l5AOrWj1Dyw+6Ge/JhYTq/2/Yvdqyhrue8RL+DGI298OJ0xcg==",
+      "version": "20.4.8",
+      "resolved": "https://registry.npmjs.org/@types/node/-/node-20.4.8.tgz",
+      "integrity": "sha512-0mHckf6D2DiIAzh8fM8f3HQCvMKDpK94YQ0DSVkfWTG9BZleYIWudw9cJxX8oCk9bM+vAkDyujDV6dmKHbvQpg==",
      "dev": true
    },
    "@types/pako": {
@@ -8200,6 +8410,11 @@
      "resolved": "https://registry.npmjs.org/base64-js/-/base64-js-1.5.1.tgz",
      "integrity": "sha512-AKpaYlHn8t4SVbOHCy+b5+KKgvR4vrsD8vbvrbiQJps7fKDTkjkDry6ji0rUJjC0kzbNePLwzxq8iypo41qeWA=="
    },
+    "before-after-hook": {
+      "version": "2.2.3",
+      "resolved": "https://registry.npmjs.org/before-after-hook/-/before-after-hook-2.2.3.tgz",
+      "integrity": "sha512-NzUnlZexiaH/46WDhANlyR2bXRopNg4F/zuSA3OpZnllCUgRaOF2znDioDWrmbNVsuZk6l9pMquQB38cfBZwkQ=="
+    },
    "big.js": {
      "version": "5.2.2",
      "resolved": "https://registry.npmjs.org/big.js/-/big.js-5.2.2.tgz",
@@ -8853,6 +9068,11 @@
      "integrity": "sha512-bd2L678uiWATM6m5Z1VzNCErI3jiGzt6HGY8OVICs40JQq/HALfbyNJmp0UDakEY4pMMaN0Ly5om/B1VI/+xfQ==",
      "dev": true
    },
+    "deprecation": {
+      "version": "2.3.1",
+      "resolved": "https://registry.npmjs.org/deprecation/-/deprecation-2.3.1.tgz",
+      "integrity": "sha512-xmHIy4F3scKVwMsQ4WnVaS8bHOx0DmVwRywosKhaILI0ywMDWPtBSku2HNxRvF7jtwDRsoEwYQSfbxj8b7RlJQ=="
+    },
    "detect-libc": {
      "version": "2.0.1",
      "resolved": "https://registry.npmjs.org/detect-libc/-/detect-libc-2.0.1.tgz",
@@ -10677,7 +10897,6 @@
      "version": "2.6.7",
      "resolved": "https://registry.npmjs.org/node-fetch/-/node-fetch-2.6.7.tgz",
      "integrity": "sha512-ZjMPFEfVx5j+y2yF35Kzx5sF7kDzxuDj6ziH4FFbOp87zKDZNx8yExJIb05OGF4Nlt9IHFIMBkRl41VdvcNdbQ==",
-      "dev": true,
      "requires": {
        "whatwg-url": "^5.0.0"
      }
@@ -10733,9 +10952,9 @@
      },
      "dependencies": {
        "semver": {
-          "version": "5.7.1",
-          "resolved": "https://registry.npmjs.org/semver/-/semver-5.7.1.tgz",
-          "integrity": "sha512-sauaDf/PZdVgrLTNYHRtpXa1iRiKcaebiKQ1BJdpQlWH2lCvexQdX55snPFyK7QzpudqbCI0qXFfOasHdyNDGQ==",
+          "version": "5.7.2",
+          "resolved": "https://registry.npmjs.org/semver/-/semver-5.7.2.tgz",
+          "integrity": "sha512-cBznnQ9KjJqU67B52RMC65CMarK2600WFnbkcaiwWq3xy/5haFJlshgnpjovMVJ+Hff49d8GEn0b87C5pDQ10g==",
          "dev": true
        }
      }
@@ -11531,9 +11750,9 @@
      }
    },
    "semver": {
-      "version": "6.3.0",
-      "resolved": "https://registry.npmjs.org/semver/-/semver-6.3.0.tgz",
-      "integrity": "sha512-b39TBaTSfV6yBrapU89p5fKekE2m/NwnDocOVruQFS1/veMgdzuPcnOM34M6CwxW8jH/lxEa5rBoDeUwu5HHTw==",
+      "version": "6.3.1",
+      "resolved": "https://registry.npmjs.org/semver/-/semver-6.3.1.tgz",
+      "integrity": "sha512-BR7VvDCVHO+q2xBEWskxS6DJE1qRnb7DxzUrogb71CWoSficBxYsiAGd+Kl0mmq/MprG9yArRkyrQxTO6XjMzA==",
      "dev": true
    },
    "serialize-javascript": {
@@ -12189,8 +12408,7 @@
    "tr46": {
      "version": "0.0.3",
      "resolved": "https://registry.npmjs.org/tr46/-/tr46-0.0.3.tgz",
-      "integrity": "sha512-N3WMsuqV66lT30CrXNbEjx4GEwlow3v6rr4mCcv6prnfwhS01rkgyFdjPNBYd9br7LpXV1+Emh01fHnq2Gdgrw==",
-      "dev": true
+      "integrity": "sha512-N3WMsuqV66lT30CrXNbEjx4GEwlow3v6rr4mCcv6prnfwhS01rkgyFdjPNBYd9br7LpXV1+Emh01fHnq2Gdgrw=="
    },
    "traverse-chain": {
      "version": "0.1.0",
@@ -12276,6 +12494,11 @@
        "which-boxed-primitive": "^1.0.2"
      }
    },
+    "universal-user-agent": {
+      "version": "6.0.0",
+      "resolved": "https://registry.npmjs.org/universal-user-agent/-/universal-user-agent-6.0.0.tgz",
+      "integrity": "sha512-isyNax3wXoKaulPDZWHQqbmIx1k2tb9fb3GGDBRxCscfYV2Ch7WxPArBsFEG8s/safwXTT7H4QGhaIkTp9447w=="
+    },
    "unordered-array-remove": {
      "version": "1.0.2",
      "resolved": "https://registry.npmjs.org/unordered-array-remove/-/unordered-array-remove-1.0.2.tgz",
@@ -12445,13 +12668,13 @@
      "dev": true
    },
    "wacoq-deps": {
-      "version": "0.1.0",
-      "resolved": "https://registry.npmjs.org/wacoq-deps/-/wacoq-deps-0.1.0.tgz",
-      "integrity": "sha512-9QbdAAcGE7J8T5xHhkWqEZhAJnKvCMXBfmZBNh6eYp/6cUunxNa/gvl32te7kWDOfUYxWTe/sRY5CNW6dxa6Rg==",
+      "version": "0.1.1",
+      "resolved": "https://registry.npmjs.org/wacoq-deps/-/wacoq-deps-0.1.1.tgz",
+      "integrity": "sha512-PMSWk0zKEQrNNYDiyAJ/Eb1jcq1psn2Uk5jMbbTHnFP8H7hiNw1QjZvP3P4TblmYaccl1hlI2CrfOrjCzv3zMQ==",
      "requires": {
        "@ocaml-wasm/4.12--janestreet-base": "^0.16.0-0",
        "@ocaml-wasm/4.12--num": "^1.4.0-0",
-        "@ocaml-wasm/4.12--zarith": "^1.12.0-0",
+        "@ocaml-wasm/4.12--zarith": "^1.13.0-0",
        "ocaml-wasm": "^4.12.0-0",
        "wasi-kernel": "^0.1.6"
      }
@@ -12604,7 +12827,6 @@
      "version": "5.0.0",
      "resolved": "https://registry.npmjs.org/whatwg-url/-/whatwg-url-5.0.0.tgz",
      "integrity": "sha512-saE57nupxk6v3HY35+jzBwYa0rKSy0XR8JSxZPwgLr7ys0IBzhGviA1/TUGJLmSVqs8pb9AnvICXEuOHLprYTw==",
-      "dev": true,
      "requires": {
        "tr46": "~0.0.3",
        "webidl-conversions": "^3.0.0"
@@ -12613,8 +12835,7 @@
        "webidl-conversions": {
          "version": "3.0.1",
          "resolved": "https://registry.npmjs.org/webidl-conversions/-/webidl-conversions-3.0.1.tgz",
-          "integrity": "sha512-2JAn3z8AR6rjK8Sm8orRC0h/bcl/DqL7tRPdGZ4I1CjdF+EaMLmYxBHyXuKL849eucPFhvBoxMsflfOb8kxaeQ==",
-          "dev": true
+          "integrity": "sha512-2JAn3z8AR6rjK8Sm8orRC0h/bcl/DqL7tRPdGZ4I1CjdF+EaMLmYxBHyXuKL849eucPFhvBoxMsflfOb8kxaeQ=="
        }
      }
    },

--- a/package.json
+++ b/package.json
 {
  "name": "jscoq",
-  "version": "0.17.0",
+  "version": "0.17.1",
  "type": "module",
  "description": "A port of Coq to JavaScript -- run Coq in your browser",
  "main": "frontend/classic/js/index.js",
@@ -18,6 +18,7 @@
    "jscoqdoc": "frontend/classic/js/jscoqdoc.cjs"
  },
  "dependencies": {
+    "@octokit/core": "^4.2.1",
    "array-equal": "^1.0.0",
    "browser-or-node": "^2.0.0",
    "child-process-promise": "^2.2.1",
@@ -35,7 +36,7 @@
    "proper-lockfile": "^4.1.2",
    "vue": "^2.6.12",
    "vue-context-menu": "^2.0.6",
-    "wacoq-deps": "^0.1.0"
+    "wacoq-deps": "0.1.1"
  },
  "devDependencies": {
    "@corwin.amber/hastebin": "^0.1.2",
@@ -45,7 +46,7 @@
    "@types/jquery": "^3.5.14",
    "@types/mkdirp": "^1.0.1",
    "@types/mocha": "^10.0.1",
-    "@types/node": "^13.11.1",
+    "@types/node": "^20.4.8",
    "@types/pako": "^2.0.0",
    "assert": "^2.0.0",
    "bootstrap": "^5.2.1",
@@ -59,7 +60,6 @@
    "path": "^0.12.7",
    "path-browserify": "^1.0.1",
    "process": "^0.11.10",
-    "ronin-p2p": "^0.1.0",
    "stream-browserify": "^3.0.0",
    "style-loader": "^1.1.3",
    "terser-webpack-plugin": "^5.3.6",
@@ -79,6 +79,8 @@
    "backend/wasm/*.wasm",
    "coq-pkgs",
    "dist",
+    "dist-cli",
+    "dist-webpack",
    "examples",
    "docs",
    "jscoq.js",

--- a/package.json.wacoq
+++ b/package.json.wacoq
-{
-  "name": "wacoq",
-  "version": "0.17.0",
-  "description": "A port of Coq to WebAssembly -- run Coq in your browser",
-  "type": "module",
-  "main": "frontend/classic/js/index.js",
-  "bin": {
-    "wacoqdoc": "frontend/classic/js/jscoqdoc.js"
-  },
-  "dependencies": {
-    "array-equal": "^1.0.0",
-    "child-process-promise": "^2.2.1",
-    "codemirror": "^5.61.0",
-    "commander": "^5.0.0",
-    "fflate-unzip": "^0.7.0",
-    "find": "^0.3.0",
-    "glob": "^7.1.3",
-    "jquery": "^3.6.0",
-    "jszip": "^3.5.0",
-    "localforage": "^1.7.3",
-    "lodash": "^4.17.20",
-    "minimatch": "^3.0.4",
-    "mkdirp": "^1.0.4",
-    "neatjson": "^0.8.3",
-    "path": "^0.12.7",
-    "proper-lockfile": "^4.1.2",
-    "vue": "^2.6.12",
-    "vue-context-menu": "^2.0.6"
-  },
-  "devDependencies": {
-    "@corwin.amber/hastebin": "^0.1.2",
-    "@types/codemirror": "^5.60.5",
-    "@types/find": "^0.2.1",
-    "@types/jquery": "^3.5.14",
-    "@types/mkdirp": "^1.0.1",
-    "@types/node": "^13.11.1",
-    "assert": "^2.0.0",
-    "bootstrap": "^5.1.3",
-    "buffer": "^6.0.3",
-    "constants-browserify": "^1.0.0",
-    "css-loader": "^5.2.4",
-    "file-loader": "^6.0.0",
-    "katex": "^0.15.3",
-    "mathjax": "^3.2.2",
-    "mocha": "^9.1.3",
-    "path-browserify": "^1.0.1",
-    "process": "^0.11.10",
-    "ronin-p2p": "^0.1.0",
-    "sass": "^1.26.3",
-    "sass-loader": "^8.0.2",
-    "stream-browserify": "^3.0.0",
-    "style-loader": "^1.1.3",
-    "ts-loader": "^9.3.1",
-    "typescript": "^4.7.4",
-    "util": "^0.12.4",
-    "vue-loader": "^15.9.8",
-    "vue-template-compiler": "^2.6.12",
-    "webpack": "^5.49.0",
-    "webpack-cli": "^4.7.2"
-  },
-  "files": [
-    "frontend",
-    "backend/*.js",
-    "backend/*.ts",
-    "examples",
-    "dist",
-    "examples",
-    "docs/*.html",
-    "jscoq.js",
-    "index.html"
-  ],
-  "scripts": {
-    "build": "webpack --mode production",
-    "build:dev": "webpack",
-    "watch": "webpack -w",
-    "prepack": "sed -i.in 's/\\(is_npm:\\) false/\\1 true/;s/\\(backend:\\) .*/\\1 '\\'wa\\',/ frontend/classic/js/index.js"
-  },
-  "repository": {
-    "type": "git",
-    "url": "git+https://github.com/jscoq/jscoq.git"
-  },
-  "author": "ejgallego",
-  "license": "AGPL-3.0-or-later",
-  "bugs": {
-    "url": "https://github.com/jscoq/jscoq/issues"
-  },
-  "homepage": "https://jscoq.github.io"
-}
--- a/coq-serapi @ 0bd0772f
+++ b/coq-serapi @ 0bd0772f
-Subproject commit 0bd0772fe683d1dbfd3bd29db5ad652e74a70f66
--- a/vendor/coq-serapi/.github/workflows/ci.yml
+++ b/vendor/coq-serapi/.github/workflows/ci.yml
+name: CI
+
+on:
+  push:
+    branches:
+    - v8.8
+    - v8.9
+    - v8.10
+    - v8.11
+    - v8.12
+    - v8.13
+    - v8.14
+    - v8.15
+    - v8.16
+    - v8.17
+    - main
+  pull_request:
+    branches:
+    - v8.8
+    - v8.9
+    - v8.10
+    - v8.11
+    - v8.12
+    - v8.13
+    - v8.14
+    - v8.15
+    - v8.16
+    - v8.17
+    - main
+  # Allows you to run this workflow manually from the Actions tab
+  workflow_dispatch:
+
+jobs:
+  build:
+    strategy:
+      fail-fast: false
+      matrix:
+        ocaml-compiler: [4.09.x, 4.10.x, 4.11.x, 4.12.x, 4.13.x, 4.14.x, 5.0.x]
+        test-target: [test]
+        extra-opam: [coq.8.17.dev coq-mathcomp-ssreflect.dev]
+        include:
+        - ocaml-compiler: ocaml-variants.4.12.1+options,ocaml-option-32bit
+          test-target: js-dune
+          extra-opam: coq.8.17.dev js_of_ocaml js_of_ocaml-lwt zarith_stubs_js
+        - ocaml-compiler: 4.13.1
+          test-target: test
+          extra-opam:
+          coq-from-git: true
+    env:
+      OPAMJOBS: "2"
+      OPAMROOTISOK: "true"
+      OPAMYES: "true"
+      NJOBS: "2"
+      COQ_REPOS: "https://github.com/coq/coq.git"
+      COQ_BRANCH: "v8.17"
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v2
+      - name: Install apt dependencies
+        run: |
+          sudo dpkg --add-architecture i386
+          sudo apt-get -o Acquire::Retries=30 update -q
+          sudo apt-get -o Acquire::Retries=30 install gcc-multilib libgmp-dev:i386 -y --allow-unauthenticated
+      - name: Set up OCaml ${{ matrix.ocaml-compiler }}
+        uses: avsm/setup-ocaml@v2
+        with:
+          ocaml-compiler: ${{ matrix.ocaml-compiler }}
+          dune-cache: true
+      - name: Basic OPAM setup for SerAPI
+        run: |
+          eval $(opam env)
+          opam repos add coq-released http://coq.inria.fr/opam/released
+          opam repos add coq-core-dev http://coq.inria.fr/opam/core-dev
+          # Only for mathcomp.dev which is needed for 8.16, remove when math-comp is fixed
+          opam repos add coq-extra-dev http://coq.inria.fr/opam/extra-dev
+          # coq-serapi already pinned by the setup-ocaml@v2 action
+          opam install --deps-only coq-serapi
+      - name: Display OPAM Setup
+        run: |
+          eval $(opam env)
+          opam list
+      - name: Install Coq via git
+        if: ${{ matrix.coq-from-git }}
+        run: |
+          eval $(opam env)
+          opam pin add -k version dune 3.3.1
+          # First we update SERAPI_COQ_HOME for future steps as per https://docs.github.com/en/actions/reference/workflow-commands-for-github-actions#setting-an-environment-variable
+          echo "SERAPI_COQ_HOME=$HOME/coq-$COQ_BRANCH/_build/install/default/lib/" >> $GITHUB_ENV
+          # Update to coq-core some day
+          # opam install --deps-only coq-core
+          opam install --deps-only coq-core
+          git clone --depth=3 -b "$COQ_BRANCH" "$COQ_REPOS" "$HOME/coq-$COQ_BRANCH"
+          # Upstream 'make -C "$HOME/coq-$COQ_BRANCH" world' target now builds coqide
+          cd "$HOME/coq-$COQ_BRANCH"
+          ./configure -prefix "$HOME/coq-$COQ_BRANCH/_build/install/default/"
+          make dunestrap
+          dune build -p coq-core,coq-stdlib,coq
+          cd "$HOME"
+          # Install math-comp using Coq from git
+          PATH="$HOME/coq-$COQ_BRANCH/_build/install/default/bin:$PATH"
+          git clone --depth=3 -b master https://github.com/math-comp/math-comp.git
+          make -C math-comp/mathcomp/ssreflect
+          make -C math-comp/mathcomp/ssreflect install
+      - name: Extra OPAM Setup (Coq, js_of_ocaml)
+        if: ${{ matrix.extra-opam != '' }}
+        run: |
+          eval $(opam env)
+          opam install ${{ matrix.extra-opam }}
+      - name: Build and Test SerAPI
+        run: |
+          eval $(opam env)
+          make -j "$NJOBS" SERAPI_COQ_HOME="$SERAPI_COQ_HOME" "${{ matrix.test-target }}"
+          ls -lR _build/install/default/ || true
+          ls -lR _build/default/sertop/*.js || true
--- a/vendor/coq-serapi/.gitignore
+++ b/vendor/coq-serapi/.gitignore
+_build
+*~
+js/sertop_js.js
+sertop/ser_version.ml
+.merlin
+*.install
--- a/vendor/coq-serapi/.ocamlformat
+++ b/vendor/coq-serapi/.ocamlformat
+sequence-style=terminator
--- a/vendor/coq-serapi/AUTHORS
+++ b/vendor/coq-serapi/AUTHORS
+Emilio Jesús Gallego Arias
+Karl Palmskog
+Vasily Pestun
+Clément Pit--Claudel
+Kaiyu Yang
--- a/vendor/coq-serapi/CHANGES.md
+++ b/vendor/coq-serapi/CHANGES.md
+## Version 0.17.3
+
+ - [serlib] Fix (@ejgallego, #398, fixes #397 fixes sr-lab/coqpyt#35 ,
+            thanks to @laetitia-teo and @Nfsaavedra for the bug
+            report)
+
+## Version 0.17.2:
+
+ - [serlib] Expose some more Ast functions required by coq-lsp's
+            auto-build support (@ejgallego, #383)
+
+## Version 0.17.1:
+
+ - [sertop] Don't initialize `CoqworkmgrApi` (@ejgallego, #340)
+ - [serlib] Compat with Jane Street libraries >= v0.16.0 (@ejgallego,
+            #351)
+
+## Version 0.17.0:
+
+ - [serlib] (!) Serialization format of generic arguments has changed
+            to be conforming to usual `ppx_sexp_conv` conventions.
+            (@ejgallego , fixes #273)
+ - [serapi] (!) support for Coq 8.17, upstream structures seem pretty
+            stable from 8.16, except for `Constr.Evar` (@ejgallego)
+ - [serapi] SerAPI is now in Coq's CI (@ejgallego @alizter)
+
+## Version 0.16.3:
+
+ - [serlib] Fix JSON serialization for generic arguments (@ejgallego, #321)
+
+## Version 0.16.2:
+
+ - [sertop] Add `--impredicative-set` command line option (@dhilst , #288)
+ - [serlib] Added support for some more plugins from coq-core (ltac2,
+            cc, micromega, number_string_notation) (@ejgallego, #284, #306)
+
+## Version 0.16.1:
+
+ - [sertop] Allow to set `--coqlib` using the `COQLIB` environment
+            variable. The cmdline argument option still has
+            precedence.
+ - [serapi] Allow to parse expressions too with
+            `(Parse (entry Constr) $text)` (@ejgallego, fixes #272)
+
+## Version 0.16.0:
+
+ - [serapi] (!) support for Coq 8.16, see upstream changes and SerAPI
+            test-suite changes for more information. Remarkable
+            changes are:
+            - kernel terms are serialized a bit differently now due to
+              KerName being used in more places upstream. Some
+              internal structures also changes in kernel's env, so be
+              attentive if you are depending on them.
+            - plugin loading is adapted for 8.16 findlib loading
+              method
+            (@ejgallego)
+ - [deps]   Require cmdliner >= 1.1.0 (@ejgallego)
+ - [deps]   Support Jane Street libraries v0.15.0 (@ejgallego)
+ - [serapi] New query `Objects` to dump Coq's libobject (@ejgallego)
+ - [serlib] Much improved yojson / json support (@ejgallego)
+ - [serlib] Coq AST now supports ppx_hash intf (ignoring locations by default)
+            (@ejgallego)
+ - [serlib] Coq AST now supports ppx_compare intf (ignoring locations by default)
+            (@ejgallego)
+ - [serlib] Large refactoring on Serlib, using functors, see serlib/README.md
+            (@ejgallego)
+ - [serapi] (!) Query `Proofs` has changed type and will now return the
+            partial terms under construction (#271 , fixes #270, @ejgallego)
+
+## Version 0.15.1:
+
+ - [serlib] Fix bad bypass of opaquetab serialization. This caused a
+            segfault in some cases.
+
+## Version 0.15.0:
+
+ - [serapi] (!) support for Coq 8.15, see upstream changes; nothing
+            too remarkable so far, except for `NewTip` -> `NewAddTip`
+            in the answer response, we may want to add a compat layer
+            for this if problematic. (#265, @ejgallego)
+
+## Version 0.14.0:
+
+ - [serapi] (!) support for Coq 8.14, see upstream changes; nothing
+            too remarkable other than `NewDoc` will now ignore
+            loadpaths due to new init setup upstream.
+            (#253, @ejgallego)
+ - [ci]     SerAPI branches should be able to build now against Coq rc
+            packages as to better integrate with Coq's platform beta
+            release; thanks to Érik Martin-Dorel, Karl Palmskog and Théo
+            Zimmermann for feedback.
+
+## Version 0.13.1:
+
+ - [serapi] New query `(Query () (LogicalPath file))` which will
+            return the logical path for a particular `.v` file
+            (@ejgallego, see also
+            https://github.com/cpitclaudel/alectryon/pull/25)
+ - [serapi] new `(SaveDoc opts)` command supporting saving of .vo
+            files even when from interactive mode; note that using
+            `--topfile` is required (fixes #238, @ejgallego, reported
+            by Jason Gross)
+ - [sertop] we don't link the OCaml `num` library anymore, this could
+            have some impact on plugins (@ejgallego)
+ - [nix]    Added Nix support (#249, fixes #248, @Zimmi48, reported
+            by @nyraghu)
+ - [serapi] Fix COQPATH support: interpret paths as absolute (#249, @Zimmi48)
+ - [serlib] Ignore `env` parameter in certain exceptions (#254, fixes #250,
+            @ejgallego, reported by @cpitclaudel)
+ - [sertop] New option `--omit_env` that will disable the serialization of
+            Coq's super heavy global environments (#254 @ejgallego)
+ - [build]  Test OCaml 4.12 (#257 @ejgallego)
+ - [sertop] Async mode was not working due to passing `-no-glob` to workers
+
+## Version 0.13.0:
+
+ - [serapi] (!) support for Coq 8.13, see upstream changes; in
+            particular there are changes in the kernel representation
+            of terms [pattern matching, new caseinvert, primitive arrays]
+            (#232, fixes #227, @ejgallego)
+
+## Version 0.12.1:
+
+ * [serapi]  (!) Bump public library versioning [breaking change]
+ * [opam]    Bump upper bound on ppx_sexp_conv to 0.15, allowing SerAPI
+             to work with the 0.14 set of Jane Street packages.
+ * [serapi]  Fix goal printing anomaly (#230, fixes #228 @corwin-of-amber)
+ * [sertop ] New `(Fork (fifo_in file) (fifo_out file))` command, that
+             will (hard) fork a new SerAPI process and redirect the
+             input / output towards the given Unix FIFOs. This API is
+             experimental but should allow quite a few advantages to
+             some users willing to perform speculative execution.
+             (#210 , improves #202 , @ejgallego)
+ - [serapi]  Fix missing newline to separate goals (#235, fixes #231, @ejgallego)
+
+## Version 0.12.0:
+
+ * [general] (!) support Coq 8.12, main changes upstream related to
+             the representation of numerals and notations.
+             The rest of the interface does remain relative stable.
+             (@ejgallego).
+
+## Version 0.11.1:
+
+ * [general] Require dune >= 2.0 (@ejgallego, ??)
+ * [serapi]  New query `Comments` to return all comments in a document
+             (@ejgallego, #20? , (partially) fixes #191 , #200 )
+ * [general] Coq's error recovery is now disabled by default
+             (@ejgallego , fixes #201)
+ * [general] New option `--error-recovery` to enable error recovery
+             (@ejgallego , #203)
+ * [general] Bump sexplib dependency to v0.13 (@ejgallego , #204)
+             Fixes incorrect change in #194.
+ * [sertop]  Set default value of allow-sprop to be true in agreement with upstream coq v8.11
+             and added option '--disallow-sprop' to optionally switch it off
+			 (--disallow-sprop forbids using the proof irrelevant SProp sort)
+             (#199, @pestun)
+ * [sertop]  Set default value of allow-sprop to be true in agreement with upstream coq v8.11
+             and added option '--disallow-sprop' to optionally switch it off
+			 (--disallow-sprop forbids using the proof irrelevant SProp sort)
+             (@pestun , #199)
+ * [sertop]  Added option `--topfile` to `sertop` to set top name from
+             a filename (#197, @pestun)
+ * [deps]    Require sexplib >= 0.12 , fixed deprecation warnings
+             (#194, @ejgallego)
+ * [general] SerAPI is now tested with OCaml 4.08 and 4.09 (#195 , @ejgallego)
+ * [sertop ] Forward port sername from 0.7.1 (@ejgallego)
+ * [serlib ] Fix #212 "Segfault on universes" (@ejgallego, reported by @cpitclaudel , #214)
+ * [serapi ] Fix #221 "Support COQPATH" (@ejgallego, reported by @cpitclaudel , #224)
+ * [sertop ] Fix #222 "Support --indices-matter" (@ejgallego, reported by @cpitclaudel , #223)
+ * [sertop ] Fix "Stack overflow in main loop" (@pestun , #216)
+
+## Version 0.11.0:
+
+ * [general] (!) support Coq 8.11, a few datatypes have changed, in
+             particular `CoqAst` handles locations as an AST node, and
+             the kernel type includes primitive floats (@ejgallego).
+ * [general] (!) Now the `sertop` and `serapi` OCaml libraries are
+             built packed, we've also bumped their compat version number
+             (#192 @ejgallego)
+
+## Version 0.7.1:
+
+ * [sertop ] Add `sername` program for batch serialization elaborated terms
+             Note that this utility will be deprecated in future versions,
+             to be subsumed by `Query`.
+             (#207, @palmskog, with help from @ejgallego)
+ * [serlib ] Expose `QueryUtil.info_of_id` and `gen_pp_obj` in `serapi_protocol.mli` to enable
+             using them in `sername` to retrieve serialized body-type pairs (@palmskog)
+ * [general] Improved compat with Jane Street v0.13 toolchain
+ * [serlib ] Only use `ssreflect` from Coq in tests (@ejgallego)
+
+## Version 0.7.0:
+
+ * [general] (!) support Coq 8.10,
+ * [serapi]  (!) `Goals` query return type has been modified due to
+             upstream changes. (@ejgallego)
+ * [serlib]  Complete (hopefully) serialization for ssreflect ASTs.
+             (#73 @ejgallego)
+ * [general] Drop support for OCaml < 4.07 (#140 @ejgallego)
+ * [serlib ] JSON serialization for kernel and AST terms (@ejgallego)
+ * [serapi ] Add `Complete` support (@ejgallego
+             c.f. https://github.com/coq/coq/pull/8766)
+ * [serlib ] Serlib is now built as a wrapped module (@ejgallego)
+ * [serapi ] (!) Goals info has been extended to print name metadata if available,
+             cc #151 (@ejgallego , suggested by @cpitclaudel)
+ * [serlib ] JSON support for vernac_expr (@ejgallego)
+ * [sertop ] (!) Do as Coq upstream and load Coq's stdlib with `-R` (closes #56)
+ * [sertop ] Follow Coq upstream and unset `indices_matter` (closes #157,
+             thanks to @palmskog for the report)
+ * [serapi ] (!) Improve CoqExn answer to have pretty-printed message (improves #162,
+             thanks to @cpitclaudel for the request)
+ * [serlib ] (!) Fix capitalization conventions for a few types in `Names`
+             (closes #167 thanks to @corwin-of-amber for the report)
+ * [serapi ] (!) Add bullet suggest information to goal query (@corwin-of-amber)
+ * [sertop ] Add `--no_prelude` option (closes #176, @ejgallego, request of @darbyhaller)
+ * [serlib ] (!) Add index to `MBId` serialization (fixes #150, @ejgallego)
+ * [serapi ] (!) Add `sid` parameter to `Print` (helps #150, @ejgallego, reported by @cpitclaudel)
+ * [sertop ] Add `sertok` program for batch serialization of tokens and their source locations (@palmskog)
+ * [serapi ] (!) Add string-formatted messages to `CoqExn` and `Message`
+             (@ejgallego closes #184 , closes #162)
+
+## Version 0.6.1:
+
+ * [serapi ] Add `Parse` command to parse a sentence; c.f.
+             https://github.com/ejgallego/coq-serapi/issues/117
+             (@ejgallego) (cc: @yangky11)
+ * [sercomp] Add "print" `--mode` to print the input Coq document
+             (@ejgallego) (cc: @Ptival)
+ * [serlib ] Serialize `Universe.t` (@ejgallego, request by @yangky11)
+ * [sercomp] Merge `sercomp` and `compser`, add `--input` parameter to `sercomp`
+             (@palmskog) (cc: @ejgallego)
+ * [serlib ] Much improved support for serialization of `Environ.env`
+             (@yangky11 and @ejgallego c.f. #118)
+ * [serapi ] Make sure every command ends with `Completed`, even if it produced
+             an exception (@brando90 and @ejgallego c.f. #124)
+ * [sercomp] Add `--mode=kexp` to output the final kernel environment.
+             (@ejgallego c.f. #119)
+ * [serlib ] Serialize more internal environment fields (@ejgallego c.f. #119)
+ * [serlib ] Improvements in serialization org (@ejgallego)
+ * [serlib ] Serialize kernel entries (@ejgallego @palmskog)
+ * [serlib ] Fix critical bug on `Constr` deserialization; reported by @palmskog,
+             fix by @SkySkimmer.
+ * [sertop]  Fix backtrace printing when using `--debug` (@ejgallego)
+ * [serlib ] Don't serialize VM values (@ejgallego, bug report by @palmskog)
+ * [serapi ] Output location on tokenization (@ejgallego , idea by @palmskog)
+ * [serapi ] Add basic documentation of the protocol (@ejgallego cc #109)
+
+## Version 0.6.0:
+
+ * [general] support Coq 8.9,
+ * [general] SerAPI now uses Dune as a build system,
+ * [opam]   install `sertop.el`,
+ * [serlib] support to serialize kernel environments,
+ * [serapi] new query `Env` that tries to print the current kernel environment,
+ * [serlib] correct field names for `CAst`,
+ * [serlib] more robust support for opaque / non-serializable types (#61, #68).
+            Thanks to @palmskog,
+ * [serlib] new option `--exn_on_opaque` to raise an exception on
+            non-serializable types; closes #61, thanks to @palmskog,
+ * [serlib] serialization test-suite from
+            https://github.com/proofengineering/serapi-tests, thanks to
+            @palmskog,
+ * [sercomp] add `--mode` option to better control output,
+ * [sercomp] add `compser` for deserialization (inverse of `sercomp`)
+             (@palmskog),
+ * [serapi]  Allow custom document creation using the `NewDoc` call.
+             Use the `--no_init` option to avoid automatic creation
+             on init. (@ejgallego)
+ * [sercomp] Allow compilers to output `.vo` (@ejgallego , suggested by
+             @palmskog)
+ * [sercomp] Serialize top-level vernaculars with their syntactic
+             attributes (such as location) (@ejgallego)
+ * [serapi]  Add `Assumptions` query, at the suggestion of @Armael
+             (@ejgallego)
+ * [sercomp] Disable error resilience mode in compilers; semantics are
+             a bit dubious see coq/coq#9204 also #94.
+             (@ejgallego, report by @palmskog)
+ * [sercomp] Add `check` mode to compilers to check all proofs without
+             outputting `.vo`. (@palmskog)
+ * [sercomp] Add "hacky" `--quick` option to skip checking of opaque
+             proofs. (@ejgallego, request by @palmskog)
+ * [sercomp] Add `--async_workers` option to set maximum number
+             of parallel async workers. (@palmskog)
+ * [sertop] Stop linking Coq plugins statically and load `serlib`
+            plugins when Coq plugins are loaded instead (@ejgallego,
+            review by @palmskog)
+
+## Version 0.5.7:
+
+ * [serlib] Fixed serializers for more tactics data, add support for
+   `ground` plugin (#68). Thanks again to @palmskog for the report.
+
+## Version 0.5.6:
+
+ * [serlib] Fixed serializers for some tactics data (#66) Thanks to
+   @palmskog for the report.
+
+## Version 0.5.5:
+
+ * [serlib] Be more lenient when parsing back `Id.t` as to accommodate
+   hacks in the Coq AST (#64) Thanks to @palmskog for the report.
+
+## Version 0.5.4:
+
+ * [serlib] Fix critical bug in handling of abstract type (#60)
+
+## Version 0.5.3:
+
+ * [sertop] Support for `-I` option (`--ml-include-path`).
+
+## Version 0.5.2:
+
+ * [serlib] Compatibility with OCaml 4.07.0 [problems with `Stdlib` packing]
+
+## Version 0.5.1:
+
+ * [serlib] (basic) support for serialization of the ssreflect grammar,
+ * [serapi] `(Query () (Ast n))` is now `(Query ((sid n)) Ast)`,
+ * [serapi] remove broken deprecated `SetOpt` and `LibAdd` commands,
+ * [doc] Improved man page.
+ * [js] Miscellaneous improvements on the js build.
+
+## Version 0.5.0:
+
+ * [general] support Coq 8.8, use improved document API,
+ * [sertop] By default `sertop` will create a new document with `doc_id` 0,
+ * [sertop] new debug options, see `sertop --help`.
+
+## Version 0.4:
+
+ * [general] support Coq 8.7 , make use of improved upstream API,
+ * [sertop] support `-R` and `-Q` options, note the slightly different
+   syntax wrt Coq upstream: `-R dir,path` in place of `-R dir path`,
+ * [serlib] support serialization of generic arguments [#41],
+ * [serapi] `(ReadFile file)`: hack to load a completed file.
+
+## Version 0.2:
+
+ * Better Query/Object system.
+
+## Version 0.1:
+
+ * Serialization-independent protocol core,
+ * [js] Javascript worker,
+ * [lib] Better Prelude support,
+ * [serlib] Full Serialization of generic arguments,
+ * [proto] Add is not a synchronous call anymore,
+ * [proto] Refactor into a flat command hierarchy,
+ * [proto] More useful queries,
+ * [proto] Guarantee initial state is 1,
+ * [proto] Support for ltac profiling,
+ * [proto] Printing: add depth limiting,
+ * [proto] Better handling of options in the sexp backend.
+
+## Version 0.03:
+
+ * **[done]** Implicit arguments.
+ * **[done]** Coq Workers support.
+ * **[done]** Advanced Sentence splitting `(Parse (Sentence string))`, which can handle the whole document.
+
+## Version 0.02:
+
+ * **[done]** Serialization of the `Proof.proof` object.
+ * **[done]** Improve API: add options.
+ * **[done]** Improve and review printing workflow.
+ * **[done]** `(Query ((Prefix "add") (Limit 10) (PpStr)) $ObjectType)`
+ * **[done]** Basic Sentence splitting `(Parse num string))`, retuns the first num end of the sentences _without_ executing them.
+              This has pitfalls as parsing is very stateful.
+ * **[done]** Basic completion-oriented Search support `(Query () Names)`
+ * **[done]** Better command line parsing (`Cmdliner`, `Core` ?)
+ * **[partial]** Print Grammar tactic. `(Query ... (Tactics))`.
+   Still we need to decide on:
+   `Coq.Init.Notations.instantiate` vs `instantiate`, the issue of
+   `Nametab.shortest_qualid_of_global` is a very sensible one for IDEs
--- a/vendor/coq-serapi/CODE_OF_CONDUCT.md
+++ b/vendor/coq-serapi/CODE_OF_CONDUCT.md
+The SerAPI project aims to be a fun and safe space where everybody is
+extremely welcome to participate and discuss. There will be zero
+tolerance to any kind of inappropriate behavior. Lets us all have fun.
+
+ -- EJGA
+
+# Contributor Covenant Code of Conduct
+
+## Our Pledge
+
+In the interest of fostering an open and welcoming environment, we as
+contributors and maintainers pledge to making participation in our project and
+our community a harassment-free experience for everyone, regardless of age, body
+size, disability, ethnicity, sex characteristics, gender identity and expression,
+level of experience, education, socio-economic status, nationality, personal
+appearance, race, religion, or sexual identity and orientation.
+
+## Our Standards
+
+Examples of behavior that contributes to creating a positive environment
+include:
+
+* Using welcoming and inclusive language
+* Being respectful of differing viewpoints and experiences
+* Gracefully accepting constructive criticism
+* Focusing on what is best for the community
+* Showing empathy towards other community members
+
+Examples of unacceptable behavior by participants include:
+
+* The use of sexualized language or imagery and unwelcome sexual attention or
+ advances
+* Trolling, insulting/derogatory comments, and personal or political attacks
+* Public or private harassment
+* Publishing others' private information, such as a physical or electronic
+ address, without explicit permission
+* Other conduct which could reasonably be considered inappropriate in a
+ professional setting
+
+## Our Responsibilities
+
+Project maintainers are responsible for clarifying the standards of acceptable
+behavior and are expected to take appropriate and fair corrective action in
+response to any instances of unacceptable behavior.
+
+Project maintainers have the right and responsibility to remove, edit, or
+reject comments, commits, code, wiki edits, issues, and other contributions
+that are not aligned to this Code of Conduct, or to ban temporarily or
+permanently any contributor for other behaviors that they deem inappropriate,
+threatening, offensive, or harmful.
+
+## Scope
+
+This Code of Conduct applies both within project spaces and in public spaces
+when an individual is representing the project or its community. Examples of
+representing a project or community include using an official project e-mail
+address, posting via an official social media account, or acting as an appointed
+representative at an online or offline event. Representation of a project may be
+further defined and clarified by project maintainers.
+
+## Enforcement
+
+Instances of abusive, harassing, or otherwise unacceptable behavior may be
+reported by contacting the project team at e@x80.org. All
+complaints will be reviewed and investigated and will result in a response that
+is deemed necessary and appropriate to the circumstances. The project team is
+obligated to maintain confidentiality with regard to the reporter of an incident.
+Further details of specific enforcement policies may be posted separately.
+
+Project maintainers who do not follow or enforce the Code of Conduct in good
+faith may face temporary or permanent repercussions as determined by other
+members of the project's leadership.
+
+## Attribution
+
+This Code of Conduct is adapted from the [Contributor Covenant][homepage], version 1.4,
+available at https://www.contributor-covenant.org/version/1/4/code-of-conduct.html
+
+[homepage]: https://www.contributor-covenant.org
+
+For answers to common questions about this code of conduct, see
+https://www.contributor-covenant.org/faq
--- a/vendor/coq-serapi/CONTRIBUTING.md
+++ b/vendor/coq-serapi/CONTRIBUTING.md
+## Contributing to SerAPI
+
+Thanks for willing to contribute to SerAPI! Contributing is usually as
+easy as opening a pull request, issue, or dropping by the Gitter
+channel and letting us know what you think of the tool.
+
+Nothing special has to be kept in mind, other than standard OCaml
+practice, we usually follow `ocp-indent` guidelines, but we are
+liberal in some places in particular with regards to intra-line
+indentation.
+
+We prefer GPG signed commits as well as `Signed-off-by` commits.
+
+## Releasing SerAPI
+
+As of today, SerAPI is released using a standard process based on
+`dune-release`; to do a release, it should suffice to do:
+
+```
+$ dune-release tag $version
+$ dune-release
+```
+
+where `$version` is `$coq-version+$serapi_version`, for example
+`8.16.2+0.16.4`. Note that `dune-release` requires you to setup a
+github token, see `dune-release` docs for more details.
+
+**Important**: note that `dune-release` will automatically generate
+the changelog from `CHANGES.md`, please keep the formatting tidy in
+that file!
+
+Note that bug https://github.com/ejgallego/coq-serapi/issues/208 may
+require you to edit the opam-repository PR if their linter fails
+[seems fixed as of today, but OMMV]
+
+### Commit tag conventions [work in progress]:
+
+We have somme
+
+- [serlib]  : Serialization lib.
+- [test]    : Adding or modifying a test.
+- [sertop]  : Sexp Toplevel.
+- [doc]     : Documentation.
+- [build]   : Build system.
+- [misc]    : Code refactoring, miscellanenous
+- [proto]   : Core protocol.
+- [control] : STM protocol.
+- [query]   : Query protocol.
+- [parse]   : Parsing protocol.
+- [print]   : Printing protocol.
+- [js]      : Javascript version.
--- a/vendor/coq-serapi/FAQ.md
+++ b/vendor/coq-serapi/FAQ.md
+## What is SerAPI?
+
+Is a library plus a set of command line tools aimed to improve the
+communication of third party tools with Coq.
+
+## How mature is SerAPI?
+
+SerAPI has _experimental_ status; while there are no protocol
+stability guarantees, we got moderate experience with it and evolution
+should be controlled. SerAPI have been used with success in several
+research projects. Protocol-breaking changes are marked in the
+changelog with `(!)`.
+
+## Which Coq versions does SerAPI support?
+
+At the moment, Coq 8.12 is the current supported version for the
+current protocol. Older versions (8.6---8.11) work, however the
+protocol and feature sets do differ.
+
+## How can I install SerAPI?
+
+The supported way is to use the OPAM package manager. The
+`.travis.yml` file contains up to date install instructions if you
+want to build SerAPI manually, see also the [build instructions](notes/build.md) file.
+
+## What serialization formats does SerAPI provide?
+
+SerAPI was built to encode Coq native data types to/from
+S-Expressions, a widely used data and code format pioneered by the
+lisp programming language.
+
+Since then, SerAPI has evolved to take advantage of other formats, and
+now provides experimental Python and JSON output formats too.
+
+## What kind of S-expressions does SerAPI use?
+
+SerAPI does use Jane Street's excellent
+[sexplib](https://github.com/janestreet/sexplib) library print and
+parse S-exps; note that there is not really a S-exp standard, for more
+details about some differences on how quoting happens in `sexplib`,
+please see issues https://github.com/ejgallego/coq-serapi/issues/3 ,
+https://github.com/ejgallego/coq-serapi/issues/8 , and
+https://github.com/ejgallego/coq-serapi/issues/22 .
+
+## SerAPI hangs with inputs larger than 4096 characters:
+
+This is due to a historical limitation of the UNIX/Linux TTY API. See
+[#38](https://github.com/ejgallego/coq-serapi/issues/38). If you
+communicate with SerAPI using a **pipe** this shouldn't be a problem.
+Alternatively, you can use the `ReadFile` experimental command.
+
+## I get an error "Cannot link ml-object ..."
+
+Your OCaml path is not properly setup, see [build instructions](notes/build.md) for more help.
+
+## Can SerAPI produce `.vo` files?
+
+Yes, see `sercomp --help`
+
+## How does SerAPI compare to TCoq
+
+[TCoq](https://github.com/ml4tp/tcoq/) provides some support for
+exporting Coq structures; the main differences with SerAPI is that
+SerAPI works against stock Coq and is maintained; it also provides a
+faithful, automatically generated printers.
+
+A more detailed comparison is needed, in particular TCoq does provide
+some hooks that insert themselves in the proof execution, it is not
+clear that SerAPI can provide that.
+
+For a more detailed discussion see
+https://github.com/ejgallego/coq-serapi/issues/109
+
+## Can SerAPI evaluate a document incrementally?
+
+Yes, by using Coq's capabilities to that effect. Just issue the proper
+`(Cancel ...)` `(Add ... ...)` sequence to simulate an update. This is
+limited now to prefix-only incremental evaluation. It will be improved
+in the future.
+
+## Does SerAPI support asynchronous proof processing?
+
+Yes, it does. Note however that asynchronous proof processing is still
+in experimental status upstream. In particular, there are some issues
+on Windows, and `EditAt` may be inconvenient to use. We recommend not
+using `EditAt` and instead using the less powerful `Cancel` for now.
+
+## Does SerAPI support Coq's command line flags:
+
+We support only a limited set of `coqtop` command line flags, in
+particular `-R` and `-Q` for setting library paths. Unfortunately, due
+to our command line parsing library, the format is slightly
+different. See `sertop --help` for a comprehensive list of flags.
+
+SerAPI aims to be "command line flag free", with all the options for
+each document passed in the document creation call, so this will be
+the preferred method.
+
+## What does SerAPI expose?
+
+SerAPI exposes all core Coq datatypes. Tactics, AST, kernel terms and
+types are all serialized. SerAPI also provide an API to manipulate and
+query "Coq documents".
+
+## How many ASTs does Coq have?
+
+That's a very interesting question! The right answer is: _countably many_!
+
+Logician jokes aside, the truth is that Coq features an _extensible_
+AST. While this gives great power to plugins, it means that consumers
+of the AST need to design their tools to support an _open_ AST.
+
+Coq's core parsing AST is called `vernac_expr`. This type represents
+the so-called "Coq vernaculars". Plugins can extend the "vernacular",
+so you should be prepared to handle arbitrary content under the
+`VernacExtend` constructor. Such arbitrary content is called in Coq
+terminology "generic arguments".
+
+### Interpretation and Terms
+
+After parsing, a term will undergo two elaboration phases before it
+will reach "kernel" form. The top-level parsing type for terms is
+`constr_expr`, which is then _internalized_ to a `glob_constr`. This
+process will perform:
+
+- Name resolution. Example `λ x : nat. x` is resolved to `λ (x: Init.nat), Var 1`
+  [using debruijn for bound variables].
+- Notation interpretation. For example, `a + b` is desugared to `Nat.add a b`.
+- Implicit argument resolution. For example `fst a` is desugared to
+  `@fst _ _ a` [note the holes].
+- Some desugaring of pattern-matching problems also takes place.
+
+The next step is type inference (called pretyping in Coq, as "typing"
+is used for the kernel-level type checking), which will turn a term
+in `glob_constr` form into a full-typed `Constr.t` value. `Constr.t`
+are the core terms manipulated by Coq's kernel and tactics.
+
+When a _generic argument_ is added to Coq's AST, we must also provide
+the corresponding _internalization_ and _pretyping_ functions. To that
+purpose, generic arguments have associated 3-levels, `raw`, `glb`, and
+`top` which correspond to parsing-level, internalized-level, and
+kernel-level.
+
+Thus, a generic argument of type `foo`, may carry 3 different OCaml
+types depending on the level the type is. This is used for example to
+define the AST of _LTAC_ tactics, where the expression `pose s := foo`
+with `foo` initially a `constr_expr` will undergo interpretation and
+inference up to a term with a fully elaborated `foo` term.
--- a/vendor/coq-serapi/LICENSE
+++ b/vendor/coq-serapi/LICENSE
+Format: http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
+Upstream-Name: coq-serapi
+Upstream-Contact: Emilio J. Gallego Arias <e@x80.org>
+Source: https://github.com/ejgallego/coq-serapi
+License: LGPL-2.1+
+Copyright: 2016-2022, MINES ParisTech / Inria
+
+Authors: Emilio J. Gallego Arias
+
+Files: notes/*
+License: LGPL-2.1+ / CC-BY-SA 3.0
+
+Files: jscoq/*
+License: GPL-3+
+
+Files: tests/genarg/*
+Authors: Karl Palmskog
+Licence: Derived from many projects as test cases, falls into fair-use
+
+Comment: the intent is to be compatible with Coq's license. Note that
+the LGPL-2.1+ allows to treat the code as GPL-3+ , and we favor
+that. In some cases, like when linking with jsCoq's code or other code
+that is GPL-3 only, the resulting .js or binaries files will be GPL-3.
+
--- a/vendor/coq-serapi/Makefile
+++ b/vendor/coq-serapi/Makefile
+.PHONY: clean all serlib sertop sercomp force js-dist js-release build build-install test doc
+
+# Leave empty to use OPAM-installed Coq
+SERAPI_COQ_HOME ?=
+# SERAPI_COQ_HOME=/home/egallego/external/coq-v8.17/_build/install/default/lib/
+
+ifneq ($SERAPI_COQ_HOME,)
+  export OCAMLPATH := $(SERAPI_COQ_HOME):$(OCAMLPATH)
+  SP_PKGS=coq-serapi
+else
+  SP_PKGS=coq-serapi
+endif
+
+all: build
+
+GITDEPS=$(ls .git/HEAD .git/index)
+sertop/ser_version.ml: $(GITDEPS)
+	echo "let ser_git_version = \"$(shell git describe --tags || cat VERSION)\";;" > $@
+
+build:
+	dune build --root . --only-packages=$(SP_PKGS) @install
+
+check:
+	dune build --root . @check
+
+build-install:
+	dune build coq-serapi.install
+
+test:
+	dune runtest --root .
+
+doc:
+	dune build @doc-private @doc
+
+browser:
+	google-chrome _build/default/_doc/_html/index.html
+
+sertop: build
+	dune exec -- rlwrap sertop
+
+#####################################################
+# Javascript support
+
+#####################################################
+# JS
+
+JSDIR=jscoq/coq-libjs
+JSFILES=$(addprefix $(JSDIR)/,mutex.js unix.js str.js coq_vm.js)
+
+JSCOQ_DEBUG=no
+JSOO_OPTS=
+ifeq "${JSCOQ_DEBUG}" "yes"
+JSOO_OPTS+= --pretty --noinline --disable shortvar --debug-info
+endif
+
+js:
+	mkdir -p js
+
+force:
+
+_build/default/sertop/sertop_js.bc: force
+	dune build --profile=release sertop/sertop_js.bc
+
+js/sertop_js.js: js _build/default/sertop/sertop_js.bc
+	js_of_ocaml --dynlink +nat.js +dynlink.js +toplevel.js $(JSOO_OPTS) $(JSFILES) _build/default/sertop/sertop_js.bc -o js/sertop_js.js
+
+# We cannot use the separate compilation mode due to Coq's VM: libcoqrun.a
+js-dune:
+	dune build --profile=release sertop/sertop_js.bc.js
+
+js-dist:
+	rsync -avp --exclude=.git --delete ~/research/jscoq/coq-pkgs/ js/coq-pkgs
+
+js-release:
+	rsync -avp --exclude=*~ --exclude=.git --exclude=README.md --exclude=get-hashes.sh --delete js/ ~/research/jscoq-builds
+
+#####################################################
+# Misc
+
+clean:
+	rm -f sertop/ser_version.ml
+	dune clean
+
+demo-sync:
+	rsync -avzp --delete js/ /home/egallego/x80/rhino-hawk/
+	cp /home/egallego/x80/rhino-hawk/term.html /home/egallego/x80/rhino-hawk/index.html
--- a/vendor/coq-serapi/README.md
+++ b/vendor/coq-serapi/README.md
+## SerAPI: Machine-Friendly, Data-Centric Serialization for Coq
+
+[![Build Status][action-badge]][action-link]
+[![Zulip][zulip-badge]][zulip-link]
+
+[action-badge]: https://github.com/ejgallego/coq-serapi/actions/workflows/ci.yml/badge.svg?branch=v8.16
+[action-link]: https://github.com/ejgallego/coq-serapi/actions/workflows/ci.yml?query=branch%3Av8.16
+
+[zulip-badge]: https://img.shields.io/badge/Zulip-chat-informational.svg
+[zulip-link]: https://coq.zulipchat.com/#narrow/stream/256331-SerAPI
+
+To install with opam:
+```
+$ opam install coq-serapi
+$ sertop --help
+```
+
+Alternatively, if you use Nix:
+```
+$ nix-shell -p coq_8_13 coqPackages_8_13.serapi
+$ sertop --help
+```
+
+SerAPI is a library for machine-to-machine interaction with the [Coq proof assistant](https://coq.inria.fr),
+with particular emphasis on applications in IDEs, code analysis tools, and machine learning.
+SerAPI provides automatic serialization of Coq's internal
+[OCaml](https://ocaml.org) datatypes from/to [JSON](https://www.json.org) or
+[S-expressions](https://en.wikipedia.org/wiki/S-expression) (sexps).
+
+SerAPI is a proof-of-concept and should be considered
+alpha-quality. However, it is fully functional and supports, among
+other things, asynchronous proof checking, full-document parsing, and
+serialization of Coq's core datatypes. SerAPI can also be run as
+[WebWorker](https://developer.mozilla.org/en-US/docs/Web/API/Web_Workers_API/Using_web_workers)
+thread, providing a self-contained Coq system inside the
+browser. Typical load times in Google Chrome are less than a second.
+
+The main design philosophy of SerAPI is to **make clients' lives easy**,
+by providing a convenient, robust interface that hides most
+of the scary details involved in interacting with Coq.
+
+Feedback from Coq users and developers is very welcome and _intrinsic_
+to the project. We are open to implementing new features and exploring
+new use cases.
+
+### Documentation and Help:
+
+- [Protocol Documentation](http://ejgallego.github.io/coq-serapi/coq-serapi/Serapi/Serapi_protocol/)
+- [interface file](serapi/serapi_protocol.mli)
+- [SerAPI's FAQ](FAQ.md)
+- [technical report](https://hal-mines-paristech.archives-ouvertes.fr/hal-01384408)
+- [issue tracker](https://github.com/ejgallego/coq-serapi/issues)
+- [Zulip chat](https://coq.zulipchat.com/#narrow/stream/256331-SerAPI)
+- [Gitter chat](https://gitter.im/coq-serapi/Lobby) channel (legacy)
+- [mailing list](https://x80.org/cgi-bin/mailman/listinfo/jscoq)
+
+**API WARNING:** _The protocol is experimental and may change often_.
+
+### Quick Overview and Install:
+
+SerAPI can be installed as the [OPAM](https://opam.ocaml.org) package `coq-serapi`
+or the [Nix](https://nixos.org) package `coqPackages_8_13.serapi`.
+See [build instructions](notes/build.md) for manual installation. The experimental
+[in-browser version](https://x80.org/rhino-hawk) is also online.
+
+SerAPI provides an interactive "Read-Print-Eval-Loop" `sertop`, a
+batch-oriented compiler `sercomp`, and a batch-oriented tokenizer `sertok`.
+See the manual pages and `--help` pages of each command for more details.
+
+To get familiar with SerAPI we recommend launching the `sertop` REPL,
+as it provides a reasonably human-friendly experience:
+
+```
+$ rlwrap sertop --printer=human
+```
+
+You can then input commands. `Ctrl-C` will interrupt a busy Coq
+process in the same way it interrupts `coqtop`.
+
+The program `sercomp` provides a command-line interface to some
+key functionality of SerAPI and can be used for batch processing
+of Coq documents, e.g., to serialize Coq source files from/to lists of
+S-expressions of Coq vernacular sentences. See `sercomp --help` for some
+usage examples and an overview of the main options. The program `sertok`
+provides similar functionality at the level of Coq source file tokens.
+
+### Protocol Commands:
+
+Interaction with `sertop` is done using _commands_, which can be optionally tagged in the form of `(tag cmd)`; otherwise, an automatic tag will be assigned.
+For every command, SerAPI **will always** reply with `(Answer tag Ack)` to indicate that the command was successfully parsed and delivered to Coq, or with a `SexpError` if parsing failed.
+
+There are three categories of [commands](serapi/serapi_protocol.mli#L147):
+
+- **Document manipulation:** `Add`, `Cancel`, `Exec`, ...: these commands instruct Coq to perform some action on the current document.
+  Every command will produce zero or more different _tagged_ [answers](serapi/serapi_protocol.mli#52), and  a final answer `(Answer tag Completed)`, indicating that there won't be more output.
+
+  SerAPI document commands are an evolution of the OCaml STM API, [here](https://github.com/ejgallego/jscoq/blob/master/etc/notes/coq-notes.md) and [here](https://github.com/siegebell/vscoq/blob/master/CoqProtocol.md) you can find a few informal notes on how it works. We are working on a more detailed specification, for now you can get some more details in the issue tracker.
+
+- **Queries:** `(Query ((opt value) ...) kind)`:
+
+  Queries stream Coq objects of type `kind`. This can range from options, goals and hypotheses, tactics, etc.
+  The first argument is a list of options: `preds` is a list of conjunctive filters, `limit` specifies how many values the query may return.
+  `pp` controls the output format: `PpSer` for full serialization, or `PpStr` for "pretty printing". For instance:
+  ```lisp
+  (tag (Query ((preds (Prefix "Debug")) (limit 10) (pp PpSexp)) Option))
+  ```
+  will stream all Coq options that start with "Debug", limiting to the first 10 and printing the full internal Coq datatype:
+  ```lisp
+  (CoqOption (Default Goal Selector)
+     ((opt_sync true) (opt_depr false) (opt_name "default goal selector")
+     (opt_value (StringValue 1))))
+  ...
+  ```
+  Options can be omitted, as in: `(tag (Query ((limit 10)) Option))`, and
+  currently supported queries can be seen [here](serapi/serapi_protocol.mli#L118)
+
+- **Printing:** `(Print opts obj)`: The `Print` command provides access to the Coq pretty printers.
+  Its intended use is for printing (maybe IDE manipulated) objects returned by `Query`.
+
+### Roadmap and Developer organization:
+
+SerAPI is organized in branches corresponding to upstream Coq
+versions; usually, branch v8.XX is compatible with Coq 8.XX, and
+corresponds to SerAPI 0.XX. These branches are stable and can be
+relied upon.
+
+The branch `main` tracks Coq `master` branch, and it is not a stable
+branch; force pushes and random rebases can happen there; handle with
+care!
+
+We are working on fixing this problematic setup, which is that way as
+in the past such branch used to be "private", but now that SerAPI is
+in Coq's CI the development workflow has changed, with developer
+submitting PRs to it.
+
+These days, most work related to SerAPI is directly happening over
+[Coq's upstream](https://github.com/coq/coq) itself. The main
+objective is to improve the proof-document model; building a rich
+query language will be next. See the [roadmap issue]() in our bug
+tracker for more information about roadmap and the [Developer
+Information](#Developer-information) section for more details on the
+development setup.
+
+### Clients and Users:
+
+SerAPI has been used in a few contexts already, we provide a few
+pointers here, feel free to add your own!
+
+- [jsCoq](https://github.com/ejgallego/jscoq) allows you to run Coq in
+  your browser. jsCoq is the predecessor of SerAPI and will shortly be
+  fully based on it.
+- [mCoq](https://github.com/EngineeringSoftware/mcoq) is a tool for mutation analysis
+  of Coq projects, based on serializing and deserializing Coq code via SerAPI.
+  See the accompanying [tool paper](https://users.ece.utexas.edu/~gligoric/papers/JainETAL20mCoqTool.pdf),
+  and the [research paper](https://users.ece.utexas.edu/~gligoric/papers/CelikETAL19mCoq.pdf)
+  which describes and evaluates the technique.
+- [elcoq](https://github.com/cpitclaudel/elcoq), an emacs technology
+  demo based on SerAPI by [Clément Pit-Claudel](https://github.com/cpitclaudel). `elcoq` is not fully
+  functional but illustrates some noteworthy features of SerAPI.
+- [PeaCoq](https://github.com/Ptival/PeaCoq), a Coq IDE for the
+  browser, has an experimental branch that uses SerAPI.
+- [GrammaTech's Software Evolution Library (SEL)](https://grammatech.github.io/sel/)
+  provides tools for programmatically modifying and evaluating software. SEL operates
+  over multiple software representations including source code in
+  several languages and compiled machine code. Its Coq module uses
+  SerAPI to serialize Coq source code into ASTs, which are parsed into
+  Common Lisp objects for further manipulation. GrammaTech uses this
+  library to synthesize modifications to software so that it satisfies
+  an objective function, e.g., a suite of unit tests.
+  SerAPI support was added to SEL by Rebecca Swords.
+- [CoqGym](https://github.com/princeton-vl/CoqGym) is a Coq-based learning environment for theorem proving.
+  It uses SerAPI to interact with Coq and perform feature-extraction. Its author notes:
+
+  > CoqGym relies heavily on SerAPI for serializing the internal structures of Coq.
+  > I tried to use Coq's native printing functions when I started with this project,
+  > but soon I found SerAPI could save a lot of the headaches with parsing Coq's output.
+  > Thanks to SerAPI authors, this project wouldn't be possible (or at least in its current form) without SerAPI.
+
+  See also the [paper](https://arxiv.org/abs/1905.09381) describing CoqGym.
+- [Proverbot9001](https://github.com/UCSD-PL/proverbot9001) is a proof search system based on machine
+  learning techniques, and uses SerAPI to interface with Coq.
+  See also the [paper](https://arxiv.org/abs/1907.07794) describing the system.
+- [Roosterize](https://github.com/EngineeringSoftware/roosterize) is a tool for
+  suggesting lemma names in Coq projects based on machine learning.
+  See the [paper](https://arxiv.org/abs/2004.07761) describing the technique and tool.
+  Additional paper with demo: https://arxiv.org/abs/2103.01346 .
+- The [paper](https://arxiv.org/abs/2006.16743) _Learning to Format Coq Code Using Language Models_
+  implements a Coq code formatter.
+- [MathComp corpus](https://github.com/EngineeringSoftware/math-comp-corpus) is a machine learning
+  dataset based on the [Mathematical Components](https://math-comp.github.io/) family of Coq projects,
+  and includes several machine-readable representations of Coq code generated via SerAPI.
+  The dataset was used to train and evaluate the Roosterize tool.
+- A Python interface for SerAPI can be found at [PyCoq](https://github.com/IBM/pycoq)
+- A direct Python interface to Coq, using `serlib` can be found at https://github.com/ejgallego/pyCoq
+- SerAPI is being used to improve the Coq regression proof
+  selection tool [iCoq](https://cozy.ece.utexas.edu/icoq/),
+  see the [paper](https://users.ece.utexas.edu/~gligoric/papers/CelikETAL17iCoq.pdf).
+- SerAPI is being used in additional software testing and machine learning projects; we will
+  update this list as papers get out of embargo.
+
+### Quick Demo (not always up to date):
+
+```lisp
+$ rlwrap sertop --printer=human
+(Add () "Lemma addn0 n : n + 0 = n. Proof. now induction n. Qed.")
+  > (Answer 0 Ack)
+  > (Answer 0 (Added 2 ((fname "") (line_nb 1) (bol_pos 0) (line_nb_last 1) (bol_pos_last 0) (bp 0) (ep 26))
+  >            NewTip))
+  > ...
+  > (Answer 0 (Added 5 ... NewTip))
+  > (Answer 0 Completed)
+
+(Exec 5)
+  > (Answer 1 Ack)
+  > (Feedback ((id 5) (route 0) (contents (ProcessingIn master))))
+  > ...
+  > (Feedback ((id 5) (route 0) (contents Processed)))
+  > (Answer 1 Completed)
+
+(Query ((sid 3)) Goals)
+  > (Answer 2 Ack)
+  > (Answer 2
+  >  (ObjList ((CoqGoal ((fg_goals (((name 5) (ty (App (Ind ...))))
+                         (bg_goals ()) (shelved_goals ()) (given_up_goals ()))))))
+  > (Answer 2 Completed)
+
+(Query ((sid 3) (pp ((pp_format PpStr)))) Goals)
+  > (Answer 3 Ack)
+  > (Answer 3 (ObjList ((CoqString
+  >   "\
+  >    \n  n : nat\
+  >    \n============================\
+  >    \nn + 0 = n"))))
+  > (Answer 3 Completed)
+
+(Query ((sid 4)) Ast)
+  > (Answer 4 Ack)
+  > (Answer 4 (ObjList ((CoqAst ((((fname "") (line_nb 1) (bol_pos 0) (line_nb_last 1)
+  >                                (bol_pos_last 0) (bp 34) (ep 50)))
+  > ...
+  >            ((Tacexp
+  >              (TacAtom
+  >                (TacInductionDestruct true false
+  > ...
+  > (Answer 4 Completed)
+
+(pp_ex (Print ((sid 4) (pp ((pp_format PpStr)))) (CoqConstr (App (Rel 0) ((Rel 0))))))
+  > (Answer pp_ex Ack)
+  > (Answer pp_ex(ObjList((CoqString"(_UNBOUND_REL_0 _UNBOUND_REL_0)"))))
+
+(Query () (Vernac "Print nat. "))
+  > (Answer 6 Ack)
+  > (Feedback ((id 5) (route 0) (contents
+  >    (Message Notice ()
+  >    ((Pp_box (Pp_hovbox 0) ...)
+  > (Answer 6 (ObjList ()))
+  > (Answer 6 Completed)
+
+(Query () (Definition nat))
+  > (Answer 7 Ack)
+  > (Answer 7 (ObjList ((CoqMInd (Mutind ....)))))
+  > (Answer 7 Completed)
+```
+
+### Technical Report:
+
+There is a brief [technical report](https://hal-mines-paristech.archives-ouvertes.fr/hal-01384408)
+describing the motivation, design, and implementation of SerAPI. If you are using
+SerAPI in a project, please cite the technical report in any related publications:
+
+```bibtex
+@techreport{GallegoArias2016SerAPI,
+  title = {{SerAPI: Machine-Friendly, Data-Centric Serialization for Coq}},
+  author = {Gallego Arias, Emilio Jes{\'u}s},
+  url = {https://hal-mines-paristech.archives-ouvertes.fr/hal-01384408},
+  institution = {MINES ParisTech},
+  year = {2016},
+  month = Oct,
+}
+```
+
+## Developer Information
+
+### Technical Details
+
+SerAPI has four main components:
+
+- `serapi`, an extended version of the current IDE protocol;
+- `serlib`, a library providing automatic de/serialization of most Coq data structures using `ppx_conv_sexp`. This should be eventually incorporated into Coq itself. Support for `ppx_deriving_yojson` is work in progress;
+- `sertop`, `sertop_js`, toplevels offering implementations of the protocol;
+- `sercomp`, `sertok`, command-line tools providing access to key features of `serlib`.
+
+Building your own toplevels using `serlib` and `serapi` is encouraged.
+
+### Advanced Use Cases
+
+With a bit more development effort, you can also:
+
+- Use SerAPI as an OCaml library. The low-level serialization library
+  [`serlib/`](/serlib) and the higher-level SerAPI protocol in
+  [`serapi/serapi_protocol.mli`](/serapi/serapi_protocol.mli) can be
+  linked standalone.
+
+- Use SerAPI's web worker [JavaScript Worker](https://developer.mozilla.org/en-US/docs/Web/API/Web_Workers_API/Using_web_workers)
+  from your web/node application. In this model, you communicate with SerAPI using
+  the typical `onmessage/postMessage` worker API. Ready-to-use builds
+  may be found at
+  [here](https://github.com/ejgallego/jscoq-builds/tree/serapi), we
+  provide an example REPL at: https://x80.org/rhino-hawk
+
+We would also like to provide a [Jupyter/IPython kernel](https://github.com/ejgallego/coq-serapi/issues/17).
+
+### Developer/Users Mailing List
+
+SerAPI development is mainly discussed [on GitHub](https://github.com/ejgallego/coq-serapi)
+and in the [Gitter channel](https://gitter.im/coq-serapi/Lobby).
+You can also use the jsCoq mailing list by subscribing at:
+https://x80.org/cgi-bin/mailman/listinfo/jscoq
+
+The mailing list archives should also be available at the Gmane group:
+`gmane.science.mathematics.logic.coq.jscoq`. You can post to the list
+using nntp.
+
+## Acknowledgments
+
+SerAPI has been developed at the
+[Centre de Recherche en Informatique](https://www.cri.ensmp.fr) of
+[MINES ParisTech](http://www.mines-paristech.fr/) (former École de
+Mines de Paris) and was partially supported by the
+[FEEVER](http://www.feever.fr) project.
--- a/vendor/coq-serapi/ROADMAP.md
+++ b/vendor/coq-serapi/ROADMAP.md
+### Full document parsing.
+
+- Full asynchronous `Add/Cancel` protocol.
+  => Add a cache so users can efficiently send full documents.
+
+### Better Locate
+
+- Implement Locate -> "file name where the object is defined".
+- Improve locate [EJGA: how?]
+- Help with complex codepaths:
+  Load Path parsing and completion code is probably one of the most complex part of company-coq
+
+### Completion / Naming
+
+- Improve the handling of names and environments, see
+
+  `Coq.Init.Notations.instantiate` vs `instantiate`, the issue of
+  `Nametab.shortest_qualid_of_global` is a very sensible one for IDEs
+
+   Maybe we could add some options `Short`, `Full`, `Best` ? ...
+   Or we could even serialize the naming structure and let the ide decide if we export the current open namespace.
+
+### Benchmarking
+
+- add bench option to queries commands
+  basically (bench (any list of serapi commands))
+  will return BenchData
+
+- Define timing info? Maybe this is best handled at the STM level.
+
+### Misc
+
+- Redo Query API, make Query language a GADT.
+
+- Support regexps in queries.
+
+- Would be easy to get a list of vernacs? Things like `Print`, `Typeclasses eauto`, etc.
+  => ppx to enumerate datatypes. Write the help command with this and also Clément suggestions about Vernac enumeration.
+
+- enable an open CoqObject tag for plugin use (see coq/coq#209 ) ?
+
+- Checkstyle support.
+
+
--- a/vendor/coq-serapi/VERSION
+++ b/vendor/coq-serapi/VERSION
+%%VERSION%%
No results found