.github/workflows/ci.yml

+name: JsCoq's CI Action
+
+on:
+  push:
+    branches:
+    - v8.8
+    - v8.9
+    - v8.10
+    - v8.11
+    - v8.12
+    - v8.13
+    - v8.14
+    - v8.15
+    - v8.16
+    - v8.17
+  pull_request:
+    branches:
+    - v8.8
+    - v8.9
+    - v8.10
+    - v8.11
+    - v8.12
+    - v8.13
+    - v8.14
+    - v8.15
+    - v8.16
+    - v8.17
+
+  # Allows you to run this workflow manually from the Actions tab
+  workflow_dispatch:
+
+jobs:
+  build:
+    strategy:
+      matrix:
+        jscoq_arch: [32, 64]
+    env:
+      OPAMJOBS: "2"
+      OPAMROOTISOK: "true"
+      OPAMYES: "true"
+      NJOBS: "2"
+      JSCOQ_ARCH: ${{ matrix.jscoq_arch }}
+      OPAM_LINUX_URL: https://github.com/ocaml/opam/releases/download/2.1.3/opam-2.1.3-x86_64-linux
+      OPAM_MACOS_URL: https://github.com/ocaml/opam/releases/download/2.1.3/opam-2.1.3-x86_64-darwin
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: 'true'
+      - name: Install apt dependencies
+        run: |
+          sudo apt-get install aptitude
+          sudo dpkg --add-architecture i386
+          sudo aptitude -o Acquire::Retries=30 update -q
+          sudo aptitude -o Acquire::Retries=30 install gcc-multilib g++-multilib libgmp-dev:i386 -y
+      - uses: actions/setup-node@v3
+        with:
+          node-version: '16'
+          cache: 'npm'
+      - name: OPAM Set up
+        run: |
+          sudo curl -sL $OPAM_LINUX_URL -o /usr/bin/opam &&
+          sudo chmod 755 /usr/bin/opam
+      - name: OCaml Set up
+        run: |
+          opam init -y --bare --disable-sandboxing || true
+          eval $(opam env)
+          ./etc/toolchain-setup.sh --"$JSCOQ_ARCH"
+          opam switch
+          opam list
+          opam config var root
+      - name: Coq build
+        run: |
+          echo 'Using Node.js:' && node --version
+          set -e
+          echo 'Building Coq...' # && echo -en 'travis_fold:start:coq.build\\r'
+          make coq-get
+          # echo -en 'travis_fold:end:coq.build\\r'
+      - name: jsCoq build
+        run: |
+          set -e
+          echo 'Building JsCoq...' # && echo -en 'travis_fold:start:jscoq.build\\r'
+          make jscoq
+          # echo -en 'travis_fold:end:jscoq.build\\r'
+          # echo 'Building Addons...' && echo -en 'travis_fold:start:addons.build\\r'
+          # EJGA: We need to resurrect this in a different way.
+          # make addons
+          # echo -en 'travis_fold:end:addons.build\\r'
+      - name: jsCoq test
+        run: |
+          set -e
+          echo 'Testing JsCoq...' # && echo -en 'travis_fold:start:jscoq.build\\r'
+          npm install # EJGA: uggg, but otherwise this won't work.
+          make test
+          # echo -en 'travis_fold:end:jscoq.build\\r'
+  docker:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v2
+      - name: Set up Docker Buildx
+        uses: docker/setup-buildx-action@v1
+      # - name: Login to DockerHub
+      #   uses: docker/login-action@v1
+      #   with:
+      #     username: ${{ secrets.DOCKERHUB_USERNAME }}
+      #     password: ${{ secrets.DOCKERHUB_TOKEN }}
+      - name: Build (no push atm)
+        id: docker_build
+        uses: docker/build-push-action@v2
+        with:
+          file: etc/docker/Dockerfile
+          context: etc/docker
+          target: jscoq-addons
+          push: false
+          tags: jscoq/jscoq:latest
+      - name: Image digest
+        run: echo ${{ steps.docker_build.outputs.digest }}

.gitignore

 # General ignores
 *~
 .*.swp
+.cache
+/dist
+/dist-cli
+/dist-webpack
+/bin
 
 # Local build configuration file
 /config.inc
@@ -15,11 +20,14 @@ _build
 
 # Node stuff
 node_modules
