.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

addons/Makefile

-PKGS =  teach equations
+PKGS =  teach
 
 CONTEXT = jscoq+32bit
 ifeq ($(DUNE_WORKSPACE:%.64=64), 64)
@@ -46,7 +46,6 @@ endif
 
 world:
 	cd teach          && make
-	cd equations      && make
 
 privates:
 

addons/equations/.gitignore

-.*.swp
-/workdir
-_build

addons/equations/Makefile

-REPO = https://github.com/mattam82/Coq-Equations.git
-TAG = v1.3-8.17
-WORKDIR = workdir
-
-.PHONY: all get
-
-all: $(WORKDIR)
-	# not parallel: some Dune dependency mixup with generating META file
-	dune build -j1
-
-get: $(WORKDIR)
-
-$(WORKDIR):
-	git clone --depth=1 --no-checkout -b $(TAG) $(REPO) $(WORKDIR)
-	( cd $(WORKDIR) && git checkout $(TAG) && git apply ../patches/legacy-compat.patch )
-	rm $(WORKDIR)/theories/HoTT/dune  # HoTT still not available for 8.14
-

addons/equations/README.md

-# addon-equations
-Coq-Equations addon plugin for jsCoq

addons/equations/coq-equations.json

-{
-    "rootdir": "workdir",
-    "builddir": "coq-pkgs",
-    "projects": {
-        "equations": {
-            "theories": {
-                "prefix": "Equations"
-            },
-            "src": {
-                "prefix": "Equations"
-            }
-        }
-    }
-}

addons/equations/dune

-
-(rule
- (targets coq-pkgs)
- (deps
-  (package coq-equations)
-  workdir/src/equations_plugin.cma
-  (:pkg-json coq-equations.json))
- (action
-  (run npx %{env:pkgtool=jscoq} build %{pkg-json})))
-
-(alias
- (name all)
- (deps package.json))
-
-(dirs workdir)

addons/equations/package.json

-{
-    "name": "@jscoq/equations",
-    "description": "Equations 1.3 for jsCoq",
-    "version": "0.17.0",
-    "files": ["README.md", "coq-pkgs"],
-    "repository": {
-        "type": "git",
-        "url": "github:jscoq/addon-equations"
-    },
-    "license": "AGPL-3.0-or-later"
-}

addons/equations/patches/legacy-compat.patch

-diff --git a/theories/Type/Loader.v b/theories/Type/Loader.v
-index c3e7ed9..16cbcca 100644
---- a/theories/Type/Loader.v
-+++ b/theories/Type/Loader.v
-@@ -11,7 +11,7 @@
- Require Import Extraction.
- 
- (** This exports tactics *)
--Declare ML Module "coq-equations.plugin".
-+Declare ML Module "equations_plugin:coq-equations.plugin".
- 
- Set Warnings "-notation-overridden".
- From Equations Require Export Init Signature.
-@@ -32,4 +32,4 @@ Global Obligation Tactic := Equations.CoreTactics.equations_simpl.
- Ltac solve_rec := simpl in * ; cbv zeta ; intros ;
-   try typeclasses eauto with subterm_relation Below rec_decision.
- 
--Export EquationsNotations.
-\ No newline at end of file
-+Export EquationsNotations.

