.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

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

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" && make coq && make jscoq && npm link` to compile everything for the first time
+- 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;

frontend/classic/js/cm-provider.ts

@@ -43,7 +43,7 @@ class CmSentence {
     end : CodeMirror.Position;
     text : string;
     mark ?: number;
-    flags : {is_comment : boolean, is_hidden : boolean};
+    flags : {is_comment : boolean, is_hidden : () => boolean};
     feedback : number[];
     action : number;
     coq_sid : string;
@@ -133,7 +133,7 @@ export class CmCoqProvider {
     constructor(element, options, replace, idx) {
 
         CmCoqProvider._config();
-
+        let readOnly = element.classList.contains("read-only");
         var cmOpts = /** @type {CodeMirror.EditorConfiguration} */ (
             { mode : { name : "coq",
                        singleLineStringErrors : false },
@@ -145,7 +145,8 @@ export class CmCoqProvider {
               styleSelectedText : true,
               dragDrop          : false, /* handled by CoqManager */
               keyMap            : "jscoq",
-              className         : "jscoq"
+              className         : "jscoq",
+              readOnly          : readOnly
             });
 
         if (options)
@@ -191,6 +192,10 @@ export class CmCoqProvider {
         editor_element.on('mouseleave', ev => this.onCMMouseLeave(ev));
         if (makeHidden && !editor_element.is(':hidden'))
             editor_element.css({display: "none"});
+        
+        if(readOnly) {
+            editor_element.addClass("read-only");
+        }
 
         // Some hack to prevent CodeMirror from consuming PageUp/PageDn
         if (replace) pageUpDownOverride(editor_element[0]);
@@ -255,7 +260,20 @@ export class CmCoqProvider {
     }
 
     isHidden() {
-        return $(this.editor.getWrapperElement()).is(':hidden');
+        let wrapper = this.editor.getWrapperElement();
+        let parent = wrapper.parentElement;
+        
+        if(parent != null && parent.tagName === "DETAILS") {
+            let details : HTMLDetailsElement = parent as HTMLDetailsElement;
+            return () => {
+                return !details.open;
+            }
+        } else {
+            let hidden = $(wrapper).is(':hidden');
+            return () => {
+                return hidden;
+            }
+        }
     }
 
     // If prev == null then get the first.

frontend/classic/js/coq-highlighter.ts

+// CM imports
+import CodeMirror from "codemirror";
+import './mode/coq-mode.js';
+import 'codemirror/lib/codemirror.css';
+import 'codemirror/addon/runmode/runmode.js';
+
+export class CoqHighlighter {
+    highlight() {
+        // Highlight, but do not create editor for code
+        (async () => {
+            const slides = document.getElementsByClassName("coq-highlight");
+            for (let i = 0; i < slides.length; i++) {
+                let element = slides.item(i) as HTMLElement;
+                let code = element.textContent;
+                element.textContent = "";
+                CodeMirror.runMode(code, "coq", element);
+            }
+        })();
+    }
+}

frontend/classic/js/coq-manager.js

@@ -712,7 +712,7 @@ export class CoqManager {
         }
 
         var back_to_stm = ArrayFuncs.findLast(this.doc.sentences.slice(0, -1),
-            stm => !(stm.flags.is_comment || stm.flags.is_hidden));
+            stm => !(stm.flags.is_comment || stm.flags.is_hidden() ));
         if (!back_to_stm) return false;
 
         var cancel_stm = this.nextAdded(back_to_stm.coq_sid);
@@ -737,7 +737,7 @@ export class CoqManager {
             queue = [next_stm];
 
         // Step over comment block and hidden sections
-        while (next_stm && (next_stm.flags.is_comment || next_stm.flags.is_hidden) &&
+        while (next_stm && (next_stm.flags.is_comment || next_stm.flags.is_hidden()) &&
             (next_stm = this.provider.getNext(next_stm, until)))
             queue.push(next_stm);
 

frontend/classic/js/index.js

 //@ts-check
 "use strict"
 
+import { CoqHighlighter } from './coq-highlighter.js';
 // Main Frontend start point
 import { CoqManager } from './coq-manager.js';
 
@@ -24,6 +25,7 @@ const JsCoq = {
         this.base_path = jscoq_opts.base_path;
         //@ts-ignore
         window.JsCoq = this; // atm this is still needed by UI addons
+        new CoqHighlighter().highlight();
         return new CoqManager(jscoq_ids, jscoq_opts);
     },
 

index.html

@@ -77,8 +77,8 @@
 
     <h4>A First Example: <code>rev</code> <code>∘</code> <code>rev = id</code></h4>
     <p>
-      The following is a simple proof that <code>rev</code>, the standard list
-      reversal function as commonly defined in ML and other languages of the
+      The following is a simple proof that <code class="coq-highlight">rev</code>, the standard list
+      reversal function as commonly <code class="cm-s-default coq-highlight">Definition x := 3.</code> defined in ML and other languages of the
       family, is an involution.
     </p>
     <p>