+# - npm packages
+/*.tgz
 
 # Links for in-place serving
 coq-pkgs
-/coq-js/jscoq_worker.js
-*.browser.js
+/backend/jsoo/jscoq_worker.bc.js
+/backend/wasm/wacoq_worker.bc
+*.wasm
 
 # Apple stuff
 .DS_Store

.gitlab-ci.yml

-lint:
-  image: ubuntu:bionic
+stages:
+  - build
+
+jscoq:
+  stage: build
+  image: i386/debian
+
   script:
-    - cat /proc/{cpu,mem}info || true
-    - ls -a # figure out if artifacts are around
-    - printenv -0 | sort -z | tr '\0' '\n'
+    - apt update && apt upgrade && apt install -y curl git make nodejs wget gcc unzip rsync g++-multilib gcc-multilib libgmp-dev bzip2 npm zip
+    - wget https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh && chmod +x install.sh && bash -c "printf '\n' | ./install.sh" && opam init -y --disable-sandboxing
+    - echo "test -r '/root/.opam/opam-init/init.sh' && . '/root/.opam/opam-init/init.sh' > /dev/null 2> /dev/null || true" >> ~/.bashrc
+    - ./etc/toolchain-setup.sh && make coq && make jscoq && npm link
+    - source ~/.bashrc
+    - make addons
+    - cp coqdoclight.py _build/jscoq+32bit/
+    - cp coqdoclight_sample.v _build/jscoq+32bit/
+    - zip -r jscoq.zip _build/jscoq+32bit/
+  when: manual
+  artifacts:
+    paths:
+      - jscoq.zip
+    expire_in: never

.gitmodules

-[submodule "CodeMirror-TeX-input"]
-	path = ui-external/CodeMirror-TeX-input
-	url = https://github.com/ejgallego/CodeMirror-TeX-input.git
-	branch = master
-[submodule "coq-serapi"]
-	path = coq-serapi
-	url = https://github.com/ejgallego/coq-serapi.git
-	branch = v8.12

.travis.yml

-language: node_js
-
-node_js:
-- "8"
-
-matrix:
-  include:
-  - os: linux
-    env: JSCOQ_ARCH=32
-  - os: osx
-    env: JSCOQ_ARCH=64
-
-branches:
-  only:
-  - v8.8
-  - v8.9
-  - v8.9+worker
-  - v8.10
-  - v8.11
-  - v8.12
-
-addons:
-  apt:
-    packages:
-    - gcc-multilib
-  homebrew:
-    update: true
-    packages:
-    - opam
-
-cache:
-  apt: true
-  directories:
-  - $HOME/.opam
-  - $HOME/Library/Caches/Homebrew
-
-env:
-  global:
-  - NJOBS="2"
-  - OPAMROOTISOK="true"
-  - OPAMYES="true"
-  - OPAMJOBS="2"
-  - OPAM_LINUX_URL=https://github.com/ocaml/opam/releases/download/2.0.6/opam-2.0.6-x86_64-linux
-
-before_install:
-- if [ "$TRAVIS_OS_NAME" = "linux" ]; then
-    sudo curl -sL $OPAM_LINUX_URL -o /usr/bin/opam &&
-    sudo chmod 755 /usr/bin/opam; fi
-
-before_cache:
-- if [ "$TRAVIS_OS_NAME" = "osx" ]; then brew cleanup; fi
-
-install:
-- opam init -y --bare --disable-sandboxing || true
-- eval $(opam env)
-- ./etc/toolchain-setup.sh --"$JSCOQ_ARCH"
-- eval $(opam env)
-- opam switch
-- opam list
-- opam config var root
-- git submodule update --remote
-
-script:
-- echo 'Using Node.js:' && node --version
-- set -e
-- echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r'
-- make coq-get
-- echo -en 'travis_fold:end:coq.build\\r'
-- echo 'Building JsCoq...' && echo -en 'travis_fold:start:jscoq.build\\r'
-- make jscoq
-- echo -en 'travis_fold:end:jscoq.build\\r'
-- echo 'Building Addons...' && echo -en 'travis_fold:start:addons.build\\r'
-- make addons
-- echo -en 'travis_fold:end:addons.build\\r'

.vscode/tasks.json

+// See https://go.microsoft.com/fwlink/?LinkId=733558
+// for the documentation about the tasks.json format
+{
+  "version": "2.0.0",
+  "tasks": [
+    {
+      "type": "npm",
+      "script": "watch",
+      "problemMatcher": "$esbuild-watch",
+      "isBackground": true,
+      "presentation": {
+        "reveal": "always"
+      },
+      "group": {
+        "kind": "build",
+        "isDefault": true
+      }
+    }
+  ]
+}

CHANGES.md

-# JsCoq 0.12 "<-as usual->"
+# jsCoq 0.17.1 "Night slip"
+---------------------------
+
+ - Update to Coq 8.17.1. (@ejgallego)
+ - Fix some dist mishaps - missing CLI, zarith version change
+   (@corwin-of-amber)
+
+# jsCoq 0.17.0 "Rocker style"
+-----------------------------
+
+ - Update to Coq 8.17.0. (@corwin-of-amber)
+ - Add support for saving and loading scratchpad snippets using Gist (@Eladkay)
+
+# jsCoq 0.16.1 "Soupe à l’oignon"
+---------------------------------
+
+ - Split source code in `backend` and `frontend` directories
+   (@ejgallego @corwin-of-amber, #287 )
+ - wacoq build is not unified in the main repos (@ejgallego
+   @corwin-of-amber, #296 )
+ - jsCoq now uses a streamlined `esbuild` bundling process, this
+   should have quite some advantages w.r.t. loading and distribution
+   (@ejgallego, #316 )
+
+# jsCoq 0.16.0 "Paris-bound"
+----------------------------
+
+ - Update to Coq 8.16.0. (@corwin-of-amber, @ejgallego)
+ - Now Coq loads plugins using findlib, but we don't yet support that;
+   most plugins can still load in legacy mode.
+ - Port the JS codebase to ES modules (@ejgallego , @corwin-of-amber, #276)
+ - Add a quick help screen in the UI (@corwin-of-amber, #290)
+
+# jsCoq 0.15.1 "Go For Your Toad, or Similar"
+---------------------------------------
+
+ - Update to Coq 8.15.1. (@corwin-of-amber)
+ - Stabilized jsCoq SDK Docker image. (@corwin-of-amber)
+ - A new landing-page example that is more focused on showing
+   jsCoq features; added links to examples. (@corwin-of-amber,
+   help & suggestions by @hannelita, @palmskog)
+ - Added symbol generation to the build pipeline, to keep
+   completion results current. (@corwin-of-amber)
+
+# jsCoq 0.15.0 "Steady State"
+------------------------------
+
+ - Update to Coq 8.15.0 (@corwin-of-amber)
+
+# jsCoq 0.14.1 "Leap of Faith"
+------------------------------
+
+ - Update to Coq 8.14.1 (@corwin-of-amber)
+
+# jsCoq 0.14.0 "Ahead of time"
+------------------------------
+
+ - Update to Coq 8.14.0 (@ejgallego @corwin-of-amber)
+
+# jsCoq 0.13.3 "The Name of the Version is Called"
+---------------------------------------
+
+ - A critical bug fix for error sentences. (#249, corwin-of-amber)
+ - Added Coqoban package :ferris_wheel: (corwin-of-amber)
+
+# jsCoq 0.13.2 "That Sounds Like an Excellent Idea"
+---------------------------------------
+
+ - Merged the `8.13+wacoq` branch. The frontend can now operate
+   with either the JavaScript backend or the WebAssembly one.
+   (#247, corwin-of-amber)
+
+# jsCoq 0.13.1 "Action Display"
+---------------------------------------
+
+ - jsCoq's CI has been moved from Travis CI to Github actions, thanks
+   to both providers for the generous support (#242, closes #224,
+   @ejgallego)
+ - Bump required compiler version to 4.12.0 (#223, @ejgallego)
+ - Added some missing symbols for code completion. (@corwin-of-amber)
+ - A utility script `jscoqdoc` to quickly generate HTML pages with
+   jsCoq embedded. (@corwin-of-amber)
+ - Some trouble with comments just before error marker. (closes #241,
+   @corwin-of-amber)
+ - Improved indentation in pretty-printing of goals and terms. (#245,
+   @corwin-of-amber)
+
+# jsCoq 0.13.0 "Better late than never"
+---------------------------------------
+
+ - Update to Coq 8.13.0 , mostly straightforward but build
+   requirements have changed, in particular we now require
+   `js_of_ocaml >= 3.8.0`. (@ejgallego)
+ - Bump required compiler version to 4.10.2. (@ejgallego)
+ - Fixed missing indentation in pretty-printing of goals. (#126,
+   @corwin-of-amber)
+ - The long-awaited settings panel. (#12, @corwin-of-amber)
+ - Added a Coq tutorial example (@corwin-of-amber, @mdnahas)
+
+# jsCoq 0.12.3 "at midday"
+---------------------------------------
+
+ - Hidden snippets: allow some of the snippets in a literate jsCoq
+   development to be hidden from view. They are still executed when
+   they are reached, and are "stepped over". (@corwin-of-amber)
+ - Integrating Collacoq functionality into the IDE proper, now available
+   in the scratchpad page. (@ejgallego, @corwin-of-amber)
+   `js_of_ocaml >= 3.8.0` (@ejgallego)
+
+# jsCoq 0.12.2 "Square Peg, Round Hole"
+---------------------------------------
+
+ - Basically just upgrade to Coq 8.12.1, as it contains some important
+   bug fixes of the v8.12 branch. (@corwin-of-amber)
+ - Allow building with OCaml 4.10.2, since it is the earliest version
+   of OCaml that supports arm64 (Apple M1). (@corwin-of-amber)
+
+# jsCoq 0.12.1 "Emilio should write this :P"
+-----------------------------------------
+
+ - Bugfix preventing use of `lia` and other tactics that might invoke
+   bytecode functionality. (#201, @corwin-of-amber)
+ - UI tidbits: only highlight-on-hover sentences that were executed in
+   proof mode, and do not highlight preceding comments of them; try not
+   to interfere with keyboard scrolling in the page. (@corwin-of-amber)
+
+# jsCoq 0.12 "<-as usual->"
 -----------------------------------------
 
  - Port to Coq 8.12 (@ejgallego)
@@ -8,8 +134,11 @@
  - Streamlined packaging of `.coq-pkg` archives using a new `jscoq` CLI.
    (@corwin-of-amber)
  - Addons have been factored out of the main jsCoq build process. They
-   are now maintained in a seperate repository,
+   are now maintained in a separate repository,
    https://github.com/jscoq/addons. (@corwin-of-amber)
+ - Project name officially stylized "jsCoq" (lowercase j).
+ - [experimental] Edit and compile multiple-file developments. 
+   (@corwin-of-amber)
 
 # JsCoq 0.11 "<-lib->"
 -----------------------------------------

Dockerfile

+FROM i386/debian AS jscoq-dev
+CMD ["/usr/bin/python3", "-m", "http.server", "-d", "/root/jscoq", "8000" ]
+RUN apt update && apt upgrade && apt install -y curl git make nodejs wget gcc unzip rsync g++-multilib gcc-multilib libgmp-dev bzip2 npm
+RUN wget https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh && chmod +x install.sh && bash -c "printf '\n' | ./install.sh" && opam init -y --disable-sandboxing
+RUN echo "test -r '/root/.opam/opam-init/init.sh' && . '/root/.opam/opam-init/init.sh' > /dev/null 2> /dev/null || true" >> ~/.bashrc
+
+
+

LICENSE

@@ -12,60 +12,60 @@ Authors: Emilio J. Gallego Arias
 Files: notes/*
 License: AGPL-3+ / CC-BY-SA 3.0 / LGPL-2.1+
 
-Files: ui-images/checked.png
+Files: frontend/classic/images/checked.png
 License: CC-BY 3.0
 Comment:
   - Check button made by Google from www.flaticon.com, licensed under CC BY 3.0
 
-Files: ui-images/dl.png
+Files: frontend/classic/images/dl.png
 License: CC-BY 3.0
 Comment: Cloud button made by Yannick, yanlu.de from www.flaticon.com, licensed under CC BY 3.0
 
-Files: ui-images/power-button-512-black.png
+Files: frontend/classic/images/power-button-512-black.png
 License: CC-BY 3.0
 Comment: Power buton made by Freepik, www.freepik.com from www.flaticon.com, licensed under CC BY 3.0
 
-Files: ui-images/log-info.png
+Files: frontend/classic/images/log-info.png
 License: CC-BY 3.0
 Comment: Kirill Kazachek, via iconfinder [https://creativecommons.org/licenses/by/3.0/]
 
-Files: ui-images/log-error.png
+Files: frontend/classic/images/log-error.png
 License: SIL OFL
 Comment: Dave Gandy (Font Awesome), via iconfinder [https://scripts.sil.org/cms/scripts/page.php?site_id=nrsi&id=OFL]
          DinosoftLabs, via iconfinder (free for commercial use).
          Combined into a single 32x32 image.
 
-Files: ui-images/log-warn.png
+Files: frontend/classic/images/log-warn.png
 License: CC-BY 2.5
 Comment: Ben Gillbanks, via iconfinder [https://creativecommons.org/licenses/by/2.5/]
 
-Files: ui-images/log-notice.png
+Files: frontend/classic/images/log-notice.png
 License: CC-BY 3.0
 Comment: Rudy Muhardika, via iconfinder [https://creativecommons.org/licenses/by/3.0/]
          Cropped so that actual image area is a little below 32x32.
 
-Files: ui-images/reset.png, ui-images/assets/reset.svg
+Files: frontend/classic/images/reset.png, frontend/classic/images/assets/reset.svg
 License: CC-BY 3.0
 Comment: Hali Gali Harun, IT, via TheNounProject
 
-Files: ui-images/{up,down}.png, ui-images/assets/arrow.svg
+Files: frontend/classic/images/{up,down}.png, frontend/classic/images/assets/arrow.svg
 Licence: CC-BY 3.0
 Comment: Dean Mocha, TW
 
-Files: ui-images/to-cursor.png, ui-images/assets/{text,to}-cursor.svg
+Files: frontend/classic/images/to-cursor.png, frontend/classic/images/assets/{text,to}-cursor.svg
 Licence: CC-BY 3.0
 Comments: Derived work from those of Dean Mocha, TW & Icon 54, via TheNounProject
 
-Files: ui-images/github.png, ui-images/themes/dark/github.png
+Files: frontend/classic/images/github.png, frontend/classic/images/themes/dark/github.png
 Licence: Proprietary
 Comments: Fair use according to the terms of https://github.com/logos.
 
-Files: ui-images/assets/sphere.svg
+Files: frontend/classic/images/assets/sphere.svg
 Licence: CC-BY 3.0
 Comments: From Wikipedia (by Geek3) https://en.wikipedia.org/wiki/Sphere.
           Reduced number of grid lines.
 
-Files: ui-images/*
+Files: frontend/classic/images/*
 License: AGPL-3
 Comment: Other graphics are parts, and so licenced, as JsCoq.
 
@@ -73,7 +73,7 @@ Files: examples/Stlc.html
 License: BSD
 Comment: From http://https://www.cis.upenn.edu/~bcpierce/sf/
 
-Files: coq-js/js_stub/marshal*.js
+Files: backend/jsoo/js_stub/marshal*.js
 Licence: LGPL2.0
 Comment: Derived from js_of_ocaml (https://github.com/ocsigen/js_of_ocaml).
  (if js_of_ocaml updates to LGPL2.1+, then these should be updated to the same.)

Makefile

 .PHONY: all clean force
 .PHONY: jscoq jscoq_worker links links-clean
-.PHONY: dist dist-upload dist-release server
+.PHONY: dist dist-upload dist-release serve
 
 -include ./config.inc
 
 # Coq Version
-COQ_VERSION := v8.12
+COQ_VERSION := v8.17
 JSCOQ_BRANCH :=
 
 JSCOQ_VERSION := $(COQ_VERSION)
@@ -19,7 +19,7 @@ OS := ${shell uname}
 ARCH := $(OS)/$(WORD_SIZE)
 
 ifeq ($(WORD_SIZE),64)
-DUNE_WORKSPACE = $(current_dir)/dune-workspace-64
+DUNE_WORKSPACE = $(current_dir)/dune-workspace.64
 VARIANT = +64bit
 else
 VARIANT = +32bit
@@ -28,21 +28,30 @@ endif
 BUILD_CONTEXT = jscoq$(VARIANT)
 BUILDDIR = _build/$(BUILD_CONTEXT)
 
+OPAMENV = eval `opam env --set-switch --switch $(BUILD_CONTEXT)`
+DUNE = $(OPAMENV) && dune
+
 # ugly but I couldn't find a better way
 current_dir := $(dir $(realpath $(lastword $(MAKEFILE_LIST))))
 
 # Directory where the Coq sources and developments are.
-ADDONS_PATH := $(current_dir)/_vendor+$(COQ_VERSION)$(VARIANT)
-COQSRC := $(ADDONS_PATH)/coq/
+VENDOR_PATH := $(current_dir)/_vendor+$(COQ_VERSION)$(VARIANT)
+COQSRC := $(VENDOR_PATH)/coq/
 
 # Directories where Dune builds and installs Coq
 COQBUILDDIR_REL := _vendor+$(COQ_VERSION)$(VARIANT)/coq
 COQBUILDDIR := $(current_dir)/_build/$(BUILD_CONTEXT)/$(COQBUILDDIR_REL)
 COQDIR := $(current_dir)/_build/install/$(BUILD_CONTEXT)
+# Dune packages to install for Coq
+COQINST := coq coq-core coq-stdlib
+COQINST_COMMAS = $(subst $(space),$(comma),$(COQINST))
 
 COQPKGS_ROOT := $(current_dir)/_build/$(BUILD_CONTEXT)/coq-pkgs
 
-DUNE_FLAGS := ${if $(DUNE_WORKSPACE), --workspace=$(DUNE_WORKSPACE),}
+# This is very convenient when calling npm, a bit less when compiling
+# OCaml code
+DUNE_FLAGS=--no-buffer
+override DUNE_FLAGS += ${if $(DUNE_WORKSPACE), --workspace=$(DUNE_WORKSPACE),}
 
 NJOBS ?= 4
 
@@ -52,111 +61,178 @@ export BUILD_CONTEXT
 export COQDIR
 export COQBUILDDIR
 export COQBUILDDIR_REL
-export ADDONS_PATH
 export COQPKGS_ROOT
 
+ifdef DEBUG
+JSCOQ_DEBUG = 1
+export JSCOQ_DEBUG
+endif
+
+null  :=
+space := $(null) #
+comma := ,
+
 all:
 	@echo "Welcome to jsCoq makefile. Targets are:"
 	@echo ""
-	@echo "     jscoq: build jscoq [javascript and libraries]"
+	@echo "     jscoq: build jsCoq [JavaScript and libraries]"
+	@echo "     wacoq: build waCoq [JavaScript and libraries]"
+	@echo ""
+	@echo "    bundle: create the core JS bundles using esbuild in dist"
+	@echo " typecheck: typecheck using tsc"
 	@echo ""
 	@echo "     links: create links that allow to serve pages from the source tree"
+	@echo "            [note: jscoq build system auto-promotoes targets so this is obsolete]"
 	@echo ""
 	@echo "      dist: create a distribution suitable for a web server"
+	@echo "  dist-npm: create NPM packages suitable for \`npm install\`"
 	@echo "       coq: download and build Coq and addon libraries"
-	@echo "   install: install Coq and jsCoq to ~/.opam/$(BUILD_CONTEXT)"
+	@echo "   install: install Coq version used by jsCoq to ~/.opam/$(BUILD_CONTEXT)"
+
+addons: force
+	cd addons && make
 
 jscoq: force
-	dune build @jscoq $(DUNE_FLAGS)
+	$(DUNE) build @jscoq $(DUNE_FLAGS)
+
+wacoq: force
+	$(DUNE) build @wacoq $(DUNE_FLAGS)
+
+coq-pkgs: force
+	$(DUNE) build coq-pkgs $(DUNE_FLAGS)
 
 jscoq_worker:
-	dune build @jscoq_worker $(DUNE_FLAGS)
+	$(DUNE) build @jscoq_worker $(DUNE_FLAGS)
+
+wacoq_worker:
+	$(DUNE) build @wacoq_worker $(DUNE_FLAGS)
 
 install:
-	dune build -p coq $(DUNE_FLAGS)
-	dune install coq $(DUNE_FLAGS)
+	$(DUNE) build -p $(COQINST_COMMAS) $(DUNE_FLAGS)
+	$(DUNE) install $(COQINST) $(DUNE_FLAGS)
 
 links:
 	ln -sf _build/$(BUILD_CONTEXT)/coq-pkgs .
-	ln -sf ../_build/$(BUILD_CONTEXT)/coq-js/jscoq_worker.bc.js coq-js/jscoq_worker.js
+	ln -sf ../../_build/$(BUILD_CONTEXT)/backend/jsoo/jscoq_worker.bc.js backend/jsoo/jscoq_worker.bc.js
+	ln -sf ../../_build/jscoq+64bit/backend/wasm/wacoq_worker.bc backend/wasm/wacoq_worker.bc
+	ln -sf ../../_build/jscoq+64bit/backend/wasm/dlllib_stubs.wasm backend/wasm/dlllib_stubs.wasm
+	ln -sf ../../_build/jscoq+64bit/backend/wasm/dllcoqrun_stubs.wasm backend/wasm/dllcoqrun_stubs.wasm
 
 links-clean:
-	rm -f coq-pkgs coq-js/jscoq_worker.js
+	rm -f coq-pkgs backend/jsoo/jscoq_worker.bc.js backend/wasm/wacoq_worker.bc \
+	       backend/wasm/dlllib_stubs.wasm backend/wasm/dllcoqrun_stubs.wasm
+
+.PHONY:modules bundle typecheck bundle-webpack
+modules:
+	$(DUNE) build node_modules
+
+bundle:
+	$(DUNE) build dist dist-cli
+
+bundle-webpack:
+	$(DUNE) build dist-webpack --no-buffer
+
+typecheck:
+	$(DUNE) build node_modules
+	$(DUNE) exec --context=$(BUILD_CONTEXT) -- npm run typecheck
 
 # Build symbol database files for autocomplete
-coq-pkgs/%.symb: coq-pkgs/%.json
-	node --max-old-space-size=2048 ui-js/coq-cli.js --require-pkg $< --inspect $@
+coq-pkgs/%.symb.json: coq-pkgs/%.coq-pkg
+	@node --max-old-space-size=2048 ./dist-cli/cli.cjs run --require-pkg $* --inspect $@
+
+libs-symb: ${patsubst %.coq-pkg, %.symb.json, ${wildcard coq-pkgs/*.coq-pkg}}
+
+########################################################################
+# Developer Zone                                                       #
+########################################################################
+
+.PHONY: test watch serve dev
 
-libs-symb: ${patsubst %.json, %.symb, coq-pkgs/init.json ${wildcard coq-pkgs/coq-*.json}}
+test:
+	$(DUNE) exec --context=$(BUILD_CONTEXT) $(DUNE_FLAGS) -- npx mocha tests/main.js
+
+watch: DUNE_FLAGS+=--watch
+watch: jscoq
+
+serve:
+	npx http-server $(BUILDDIR) -p 8013 -c 0
+
+dev:
+	$(MAKE) serve &
+	$(MAKE) watch
 
 ########################################################################
 # Clean                                                                #
 ########################################################################
 
 clean:
-	dune clean
+	$(DUNE) clean
+	rm -f jscoq-*.tgz
+
+distclean: clean
+	rm -rf $(COQSRC)
 
 ########################################################################
 # Dists                                                                #
 ########################################################################
 
+dist: dist-npm dist-tarball
+
 BUILDOBJ = ${addprefix $(BUILDDIR)/./, \
-	cli.js coq-js/jscoq_worker.bc.js coq-pkgs \
-	ui-js ui-css ui-images examples \
-	node_modules ui-external/CodeMirror-TeX-input}
+	jscoq.js coq-pkgs frontend backend dist dist-cli dist-webpack examples docs}
 DISTOBJ = README.md index.html package.json package-lock.json $(BUILDOBJ)
 DISTDIR = _build/dist
 
 PACKAGE_VERSION = ${shell node -p 'require("./package.json").version'}
 
-dist: jscoq
-	mkdir -p $(DISTDIR)
-	rsync -apR --delete $(DISTOBJ) $(DISTDIR)
-
-TAREXCLUDE = --exclude node_modules --exclude '*.cma' \
+TAREXCLUDE = --exclude assets --exclude '*.cma' \
+	--exclude '*.bak' --exclude '*.tgz' \
     ${foreach dir, Coq Ltac2 mathcomp, \
 		--exclude '${dir}/**/*.vo' --exclude '${dir}/**/*.cma.js'}
 
