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.py

+"""
+Coqdoclight
+A script to turn coq files into worksheets
+"""
+import sys, html, pathlib
+
+
+def err(x):
+    print("####### ERROR ########")
+    print(x, file=sys.stderr)
+    print("######################")
+    exit(1)
+
+def dbg(x):
+    print(x, file=sys.stderr)
+
+def out(x):
+    print(x, end="")
+
+def out_rw_snippet():
+    out('<textarea class="snippet">')
+
+def out_ro_snippet():
+    out('<textarea class="snippet read-only">')
+
+out_snippet = out_rw_snippet
+
+def trimout(x):
+    out(x.strip())
+
+def html_out(x):
+    out(html.escape(x))
+    out("\n")
+
+"""
+Token interface
+"""
+class Token:
+    """
+    Eat a character, return None if there is no match yet,
+    or the length of the match
+    """
+    def eat(self, c):
+        pass
+    """
+    Reset the internal state of the tokenizer
+    """
+    def reset(self):
+        pass
+    
+class Char(Token):
+    def __init__(self,c):
+        self.c = c
+        
+    def eat(self, x):
+        if x == self.c:
+            return 1
+
+class Stars(Token):
+    def __init__(self):
+        self.reset()
+    
+    def reset(self):
+        self.newline = True
+        self.stars = 0
+    
+    def eat(self,c):
+        if c == '\n':
+            self.newline = True
+            self.stars = 0
+        elif self.newline:
+            if c == '*':
+                self.stars += 1
+            elif c == ' ' and self.stars > 0:
+                ret=self.stars+1
+                self.stars=0
+                self.newline=False
+                return ret
+            elif not c.isspace():
+                self.newline = False
+                self.stars = 0
+
+class Leading(Token):
+    def __init__(self,lit):
+        self.lit = lit
+        self.idx = 0
+        self.newline = True
+    
+    def reset(self):
+        self.newline = True
+        self.idx = 0
+
+    def eat(self,c):
+        if c == '\n':
+            self.newline = True
+        if self.newline:
+            if c == self.lit[self.idx]:
+                self.idx += 1
+                if self.idx == len(self.lit):
+                    self.idx = 0
+                    self.newline = c == '\n'
+                    return len(self.lit)
+            else:
+                self.newline = c.isspace()
+                self.idx = 0
+        else:
+            self.newline = c.isspace()
+            self.idx = 0
+        
+class Lit(Token):
+    def __init__(self,lit):
+        self.idx = 0
+        self.lit = lit
+        self.len = len(lit)
+
+    def reset(self):
+        self.idx = 0
+
+    def eat(self, x):
+        if self.lit[self.idx] == x:
+            self.idx += 1
+            if self.idx == self.len:
+                self.reset()
+                return self.len
+        else:
+            self.idx = 0
+
+class Scanner:
+    def __init__(self,src):
+        self.rules = []
+        self.i = 0
+        self.process = err
+        self.src = src
+        self.stack = []
+        self.cleanup = []
+    
+    def prev(self):
+        if self.i > 0:
+            return self.src[self.i-1]
+
+    def push(self,rules,process):
+        self.stack.append((self.rules, self.process, self.cleanup))
+        self.rules = rules
+        self.process = process
+        self.cleanup = []
+
+    def pop(self):
+        for c in list(self.cleanup):
+            c.action(sc,self.i,self.i)
+        (self.rules, self.process, self.cleanup) = self.stack[-1]
+        self.stack.pop()
+        
+    def consecutive(self):
+        c = self.src[self.i]
+        i = self.i+1
+        for i in range(i,len(self.src)):
+            if self.src[i] != c:
+                i-=1
+                break
+        return (i+1)-self.i
+
+    def eat(self,c):
+        for ru in self.rules:
+            r = ru.token.eat(c)
+            if r:
+                self.reset()
+                return (ru, r)
+    
+    def reset(self):
+        for ru in self.rules:
+            ru.token.reset()
+
+    def find_next(self):
+        comments=0
+        first_comment=0
+        while self.i < len(self.src):
+            c = self.src[self.i]
+            r = self.eat(c)
+
+            if c == '*' and self.prev() == '(':
+                if comments == 0:
+                    first_comment = self.i-1
+                comments += 1
+            
+            if comments > 0 and c == ')' and self.prev() == '*':
+                comments -= 1
+                self.reset()
+
+            if r:
+                (ru,l) = r
+                tokstart=self.i-l+1
+                tokend=self.i+1
+                if comments == 0 or tokstart <= first_comment: # if the token includes the comment, we accept it
+                    return (ru,tokstart,tokend)
+            
+            self.i += 1
+
+    def scan(self):
+        cstart = 0
+        cend = 0
+        alive = True
+        while alive:
+            r = self.find_next()
+            if not r:
+                alive=False
+                cend=len(self.src)
+            else:
+                # Set the cursor end to the start of the token
+                (_,cend,_) = r 
+            
+            buf=self.src[cstart:cend]
+            if buf and not buf.isspace():
+                #dbg(f"PR:{self.process.__name__}:@@@{buf}@@@")
+                self.process(buf)
+                
+            
+            if r:
+                (ru,s,e) = r
+                #dbg(f"RU:{type(ru).__name__}:{type(ru.token).__name__}:@@@{self.src[s:e]}@@@")
+                ru.action(self,s,e)
+                self.i+=1
+                cstart=self.i
+                
+
+class Rule:
+    # sc = scanner
+    # s = beginning index of the match
+    # e = end index of the match
+    def action(self,sc,s,e):
+        pass
+
+# Coqdoc
+TOK_BEGIN_CODE = Char('[')
+TOK_END_CODE_COQ = Char(']')
+TOK_END_CODE = Lit(']]')
+
+TOK_BEGIN_VERBATIM = Leading("<<\n")
+TOK_END_VERBATIM = Leading(">>\n")
+
+TOK_BEGIN_COM = Lit("(*")
+TOK_END_COM = Lit("*)")
+
+TOK_DASH = Leading("-")
+TOK_STARS = Stars()
+TOK_ENDLINE = Char('\n')
+TOK_BLANKLINE = Lit("\n\n")
+TOK_UNDERSCORE = Char('_')
+TOK_SHARP = Char('#')
+
+class Code(Rule):
+    def __init__(self):
+        self.set_start()
+
+    def set_start(self):
+        self.token = TOK_BEGIN_CODE
+        self.action = self.start_action
+
+    def start_action(self,sc,s,e):
+        self.action = self.end_action
+        sc.push([self], trimout)
+        if sc.consecutive() < 2: # coq code
+            out('<code class="cm-s-default coq-highlight">')
+            self.token = TOK_END_CODE_COQ
+        else: # non-coq code
+            out('<code>')
+            self.token = TOK_END_CODE
+            sc.i += 1 # skip second [
+            
+
+    def end_action(self,sc,s,e):
+        out('</code>')
+        sc.pop()
+        self.set_start()
+
+class Html(Rule):
+    def __init__(self):
+        self.token = TOK_SHARP
+        self.set_start()
+
+    def set_start(self):
+        self.action = self.start_action
+
+    def start_action(self,sc,s,e):
+        self.action = self.end_action
+        sc.push([self], trimout)
+        
+    def end_action(self,sc,s,e):
+        sc.pop()
+        self.set_start()
+        
+class Comment(Rule):
+    def __init__(self):
+        self.set_start()
+
+    def set_start(self):
+        self.token = TOK_BEGIN_COM
+        self.action = self.start_action
+
+    def start_action(self,sc,s,e):
+        self.action = self.end_action
+        sc.push([self], trimout)
+        out('<code class="cm-s-default coq-highlight">(*')
+        self.token = TOK_END_COM
+        
+    def end_action(self,sc,s,e):
+        sc.pop()
+        self.set_start()
+        out('*)</code>')
+        
+class Title(Rule):
+    def __init__(self):
+        self.set_start()
+
+    def set_start(self):
+        self.token = TOK_STARS
+        self.action = self.start_action
+
+    def start_action(self,sc,s,e):
+        self.action = self.end_action
+        self.hlevel = e-s-1 # the blank space
+        out(f'<h{self.hlevel}>')
+        self.token = TOK_ENDLINE
+        sc.cleanup.append(self)
+
+    def end_action(self,sc,s,e):
+        self.set_start()
+        sc.cleanup.remove(self)
+        out(f'</h{self.hlevel}>\n')
+
+class ListEnd(Rule):
+    def __init__(self,start_rule):
+        self.start_rule = start_rule
+        self.token = TOK_BLANKLINE
+
+    def action(self,sc,s,e):
+        sc.cleanup.remove(self)
+        sc.rules.remove(self)
+        self.start_rule.action = self.start_rule.start_action
+        out("</li>")
+        for _ in range(0,self.start_rule.deepness):
+            out("</ul>")
+        out("\n")
+        
+class ListStart(Rule):
+    def __init__(self):
+        self.token = TOK_DASH
+        self.action = self.start_action
+    
+    def start_action(self,sc,s,e):
+        cons=sc.consecutive()
+        if cons >= 4: # this is a horizontal rule
+            out("<hr />\n")
+            sc.i+=cons-1
+            return
+        self.action = self.in_action
+        self.deepness = 0
+        listend = ListEnd(self)
+        sc.rules.append(listend)
+        sc.cleanup.append(listend)
+        self.in_action(sc,s,e)
+    
+    def in_action(self,sc,s,e):
+        level=sc.consecutive()
+        sc.i += level-1
+        if level > self.deepness:
+            for _ in range(0,level-self.deepness):
+                out("<ul>")
+        elif level < self.deepness:
+            for _ in range(0,self.deepness-level):
+                out("</ul>")
+        elif self.deepness != 0:
+            out("</li>")
+        
+        self.deepness = level
+        out("<li>\n")
+        
+class Italic(Rule):
+    def __init__(self):
+        self.token = TOK_UNDERSCORE
+        self.set_start()
+
+    def set_start(self):
+        self.action = self.start_action
+    
+    def start_action(self,sc,s,e):
+        out("<i>")
+        self.action = self.end_action
+    
+    def end_action(self,sc,s,e):
+        out("</i>")
+        self.set_start()
+
+class Verbatim(Rule):
+    def __init__(self):
+        self.set_start()
+
+    def set_start(self):
+        self.token = TOK_BEGIN_VERBATIM
+        self.action = self.start_action
+
+    def start_action(self,sc,s,e):
+        self.action = self.end_action
+        self.token = TOK_END_VERBATIM
+        sc.push([self], trimout)
+        out('<pre>')
+
+    def end_action(self,sc,s,e):
+        sc.pop()
+        self.set_start()
+        out('</pre>\n')
+
+class Ignore(Rule):
+    def __init__(self,token):
+        self.token = token
+        self.set_start()
+
+    def set_start(self):
+        self.action = self.start_action
+
+    def start_action(self,sc,s,e):
+        self.action = self.end_action
+        sc.push([self], len)
+
+    def end_action(self,sc,s,e):
+        sc.pop()
+        self.set_start()
+
+class EndCoqdoc(Rule):
+    def __init__(self):
+        self.token = TOK_END_COM
+    def action(self,sc,s,e):
+        sc.pop()
+        out("</p>\n")
+
+# Top tokens
+TOK_BEGIN_HIDE = Lit("(* begin hide *)")
+TOK_END_HIDE = Lit("(* end hide *)")
+
+TOK_BEGIN_SHOW = Lit("(* begin show *)")
+TOK_END_SHOW = Lit("(* end show *)")
+
+TOK_BEGIN_DETAILS=Lit("(* begin details ")
+TOK_END_DETAILS=Lit("(* end details *)")
+
+TOK_BEGIN_READ_ONLY=Lit("(* begin read-only *)")
+TOK_END_READ_ONLY=Lit("(* end read-only *)")
+
+TOK_BEGIN_DOC = Lit("(**")
+
+class Show(Rule):
+    def __init__(self):
+        self.set_start()
+    
+    def set_start(self):
+        self.token = TOK_BEGIN_SHOW
+        self.action = self.start_action
+    
+    def start_action(self,sc,s,e):
+        out('</textarea>')
+        self.token = TOK_END_SHOW
+        self.action = self.end_action
+        push_top(sc)
+        sc.rules.append(self)
+    
+    def end_action(self,sc,s,e):
+        out('<textarea style="display:none;" class="snippet">\n')
+        self.set_start()
+        sc.pop()
+
+class Hide(Rule):
+    def __init__(self):
+        self.set_start()
+
+    def set_start(self):
+        self.token = TOK_BEGIN_HIDE
+        self.action = self.start_action
+
+    def start_action(self,sc,s,e):
+        self.action = self.end_action
+        self.token = TOK_END_HIDE
+        out('<textarea style="display:none;" class="snippet">\n')
+        sc.push([self, Show()], trimout)
+
+    def end_action(self,sc,s,e):
+        out('</textarea>')
+        sc.pop()
+        self.set_start()
+
+class Details(Rule):
+    def __init__(self):
+        self.set_start()
+
+    def set_start(self):
+        self.token = TOK_BEGIN_DETAILS
+        self.action = self.start_action
+
+    def start_action(self,sc,s,e):
+        self.action = self.com_action
+        self.token = TOK_END_COM
+        self.details_name = None
+        def set_details_name(x):
+            self.details_name = x[1:]
+        sc.push([self], set_details_name)
+
+    def com_action(self,sc,s,e):
+        self.action = self.end_action
+        self.token = TOK_END_DETAILS
+        sc.process = trimout
+        out('<details>\n')
+        if self.details_name:
+            out(f'<summary>{self.details_name}</summary>\n')
+        out_snippet()
+
+    def end_action(self,sc,s,e):
+        out('</textarea>\n</details>')
+        sc.pop()
+        self.set_start()
+
+class ReadOnly(Rule):
+    def __init__(self):
+        self.set_start()
+
+    def set_start(self):
+        self.token = TOK_BEGIN_READ_ONLY
+        self.action = self.start_action
+
+    def start_action(self,sc,s,e):
+        global out_snippet
+        self.action = self.end_action
+        self.token = TOK_END_READ_ONLY
+        out_snippet = out_ro_snippet
+
+    def end_action(self,sc,s,e):
+        global out_snippet
+        self.set_start()
+        out_snippet = out_rw_snippet
+
+    
+class Coqdoc(Rule):
+    def __init__(self):
+        self.token = TOK_BEGIN_DOC
+    
+    def action(self,sc,s,e):
+        out("<p>\n")
+        rules=[
+            Code (), 
+            Verbatim (), 
+            EndCoqdoc (), 
+            Title (), 
+            Italic (), 
+            Comment (), 
+            ListStart (), 
+            Html (),
+            Ignore (Char('$')), # Ignore latex
+            Ignore (Char('%')), # idem
+        ]
+        sc.push(rules, html_out)
+
+def push_top(sc):
+    def snippet_out(x):
+        out_snippet()
+        out(x.strip())
+        out('</textarea>\n')
+    sc.push([Hide (), Coqdoc (), Details (), ReadOnly ()], snippet_out)
+    
+
+if len(sys.argv) < 2:
+    err("moulinette expect one argument: the path of the coq file")
+
+with open(sys.argv[1], 'r') as file:
+    global sc
+    sc = Scanner(file.read())
+
+filename=pathlib.Path(sys.argv[1]).name
+
+out("""
+<!DOCTYPE html>
+<html xmlns="http://www.w3.org/1999/xhtml">
+  <head>
+    <title>jsCoq – Use Coq in Your Browser</title>
+    <meta http-equiv="content-type" content="text/html;charset=utf-8" />
+    <meta name="description" content="An Online IDE for the Coq Theorem Prover" />
+    <!-- Move to copy with the bundle -->
+    <link rel="icon" href="frontend/classic/images/favicon.png">
+    <style>body { visibility: hidden; } /* FOUC avoidance */</style>
+    <link rel="stylesheet" type="text/css" href="./dist/frontend/index.css">
+  </head>
+
+<body class="jscoq-main">
+  <div id="ide-wrapper" class="toggled">
+  <div id="code-wrapper">
+  <div id="document-wrapper">
+""")
+
+out(f'<div id="document" data-filename="{filename}">')
+push_top(sc)
+sc.scan()
+# TODO: Options for addons
+out("""
+</div> <!-- /#document -->
+  </div> <!-- /#document-wrapper -->
+  </div> <!-- /#code-wrapper -->
+  </div> <!-- /#ide-wrapper -->
+
+  <script type="module">
+    import { JsCoq } from './jscoq.js';
+
+    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') ?? ifHas('wa'),
+        implicit_libs: false,
+        focus: false,
+        editor: { mode: { 'company-coq': true } },
+        all_pkgs: {'./coq-pkgs': ['coq'], './addons/teach/coq-pkgs': ['teach']}
+    };
+
+    JsCoq.start(jscoq_ids, jscoq_opts).then(res => {
+        /* Global reference */
+        window.coq = res;
+    });
+  </script>
+</body>
+</html>
+""")

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');
     });