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

Note: this is still not working due to version mismatches with the SDK.

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,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,14 @@ $ 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`
+- Auto-import is not working, you'll have to click on the package
+  manager
+
 # 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_2.v

@@ -5,6 +5,10 @@ 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