diff --git a/.gitignore b/.gitignore
index 1e421eb..7c1d595 100644
--- a/.gitignore
+++ b/.gitignore
@@ -7,3 +7,4 @@
 node_modules
 *.html
 coqdoc.css
+coq-pkgs
diff --git a/Makefile b/Makefile
index 43c6f46..f20d658 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,4 @@
-.PHONY: all clean serve
+.PHONY: all clean serve docker-setup
 
 COQDOC_AUTO=coqdoc.css
 
@@ -11,7 +11,7 @@ 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)
@@ -19,5 +19,15 @@ clean:
 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
diff --git a/README.md b/README.md
index 54cd1b4..cc9342d 100644
--- a/README.md
+++ b/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:
diff --git a/jscoq-agent.js b/jscoq-agent.js
index 224fdfb..97e2fae 100644
--- a/jscoq-agent.js
+++ b/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
 };
diff --git a/lesson_1.v b/lesson_1.v
index b6cf849..9313aea 100644
--- a/lesson_1.v
+++ b/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.
diff --git a/lesson_2.v b/lesson_2.v
index 2e49fd8..173cfdd 100644
--- a/lesson_2.v
+++ b/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. *)