[build] Add support for building a lessons coq-pkg package

.gitignore

@@ -7,3 +7,4 @@
 node_modules
 *.html
 coqdoc.css
+coq-pkgs

Makefile

@@ -1,4 +1,4 @@
-.PHONY: all clean serve
+.PHONY: all clean serve docker-setup
 
 COQDOC_AUTO=coqdoc.css
 
@@ -11,13 +11,23 @@ all: $(FILES_HTML)
 	./jscoqdoc $<
 
 %.glob: %.v
-	coqc $<
+	npx jscoq sdk coqc -R . MyCourse $<
 
 clean:
 	rm -f *.vo *.vok .*.aux *.glob *.vos $(FILES_HTML) $(COQDOC_AUTO)
 
 node_modules: package.json package-lock.json
 	npm i
 
-serve: node_modules
+serve: node_modules coq-pkgs/my_course.coq-pkg
 	./node_modules/.bin/http-server .
+
+coq-pkgs/my_course.coq-pkg: $(FILES_HTML) docker-setup
+	npx jscoq build . --top MyCourse --package $@
+	cp -a coq-pkgs/* node_modules/jscoq/coq-pkgs/
+
+SDK_VERSION=v8.17
+
+docker-setup:
+	docker pull jscoq/jscoq:$(SDK_VERSION)-sdk
+	docker tag jscoq/jscoq:$(SDK_VERSION)-sdk jscoq:sdk

README.md

@@ -15,6 +15,18 @@ $ make serve # Open a web server with the jsCoq files
 Note that `make serve` doesn't need to be restarted after a regular
 `make`.
 
+# Building multiple files with the jsCoq SDK
+
+This is WIP, for now you can do:
+
+- `make coq-pkgs/my_course.coq-pkg`
+
+## TODO / Known issues
+
+- Auto-import is not working, you'll have to click on the package
+  manager
+- the jsCoq SDK cannot locate external libs, such as math-comp
+
 # Tweaks from official distro
 
 We have customized the following files from the oficial distro:

jscoq-agent.js

@@ -35,7 +35,7 @@ var jscoq_opts = {
     // editor:    { mode: { 'company-coq': true }, className: 'jscoq code-tight' },
     editor:    { className: 'jscoq code-tight' },
     init_pkgs: ['init'],
-    all_pkgs:  { '+': ['coq', 'mathcomp'] },
+    all_pkgs:  { '+': ['coq', 'mathcomp', 'my_course'] },
     init_import: ['utf8'],
     implicit_libs: true
 };

lesson_1.v

@@ -11,7 +11,9 @@ In this course, we will use a mature Coq library, "The Mathematical
 Components Library" which will provide us with a rich theory on data
 types and mathematics. *)
 
-From mathcomp Require Import all_ssreflect.
+(* From mathcomp Require Import all_ssreflect. *)
+
+From Coq Require Import ssreflect.
 
 Set Implicit Arguments.
 Unset Strict Implicit.

lesson_2.v

@@ -1,10 +1,15 @@
 (** * Lesson 2: Data Structures and Class Hierarchies *)
-From mathcomp Require Import all_ssreflect.
+From Coq Require Import ssreflect.
+(* From mathcomp Require Import all_ssreflect. *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+From MyCourse Require Import lesson_1.
+
+About x_implies_x.
+
 Definition sorry {T} : T. Admitted.
 (** ** Reflection and proving with computation
 
@@ -24,23 +29,23 @@ Coq Standard library vs as it is defined in math-comp: *)
 About le.
 Print le.
 
-About leq.
-Print leq.
+(* About leq. *)
+(* Print leq. *)
 
 Lemma le_1 : 100 <= 200.
 Proof. Admitted.
 
 Print le_1.
 
-Lemma le_2 : (100 <= 200)%coq_nat.
-Proof. Admitted.
+(* Lemma le_2 : (100 <= 200)%coq_nat. *)
+(* Proof. Admitted. *)
 
-Print le_2.
+(* Print le_2. *)
 
-Lemma lt_1 n : ~~ (n < n).
-Proof. Admitted.
+(* Lemma lt_1 n : ~~ (n < n). *)
+(* Proof. Admitted. *)
 
-Lemma lt_2 n : ~ (n < n)%coq_nat.
-Proof. Admitted.
+(* Lemma lt_2 n : ~ (n < n)%coq_nat. *)
+(* Proof. Admitted. *)
 (** Moreover, the math-comp version, by virtue of being in [bool],
 inherits some nice properties, like decidability, for free. *)