addons/teach/workdir/theories/dune

+(coq.theory
+ ; This determines the -R flag
+ (name Teach)
+ (package teach)
+ (synopsis "Teach math using coq")
+ (modules :standard \ IdDec NoCycle))
+
+(include_subdirs no)
\ No newline at end of file

backend/coq-worker.ts

@@ -8,7 +8,7 @@ type Block_type =
   | ['Pp_hvbox', number]
   | ['Pp_hovbox', number];
 
-  export type Pp =
+export type Pp =
     ['Pp_empty']
   | ['Pp_string', string]
   | ['Pp_glue', Pp[]]
@@ -46,7 +46,7 @@ export class CoqWorkerConfig {
      * from which this script is loaded.
      */
     static determineWorkerPath(basePath: string | URL, backend: backend): URL {
-        return new URL({'js': "backend/jsoo/jscoq_worker.bc.cjs",
+        return new URL({'js': "backend/jsoo/jscoq_worker.bc.js",
                         'wa': "dist/wacoq_worker.js"
                        }[backend], basePath);
     }

backend/jsoo/dune

@@ -14,11 +14,6 @@
  ; The old makefile set: -noautolink -no-check-prims
  (libraries num zarith_stubs_js jscoq_core js_of_ocaml-lwt))
 
-(rule
- (target jscoq_worker.bc.cjs)
- (mode promote)
- (action (copy jscoq_worker.bc.js jscoq_worker.bc.cjs)))
-
 (rule
  (targets marshal-arch.js)
  (action

backend/jsoo/js_stub/coq_vm.js

@@ -202,6 +202,9 @@ function coq_set_drawinstr()      { vm_ll('coq_set_drawinstr', arguments); }
 // Provides: coq_tcode_array
 // Requires: vm_ll
 function coq_tcode_array()        { vm_ll('coq_tcode_array', arguments); }
+// Provides: coq_obj_set_tag
+// Requires: vm_ll
+function coq_obj_set_tag()        { vm_ll('coq_obj_set_tag', arguments); }
 
 // Provides: coq_fadd_byte
 function coq_fadd_byte(r1, r2) {

backend/wasm/byterun_stubs.c

@@ -72,3 +72,4 @@ CAMLprim value coq_set_bytecode_field(value v, value i, value code)    STUB
 CAMLprim value coq_offset_tcode(value code, value offset)              STUB
 CAMLprim value coq_int_tcode(value pc, value offset)                   STUB
 CAMLprim value coq_tcode_array(value tcodes)                           STUB
+CAMLprim value coq_obj_set_tag (value arg, value new_tag)              STUB

coqdoclight_sample.v

+(** **** Example coq source file using coqdoc *)
+
+(** [[coqdoc]] is a tool to convert Coq source files into html or LaTeX documents.
+We include in this repository an alternative implementation of coqdoc, [[coqdoclight.py]].
+It does not generate LaTeX files, but it is able to generate interactive html documents using JsCoq.
+This script requires no dependencies other than Python 3, and supports most coqdoc features:
+
+- Titles (using leadings [[ * ]])
+- Lists (using leadings [[ - ]])
+  -- Including nested lists
+- _Emphasis_
+- #<marquee>Custom html tags</marquee>#
+- Hiding code (see below for a more concrete example)
+- Hiding code, allowing the user to reveal it (see (* begin details *) below)
+- Inline coq code, for example: [forall Q : Prop, Q -> Q]
+- Inline preformatted code, using (* [[ *) and (* ]] *)
+- Verbatim using leadings [[<<]] and [[>>]]
+- Horizontal rules to separates content
+
+------------------------------------
+↑ This is a horizontal rule
+*)
+
+(** The only features [[coqdoclight.py]] does not support is pretty-printing certain tokens;
+It is normally registered using the special coqdoc comment:
+<<
+(** printing  *token* %...LATEX...% #...html...# *)
+>>
+But it will be ignored by [[coqdoclight.py]]
+*)
+
+(* begin read-only *)
+
+Definition x := 3.
+
+Goal forall (x:nat), x = x.
+Proof.
+intro x. reflexivity.
+Qed.
+
+(* end read-only *)
+
+(* begin hide *)
+(* This code is not shown in the document, but it is still ran *)
+Definition universe_solution := 42.
+(* end hide *)
+
+(** [universe_solution] is defined in a hidden code block. *)
+
+Check universe_solution.
+
+(** We can also hide code, but still let the user reveal it if needed.
+Notice that when the widget is in hidden state, all the code is ran at once, however if we open it,
+we can go step by step
+*)
+(* begin details *)
+Goal forall (x y z : nat), x = y -> y = z -> x = z.
+Proof.
+intros x y z h1 h2.
+rewrite h1.
+rewrite h2.
+reflexivity.
+Qed.
+(* end details *)
+
+(** 
+We can also add a summary describing the snippet
+*)
+
+(* begin details : Proof that 42 is the solution to the universe *)
+Goal 42 = universe_solution.
+Proof.
+reflexivity.
+Qed.
+(* end details *)

docs/build.md

@@ -6,10 +6,19 @@ on a Unix-like system. The required packages can be obtained using
 
 ## Prerequisites
 
- * OPAM 2 (you can get the installer from https://opam.ocaml.org/doc/Install.html)
+We recommend looking at our [Dockerfile](../etc/Docker/Dockerfile)
+which contains detailed package lists for Debian (and please feel free
+to contribute a OSX CI job).
+
+To build jsCoq you will need a modern Unix system (Linux or macOS), and:
+
+ * OPAM 2.1 (you can get the installer from https://opam.ocaml.org/doc/Install.html)
    - `bubblewrap` is a dependency of OPAM, you can either install it (`apt install bubblewrap`),
      or skip it by running `opam init --disable-sandboxing`
- * m4 (`apt install m4`)
+ * Coq dependencies system dependencies, currently `libgmp`
+   + `apt install libgmp-dev`
+   + or `apt install libgmp-dev:i386` if you are using the 32 bit
+   OCaml version (see below)
  * Node.js 16.x or above + NPM
    - Default versions from `apt` are typically too old; follow the
      [Node.js installation instructions](https://nodejs.org/en/download/package-manager/) to get a newer version.
@@ -45,7 +54,7 @@ cd jscoq
 of OCaml and Coq.
 For Dune builds, configure the switch in your `dune-workspace`.
 
- 3. Fetch Coq 8.16 sources from the repository and configure it for build.
+ 3. Fetch Coq 8.17 sources from the repository and configure it for build.
 ```sh
 make coq
 ```
@@ -57,7 +66,7 @@ make jscoq
 
 This will create a working distribution under `_build/jscoq+32bit/` (or `_build/jscoq+64bit`).
 
-Now serve the files from the distribution directory via HTTP (`make server`), and
+Now serve the files from the distribution directory via HTTP (`make serve`), and
 navigate your browser to `http://localhost/index.html`, or run them locally:
 ```sh
  google-chrome --allow-file-access-from-files --js-flags="--harmony-tailcalls" --js-flags="--stack-size=65536" _build/jscoq+32bit

docs/quick-help.html

@@ -98,7 +98,26 @@
                     Open file (prompts for local file name from list, supports tab completion).
                 </td>
             </tr>
-        </table>
+            <tr>
+              <td></td>
+              <td class="has-kbd nowrap">
+                  <kbd>Ctrl</kbd>+<kbd>F</kbd>
+              </td>
+              <td>
+                  Search in current editor.<br/>Use <kbd>Enter</kbd>/<kbd>Shift</kbd>+<kbd>Enter</kbd>
+                  to jump to next/previous match.
+              </td>
+          </tr>
+          <tr>
+            <td></td>
+            <td class="has-kbd nowrap">
+                <kbd>Alt</kbd>+<kbd>G</kbd>
+            </td>
+            <td>
+                Jump to line or line:column.
+            </td>
+        </tr>
+    </table>
         On Mac, replace <kbd>Ctrl</kbd> with <kbd>⌘</kbd> (command) and <kbd>Alt</kbd> with
         <kbd>⌥</kbd> (option), as is traditional.
 

dune

@@ -27,13 +27,13 @@
    package.json
    package-lock.json)
  (action
-  (run npm install --no-save)))
+  (run npm install --no-progress --no-save)))
 
 (alias
  (name jscoq)
  (deps
   (alias shared)
-  backend/jsoo/jscoq_worker.bc.cjs))
+  backend/jsoo/jscoq_worker.bc.js))
 
 (alias
  (name wacoq)
@@ -48,6 +48,8 @@
   (source_tree examples)
   (source_tree docs)  ; for `quick-help.html`
   dist
+  jscoq.js
+  dist-webpack
   index.html
   coq-pkgs))
 
@@ -69,7 +71,7 @@
  (targets (dir dist-cli))
  (mode (promote (until-clean)))
  (deps
-  backend/jsoo/jscoq_worker.bc.cjs
+  backend/jsoo/jscoq_worker.bc.js
   etc/pkg-metadata/coq-pkgs.json
   (source_tree backend)
   (source_tree frontend)
@@ -96,7 +98,7 @@
 (alias
   (name jscoq_worker)
   (deps
-    backend/jsoo/jscoq_worker.bc.cjs))
+    backend/jsoo/jscoq_worker.bc.js))
 
 (alias
   (name wacoq_worker)

esbuild-cli.mjs

@@ -30,9 +30,6 @@ var nodecli = esbuild
     bundle: true,
     platform: "node",
     format: "cjs",
-    loader: {
-      '.bc.cjs': 'copy'
-    },
     outfile: "dist-cli/cli.cjs",
     ...sourcemap,
     minify,

esbuild.mjs

@@ -57,7 +57,7 @@ var frontend = esbuild
     format: "esm",
     loader: {
       '.png': 'binary',
-      '.svg': 'binary'
+      '.svg': 'dataurl'
     },
     outdir: "dist/frontend",
     minify,

etc/docker/Dockerfile

-ARG BRANCH=v8.16
+ARG BRANCH=v8.17
 
 ARG WORDSIZE=32
 ARG SWITCH=jscoq+${WORDSIZE}bit
@@ -90,7 +90,7 @@ RUN eval $(opam env) && make jscoq
 RUN eval $(opam env) && make wacoq
 
 # - dist tarballs
-RUN eval $(opam env) && make dist \
+RUN eval $(opam env) && make dist && make dist-npm \
         && mkdir -p dist && mv _build/dist/*.tgz dist
 
 # --------------
@@ -117,7 +117,7 @@ RUN git clone --recursive -b ${ADDONS_BRANCH} ${ADDONS_REPO} jscoq-addons
 
 WORKDIR jscoq-addons
 RUN make set-ver VER=`jscoq --version`
-RUN eval $(opam env) && make CONTEXT=${SWITCH}
+RUN eval $(opam env) && git pull && git submodule update && make CONTEXT=${SWITCH}
 
 # Private repos: re-enable SSH
 COPY Dockerfile _ssh* /root/_ssh/

etc/docker/Makefile

@@ -2,7 +2,7 @@
 
 WHO = jscoq
 
-BRANCH = v8.16
+BRANCH = v8.17
 
 export JSCOQ_REPO = https://github.com/$(WHO)/jscoq.git
 export JSCOQ_BRANCH = $(BRANCH)
@@ -27,7 +27,7 @@ BUILD_ARGS = BRANCH SUB_BRANCH NJOBS WORDSIZE \
              JSCOQ_REPO JSCOQ_BRANCH WACOQ_BIN_REPO WACOQ_BIN_BRANCH
 
 ARGS = $(addprefix --platform , $(firstword ${ARCH})) \
-       $(addprefix --build-arg , $(BUILD_ARGS))
+       $(addprefix --build-arg , $(BUILD_ARGS) BUILDKIT_INLINE_CACHE=1)
 
 -include _config.mk
 
@@ -64,7 +64,7 @@ wa-build-core:
 wa-build-addons: wa-build-core
 	docker build . --target wacoq-addons     $(ARGS)  -t wacoq:addons
 
-dist: js-dist wa-dist
+dist: js-dist
 
 clean-dist:
 	rm -rf ./dist
@@ -72,8 +72,8 @@ clean-dist:
 js-dist: clean-dist
 	docker run --name jscoq-get-dist jscoq:addons \
 		sh -c 'mkdir -p dist && cp _build/jscoq+*/*.tgz dist'
-	docker cp jscoq-get-dist:/root/jscoq/dist .
-	docker cp jscoq-get-dist:/root/jscoq-addons/dist .
+	docker cp --quiet jscoq-get-dist:/root/jscoq/dist .
+	docker cp --quiet jscoq-get-dist:/root/jscoq-addons/dist .
 	docker rm jscoq-get-dist
 
 wa-dist: clean-dist
@@ -86,7 +86,7 @@ wa-dist: clean-dist
 # For getting just the jsCoq package, w/o addons
 js-dist-core: clean-dist
 	docker run --name jscoq-get-dist jscoq
-	docker cp jscoq-get-dist:/root/jscoq/dist .
+	docker cp --quiet jscoq-get-dist:/root/jscoq/dist .
 	docker rm jscoq-get-dist
 
 # For updating the dist with the result of incremental build
@@ -128,15 +128,19 @@ wa-clean-slate:
 	docker system prune $(CLEAN_FLAGS)
 
 js-upload:
-	docker tag jscoq:sdk jscoq/jscoq:sdk-${M}
-	docker push jscoq/jscoq:sdk-${M}
+	docker tag jscoq:sdk jscoq/jscoq:$(BRANCH)-sdk-${M}
+	docker push jscoq/jscoq:$(BRANCH)-sdk-${M}
+
+from-local:
+	rsync -a ../../.git/ _work-git
 
 # Update the multi-arch manifest
 MANIFEST_ARCHS = x86_64 arm64
+MANIFEST_TAG = $(BRANCH)-sdk
 js-upload-manifest:
-	docker manifest create --amend jscoq/jscoq:sdk \
-	       $(addprefix jscoq/jscoq:sdk-, ${MANIFEST_ARCHS})
-	docker manifest push jscoq/jscoq:sdk
+	docker manifest create --amend jscoq/jscoq:$(MANIFEST_TAG) \
+	       $(addprefix jscoq/jscoq:$(BRANCH)-sdk-, ${MANIFEST_ARCHS})
+	docker manifest push jscoq/jscoq:$(MANIFEST_TAG)
 
 serve:
 	docker run --publish 8080:8080 --rm -it jscoq \
@@ -146,4 +150,4 @@ dist-serve:
 	npx http-server -p 8080 dist
 
 ci:
-	make clean && make js-build wa-build && make dist
+	make clean && make js-build && make dist

etc/patches/timeout.patch

@@ -64,7 +64,7 @@ index 43ee8f7..ac82c4e 100644
 + (foreign_stubs
 +  (language c)
 +  (names jscoq_extern)
-+  (flags (:include %{project_root}/config/dune.c_flags)))
++  (flags :standard (:include %{project_root}/config/dune.c_flags)))
   (libraries coq-core.boot coq-core.clib coq-core.config))
 diff --git a/lib/jscoq_extern.c b/lib/jscoq_extern.c
 new file mode 100644

etc/wacoq-deps/package.json

+{
+  "name": "wacoq-deps",
+  "description": "meta-package for waCoq binary dependencies",
+  "version": "0.1.1",
+  "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.13.0-0",
+    "ocaml-wasm": "^4.12.0-0",
+    "wasi-kernel": "^0.1.6"
+  },
+  "repository": {
+    "type": "git",
+    "url": "git+https://github.com/jscoq/jscoq.git"
+  },
+  "files": []
+}

examples/Makefile

@@ -7,7 +7,7 @@ WORD_SIZE ?= 32
 
 CONTEXT = jscoq+$(WORD_SIZE)bit
 COQC = ../_build/install/$(CONTEXT)/bin/coqc
-JSCOQ_CLI = ../_build/$(CONTEXT)/dist/cli/cli.cjs
+JSCOQ_CLI = ../_build/$(CONTEXT)/dist-cli/cli.cjs
 ###
 
 all: examples.coq-pkg examples.symb.json sqrt_2.html nahas_tutorial.html

examples/playful.html

@@ -26,7 +26,7 @@
     (async () => {
       await JsCoq.load();
 
-      coq = new CoqWorker(new URL('../coq-js/jscoq_worker.bc.cjs', window.location));
+      coq = new CoqWorker(new URL('../coq-js/jscoq_worker.bc.js', window.location));
       pm = new PackageManager(document.createElement('div'),  /* need a div, sry */
                               {'../coq-pkgs/': ['coq']}, {}, coq);
 

examples/scratchpad.html

@@ -6,6 +6,7 @@
     <link rel="icon" href="../frontend/classic/images/favicon.png">
 
     <title>jsCoq – The Coq Theorem Prover Online IDE</title>
+    <link rel="stylesheet" type="text/css" href="../dist/frontend/index.css">
     <style>
       /* Allow some extra scroll space at the bottom & to the right */
       .CodeMirror-lines {
@@ -24,13 +25,15 @@
     import { JsCoq } from "../jscoq.js";
 
     var sp = new URLSearchParams(location.search),
-        panel_theme = sp.has('dark') ? 'dark' : sp.get('theme') || 'light',
-        editor_theme = sp.get('editor_theme') || (panel_theme == 'dark' ? 'blackboard' : 'default');
+        ifHas = x => sp.has(x) ? x : undefined,
+        panel_theme = ifHas('dark') ?? sp.get('theme') ?? 'light',
+        editor_theme = sp.get('editor_theme') ?? (panel_theme == 'dark' ? 'blackboard' : 'default');
 
 
     var jscoq_opts = {
-        backend:   sp.get('backend'),
-        subproc:   sp.has('app'),
+        backend: sp.get('backend') ?? ifHas('wa'),
+        subproc: sp.has('app'),
+        node_modules_path: '../node_modules/',
         file_dialog: true,
         implicit_libs: true,
         editor: { mode: { 'company-coq': true }, theme: editor_theme },
@@ -42,15 +45,15 @@
         set_filename = fn => document.getElementById('ide-wrapper')
                                      .setAttribute('data-filename', fn);
 
-
     if (sp.has('code')) set_filename('');
     else if (last_filename) set_filename(last_filename);
 
     JsCoq.start(jscoq_opts).then(res => {
       coq = res;
+      window.coq = coq;
       if (sp.has('project'))     coq.openProject(sp.get('project'));
       if (sp.has('share'))       coq.openCollab({hastebin: sp.get('share')});
-      if (sp.has('p2p'))         coq.openCollab({p2p: sp.get('p2p')});
+      if (sp.has('gist'))        coq.openCollab({gist: sp.get('gist')});
       if (sp.has('code'))        coq.provider.load(sp.get('code'), sp.get('fn') || 'playground');
     });