coqdoclight.py

 """
-Moulinette2
+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")
@@ -69,25 +84,29 @@ class Leading(Token):
     def __init__(self,lit):
         self.lit = lit
         self.idx = 0
-        self.newline = False
+        self.newline = True
     
     def reset(self):
-        self.newline = False
+        self.newline = True
+        self.idx = 0
 
     def eat(self,c):
         if c == '\n':
-            self.idx = 0
             self.newline = True
-        elif self.newline:
+        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
@@ -106,7 +125,6 @@ class Lit(Token):
         else:
             self.idx = 0
 
-
 class Scanner:
     def __init__(self,src):
         self.rules = []
@@ -119,7 +137,7 @@ class Scanner:
     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
@@ -175,7 +193,6 @@ class Scanner:
                 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):
@@ -193,10 +210,13 @@ class Scanner:
             
             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
@@ -211,23 +231,21 @@ class Rule:
 
 # Coqdoc
 TOK_BEGIN_CODE = Char('[')
-TOK_END_CODE_COQ = Lit("]]")
-TOK_END_CODE = Char(']')
-
-TOK_BEGIN_CODE_ALT=Lit("<<")
-TOK_END_CODE_ALT=Lit(">>")
+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):
@@ -239,39 +257,37 @@ class Code(Rule):
 
     def start_action(self,sc,s,e):
         self.action = self.end_action
-        sc.push([self], out)
-        if sc.consecutive() < 2: # non-coq code
-            out('<code>')
-            self.token = TOK_END_CODE
-        else: # coq code
+        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()
-        out('</code>')
 
-class AltCode(Rule):
+class Html(Rule):
     def __init__(self):
+        self.token = TOK_SHARP
         self.set_start()
 
     def set_start(self):
-        self.token = TOK_BEGIN_CODE_ALT
         self.action = self.start_action
 
     def start_action(self,sc,s,e):
         self.action = self.end_action
-        sc.push([self], out)
-        out('<code>')
-        self.token = TOK_END_CODE_ALT
+        sc.push([self], trimout)
         
     def end_action(self,sc,s,e):
         sc.pop()
         self.set_start()
-        out('</code>')
-
+        
 class Comment(Rule):
     def __init__(self):
         self.set_start()
@@ -282,7 +298,7 @@ class Comment(Rule):
 
     def start_action(self,sc,s,e):
         self.action = self.end_action
-        sc.push([self], out)
+        sc.push([self], trimout)
         out('<code class="cm-s-default coq-highlight">(*')
         self.token = TOK_END_COM
         
@@ -311,6 +327,53 @@ class Title(Rule):
         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
@@ -338,7 +401,7 @@ class Verbatim(Rule):
     def start_action(self,sc,s,e):
         self.action = self.end_action
         self.token = TOK_END_VERBATIM
-        sc.push([self], out)
+        sc.push([self], trimout)
         out('<pre>')
 
     def end_action(self,sc,s,e):
@@ -346,6 +409,22 @@ class Verbatim(Rule):
         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
@@ -356,8 +435,38 @@ class EndCoqdoc(Rule):
 # 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()
@@ -369,26 +478,90 @@ class Hide(Rule):
     def start_action(self,sc,s,e):
         self.action = self.end_action
         self.token = TOK_END_HIDE
-        sc.push([self], len) # len is used as as dummy function that prints nothing
+        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")
-        sc.push([Code (), Verbatim (), EndCoqdoc (), Title (), Italic (), Comment (), AltCode ()], html_out)
+        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('<textarea class="snippet">')
+        out_snippet()
         out(x.strip())
         out('</textarea>\n')
-    sc.push([Hide (), Coqdoc ()], snippet_out)
+    sc.push([Hide (), Coqdoc (), Details (), ReadOnly ()], snippet_out)
     
 
 if len(sys.argv) < 2:
@@ -444,7 +617,7 @@ out("""
         implicit_libs: false,
         focus: false,
         editor: { mode: { 'company-coq': true } },
-        all_pkgs: {'./coq-pkgs': ['coq'], './addons/teach/coq-pkgs': ['teach'], './addons/equations/coq-pkgs': ['equations']}
+        all_pkgs: {'./coq-pkgs': ['coq'], './addons/teach/coq-pkgs': ['teach']}
     };
 
     JsCoq.start(jscoq_ids, jscoq_opts).then(res => {

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

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

index.html

@@ -256,7 +256,7 @@ Qed.</textarea>
         implicit_libs: false,
         focus: false,
         editor: { mode: { 'company-coq': true } },
-        all_pkgs: {'./coq-pkgs': ['coq'], './addons/teach/coq-pkgs': ['teach'], './addons/equations/coq-pkgs': ['equations']}
+        all_pkgs: {'./coq-pkgs': ['coq'], './addons/teach/coq-pkgs': ['teach']}
     };
 
     JsCoq.start(jscoq_ids, jscoq_opts).then(res => {