diff --git a/.gitignore b/.gitignore
index 9de11b1409ae1bc46101579057c01af6272b655c..18a43fc1e3b60093cbc67b84479878d2cfb5c356 100644
--- a/.gitignore
+++ b/.gitignore
@@ -19,3 +19,5 @@ Makefile*
 /proof-state
 /with-proof-state
 /html-alectryon
+_esy
+esy.lock/
diff --git a/README.md b/README.md
index e85a1cdac0d05a91d00b23df01fc29aed5013249..e65132a0569b7016cc0e7d31f2ed0ce5f3e13a2a 100644
--- a/README.md
+++ b/README.md
@@ -46,7 +46,31 @@ opam update
 opam install coq-prosa
 ```
 
-### From sources
+### From Sources With `esy`
+
+Prosa can be installed using [esy](https://esy.sh/).
+
+#### Installing `esy`
+
+`esy` itself can typically be installed through `npm`.
+It should look something like this on most `apt`-based systems:
+```
+sudo apt install npm
+sudo npm install --global esy@latest
+```
+
+#### Installing Prosa
+
+With `esy` in place, it is easy to compile Prosa in one go. To download and compile all of Prosa's dependencies (including Coq), and then to compile Prosa itself, simply issue the command:
+```
+esy
+```
+
+Note that `esy` uses an internal compilation environment, which is not exported to the current shell.
+To work within this environment, prefix any command with `esy`: for instance `esy coqide` to run your system’s coqIDE within the right environment.
+Alternatively, `esy shell` opens a shell within its environment.
+
+### Manually From Sources
 
 #### Dependencies
 
diff --git a/package.json b/package.json
new file mode 100644
index 0000000000000000000000000000000000000000..773efb5af7d6ed7e5eb0cc2c21dc049433d4817e
--- /dev/null
+++ b/package.json
@@ -0,0 +1,55 @@
+{
+	"name": "coq-prosa",
+	"version": "1.0",
+	"description": "A Foundation for Formally Proven Schedulability Analysis",
+	"license": "BSD",
+	"esy": {
+		"buildsInSource": true,
+		"buildEnv": {
+			"COQBIN": "#{@opam/coq.bin}/",
+			"COQLIB": "#{@opam/coq.lib}/coq/",
+			"COQPATH": "#{coq-mathcomp-ssreflect.install}/user-contrib",
+			"DESTDIR": "#{self.install}"
+		},
+		"build": [
+			["./create_makefile.sh"],
+			["make", "-j"]
+		],
+		"install": "make install"
+	},
+	"scripts": {
+		"clean": "make clean",
+		"doc": "make html -j"
+	},
+	"dependencies": {
+		"@opam/coq": "8.13.2",
+		"@opam/ocamlfind": "1.8.1",
+		"coq-mathcomp-ssreflect": "1.12.0"
+	},
+	"devDependencies": {},
+	"resolutions": {
+		"coq-mathcomp-ssreflect": {
+			"source": "github:math-comp/math-comp#6bff567e84b01c1b3502985ec936b9e74ea252b4",
+			"version": "1.12.0",
+			"override": {
+				"dependencies": {
+					"@opam/coq": "8.13.2"
+				},
+				"buildsInSource": true,
+				"buildEnv": {
+					"HOME": "#{self.target_dir}",
+					"COQBIN": "#{@opam/coq.bin}/",
+					"COQLIB": "#{@opam/coq.lib}/coq/",
+					"COQPATH": "#{@opam/coq.lib}/coq/user-contrib",
+					"COQMAKEFILEOPTIONS": "DESTDIR = '#{self.install}' COQMF_WINDRIVE = '#{@opam/coq.lib}/coq'"
+				},
+				"build": [
+					[ "make", "-C", "mathcomp/ssreflect", "-j" ]
+				],
+				"install": [
+					[ "make", "-C", "mathcomp/ssreflect", "install" ]
+				]
+			}
+		}
+	}
+}
diff --git a/scripts/Makefile.patch b/scripts/Makefile.patch
index 907207cce07d262313d7881e75e76006c1844418..110128527a250e933bef9240af89da99d6e10307 100644
--- a/scripts/Makefile.patch
+++ b/scripts/Makefile.patch
@@ -1,6 +1,18 @@
---- Makefile.orig	2019-10-15 22:37:51.000000000 +0200
-+++ Makefile	2019-10-15 22:33:50.000000000 +0200
-@@ -179,7 +179,7 @@
+--- Makefile.orig	2021-10-04 11:15:22.592822933 +0200
++++ Makefile	2021-10-04 11:17:18.684584261 +0200
+@@ -15,6 +15,11 @@
+ SELF := $(lastword $(MAKEFILE_LIST))
+ PARENT := $(firstword $(MAKEFILE_LIST))
+ 
++# In the esy container, $HOME is hidden, but this causes Coq to complain.
++# We thus include a dummy $HOME value.
++HOME ?= $(DESTDIR)
++export HOME
++
+ # This file is generated by coq_makefile and contains many variable
+ # definitions, like the list of .v files or the path to Coq
+ include Makefile.conf
+@@ -211,7 +216,7 @@
  # these flags do NOT contain the libraries, to make them easier to overwrite
  COQFLAGS?=-q $(OTHERFLAGS) $(COQEXTRAFLAGS)
  COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS)
@@ -9,7 +21,7 @@
  
  COQDOCLIBS?=$(COQLIBS_NOML)
  
-@@ -422,6 +422,9 @@
+@@ -480,6 +485,9 @@
  	$(HIDE)mkdir -p html
  	$(HIDE)$(COQDOC) \
  		-toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES)
@@ -19,7 +31,7 @@
  
  mlihtml: $(MLIFILES:.mli=.cmi)
  	$(SHOW)'CAMLDOC -d $@'
-@@ -446,6 +449,10 @@
+@@ -504,6 +512,10 @@
  		-toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \
  		-o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
  
@@ -30,7 +42,7 @@
  # FIXME: not quite right, since the output name is different
  gallinahtml: GAL=-g
  gallinahtml: html
-@@ -585,6 +591,17 @@
+@@ -646,6 +658,17 @@
  	$(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx)
  .PHONY: archclean
  
@@ -45,6 +57,6 @@
 +
 +spell::
 +	./scripts/flag-typos-in-comments.sh `find .  -iname '*.v' ! -path './classic/*'`
-
+ 
  # Compilation rules ###########################################################