[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,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_1.v

@@ -11,7 +11,10 @@ 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 Coq Require Import ssreflect.
+
+(* Not working due to the SDK not including math-comp yet, will fix *)
+(* From mathcomp Require Import all_ssreflect. *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.

lesson_2.v

@@ -1,10 +1,14 @@
 (** * 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.
+
 Definition sorry {T} : T. Admitted.
 (** ** Reflection and proving with computation
 
@@ -24,23 +28,24 @@ 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_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. *)