Adding a dummy HOME into the Makefile to avoid warnings.

README.md

@@ -56,13 +56,14 @@ sudo apt install npm
 sudo npm install --global esy@latest
 ```
 
-Then to download and compile the dependencies, and compile the sources:
+Then to download and compile all dependencies (including Coq), and compile the sources:
 ```
 esy
 ```
 
 Note that `esy` uses a specific compiling environment, which is not exported to the current shell.
-To work within this environment, either prefix any command with `esy` (e.g. `esy emacs` to run Emacs with Proof General), or type `esy shell` to open a shell with the right environment.
+To work within this environment, prefix any command with `esy`, e.g. `esy coqide` to run your system’s coqIDE within the right environment.
+Alternatively, `esy shell` opens a shell with this environment.
 
 ### From sources
 

package.json

@@ -15,7 +15,7 @@
 			["./create_makefile.sh"],
 			["make", "-j"]
 		],
-		"install": ["make install"]
+		"install": "make install"
 	},
 	"scripts": {
 		"clean": "make clean",

scripts/Makefile.patch

---- 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 ###########################################################