-dist-tarball: dist
-	# Hack to make the tar contain a jscoq-x.x directory
+dist-tarball:
+	@echo
+	mkdir -p $(DISTDIR)
+	rsync -apR --delete $(DISTOBJ) $(DISTDIR)
+	@# Hack to make the tar contain a jscoq-x.x directory
 	@rm -f _build/jscoq-$(PACKAGE_VERSION)
 	ln -fs dist _build/jscoq-$(PACKAGE_VERSION)
-	tar zcf /tmp/jscoq-$(PACKAGE_VERSION).tar.gz   \
-	    -C _build $(TAREXCLUDE) --exclude '*.bak' --exclude '*.tar.gz' \
+	tar zcf /tmp/jscoq-$(PACKAGE_VERSION)-dist.tgz -C _build $(TAREXCLUDE) \
 	    --dereference jscoq-$(PACKAGE_VERSION)
-	mv /tmp/jscoq-$(PACKAGE_VERSION).tar.gz $(DISTDIR)
+	mv /tmp/jscoq-$(PACKAGE_VERSION)-dist.tgz $(DISTDIR)
 	@rm -f _build/jscoq-$(PACKAGE_VERSION)
+	@echo ">" $(DISTDIR)/jscoq-$(PACKAGE_VERSION)-dist.tgz
 
