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>
+""")

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

dune

@@ -49,6 +49,7 @@
   (source_tree docs)  ; for `quick-help.html`
   dist
   jscoq.js
+  dist-webpack
   index.html
   coq-pkgs))