From 798d2dc57b9bcb0477b70d19508e280142a0e54e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Martin=20Constantino=E2=80=93Bodin?=
<martin.bodin@ens-lyon.org>
Date: Tue, 12 Oct 2021 08:23:42 +0000
Subject: [PATCH] add a `package.json` file to turn Prosa into an `esy`
package.
`esy` is an `npm`-like package manager and build tool designed for
reproducibility, by preventing the use of unlisted dependencies and
pinning the exact version of each of these (a bit like `opam`, but
with more guarantees).
A nice feature of `esy` is ease of installation:
1. Install `esy` through `npm`. (However, note that `esy` is not a
JavaScript program; the `esy` project just uses `npm` as a code
hoster.
2. Run `esy` in the Prosa repository.
This will download and compile all dependencies and compile the
repository. (On the flip side, this also means that Coq will be
compiled, so the first time, compilation will be slow.)
See the README.md file for usage instructions.
See also the discussion: https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/80
For more information about `esy`, see: https://esy.sh/
---
.gitignore | 2 ++
README.md | 26 +++++++++++++++++++-
package.json | 55 ++++++++++++++++++++++++++++++++++++++++++
scripts/Makefile.patch | 26 ++++++++++++++------
4 files changed, 101 insertions(+), 8 deletions(-)
create mode 100644 package.json
diff --git a/.gitignore b/.gitignore
index 9de11b140..18a43fc1e 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 e85a1cdac..e65132a05 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 000000000..773efb5af
--- /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 907207cce..110128527 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 ###########################################################
--
GitLab