-NPMOBJ = ${filter-out %/node_modules %/index.html, $(DISTOBJ)}
+NPMOBJ = ${filter-out index.html package-lock.json, $(DISTOBJ)}
 NPMSTAGEDIR = _build/package
-NPMEXCLUDE = --delete-excluded --exclude '*.cma' \
-    ${foreach dir, Coq Ltac2 mathcomp, \
-		--exclude '${dir}/**/*.vo' --exclude '${dir}/**/*.cma.js'}
+NPMEXCLUDE = --delete-excluded --exclude assets --exclude _build
 
 dist-npm:
+	@echo
 	mkdir -p $(NPMSTAGEDIR) $(DISTDIR)
 	rsync -apR --delete $(NPMEXCLUDE) $(NPMOBJ) $(NPMSTAGEDIR)
 	cp docs/npm-landing.html $(NPMSTAGEDIR)/index.html
-	sed -i.bak 's/\(is_npm:\) false/\1 true/' $(NPMSTAGEDIR)/ui-js/jscoq-loader.js
-	tar zcf $(DISTDIR)/jscoq-$(PACKAGE_VERSION)-npm.tar.gz   \
-	    -C ${dir $(NPMSTAGEDIR)} --exclude '*.bak' ${notdir $(NPMSTAGEDIR)}
-
-########################################################################
-# Local stuff and distributions
-########################################################################
-
-# Private paths, for releases and local builds.
-WEB_DIR=~/x80/jscoq-builds/$(JSCOQ_VERSION)/
-RELEASE_DIR=~/research/jscoq-builds/
+	cd $(DISTDIR) && npm pack $(PWD)/$(NPMSTAGEDIR)
+	@echo ">" $(DISTDIR)/jscoq-$(PACKAGE_VERSION).tgz
 
-dist-upload: dist
-	rsync -avzp --delete $(DISTDIR)/ $(WEB_DIR)
+#
+# The following needs to be changed if we want to create separate `jscoq` and `wacoq` packages
+#
+WACOQ_NPMOBJ = README.md \
+	jscoq.js frontend backend examples dist docs
+# ^ plus `package.json` and `docs/npm-landing.html` that have separate treatment
 
-dist-release: dist
-	rsync -avzp --delete --exclude=README.md --exclude=get-hashes.sh --exclude=.git $(DISTDIR)/ $(RELEASE_DIR)
+dist-npm-wacoq:
+	mkdir -p $(NPMSTAGEDIR) $(DISTDIR)
+	rm -rf ${add-prefix $(NPMSTAGEDIR)/, backend coq-pkgs}  # in case these were created by jsCoq :/
+	rsync -apR --delete $(NPMEXCLUDE) $(WACOQ_NPMOBJ) $(NPMSTAGEDIR)
+	cp package.json.wacoq $(NPMSTAGEDIR)/package.json
+	cp docs/npm-landing.html $(NPMSTAGEDIR)/index.html
+	npm pack ./$(NPMSTAGEDIR)
 
