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

Note: this is not working due to version mismatches.

Author: ejgallego

.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,21 @@ 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/wacoq-bin/bin/coq/
+
+docker-setup:
+	docker pull jscoq/jscoq:v8.16-sdk
+	docker tag jscoq/jscoq:v8.16-sdk jscoq:sdk

jscoq-agent.js

@@ -31,7 +31,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_2.v

@@ -5,6 +5,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+From MyCourse Require Import lesson_1.
+
 Definition sorry {T} : T. Admitted.
 (** ** Reflection and proving with computation