.gitlab-ci.yml

+stages:
+  - build
+
+jscoq:
+  stage: build
+  image: i386/debian
+
+  script:
+    - 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 = frontend/classic/external/CodeMirror-TeX-input
-	url = https://github.com/ejgallego/CodeMirror-TeX-input.git
-[submodule "vendor/coq-serapi"]
-	path = vendor/coq-serapi
-	url = https://github.com/ejgallego/coq-serapi.git

Dockerfile

-FROM i386/debian as jscoq-dev
+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

Makefile

@@ -93,7 +93,6 @@ addons: force
 	cd addons && make
 
 jscoq: force
-	cd addons && make 
 	$(DUNE) build @jscoq $(DUNE_FLAGS)
 
 wacoq: force

README.md

@@ -17,7 +17,7 @@ sudo docker container create -p 8000:8000 --mount type=bind,source=.,target=/roo
 
 - 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`.
 
-- After the container has been started, run `sudo docker exec -it jscoq-dev bash -c "cd /root/jscoq && ./etc/toolchain-setup.sh"` to install jscoq SDK inside the container.
+- 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
 
 ### Compiling jscoq
 
@@ -43,4 +43,4 @@ Then, you will be able to use `From Teach Require Import YourFile` in jscoq.
 ### Creating your own worksheets
 
 You can modify `index.html` to create your own worksheet. 
-(TODO: expand on this).
\ No newline at end of file
+(TODO: expand on this).

addons/Makefile

-PKGS =  teach 
+PKGS =  teach
 
 CONTEXT = jscoq+32bit
 ifeq ($(DUNE_WORKSPACE:%.64=64), 64)

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 *)

etc/toolchain-setup.sh

@@ -69,5 +69,3 @@ if [ $WRITE_CONFIG == yes ] ; then echo "WORD_SIZE=$WORD_SIZE" > config.inc ; fi
 create_switch
 install_deps
 post_install
-cd /root/jscoq
-npm link
\ No newline at end of file

flake.lock

+{
+  "nodes": {
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1726560853,
+        "narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1728492678,
+        "narHash": "sha256-9UTxR8eukdg+XZeHgxW5hQA9fIKHsKCdOIUycTryeVw=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "5633bcff0c6162b9e4b5f1264264611e950c8ec7",
+        "type": "github"
+      },
+      "original": {
+        "id": "nixpkgs",
+        "ref": "nixos-unstable",
+        "type": "indirect"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}

flake.nix

+{
+  inputs = {
+    nixpkgs.url = "nixpkgs/nixos-unstable";
+    flake-utils.url = "github:numtide/flake-utils";
+  };
+  
+  outputs = { self, nixpkgs, flake-utils, ... }: flake-utils.lib.eachDefaultSystem (system:
+    let
+      pkgs = nixpkgs.legacyPackages.${system};
+    in {
+      devShell = pkgs.mkShell {
+        packages = with pkgs; [
+          (vscode-with-extensions.override {
+            vscodeExtensions = with vscode-extensions.ms-python; [
+              python
+              debugpy
+              vscode-pylance
+            ];
+          })
+        ];
+      };
+    });
+}
+

frontend/classic/css/coq-light.css

@@ -84,6 +84,10 @@ body.jscoq-main #document {
   background: #f1f1f1;
 }
 
+.read-only {
+  outline:thick solid #FF7F7F;
+}
+
 .cm-s-default .CodeMirror-dialog {
   border-bottom: 1px solid #bbb;
   box-shadow: 0px 1px 5px 0px #00000059;

CodeMirror-TeX-input @ 698ba2e3

-Subproject commit 698ba2e3e6364a92dc966a60a2242633fb0e2474

frontend/classic/external/CodeMirror-TeX-input/.gitignore

+*~

frontend/classic/external/CodeMirror-TeX-input/LICENSE

+TeX-style completion, written by Emilio J. Gallego Arias.
+
+Copyright (C) 2016 by Marijn Haverbeke <marijnh@gmail.com> and others
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+THE SOFTWARE.
+

frontend/classic/external/CodeMirror-TeX-input/README.md

+# TeX-style input for CodeMirror
+
+This addon provides a completion hint for CodeMirror which allows to
+use the backslash key `\` to compose Unicode characters in TeX style.
+
+It was inspired by Emacs' `qual-completion`, but it differs a bit on feeling.
+
+See a demo here:
+https://ejgallego.github.io/CodeMirror-TeX-input/demo/tex-input.html
+
+See also a demo of the Emacs mode here here: https://youtu.be/3hwUnhdKWiI?t=5m55s
+
+_Warning_: The project is in α-state :)
+
+## How to install
+
+Just include the `addon/hint/tex-input-hint.js` file.
+
+## TODO
+
+The mode pretty much works, we need:
+
+- Add a much larger Unicode table.
+- Add support for options, such that users can configure completion
+  on space, add new symbols to the table, etc...

frontend/classic/external/CodeMirror-TeX-input/addon/hint/tex-input-hint.js

+// CodeMirror, copyright (c) by Marijn Haverbeke and others
+// Distributed under an MIT license: http://codemirror.net/LICENSE
+
+// TeX-style completion, written by Emilio J. Gallego Arias.
+
+// No merge into CodeMirror is planned for now.
+
+/*
+
+  List of open issues:
+
+  - Make the unicode table a parameter.
+
+  - Review if the way we capture the '\' keypress comforms to CM
+    coding standards.
+
+*/
+
+(function(mod) {
+  if (typeof exports == "object" && typeof module == "object") // CommonJS
+    mod(require("codemirror"));
+  else if (typeof define == "function" && define.amd) // AMD
+    define(["codemirror"], mod);
+  else // Plain browser env
+    mod(CodeMirror);
+})(function(CodeMirror) {
+
+  var Pos = CodeMirror.Pos;
+
+  // XXX: Generate automatically...
+  var unicodePreTable = [
+    { text: "\\",       symbol: "\\"},
+    { text: "\\_1",     symbol: "₁" },
+    { text: "\\_2",     symbol: "₂" },
+    { text: "\\alpha",  symbol: "α" },
+    { text: "\\beta",   symbol: "β" },
+    { text: "\\circ",   symbol: "∘" },
+    { text: "\\delta",  symbol: "δ" },
+    { text: "\\epsilon", symbol: "ε" },
+    { text: "\\exists", symbol: "∃" },
+    { text: "\\forall", symbol: "∀" },
+    { text: "\\gamma",  symbol: "γ" },
+    { text: "\\lambda", symbol: "λ" },
+    { text: "\\land",   symbol: "∧" },
+    { text: "\\llbracket", symbol: "〚"},
+    { text: "\\lnot",   symbol: "¬" },
+    { text: "\\lor",    symbol: "∨" },
+    { text: "\\mid",    symbol: "∣" },
+    { text: "\\models", symbol: "⊧" },
+    { text: "\\oplus",  symbol: "⊕" },
+    { text: "\\otimes", symbol: "⊗" },
+    { text: "\\omega",  symbol: "ω" },
+    { text: "\\pi",     symbol: "π" },
+    { text: "\\phi",    symbol: "φ" },
+    { text: "\\psi",    symbol: "ψ" },
+    { text: "\\rrbracket", symbol: "〛"},
+    { text: "\\sigma",  symbol: "σ" },
+    { text: "\\times",  symbol: "×" },
+    { text: "\\theta",  symbol: "θ" },
+    { text: "\\to",     symbol: "→" },
+    { text: "\\vdash",  symbol: "⊢" },
+    { text: "\\Delta",  symbol: "Δ" },
+    { text: "\\Gamma",  symbol: "Γ" },
+    { text: "\\Lambda", symbol: "Λ" },
+    { text: "\\Omega",  symbol: "Ω" },
+    { text: "\\Pi",     symbol: "Π" },
+    { text: "\\Phi",    symbol: "Φ" },
+    { text: "\\Psi",    symbol: "Ψ" },
+    { text: "\\Sigma",  symbol: "Σ" },
+    { text: "\\Theta",  symbol: "Θ" }
+  ];
+
+  /* How our TeX-style completion works:
+
+     We always complete on a press of "\", then we scan back to read
+     the token. More fancy things could happen but this works
+     reasonably well for now.
+   */
+
+  function TeX_input_hint(editor, _options) {
+
+    var cur = editor.getCursor();
+
+    // IMPORTANT: We want to be mode independent so we match backwards
+    // from the cursor to the first \.
+
+    var curPos   = Pos(cur.line, cur.ch);
+    var matchEnd = Pos(cur.line, cur.ch);
+
+    var match = "";
+
+    while ( 0 <= curPos.ch ) {
+      curPos.ch--;
+      match = editor.getRange(curPos, matchEnd);
+      if (match[0] == '\\') break;
+    }
+
+    var matchStart = curPos;
+
+    console.log('cur/tok', cur, match);
+
+    // Replace the current token !
+    var insertFun = function(cm, _self, data) {
+      cm.replaceRange(data.symbol, matchStart, matchEnd);
+    };
+
+    var rList = [];
+
+    // Build of our table
+    unicodePreTable.map( function(obj) {
+      console.log('Considering: ', obj, ' for ', match);
+
+      if ( obj.text.startsWith(match) ) {
+        // XXX: This can be improved for sure.
+        obj.displayText = obj.symbol + ' ' + obj.text;
+        obj.hint = insertFun;
+        rList.push(obj);
+      }
+    });
+
+    return { list:  rList,
+             from:  matchStart,
+             to:    matchEnd,
+             eager: true
+           }
+  };
+
+  // We bind '\\'
+  function initTexInput (CodeMirror) {
+
+    // We bind slash to the latex autocomplete symbol.
+    // We also bind Space to insert current hint.
+    CodeMirror.defineInitHook(function (cm) {
+
+      // XXX: Do we want to hook on "_" and "^", etc... ?
+      cm.addKeyMap({"\\": function(cm)
+                    {
+                      cm.replaceSelection("\\");
+                      cm.execCommand("autocomplete");
+                    }});
+
+      // We need to update the local keymap to the hints.
+      var extraHintKeyMap = { Space: function(cm) {
+
+        var cA = cm.state.completionActive;
+
+        if (cA && cA.data.eager) {
+          cA.widget.pick();
+        }
+        return CodeMirror.Pass;  // fall through to default handler
+      } };
+
+      var cmplOpt = cm.getOption("hintOptions");
+
+      cmplOpt = cmplOpt || {};
+      cmplOpt['extraKeys'] = extraHintKeyMap;
+      cm.setOption("hintOptions", cmplOpt);
+
+    });
+
+    CodeMirror.registerGlobalHelper("hint", "tex-input",
+                                    (function () { return true; }), TeX_input_hint);
+  }
+
+  initTexInput(CodeMirror);
+});
+
+// Local Variables:
+// js-indent-level: 2
+// End:
+

frontend/classic/external/CodeMirror-TeX-input/demo/tex-input.html

+<!doctype html>
+
+<title>CodeMirror: Markdown mode</title>
+<meta charset="utf-8"/>
+<link rel=stylesheet href="../doc/docs.css">
+
+<link rel="stylesheet" href="../lib/codemirror.css">
+<link rel="stylesheet" href="../addon/hint/show-hint.css">
+
+<script src="../lib/codemirror.js"></script>
+<script src="../mode/markdown/markdown.js"></script>
+<script src="../addon/hint/show-hint.js"></script>
+<script src="../addon/hint/tex-input-hint.js"></script>
+
+<style type="text/css">
+      .CodeMirror {border-top: 1px solid black; border-bottom: 1px solid black;}
+      .cm-s-default .cm-trailing-space-a:before,
+      .cm-s-default .cm-trailing-space-b:before {position: absolute; content: "\00B7"; color: #777;}
+      .cm-s-default .cm-trailing-space-new-line:before {position: absolute; content: "\21B5"; color: #777;}
+    </style>
+<div id=nav>
+  <a href="http://codemirror.net"><h1>CodeMirror</h1><img id=logo src="../doc/logo.png"></a>
+
+  <ul>
+    <li><a href="../index.html">Home</a>
+    <li><a href="../doc/manual.html">Manual</a>
+    <li><a href="https://github.com/codemirror/codemirror">Code</a>
+  </ul>
+  <ul>
+    <li><a href="../index.html">Language modes</a>
+    <li><a class=active href="#">Markdown</a>
+  </ul>
+</div>
+
+<article>
+<h2>Markdown mode</h2>
+<form><textarea id="code" name="code">
+*Using TeX-style Symbols*
+------------------------------------------------
+
+_TeX_-style symbols are names prefixed by a `\`.
+
+You can try to input symbols in this buffer by pressing `\`,
+
+Typing `\alpha` should input α.
+
+You can try more. This completion should work anywhere on the text,
+but beware is experimental.
+
+## Some more symbols:
+
+- \Gamma : Γ
+- \lnot: ¬
+
+</textarea></form>
+
+  <p>Press <strong>\</strong> to activate autocompletion. Built
+  on top of the <a href="../doc/manual.html#addon_show-hint"><code>show-hint</code></a>
+  and <a href="../doc/manual.html#addon_tex-input-hint"><code>TeX-input-hint</code></a>
+  addons.</p>
+
+    <script>
+      var editor = CodeMirror.fromTextArea(document.getElementById("code"), {
+        mode: 'markdown',
+        lineNumbers: true,
+        theme: "default",
+        extraKeys: {"Enter": "newlineAndIndentContinueMarkdownList"}
+      });
+    </script>
+
+  </article>

frontend/classic/external/CodeMirror-TeX-input/package.json

+{
+  "name": "codemirror-tex-input",
+  "version": "1.0.0",
+  "description": "This addon provides a completion hint for CodeMirror which allows to use the backslash key `\\` to compose Unicode characters in TeX style.",
+  "main": "demo/tex-input.html",
+  "directories": {
+    "doc": "doc"
+  },
+  "keywords": [
+    "CodeMirror",
+    "TeX",
+    "Hints"
+  ],
+  "repository": {
+    "type": "git",
+    "url": "git+https://github.com/ejgallego/CodeMirror-TeX-input.git"
+  },
+  "author": "Emilio Jesús Gallego Arias",
+  "license": "ISC"
+}