-# all-dist: dist dist-release dist-upload
-all-dist: dist dist-release dist-upload
+# The need to maintain and update `package.json.wacoq` alongside `package.json`
+# is absolutely bothersome. I could not conjure a more sustainable way to emit
+# two separate NPM packages from the same source tree, though.
 
 ########################################################################
 # Externals
@@ -164,45 +240,28 @@ all-dist: dist dist-release dist-upload
 
 .PHONY: coq coq-get coq-get-latest coq-build
 
-COQ_BRANCH = V8.12.0
-COQ_BRANCH_LATEST = v8.12
+COQ_BRANCH = V8.17.1
+COQ_BRANCH_LATEST = v8.17
 COQ_REPOS = https://github.com/coq/coq.git
 
-COQ_PATCHES = trampoline cps timeout $(COQ_PATCHES|$(WORD_SIZE)) $(COQ_PATCHES|$(ARCH))
+COQ_PATCHES = trampoline fold timeout $(COQ_PATCHES|$(WORD_SIZE)) $(COQ_PATCHES|$(ARCH))
 
 COQ_PATCHES|64 = coerce-32bit
-COQ_PATCHES|Darwin/32 = byte-only
 
 $(COQSRC):
-	git clone --depth=1 -b $(COQ_BRANCH) $(COQ_REPOS) $@
+	git -c advice.detachedHead=false clone --depth=1 -b $(COQ_BRANCH) $(COQ_REPOS) $@
 	cd $@ && git apply ${foreach p,$(COQ_PATCHES),$(current_dir)/etc/patches/$p.patch}
 
+coq_configure=./tools/configure/configure.exe
+
 coq-get: $(COQSRC)
-	eval `opam env --switch=$(BUILD_CONTEXT)` && \
-	cd $(COQSRC) && ./configure -prefix $(COQDIR) -native-compiler no -bytecode-compiler no -coqide no
+	$(OPAMENV) && \
+	cd $(COQSRC) && dune exec $(DUNE_FLAGS) $(coq_configure) --context=$(BUILD_CONTEXT) -- -prefix $(COQDIR) -native-compiler no -bytecode-compiler no
+	# Temporarily re-enable Dune for libs (disabled in 8.17)
+	cd $(COQSRC) && cp theories/dune.disabled theories/dune
+	cd $(COQSRC) && cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune
 
 coq-get-latest: COQ_BRANCH = $(COQ_BRANCH_LATEST)
 coq-get-latest: coq-get
 
 coq: coq-get
-
-test:
-	@cp -r tests $(BUILDDIR)
-	cd $(BUILDDIR) && npx mocha tests/main.js
-
-server:
-	npx http-server $(BUILDDIR) -p 8012
-
-
-# - These are deprecated (use jscoq/addons repo instead)
-
-addon-%-get:
-	make -f coq-addons/$*.addon get
-
-addon-%-build:
-	make -f coq-addons/$*.addon build
-
-addons-get: ${foreach v,$(ADDONS),addon-$(v)-get}
-addons-build: ${foreach v,$(ADDONS),addon-$(v)-build}
-
-addons: addons-get addons-build

README.md

-Run the Coq Proof Assistant in your browser!
-------------------------
+jscoq light
+--------------------
 
-[![Build Status](https://travis-ci.org/jscoq/jscoq.svg?branch=v8.12)](https://travis-ci.org/ejgallego/jscoq) [![Gitter](https://badges.gitter.im/jscoq/Lobby.svg)](https://gitter.im/jscoq/Lobby)
+A trimmed down version of jscoq for teaching purposes.
 
-jsCoq is an Online Integrated Development Environment for the
-[Coq](https://coq.inria.fr) proof assistant and runs in your browser!
-We aim to enable new UI/interaction possibilities and to improve the
-accessibility of the Coq platform itself. Current stable version is
-jsCoq v8.12+0.12.0 supporting Coq 8.12.0, try it:
+### First time setup
 
-<https://jscoq.github.io>
+- Install docker. Docker requires `sudo` by default, because it uses `chroot` to create a lightweight "virtual machine".
+If you are not comfortable with this, there exists an experimental [rootless version of Docker ](https://docs.docker.com/engine/security/rootless/). However, I haven't yet tested whether it works.
 
-jsCoq is written to conform to ES2017, any recent standard-compliant
-browser. No servers or external programs are needed. See the
-[Troubleshooting](#Troubleshooting) section if you have problems.
-
-jsCoq is community-developed by a [team of contributors](#Credits).
-
-## Are you a jsCoq user?
-
-Have you developed or taught a course **using jsCoq**? Do you have some feedback for us?
-
-If so, please submit a pull request or an issue so we can add your
-lectures to the list of [jsCoq users](#jsCoq-Users). This is essential
-to guarantee future funding of the project.
-
-## Basic Usage
-
-The main page showcases jsCoq by walking through a proof for the infinitude of primes using
-[`math-comp`](https://github.com/math-comp/math-comp), due to Georges Gonthier.
-
-Once jsCoq finishes loading, you can step through the proof using the
-arrow buttons on the toolbar (top right), or using these keyboard
-shortcuts:
-
-| Shortcut           | Action           |
-|--------------------|------------------|
-| Alt-N or Alt-↓     | Go to next       |
-| Alt-P or Alt-↑     | Go to previous   |
-| Alt-Enter or Alt-→ | Go to cursor     |
-
-You can open a blank editor and experiment with your own Coq developments using the
-[scratchpad](https://jscoq.github.io/node_modules/jscoq/examples/scratchpad.html).
-The same keyboard shortcuts apply here.
-
-The scratchpad's contents are saved in your browser's local storage (IndexedDB, specifically),
-so they are not lost if you close the browser window or refresh the page.
-You can, in fact, store more than one document using the local open/save file dialogs:
-
-| Shortcut           | Action                                                                       |
-|--------------------|------------------------------------------------------------------------------|
-| Ctrl-S             | Save file (with the last name provided, or `untitled.v`)                     |
-| Ctrl-Shift-S       | Save file as (prompts for file name)                                         |
-| Ctrl-Alt-S         | Save file to disk (using the browser's Save dialog, or preset destination)   |
-| Ctrl-O             | Open file (prompts for file name, supports tab completion)                   |
-| Ctrl-Alt-O         | Open file from disk (using the browser's Open dialog)                        |
-
-On Mac, replace Ctrl with ⌘ (command) and Alt with ⌥ (option), as is traditional.
-
-## How to build your own jsCoq documents
-
-See the [dedicated page](docs/embedding.md) for information on advanced
-options and jsCoq HTML embedding API. A quick setup can be done with:
+- In the root of the project run `sudo docker build --tag jscoq-dev-image .` this will take a while.
 
+- While still in the root of the project, create a container using 
 ```
-$ npm install jscoq
+sudo docker container create -p 8000:8000 --mount type=bind,source=.,target=/root/jscoq --name jscoq-dev jscoq-dev-image
 ```
 
-then copy and adapt the [template page](https://github.com/ejgallego/jscoq/blob/v8.12/examples/npm-template.html)
-page to your needs.
-
-*For a more detailed tutorial and information, refer to* [docs/embedding.md](docs/embedding.md).
-
-## Collacoq
-
-A small pastebin-like server based on haste is available at
-https://x80.org/collacoq.
-Note that this service is experimental, data loss is guaranteed as we don't backup the server.
-
-The `haste` branch we use is available at https://github.com/ejgallego/haste-server/tree/collacoq
-Help with Collacoq is very welcome!
-
-##  Contributing and Developer Information
-
-See the [dedicated page](docs/developing.md) for developer information
-as well as links to past versions and tools.
-
-This is a beta-status project, but any contribution or comment is
-really welcome! See [the contributing guide](CONTRIBUTING.md) for more
-information.
-
-## Publications
-
-See the [dedicated file](docs/papers.md)
-
-## Examples
-
-The main page includes a proof of the infinitude of primes by
-G. Gonthier. We provide some more examples as a showcase of the tool:
-
-- The Logical Foundations suite:
-  + https://x80.org/rhino-coq/v8.11/examples/lf/
-  + https://x80.org/rhino-coq/v8.11/examples/plf/
-
-- dft.v: https://x80.org/rhino-coq/v8.11/examples/dft.html
-
-  A small development of the theory of the Fourier Transform following
-  Julius Orion Smith III's "The Mathematics of the Discrete Fourier
-  Transform"
-
-- equations: https://x80.org/rhino-coq/v8.11/examples/equations_intro.htmla
-
-  Introduction to the [Coq Equations](https://github.com/mattam82/Coq-Equations) package from
-  the official documentation.
-
-- Stlc: The "Simply Typed Lambda Calculus" chapter from Software
-  Foundations by Benjamin Pierce et al:
-
-  https://x80.org/rhino-coq/v8.11/examples/Stlc.html
-
-- Mike's Nahas Tutorial: https://corwin-of-amber.github.io/jscoq/tut/nahas/nahas_tutorial.html
-
-### Outdated examples [but still working]
-
-- The IRIS program logic, by Robbert Krebbers et al.
-
-  https://x80.org/rhino-coq/v8.9/examples/iris.html
-
-- Mtac: The Mtac tutorial by Beta Zilliani:
-
-  https://x80.org/rhino-coq/v8.5/examples/mtac_tutorial.html
-
-- StackMachine: The First chapter of the book "Certified Programming
-  with Dependent Types" by Adam Chlipala:
-
-  https://x80.org/rhino-coq/v8.5/examples/Cpdt.StackMachine.html
-
-- MirrorCore:
-
-  - A simple demo:
-    https://x80.org/rhino-coq/v8.5/examples/mirrorcore.html
-
-  - A demo of developing a cancellation algorithm for commutative
-    monoids:
-    https://x80.org/rhino-coq/v8.5/examples/mirror-core-rtac-demo.html
-
-## jsCoq Users:
-
-Incomplete list of places where jsCoq has been used:
-
-* Coq Winter School 2016: “Advanced Software Verification And Computer Proof”. _Sophia Antipolis_
-  https://team.inria.fr/marelle/en/advanced-coq-winter-school-2016/
-* Coq Winter School 2016-2017 (SSReflect & MathComp) “Advanced
-  Software Verification And Computer Proof”. _Sophia Antipolis_
-  https://team.inria.fr/marelle/en/advanced-coq-winter-school-2016-2017/
-* Mathematical Components, an Introduction, _Satellite workshop of the ITP 2016 conference_, August 27th, Nancy, France
-  https://github.com/math-comp/wiki/wiki/tutorial-itp2016
-* Several examples of the "Mathematical Components Book" https://math-comp.github.io/mcb/
-* School on "Preuves et Programmes" at l'École de Mines https://www-sop.inria.fr/marelle/mines/
-* Mini Corso di Coq a Pavoda: http://www-sop.inria.fr/members/Enrico.Tassi/padova2017/
-* Elpi Tutorial / Demo at CoqPL 2017 _Los Angeles_ https://lpcic.github.io/coq-elpi-www/tutorial-demo_CoqPL2018.html
-* Coq Winter School 2017-2018 (SSReflect & MathComp) _Sophia Antipolis_ https://team.inria.fr/marelle/en/coq-winter-school-2017-2018-ssreflect-mathcomp/
-* Lectures at the "Journées Nationales du Calcul Formel" by Assia Mahboubi:
-  https://specfun.inria.fr/amahboub/Jncf18/cours2.html
-* [Types Summer School](https://sites.google.com/view/2018eutypesschool/home): http://www-sop.inria.fr/teams/marelle/types18/
-* Coq Winter School 2018-2019 (SSReflect & MathComp)  https://team.inria.fr/marelle/en/coq-winter-school-2018-2019-ssreflect-mathcomp/
-* CASS 2020, Coq Andes Summer School https://cass.pleiad.cl/
-* [Lectures on Separation Logic](https://madiot.fr/sepcourse/) by Jean-Marie Madiot in MPRI's course "Proofs of programs", using Arthur Charguéraud's material. [See it in action!](https://madiot.fr/sepcourse/coq/)
-
-### jsCoq in the press
-
-- http://www.mines-paristech.fr/Actualites/jsCoq-ou-Coq-dans-un-navigateur/2118
-- https://news.ycombinator.com/item?id=9836900
-
-### Addon Packages:
-
-One of jsCoq's strengths is its support for bundling addon
-packages. In order to add your Coq package to jsCoq, you need to add a
-definition file in the `coq-addons` repository. We recommend you use
-one of the existing files as a model.
-
-Also, you need to define a jsCoq package by editing the
-`coq-jslib/dftlibs.ml` file. Once that is done, call `make jscoq`
-again.
-
-## Troubleshooting
-
-**Are you getting a `StackOverflow` exception?** Unfortunately these
-are hard to fix; you may be stuck with them for a while.
-
-* Clearing the browser cache usually solves lots of issues.
-* Change browser, if using Firefox try Chrome, if using Chrome try Firefox.
-
-### Reporting Bugs ###
-
-Feel free to use the issue tracker. Please include your
-browser/OS/user-agent and command line options.
-
-### Contact and on-line help ###
-
-- [jsCoq's gitter](https://gitter.im/jscoq/Lobby): main developer chat
-
-- The jsCoq mailing list:
-  https://x80.org/cgi-bin/mailman/listinfo/jscoq
-
-  The list archives should be also available through Gmane at group:
-  `gmane.science.mathematics.logic.coq.jscoq`
-  you can post to the list using nntp.
-
-- Coq's discourse [use the jscoq tag] https://coq.discourse.group/
-- StackOverflow [use the jscoq tag] https://stackoverflow.com/
-
-### What is broken ###
-
-* Loading ML modules is slow.
-* Loading `.vo` files is slow.
-* There surely are threading and performance problems.
-* `vm_compute` and `native_compute` fall back to regular `compute`.
+- You can now start the container using `sudo docker container start jscoq-dev`. This runs a web server hosting your local version of jscoq on port 8000. You can stop it using `sudo docker container stop jscoq-dev`.
 
-## Documents
+- After the container has been started, run `sudo docker exec -it jscoq-dev bash -c "cd /root/jscoq && ./etc/toolchain-setup.sh && make coq && make jscoq && npm link"` to compile everything for the first time
 
-See the `etc/notes/` directory for some random notes about the project.
+### Compiling jscoq
 
-## Credits
+- Make sure the container is started by running `sudo docker container start jscoq-dev`
 
-### Core developer team
+- Run `sudo docker exec -it jscoq-dev bash` : you are now in a shell inside the container.
 
-- [Emilio Jesús Gallego Arias](https://www.irif.fr/~gallego/) , Inria, Université de Paris, IRIF
-- [Shachar Itzhaky](https://cs.technion.ac.il/~shachari/) , Technion
+- `cd /root/jscoq` to enter to the `jscoq` directory source. 
+This is a bind mount, meaning `/root/jscoq` inside the container is actually the same directory as the git repository on your machine. You can edit the source code of jscoq outside of the container and the changes will be reflected inside the container.
 
-### Past Contributors
+- To compile jscoq, run `make jscoq`. The result will be saved in `_build/jscoq+32bit`. You can upload this directory to a web server; it contains an `index.html` which should work in your browser.
 
-- Benoît Pin, [CRI, MINES ParisTech](https://www.cri.ensmp.fr)
+- You don't need to copy this directory to a web server to test your version, [the docker container runs a web server for this purpose](http://localhost:8000/_build/jscoq%2B32bit/).
 
-## Acknowledgements
 
-![FEEVER Logo](/ui-images/feever-logo.png?raw=true "Feever Logo")
+### Adding your own Coq files
 
-jsCoq was made possible thanks to funding by the
-[FEEVER](http://feever.fr) project and support from [MINES
-ParisTech](http://www.mines-paristech.eu)
+You can add your own Coq files in the directory `./addons/teach/workdir/theories/` if you recompile jscoq (using `make jscoq`) they will be compiled. 
+You can compile only your files using `make addons` at the root of the directory inside the container.
 
-We want to _strongly thank_ the `js_of_ocaml` developers. Without
-their great and quick support jsCoq wouldn't have been possible.
+Then, you will be able to use `From Teach Require Import YourFile` in jscoq.
 
-[CodeMirror](https://codemirror.net/) has played a crucial role in the
-project, we are very happy with it, thanks a lot!
+### Creating your own worksheets
 
-Please consider supporting the development of CodeMirror with a donation.
+You can modify `index.html` to create your own worksheet. 
+(TODO: expand on this).

README.original.md

+Run the Coq Proof Assistant in your browser!
+------------------------
+
+![Build Status](https://github.com/jscoq/jscoq/actions/workflows/ci.yml/badge.svg)
+
+jsCoq is an Online Integrated Development Environment for the
+[Coq](https://coq.inria.fr) proof assistant and runs in your browser!
+We aim to enable new UI/interaction possibilities and to improve the
+accessibility of the Coq platform itself. Current stable version is
+jsCoq 0.16.1 supporting Coq 8.16.0, try it:
+
+<https://coq.vercel.app>
+
+jsCoq is written to conform to ES2017; any recent standard-compliant
+browser should be able to run it. No servers or external programs are needed.
+See the [Troubleshooting](#Troubleshooting) section if you have problems.
+
+jsCoq is community-developed by a [team of contributors](#Credits).
+
+## Are you a jsCoq user?
+
+Have you developed or taught a course **using jsCoq**? Do you have some feedback for us?
+
+If so, please submit a pull request or an issue so we can add your
+lectures to the list of [jsCoq users](#jsCoq-Users). This is essential
+to guarantee future funding of the project.
+
+## Basic Usage
+
+The main page showcases jsCoq by walking through a proof for the infinitude of primes using
+[`math-comp`](https://github.com/math-comp/math-comp), due to Georges Gonthier.
+
+Once jsCoq finishes loading, you can step through the proof using the
+arrow buttons on the toolbar (top right), or using these keyboard
+shortcuts:
+
+| Shortcut           | Action           |
+|--------------------|------------------|
+| Alt-N or Alt-↓     | Go to next       |
+| Alt-P or Alt-↑     | Go to previous   |
+| Alt-Enter or Alt-→ | Go to cursor     |
+
+You can open a blank editor and experiment with your own Coq developments using the
+[scratchpad](https://coq.vercel.app/scratchpad.html).
+The same keyboard shortcuts apply here.
+
+The scratchpad's contents are saved in your browser's local storage (IndexedDB, specifically),
+so they are not lost if you close the browser window or refresh the page.
+You can, in fact, store more than one document using the local open/save file dialogs:
+
+| Shortcut           | Action                                                                       |
+|--------------------|------------------------------------------------------------------------------|
+| Ctrl-S             | Save file (with the last name provided, or `untitled.v`)                     |
+| Ctrl-Shift-S       | Save file as (prompts for file name; also has options to download or share the content)  |
+| Ctrl-Alt-S         | Save file to disk (using the browser's Save dialog, or preset destination)   |
+| Ctrl-O             | Open file (prompts for file name, supports tab completion)                   |
+| Ctrl-Alt-O         | Open file from disk (using the browser's Open dialog)                        |
+
+On Mac, replace Ctrl with ⌘ (command) and Alt with ⌥ (option), as is traditional.
+
+Drag `.v` files from your local drive onto the scratchpad to open them.
+You can also drag multiple files, which will open up a project pane to the left of the editor, allowing you to switch between them; this functionality is still experimental.
+
+### Sharing your development
+
+A small pastebin-like server based on [Hastebin](https://hastebin.com) is available for sharing `.v` files between users.
+Open the save dialog (Ctrl-Shift-S) and click "Share"; then share the URL from your browser's location bar with anyone you like.
+The URL represents the state of the document at the moment it was shared, and this state is read-only. Every time you click "Share", a fresh URL is generated.
+Shared content is not saved forever, though; documents are typically available for a period of ~30 days.
+
+## How to build your own jsCoq documents
+
+See the [dedicated page](docs/embedding.md) for information on advanced
+options and jsCoq HTML embedding API. A quick setup can be done with:
+
+```
+$ npm install jscoq
+```
+
+then copy and adapt the [template page](https://github.com/ejgallego/jscoq/blob/v8.14/examples/npm-template.html)
+page to your needs.
+
+*For a more detailed tutorial and information, refer to* [docs/embedding.md](docs/embedding.md).
+
+##  Contributing and Developer Information
+
+See the [dedicated page](docs/developing.md) for developer information
+as well as links to past versions and tools.
+
+This is a beta-status project, but any contribution or comment is
+really welcome! See [the contributing guide](CONTRIBUTING.md) for more
+information.
+
+## Publications
+
+See the [dedicated file](docs/papers.md)
+
+## Examples
+
+The main page includes a proof of the infinitude of primes by
+G. Gonthier. We provide some more examples as a showcase of the tool:
+
+- The Software Foundations suite (so far, LF and PLF volumes):
+  + https://jscoq.github.io/ext/sf
+
+ - Mike Nahas's Coq Tutorial: https://corwin-of-amber.github.io/jscoq/tut/nahas/nahas_tutorial.html
+
+### Outdated examples [but still working]
+
+- dft.v: https://x80.org/rhino-coq/v8.11/examples/dft.html
+
+  A small development of the theory of the Fourier Transform following
+  Julius Orion Smith III's "The Mathematics of the Discrete Fourier
+  Transform"
+
+- equations: https://x80.org/rhino-coq/v8.11/examples/equations_intro.htmla
+
+  Introduction to the [Coq Equations](https://github.com/mattam82/Coq-Equations) package from
+  the official documentation.
+
+- The IRIS program logic, by Robbert Krebbers et al.
+
+  https://x80.org/rhino-coq/v8.9/examples/iris.html
+
+- Mtac: The Mtac tutorial by Beta Zilliani:
+
+  https://x80.org/rhino-coq/v8.5/examples/mtac_tutorial.html
+
+- StackMachine: The First chapter of the book "Certified Programming
+  with Dependent Types" by Adam Chlipala:
+
+  https://x80.org/rhino-coq/v8.5/examples/Cpdt.StackMachine.html
+
+- MirrorCore:
+
+  - A simple demo:
+    https://x80.org/rhino-coq/v8.5/examples/mirrorcore.html
+
+  - A demo of developing a cancellation algorithm for commutative
+    monoids:
+    https://x80.org/rhino-coq/v8.5/examples/mirror-core-rtac-demo.html
+
+## jsCoq Users:
+
+Incomplete list of places where jsCoq has been used:
+
+* Coq Winter School 2016: “Advanced Software Verification And Computer Proof”. _Sophia Antipolis_
+  https://team.inria.fr/marelle/en/advanced-coq-winter-school-2016/
+* Coq Winter School 2016-2017 (SSReflect & MathComp) “Advanced
+  Software Verification And Computer Proof”. _Sophia Antipolis_
+  https://team.inria.fr/marelle/en/advanced-coq-winter-school-2016-2017/
+* Mathematical Components, an Introduction, _Satellite workshop of the ITP 2016 conference_, August 27th, Nancy, France
+  https://github.com/math-comp/wiki/wiki/tutorial-itp2016
+* Several examples of the "Mathematical Components Book" https://math-comp.github.io/mcb/
+* School on "Preuves et Programmes" at l'École de Mines https://www-sop.inria.fr/marelle/mines/
+* Mini Corso di Coq a Pavoda: http://www-sop.inria.fr/members/Enrico.Tassi/padova2017/
+* Elpi Tutorial / Demo at CoqPL 2017 _Los Angeles_ https://lpcic.github.io/coq-elpi-www/tutorial-demo_CoqPL2018.html
+* Coq Winter School 2017-2018 (SSReflect & MathComp) _Sophia Antipolis_ https://team.inria.fr/marelle/en/coq-winter-school-2017-2018-ssreflect-mathcomp/
+* Lectures at the "Journées Nationales du Calcul Formel" by Assia Mahboubi:
+  https://specfun.inria.fr/amahboub/Jncf18/cours2.html
+* [Types Summer School](https://sites.google.com/view/2018eutypesschool/home): http://www-sop.inria.fr/teams/marelle/types18/
+* Coq Winter School 2018-2019 (SSReflect & MathComp)  https://team.inria.fr/marelle/en/coq-winter-school-2018-2019-ssreflect-mathcomp/
+* CASS 2020, Coq Andes Summer School https://cass.pleiad.cl/
+* [Lectures on Separation Logic](https://madiot.fr/sepcourse/) by Jean-Marie Madiot in MPRI's course "Proofs of programs", using Arthur Charguéraud's material. [See it in action!](https://madiot.fr/sepcourse/coq/)
+* [EPIT 2020 - Spring School on Homotopy Type Theory](https://github.com/HoTT/EPIT-2020)
+
+### jsCoq in the press
+
+- http://www.mines-paristech.fr/Actualites/jsCoq-ou-Coq-dans-un-navigateur/2118
+- https://news.ycombinator.com/item?id=9836900
+
+### Addon Packages
+
+One of jsCoq's strengths is its support for bundling addon
+packages. In order to add your Coq package to jsCoq, you need to compile
+it with jsCoq's version of Coq.
+Head over to [jscoq/addons](https://github.com/jscoq/addons) for pointers to
+some well-known packages that have been compiled for jsCoq and are bundled
+with every version of jsCoq.
+You can use these as examples for bundling your own libraries.
+
+## Troubleshooting
+
+**Are you getting a `StackOverflow` exception?** Unfortunately these
+are hard to fix; you may be stuck with them for a while.
+
+* Clearing the browser cache usually solves lots of issues.
+* Change browser, if using Firefox try Chrome, if using Chrome try Firefox.
+
+### Reporting Bugs ###
+
+Feel free to use the issue tracker. Please include your
+browser/OS/user-agent and any command-line options.
+
+### Contact and on-line help ###
+
+- [jsCoq's Zulip Room](https://coq.zulipchat.com/#narrow/stream/256336-jsCoq), main developer chat
+- [jsCoq's gitter](https://gitter.im/jscoq/Lobby), legacy developer chat
+- [Coq's discourse](https://coq.discourse.group/) [use the jscoq tag], for general announcements and questions
+- [StackOverflow](https://stackoverflow.com/) [use the jscoq tag]
+
+### What is broken ###
+
+* Loading ML modules is slow.
+* Loading `.vo` files is slow.
+* There surely are threading and performance problems.
+* `vm_compute` and `native_compute` fall back to regular `compute`.
+
+## Documents
+
+See the `etc/notes/` directory for some random notes about the project.
+
+## Credits
+
+### Core developer team
+
+- [Emilio Jesús Gallego Arias](https://www.irif.fr/~gallego/) , Inria, Université de Paris, IRIF
+- [Shachar Itzhaky](https://cs.technion.ac.il/~shachari/) , Technion
+
+### Past Contributors
+
+- Benoît Pin, [CRI, MINES ParisTech](https://www.cri.ensmp.fr)
+
+## Acknowledgements
+
+![FEEVER Logo](/frontend/classic/images/feever-logo.png?raw=true "Feever Logo")
+
+jsCoq was made possible thanks to funding by the
+[FEEVER](http://feever.fr) project and support from [MINES
+ParisTech](http://www.mines-paristech.eu)
+
+We want to _strongly thank_ the `js_of_ocaml` developers. Without
+their great and quick support jsCoq wouldn't have been possible.
+
+[CodeMirror](https://codemirror.net/) has played a crucial role in the
+project, we are very happy with it, thanks a lot!
+
+Please consider supporting the development of CodeMirror with a donation.

addons/.gitignore

+.*.swp
+.DS_Store
+_build
+node_modules

addons/Makefile

+PKGS =  teach
+
+CONTEXT = jscoq+32bit
+ifeq ($(DUNE_WORKSPACE:%.64=64), 64)
+CONTEXT = jscoq+64bit
+endif
+ifeq ($(DUNE_WORKSPACE:%.wacoq=wacoq), wacoq)
+CONTEXT = wacoq
+endif
+
+# needed when invoking `opam install`
+OPAMSWITCH = $(CONTEXT)
+export OPAMSWITCH
+
+ifeq ($(DUNE_WORKSPACE),)
+ifeq ($(CONTEXT), wacoq)
+DUNE_WORKSPACE = $(PWD)/dune-workspace.wacoq
+endif
+ifeq ($(CONTEXT), jscoq+64bit)
+DUNE_WORKSPACE = $(PWD)/dune-workspace.64
+endif
+endif
+
+ifneq ($(DUNE_WORKSPACE),)
+export DUNE_WORKSPACE
+endif
+
+OPAM_ENV = eval `opam env`
+
+BUILT_PKGS = ${filter $(PKGS), ${notdir ${wildcard _build/$(CONTEXT)/*}}}
+
+_V = ${firstword $(VERSION) $(VER) $(V)}
+
+COMMIT_FLAGS = -a
+
+ifneq ($(_V),)
+MSG = [deploy] Prepare for $(_V).
+else
+ifeq ($(CONTEXT), wacoq)
+_V = ${shell wacoq --version}
+else
+_V = ${shell jscoq --version}
+endif
+MSG = ${error MSG= is mandatory}
+endif
+
+world:
+	cd teach          && make
+
+privates:
+
+.PHONY: %
+
+env:
+	@echo export DUNE_WORKSPACE=$(DUNE_WORKSPACE)
+
+set-ver:
+	_scripts/set-ver ${addprefix @,$(CONTEXT)} $(_V)
+	if [ -e _build/$(CONTEXT) ] ; then \
+	  $(OPAM_ENV) && dune build _build/$(CONTEXT)/*/package.json ; fi  # update build directory as well
+
+pack:
+	rm -rf _build/$(CONTEXT)/*.tgz
+	_scripts/set-ver ${addprefix @,$(CONTEXT)} $(_V) _build/$(CONTEXT)
+	cd _build/$(CONTEXT) && npm pack ${addprefix ./, $(BUILT_PKGS)}
+
+commit-all:
+	for d in $(PKGS); do ( cd $$d && git commit $(COMMIT_FLAGS) -m "$(MSG)" ); done
+	git commit $(COMMIT_FLAGS) -m "$(MSG)"
+
+push-all:
+	for d in $(PKGS); do ( cd $$d && git push $(PUSH_FLAGS) ); done
+
+commit+push-all:
+	for d in $(PKGS); do ( cd $$d && \
+	   	git commit $(COMMIT_FLAGS) -m "$(MSG)" && \
+	    git push $(PUSH_FLAGS) ); done
+	git commit $(COMMIT_FLAGS) -m "$(MSG)" && git push $(PUSH_FLAGS)
+
+clean-slate:
+	rm -rf */workdir
+	rm -rf _build
+
+ci:
+	$(MAKE) clean-slate
+	$(OPAM_ENV) && $(MAKE)
+	$(MAKE) pack

addons/README.md

+# jsCoq Addons Central
+
+This is a meta-repo with references to jsCoq addon libraries as submodules.
+These submodules contain "recipes" for downloadining, compiling and packaging
+these libraries as jsCoq packages (`.json` and `.coq-pkg` files).

addons/_scripts/set-ver

+#!/usr/bin/env node
+
+/**
+ * Sets the "version" field in `package.json` for all
+ * modules at once.
+ * (useful for release candidates)
+ */
+import * as fs from 'fs';
+import * as path from 'path';
+import * as assert from 'assert';
+
+function setAll(ver, scope='@jscoq', workspaceDir='.') {
+    for (let d of fs.readdirSync(workspaceDir)) {
+        var fn = path.join(workspaceDir, d, 'package.json');
+        if (fs.existsSync(fn)) {
+            var inp = fs.readFileSync(fn, 'utf-8');
+            var out = inp.replace(/"version": .*/, `"version": "${ver}",`)
+                         .replace(/"name": "@[^/]+\// /*"*/, `"name": "${scope}/`);
+            var v = JSON.parse(out); // make sure
+            console.log(v.name, v.version);
+            assert(v.version === ver);
+            fs.chmodSync(fn, "0644");  // allow running in Dune build dir
+            fs.writeFileSync(fn, out);
+        }
+    }
+}
+
+
+function parseArgs() {
+    var opts = {};
+    for (let arg of process.argv.slice(2)) {
+        if (arg.startsWith('@')) opts.scope = arg.replace(/\+.*/, ''); // remove e.g. +32bit
+        else if (arg.match(/^\d/)) opts.ver = arg;
+        else if (!opts.dir) opts.dir = arg;
+        else console.warn(`[set-ver] extraneous argument: '${arg}'`);
+    }
+    return opts;
+}
+
+var opts = parseArgs();
+
+if (opts.ver) {
+    setAll(opts.ver, opts.scope, opts.dir);
+}
+else {
+    console.log("usage: set-ver [scope] <version-number>");
+}

addons/dune

+(dirs :standard \ node_modules)

addons/dune-project

+(lang dune 2.5)
+(using coq 0.2)