diff --git a/.gitignore b/.gitignore
index 9de11b1409ae1bc46101579057c01af6272b655c..891a5ae8f59dcc566c25d0d5c569b1bc132709e9 100644
--- a/.gitignore
+++ b/.gitignore
@@ -19,3 +19,4 @@ Makefile*
/proof-state
/with-proof-state
/html-alectryon
+_esy
diff --git a/README.md b/README.md
index e85a1cdac0d05a91d00b23df01fc29aed5013249..4905b1be9332925d51f66f124ba9e05c6291d406 100644
--- a/README.md
+++ b/README.md
@@ -46,6 +46,24 @@ opam update
opam install coq-prosa
```
+#### From sources, with `esy`
+
+Prosa can be installed using [esy](https://esy.sh/).
+
+`esy` itself can be typically installed through `npm`:
+```
+sudo apt install npm
+sudo npm install --global esy@latest
+```
+
+Then to download and compile the dependencies, 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.
+
### From sources
#### Dependencies
diff --git a/esy.lock/.gitattributes b/esy.lock/.gitattributes
new file mode 100644
index 0000000000000000000000000000000000000000..e0b4e26c5ad07b19ff601d02a4642205affc18a3
--- /dev/null
+++ b/esy.lock/.gitattributes
@@ -0,0 +1,3 @@
+
+# Set eol to LF so files aren't converted to CRLF-eol on Windows.
+* text eol=lf linguist-generated
diff --git a/esy.lock/.gitignore b/esy.lock/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..a221be227e34801da7d11c5214d2ccc716a73465
--- /dev/null
+++ b/esy.lock/.gitignore
@@ -0,0 +1,3 @@
+
+# Reset any possible .gitignore, we want all esy.lock to be un-ignored.
+!*
diff --git a/esy.lock/index.json b/esy.lock/index.json
new file mode 100644
index 0000000000000000000000000000000000000000..f25114376ea389b8e8e3d94433255605a802bd25
--- /dev/null
+++ b/esy.lock/index.json
@@ -0,0 +1,297 @@
+{
+ "checksum": "ad73638467e1ac54c6475a3fb959e0b6",
+ "root": "coq-prosa@link-dev:./package.json",
+ "node": {
+ "ocaml@4.12.0@d41d8cd9": {
+ "id": "ocaml@4.12.0@d41d8cd9",
+ "name": "ocaml",
+ "version": "4.12.0",
+ "source": {
+ "type": "install",
+ "source": [
+ "archive:https://registry.npmjs.org/ocaml/-/ocaml-4.12.0.tgz#sha1:2a979f37535faaded8aa3fdf82b6f16f2c71e284"
+ ]
+ },
+ "overrides": [],
+ "dependencies": [],
+ "devDependencies": []
+ },
+ "esy-m4@github:esy-packages/esy-m4#c7cf0ac9221be2b1f9d90e83559ca08397a629e7@d41d8cd9": {
+ "id":
+ "esy-m4@github:esy-packages/esy-m4#c7cf0ac9221be2b1f9d90e83559ca08397a629e7@d41d8cd9",
+ "name": "esy-m4",
+ "version":
+ "github:esy-packages/esy-m4#c7cf0ac9221be2b1f9d90e83559ca08397a629e7",
+ "source": {
+ "type": "install",
+ "source": [
+ "github:esy-packages/esy-m4#c7cf0ac9221be2b1f9d90e83559ca08397a629e7"
+ ]
+ },
+ "overrides": [],
+ "dependencies": [],
+ "devDependencies": []
+ },
+ "esy-gmp@archive:https://gmplib.org/download/gmp/gmp-6.2.1.tar.xz#sha1:0578d48607ec0e272177d175fd1807c30b00fdf2@d3dc108f": {
+ "id":
+ "esy-gmp@archive:https://gmplib.org/download/gmp/gmp-6.2.1.tar.xz#sha1:0578d48607ec0e272177d175fd1807c30b00fdf2@d3dc108f",
+ "name": "esy-gmp",
+ "version":
+ "archive:https://gmplib.org/download/gmp/gmp-6.2.1.tar.xz#sha1:0578d48607ec0e272177d175fd1807c30b00fdf2",
+ "source": {
+ "type": "install",
+ "source": [
+ "archive:https://gmplib.org/download/gmp/gmp-6.2.1.tar.xz#sha1:0578d48607ec0e272177d175fd1807c30b00fdf2"
+ ]
+ },
+ "overrides": [ "esy.lock/overrides/d3dc108f8f9f64699d29c9c180f20b50" ],
+ "dependencies": [],
+ "devDependencies": []
+ },
+ "coq-prosa@link-dev:./package.json": {
+ "id": "coq-prosa@link-dev:./package.json",
+ "name": "coq-prosa",
+ "version": "link-dev:./package.json",
+ "source": {
+ "type": "link-dev",
+ "path": ".",
+ "manifest": "package.json"
+ },
+ "overrides": [],
+ "dependencies": [
+ "coq-mathcomp-ssreflect@github:math-comp/math-comp#6bff567e84b01c1b3502985ec936b9e74ea252b4@6a993023",
+ "@opam/ocamlfind@opam:1.8.1@b7dc3072",
+ "@opam/coq@opam:8.13.2@b084b257"
+ ],
+ "devDependencies": []
+ },
+ "coq-mathcomp-ssreflect@github:math-comp/math-comp#6bff567e84b01c1b3502985ec936b9e74ea252b4@6a993023": {
+ "id":
+ "coq-mathcomp-ssreflect@github:math-comp/math-comp#6bff567e84b01c1b3502985ec936b9e74ea252b4@6a993023",
+ "name": "coq-mathcomp-ssreflect",
+ "version":
+ "github:math-comp/math-comp#6bff567e84b01c1b3502985ec936b9e74ea252b4",
+ "source": {
+ "type": "install",
+ "source": [
+ "github:math-comp/math-comp#6bff567e84b01c1b3502985ec936b9e74ea252b4"
+ ]
+ },
+ "overrides": [
+ {
+ "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" ] ]
+ }
+ ],
+ "dependencies": [ "@opam/coq@opam:8.13.2@b084b257" ],
+ "devDependencies": []
+ },
+ "@opam/zarith@opam:1.12@232cc7f2": {
+ "id": "@opam/zarith@opam:1.12@232cc7f2",
+ "name": "@opam/zarith",
+ "version": "opam:1.12",
+ "source": {
+ "type": "install",
+ "source": [
+ "archive:https://opam.ocaml.org/cache/md5/bf/bf368f3d9e20b6b446d54681afc05a04#md5:bf368f3d9e20b6b446d54681afc05a04",
+ "archive:https://github.com/ocaml/Zarith/archive/release-1.12.tar.gz#md5:bf368f3d9e20b6b446d54681afc05a04"
+ ],
+ "opam": {
+ "name": "zarith",
+ "version": "1.12",
+ "path": "esy.lock/opam/zarith.1.12"
+ }
+ },
+ "overrides": [
+ {
+ "opamoverride":
+ "esy.lock/overrides/opam__s__zarith_opam__c__1.12_opam_override"
+ }
+ ],
+ "dependencies": [
+ "ocaml@4.12.0@d41d8cd9", "@opam/ocamlfind@opam:1.8.1@b7dc3072",
+ "@opam/conf-gmp@opam:3@a623586f", "@esy-ocaml/substs@0.0.1@d41d8cd9"
+ ],
+ "devDependencies": [
+ "ocaml@4.12.0@d41d8cd9", "@opam/ocamlfind@opam:1.8.1@b7dc3072",
+ "@opam/conf-gmp@opam:3@a623586f"
+ ]
+ },
+ "@opam/ocamlfind@opam:1.8.1@b7dc3072": {
+ "id": "@opam/ocamlfind@opam:1.8.1@b7dc3072",
+ "name": "@opam/ocamlfind",
+ "version": "opam:1.8.1",
+ "source": {
+ "type": "install",
+ "source": [
+ "archive:https://opam.ocaml.org/cache/md5/18/18ca650982c15536616dea0e422cbd8c#md5:18ca650982c15536616dea0e422cbd8c",
+ "archive:http://download2.camlcity.org/download/findlib-1.8.1.tar.gz#md5:18ca650982c15536616dea0e422cbd8c",
+ "archive:http://download.camlcity.org/download/findlib-1.8.1.tar.gz#md5:18ca650982c15536616dea0e422cbd8c"
+ ],
+ "opam": {
+ "name": "ocamlfind",
+ "version": "1.8.1",
+ "path": "esy.lock/opam/ocamlfind.1.8.1"
+ }
+ },
+ "overrides": [
+ {
+ "opamoverride":
+ "esy.lock/overrides/opam__s__ocamlfind_opam__c__1.8.1_opam_override"
+ }
+ ],
+ "dependencies": [
+ "ocaml@4.12.0@d41d8cd9", "@opam/conf-m4@opam:1@196bf219",
+ "@esy-ocaml/substs@0.0.1@d41d8cd9"
+ ],
+ "devDependencies": [ "ocaml@4.12.0@d41d8cd9" ]
+ },
+ "@opam/num@opam:1.4@15ff926d": {
+ "id": "@opam/num@opam:1.4@15ff926d",
+ "name": "@opam/num",
+ "version": "opam:1.4",
+ "source": {
+ "type": "install",
+ "source": [
+ "archive:https://opam.ocaml.org/cache/md5/cd/cda2b727e116a0b6a9c03902cc4b2415#md5:cda2b727e116a0b6a9c03902cc4b2415",
+ "archive:https://github.com/ocaml/num/archive/v1.4.tar.gz#md5:cda2b727e116a0b6a9c03902cc4b2415"
+ ],
+ "opam": {
+ "name": "num",
+ "version": "1.4",
+ "path": "esy.lock/opam/num.1.4"
+ }
+ },
+ "overrides": [
+ {
+ "opamoverride":
+ "esy.lock/overrides/opam__s__num_opam__c__1.4_opam_override"
+ }
+ ],
+ "dependencies": [
+ "ocaml@4.12.0@d41d8cd9", "@opam/ocamlfind@opam:1.8.1@b7dc3072",
+ "@esy-ocaml/substs@0.0.1@d41d8cd9"
+ ],
+ "devDependencies": [ "ocaml@4.12.0@d41d8cd9" ]
+ },
+ "@opam/coq@opam:8.13.2@b084b257": {
+ "id": "@opam/coq@opam:8.13.2@b084b257",
+ "name": "@opam/coq",
+ "version": "opam:8.13.2",
+ "source": {
+ "type": "install",
+ "source": [
+ "archive:https://opam.ocaml.org/cache/sha256/1e/1e7793d8483f1e939f62df6749f843df967a15d843a4a5acb024904b76e25a14#sha256:1e7793d8483f1e939f62df6749f843df967a15d843a4a5acb024904b76e25a14",
+ "archive:https://github.com/coq/coq/archive/V8.13.2.tar.gz#sha256:1e7793d8483f1e939f62df6749f843df967a15d843a4a5acb024904b76e25a14"
+ ],
+ "opam": {
+ "name": "coq",
+ "version": "8.13.2",
+ "path": "esy.lock/opam/coq.8.13.2"
+ }
+ },
+ "overrides": [],
+ "dependencies": [
+ "ocaml@4.12.0@d41d8cd9", "@opam/zarith@opam:1.12@232cc7f2",
+ "@opam/ocamlfind@opam:1.8.1@b7dc3072", "@opam/num@opam:1.4@15ff926d",
+ "@opam/conf-findutils@opam:1@34f14152",
+ "@esy-ocaml/substs@0.0.1@d41d8cd9"
+ ],
+ "devDependencies": [
+ "ocaml@4.12.0@d41d8cd9", "@opam/zarith@opam:1.12@232cc7f2",
+ "@opam/num@opam:1.4@15ff926d"
+ ]
+ },
+ "@opam/conf-m4@opam:1@196bf219": {
+ "id": "@opam/conf-m4@opam:1@196bf219",
+ "name": "@opam/conf-m4",
+ "version": "opam:1",
+ "source": {
+ "type": "install",
+ "source": [ "no-source:" ],
+ "opam": {
+ "name": "conf-m4",
+ "version": "1",
+ "path": "esy.lock/opam/conf-m4.1"
+ }
+ },
+ "overrides": [
+ {
+ "opamoverride":
+ "esy.lock/overrides/opam__s__conf_m4_opam__c__1_opam_override"
+ }
+ ],
+ "dependencies": [
+ "esy-m4@github:esy-packages/esy-m4#c7cf0ac9221be2b1f9d90e83559ca08397a629e7@d41d8cd9",
+ "@esy-ocaml/substs@0.0.1@d41d8cd9"
+ ],
+ "devDependencies": []
+ },
+ "@opam/conf-gmp@opam:3@a623586f": {
+ "id": "@opam/conf-gmp@opam:3@a623586f",
+ "name": "@opam/conf-gmp",
+ "version": "opam:3",
+ "source": {
+ "type": "install",
+ "source": [ "no-source:" ],
+ "opam": {
+ "name": "conf-gmp",
+ "version": "3",
+ "path": "esy.lock/opam/conf-gmp.3"
+ }
+ },
+ "overrides": [
+ {
+ "opamoverride":
+ "esy.lock/overrides/opam__s__conf_gmp_opam__c__3_opam_override"
+ }
+ ],
+ "dependencies": [
+ "esy-gmp@archive:https://gmplib.org/download/gmp/gmp-6.2.1.tar.xz#sha1:0578d48607ec0e272177d175fd1807c30b00fdf2@d3dc108f",
+ "@esy-ocaml/substs@0.0.1@d41d8cd9"
+ ],
+ "devDependencies": []
+ },
+ "@opam/conf-findutils@opam:1@34f14152": {
+ "id": "@opam/conf-findutils@opam:1@34f14152",
+ "name": "@opam/conf-findutils",
+ "version": "opam:1",
+ "source": {
+ "type": "install",
+ "source": [ "no-source:" ],
+ "opam": {
+ "name": "conf-findutils",
+ "version": "1",
+ "path": "esy.lock/opam/conf-findutils.1"
+ }
+ },
+ "overrides": [],
+ "dependencies": [ "@esy-ocaml/substs@0.0.1@d41d8cd9" ],
+ "devDependencies": []
+ },
+ "@esy-ocaml/substs@0.0.1@d41d8cd9": {
+ "id": "@esy-ocaml/substs@0.0.1@d41d8cd9",
+ "name": "@esy-ocaml/substs",
+ "version": "0.0.1",
+ "source": {
+ "type": "install",
+ "source": [
+ "archive:https://registry.npmjs.org/@esy-ocaml/substs/-/substs-0.0.1.tgz#sha1:59ebdbbaedcda123fc7ed8fb2b302b7d819e9a46"
+ ]
+ },
+ "overrides": [],
+ "dependencies": [],
+ "devDependencies": []
+ }
+ }
+}
\ No newline at end of file
diff --git a/esy.lock/opam/conf-findutils.1/opam b/esy.lock/opam/conf-findutils.1/opam
new file mode 100644
index 0000000000000000000000000000000000000000..c00d47b25fb2c2a616de37716c5fdb9801e731fe
--- /dev/null
+++ b/esy.lock/opam/conf-findutils.1/opam
@@ -0,0 +1,21 @@
+opam-version: "2.0"
+homepage: "https://www.gnu.org/software/findutils/"
+bug-reports: "https://github.com/ocaml/opam-repository/issues"
+authors: "GNU Project"
+license: "GPL-3.0-or-later"
+build: [["sh" "-exc" "find . -name ."]]
+depexts: [
+ ["findutils"] {os-family = "debian"}
+ ["findutils"] {os-distribution = "fedora"}
+ ["findutils"] {os-distribution = "rhel"}
+ ["findutils"] {os-distribution = "centos"}
+ ["findutils"] {os-distribution = "alpine"}
+ ["findutils"] {os-distribution = "nixos"}
+ ["findutils"] {os-family = "suse"}
+ ["findutils"] {os-distribution = "ol"}
+ ["findutils"] {os-distribution = "arch"}
+]
+synopsis: "Virtual package relying on findutils"
+description:
+ "This package can only install if the findutils binary is installed on the system."
+flags: conf
diff --git a/esy.lock/opam/conf-gmp.3/files/test.c b/esy.lock/opam/conf-gmp.3/files/test.c
new file mode 100644
index 0000000000000000000000000000000000000000..da9c0b59a8116db9fdd945972d4b8cba3e1b4964
--- /dev/null
+++ b/esy.lock/opam/conf-gmp.3/files/test.c
@@ -0,0 +1,10 @@
+#include <gmp.h>
+#ifndef __GMP_H__
+#error "No GMP header"
+#endif
+
+void test(void) {
+ mpz_t n;
+ mpz_init(n);
+ mpz_clear(n);
+}
diff --git a/esy.lock/opam/conf-gmp.3/opam b/esy.lock/opam/conf-gmp.3/opam
new file mode 100644
index 0000000000000000000000000000000000000000..176911ba704ea6b45562c813ba40b8262ee30c0f
--- /dev/null
+++ b/esy.lock/opam/conf-gmp.3/opam
@@ -0,0 +1,32 @@
+opam-version: "2.0"
+maintainer: "nbraud"
+homepage: "http://gmplib.org/"
+bug-reports: "https://github.com/ocaml/opam-repository/issues"
+license: "GPL-1.0-or-later"
+build: [
+ ["sh" "-exc" "cc -c $CFLAGS -I/usr/local/include test.c"] {os != "macos"}
+ [
+ "sh"
+ "-exc"
+ "cc -c $CFLAGS -I/opt/homebrew/include -I/opt/local/include -I/usr/local/include test.c"
+ ] {os = "macos"}
+]
+depexts: [
+ ["libgmp-dev"] {os-family = "debian"}
+ ["libgmp-dev"] {os-family = "ubuntu"}
+ ["gmp"] {os = "macos" & os-distribution = "homebrew"}
+ ["gmp"] {os-distribution = "macports" & os = "macos"}
+ ["gmp" "gmp-devel"] {os-distribution = "centos"}
+ ["gmp" "gmp-devel"] {os-distribution = "fedora"}
+ ["gmp" "gmp-devel"] {os-distribution = "ol"}
+ ["gmp"] {os = "openbsd"}
+ ["gmp"] {os = "freebsd"}
+ ["gmp-dev"] {os-distribution = "alpine"}
+ ["gmp-devel"] {os-family = "suse"}
+]
+synopsis: "Virtual package relying on a GMP lib system installation"
+description:
+ "This package can only install if the GMP lib is installed on the system."
+authors: "nbraud"
+extra-files: ["test.c" "md5=2fd2970c293c36222a6d299ec155823f"]
+flags: conf
diff --git a/esy.lock/opam/conf-m4.1/opam b/esy.lock/opam/conf-m4.1/opam
new file mode 100644
index 0000000000000000000000000000000000000000..c6feb2a7468cd110a5c6d49d9aed691493a21539
--- /dev/null
+++ b/esy.lock/opam/conf-m4.1/opam
@@ -0,0 +1,22 @@
+opam-version: "2.0"
+maintainer: "tim@gfxmonk.net"
+homepage: "http://www.gnu.org/software/m4/m4.html"
+bug-reports: "https://github.com/ocaml/opam-repository/issues"
+authors: "GNU Project"
+license: "GPL-3.0-only"
+build: [["sh" "-exc" "echo | m4"]]
+depexts: [
+ ["m4"] {os-family = "debian"}
+ ["m4"] {os-distribution = "fedora"}
+ ["m4"] {os-distribution = "rhel"}
+ ["m4"] {os-distribution = "centos"}
+ ["m4"] {os-distribution = "alpine"}
+ ["m4"] {os-distribution = "nixos"}
+ ["m4"] {os-family = "suse"}
+ ["m4"] {os-distribution = "ol"}
+ ["m4"] {os-distribution = "arch"}
+]
+synopsis: "Virtual package relying on m4"
+description:
+ "This package can only install if the m4 binary is installed on the system."
+flags: conf
diff --git a/esy.lock/opam/coq.8.13.2/files/coq.install b/esy.lock/opam/coq.8.13.2/files/coq.install
new file mode 100644
index 0000000000000000000000000000000000000000..5642d888dd7fb0d114d25b40cffabb0d71c5c6a3
--- /dev/null
+++ b/esy.lock/opam/coq.8.13.2/files/coq.install
@@ -0,0 +1,12 @@
+bin: [
+ "bin/coqwc"
+ "bin/coqtop"
+ "bin/coqtop.byte"
+ "bin/coqdoc"
+ "bin/coqdep"
+ "bin/coqchk"
+ "bin/coqc"
+ "bin/coq_makefile"
+ "bin/coq-tex"
+ "bin/coqworkmgr"
+]
diff --git a/esy.lock/opam/coq.8.13.2/opam b/esy.lock/opam/coq.8.13.2/opam
new file mode 100644
index 0000000000000000000000000000000000000000..2a47cfca6341fa3c72e25933cf1f4e73f47271d8
--- /dev/null
+++ b/esy.lock/opam/coq.8.13.2/opam
@@ -0,0 +1,60 @@
+opam-version: "2.0"
+maintainer: "coqdev@inria.fr"
+authors: "The Coq development team, INRIA, CNRS, and contributors."
+homepage: "https://coq.inria.fr/"
+bug-reports: "https://github.com/coq/coq/issues"
+dev-repo: "git+https://github.com/coq/coq.git"
+license: "LGPL-2.1-only"
+synopsis: "Formal proof management system"
+description: """
+The Coq proof assistant provides a formal language to write
+mathematical definitions, executable algorithms, and theorems, together
+with an environment for semi-interactive development of machine-checked
+proofs. Typical applications include the certification of properties of programming
+languages (e.g., the CompCert compiler certification project and the
+Bedrock verified low-level programming library), the formalization of
+mathematics (e.g., the full formalization of the Feit-Thompson theorem
+and homotopy type theory) and teaching.
+"""
+
+depopts: [
+ "coq-native"
+]
+depends: [
+ "ocaml" {>= "4.05.0"}
+ "ocamlfind" {build}
+ "num"
+ "conf-findutils" {build}
+ "zarith" {>= "1.10"}
+]
+conflicts: [
+ "ocaml-option-nnp"
+]
+build: [
+ [
+ "./configure"
+ "-configdir" "%{lib}%/coq/config"
+ "-prefix" prefix
+ "-mandir" man
+ "-docdir" doc
+ "-libdir" "%{lib}%/coq"
+ "-datadir" "%{share}%/coq"
+ "-coqide" "no"
+ "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
+ ]
+ [make "-j%{jobs}%"]
+ [make "-j%{jobs}%" "byte"]
+]
+install: [
+ [make "install"]
+ [make "install-byte"]
+]
+
+extra-files: [
+ ["coq.install" "sha512=b501737b4dbd22adc1c0377d744448056fb1dc493caf72c05f57c8463cf23f758373605ab3a50b9f505e4c856c41039d0bd7f81f96ed62adc6a674179523e7d2"]
+]
+
+url {
+ src: "https://github.com/coq/coq/archive/V8.13.2.tar.gz"
+ checksum: "sha256=1e7793d8483f1e939f62df6749f843df967a15d843a4a5acb024904b76e25a14"
+}
diff --git a/esy.lock/opam/num.1.4/opam b/esy.lock/opam/num.1.4/opam
new file mode 100644
index 0000000000000000000000000000000000000000..0e39879b2bd6f63640bff57b0e52970b7ad79d7d
--- /dev/null
+++ b/esy.lock/opam/num.1.4/opam
@@ -0,0 +1,27 @@
+opam-version: "2.0"
+synopsis:
+ "The legacy Num library for arbitrary-precision integer and rational arithmetic"
+maintainer: "Xavier Leroy <xavier.leroy@inria.fr>"
+authors: ["Valérie Ménissier-Morain" "Pierre Weis" "Xavier Leroy"]
+license: "LGPL-2.1-only WITH OCaml-LGPL-linking-exception"
+homepage: "https://github.com/ocaml/num/"
+bug-reports: "https://github.com/ocaml/num/issues"
+depends: [
+ "ocaml" {>= "4.06.0"}
+ "ocamlfind" {build & >= "1.7.3"}
+]
+conflicts: ["base-num"]
+build: make
+install: [
+ make
+ "install" {!ocaml:preinstalled}
+ "findlib-install" {ocaml:preinstalled}
+]
+dev-repo: "git+https://github.com/ocaml/num.git"
+url {
+ src: "https://github.com/ocaml/num/archive/v1.4.tar.gz"
+ checksum: [
+ "md5=cda2b727e116a0b6a9c03902cc4b2415"
+ "sha512=0cc9be8ad95704bb683b4bf6698bada1ee9a40dc05924b72adc7b969685c33eeb68ccf174cc09f6a228c48c18fe94af06f28bebc086a24973a066da620db8e6f"
+ ]
+}
\ No newline at end of file
diff --git a/esy.lock/opam/ocamlfind.1.8.1/files/ocaml-stub b/esy.lock/opam/ocamlfind.1.8.1/files/ocaml-stub
new file mode 100644
index 0000000000000000000000000000000000000000..e5ad9907e804afb4c84b3f7edacdb1806f4486f5
--- /dev/null
+++ b/esy.lock/opam/ocamlfind.1.8.1/files/ocaml-stub
@@ -0,0 +1,4 @@
+#!/bin/sh
+
+BINDIR=$(dirname "$(command -v ocamlc)")
+"$BINDIR/ocaml" -I "$OCAML_TOPLEVEL_PATH" "$@"
diff --git a/esy.lock/opam/ocamlfind.1.8.1/files/ocamlfind.install b/esy.lock/opam/ocamlfind.1.8.1/files/ocamlfind.install
new file mode 100644
index 0000000000000000000000000000000000000000..295c62545fdfc3534cefa45aea9a5bd2ae40b4cc
--- /dev/null
+++ b/esy.lock/opam/ocamlfind.1.8.1/files/ocamlfind.install
@@ -0,0 +1,6 @@
+bin: [
+ "src/findlib/ocamlfind" {"ocamlfind"}
+ "?src/findlib/ocamlfind_opt" {"ocamlfind"}
+ "?tools/safe_camlp4"
+]
+toplevel: ["src/findlib/topfind"]
diff --git a/esy.lock/opam/ocamlfind.1.8.1/opam b/esy.lock/opam/ocamlfind.1.8.1/opam
new file mode 100644
index 0000000000000000000000000000000000000000..04cbc6ccaf79c33599fe28ef2ff17a8b1e764d5c
--- /dev/null
+++ b/esy.lock/opam/ocamlfind.1.8.1/opam
@@ -0,0 +1,64 @@
+opam-version: "2.0"
+synopsis: "A library manager for OCaml"
+maintainer: "Thomas Gazagnaire <thomas@gazagnaire.org>"
+authors: "Gerd Stolpmann <gerd@gerd-stolpmann.de>"
+homepage: "http://projects.camlcity.org/projects/findlib.html"
+bug-reports: "https://gitlab.camlcity.org/gerd/lib-findlib/issues"
+dev-repo: "git+https://gitlab.camlcity.org/gerd/lib-findlib.git"
+description: """
+Findlib is a library manager for OCaml. It provides a convention how
+to store libraries, and a file format ("META") to describe the
+properties of libraries. There is also a tool (ocamlfind) for
+interpreting the META files, so that it is very easy to use libraries
+in programs and scripts.
+"""
+build: [
+ [
+ "./configure"
+ "-bindir"
+ bin
+ "-sitelib"
+ lib
+ "-mandir"
+ man
+ "-config"
+ "%{lib}%/findlib.conf"
+ "-no-custom"
+ "-no-camlp4" {!ocaml:preinstalled & ocaml:version >= "4.02.0"}
+ "-no-topfind" {ocaml:preinstalled}
+ ]
+ [make "all"]
+ [make "opt"] {ocaml:native}
+]
+install: [
+ [
+ "./configure"
+ "-bindir"
+ bin
+ "-sitelib"
+ lib
+ "-mandir"
+ man
+ "-config"
+ "%{lib}%/findlib.conf"
+ "-no-custom"
+ "-no-camlp4" {!ocaml:preinstalled & ocaml:version >= "4.02.0"}
+ "-no-topfind" {ocaml:preinstalled}
+ ]
+ [make "install"]
+ ["install" "-m" "0755" "ocaml-stub" "%{bin}%/ocaml"] {ocaml:preinstalled}
+]
+depends: [
+ "ocaml" {>= "4.00.0" & < "4.13"}
+ "conf-m4" {build}
+]
+extra-files: [
+ ["ocamlfind.install" "md5=06f2c282ab52d93aa6adeeadd82a2543"]
+ ["ocaml-stub" "md5=181f259c9e0bad9ef523e7d4abfdf87a"]
+]
+url {
+ src: "http://download.camlcity.org/download/findlib-1.8.1.tar.gz"
+ checksum: "md5=18ca650982c15536616dea0e422cbd8c"
+ mirrors: "http://download2.camlcity.org/download/findlib-1.8.1.tar.gz"
+}
+depopts: ["graphics"]
diff --git a/esy.lock/opam/zarith.1.12/opam b/esy.lock/opam/zarith.1.12/opam
new file mode 100644
index 0000000000000000000000000000000000000000..aae31e5031ef792d378f6bb9a36a10aafdd83b81
--- /dev/null
+++ b/esy.lock/opam/zarith.1.12/opam
@@ -0,0 +1,56 @@
+opam-version: "2.0"
+maintainer: "Xavier Leroy <xavier.leroy@inria.fr>"
+authors: [
+ "Antoine Miné"
+ "Xavier Leroy"
+ "Pascal Cuoq"
+]
+homepage: "https://github.com/ocaml/Zarith"
+bug-reports: "https://github.com/ocaml/Zarith/issues"
+dev-repo: "git+https://github.com/ocaml/Zarith.git"
+build: [
+ ["./configure"] {os != "openbsd" & os != "freebsd" & os != "macos"}
+ [
+ "sh"
+ "-exc"
+ "LDFLAGS=\"$LDFLAGS -L/usr/local/lib\" CFLAGS=\"$CFLAGS -I/usr/local/include\" ./configure"
+ ] {os = "openbsd" | os = "freebsd"}
+ [
+ "sh"
+ "-exc"
+ "LDFLAGS=\"$LDFLAGS -L/opt/local/lib -L/usr/local/lib\" CFLAGS=\"$CFLAGS -I/opt/local/include -I/usr/local/include\" ./configure"
+ ] {os = "macos" & os-distribution != "homebrew"}
+ [
+ "sh"
+ "-exc"
+ "LDFLAGS=\"$LDFLAGS -L/opt/local/lib -L/usr/local/lib\" CFLAGS=\"$CFLAGS -I/opt/local/include -I/usr/local/include\" ./configure"
+ ] {os = "macos" & os-distribution = "homebrew" & arch = "x86_64" }
+ [
+ "sh"
+ "-exc"
+ "LDFLAGS=\"$LDFLAGS -L/opt/homebrew/lib\" CFLAGS=\"$CFLAGS -I/opt/homebrew/include\" ./configure"
+ ] {os = "macos" & os-distribution = "homebrew" & arch = "arm64" }
+ [make]
+]
+install: [
+ [make "install"]
+]
+depends: [
+ "ocaml" {>= "4.04.0"}
+ "ocamlfind"
+ "conf-gmp"
+]
+synopsis:
+ "Implements arithmetic and logical operations over arbitrary-precision integers"
+description: """
+The Zarith library implements arithmetic and logical operations over
+arbitrary-precision integers. It uses GMP to efficiently implement
+arithmetic over big integers. Small integers are represented as Caml
+unboxed integers, for speed and space economy."""
+url {
+ src: "https://github.com/ocaml/Zarith/archive/release-1.12.tar.gz"
+ checksum: [
+ "md5=bf368f3d9e20b6b446d54681afc05a04"
+ "sha512=8075573ae65579a2606b37dd1b213032a07d220d28c733f9288ae80d36f8a2cc4d91632806df2503c130ea9658dc207ee3a64347c21aa53969050a208f5b2bb4"
+ ]
+}
diff --git a/esy.lock/overrides/d3dc108f8f9f64699d29c9c180f20b50/.gitignore b/esy.lock/overrides/d3dc108f8f9f64699d29c9c180f20b50/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..678a8a2c9fa7c24a418d97fd2c1b0e539d238cbd
--- /dev/null
+++ b/esy.lock/overrides/d3dc108f8f9f64699d29c9c180f20b50/.gitignore
@@ -0,0 +1,3 @@
+node_modules
+_esy
+*~
\ No newline at end of file
diff --git a/esy.lock/overrides/d3dc108f8f9f64699d29c9c180f20b50/package.json b/esy.lock/overrides/d3dc108f8f9f64699d29c9c180f20b50/package.json
new file mode 100644
index 0000000000000000000000000000000000000000..a2055c36eb3b62f79be266a2be6e0e0e602b2e00
--- /dev/null
+++ b/esy.lock/overrides/d3dc108f8f9f64699d29c9c180f20b50/package.json
@@ -0,0 +1,43 @@
+{
+ "name": "esy-gmp",
+ "version": "6.2.0",
+ "description": "GMP packaged for esy",
+ "source": "https://gmplib.org/download/gmp/gmp-6.2.1.tar.xz#0578d48607ec0e272177d175fd1807c30b00fdf2",
+ "override": {
+ "buildsInSource": true,
+ "build": [
+ "find ./ -exec touch -t 200905010101 {} +",
+ "./configure --enable-fat --prefix=#{self.install} #{os == 'windows' ? '--host x86_64-w64-mingw32' : ''} --with-pic",
+ "make -j4"
+ ],
+ "install": [
+ "make install"
+ ],
+ "exportedEnv": {
+ "LDFLAGS": {
+ "scope": "global",
+ "val": "-L#{self.lib} -lgmp"
+ },
+ "CPPFLAGS": {
+ "scope": "global",
+ "val": "-I#{self.install / 'include'}"
+ },
+ "LD_LIBRARY_PATH": {
+ "scope": "global",
+ "val": "#{self.lib}:$LD_LIBRARY_PATH"
+ },
+ "LIBRARY_PATH": {
+ "scope": "global",
+ "val": "#{self.lib}:$LIBRARY_PATH"
+ },
+ "CPATH": {
+ "scope": "global",
+ "val": "#{self.install / 'include'}:$CPATH"
+ },
+ "PKG_CONFIG_PATH": {
+ "val": "#{self.lib / 'pkgconfig' : $PKG_CONFIG_PATH}",
+ "scope": "global"
+ }
+ }
+ }
+}
diff --git a/esy.lock/overrides/d3dc108f8f9f64699d29c9c180f20b50/test/package.json b/esy.lock/overrides/d3dc108f8f9f64699d29c9c180f20b50/test/package.json
new file mode 100644
index 0000000000000000000000000000000000000000..c00c5752c02f10cda9de581d1700d96ed9a78ac5
--- /dev/null
+++ b/esy.lock/overrides/d3dc108f8f9f64699d29c9c180f20b50/test/package.json
@@ -0,0 +1,17 @@
+{
+ "name": "esy-gmp-test",
+ "description": "For manual testing only",
+ "version": "0.1.0",
+ "description": "GMP packaged for esy",
+ "license": "MIT",
+ "esy": {
+ "buildsInSource": true,
+ "build": [
+ "#{os == 'windows' ? 'x86_64-w64-mingw32-gcc': 'gcc'} $CFLAGS -o testinggmp test.c $LDFLAGS"
+ ],
+ "install": "cp testinggmp #{self.bin}"
+ },
+ "dependencies": {
+ "gmp": "esy-packages/esy-gmp"
+ }
+}
diff --git a/esy.lock/overrides/d3dc108f8f9f64699d29c9c180f20b50/test/test.c b/esy.lock/overrides/d3dc108f8f9f64699d29c9c180f20b50/test/test.c
new file mode 100644
index 0000000000000000000000000000000000000000..7162f628d0e6dff7f70af0f6161fbb9d4ee63daf
--- /dev/null
+++ b/esy.lock/overrides/d3dc108f8f9f64699d29c9c180f20b50/test/test.c
@@ -0,0 +1,14 @@
+#include <gmp.h>
+#include <stdlib.h>
+#include <stdio.h>
+
+int main() {
+ mpz_t i, j, k;
+ mpz_init_set_str (i, "1a", 16);
+ mpz_init (j);
+ mpz_init (k);
+ mpz_sqrtrem (j, k, i);
+ if (mpz_get_si (j) != 5 || mpz_get_si (k) != 1) abort();
+ printf("%s\n", "Works as expected");
+ return 0;
+}
diff --git a/esy.lock/overrides/opam__s__conf_gmp_opam__c__3_opam_override/package.json b/esy.lock/overrides/opam__s__conf_gmp_opam__c__3_opam_override/package.json
new file mode 100644
index 0000000000000000000000000000000000000000..d58aaec93fef1c057d3dd6b63ba6dbc51c727ca6
--- /dev/null
+++ b/esy.lock/overrides/opam__s__conf_gmp_opam__c__3_opam_override/package.json
@@ -0,0 +1,15 @@
+{
+ "build": [
+ [
+ "#{os == 'windows' ? 'x86_64-w64-mingw32-gcc' : 'cc'}",
+ "-c",
+ "${CFLAGS:--g}",
+ "$CPPFLAGS",
+ "$LDFLAGS",
+ "test.c"
+ ]
+ ],
+ "dependencies": {
+ "esy-gmp": "esy-packages/esy-gmp#e27cb300adfb0c0b320c273082c5affafcd225fa"
+ }
+}
diff --git a/esy.lock/overrides/opam__s__conf_m4_opam__c__1_opam_override/package.json b/esy.lock/overrides/opam__s__conf_m4_opam__c__1_opam_override/package.json
new file mode 100644
index 0000000000000000000000000000000000000000..ca6a373d8c959f831c3f7b55aafde44acef4fe09
--- /dev/null
+++ b/esy.lock/overrides/opam__s__conf_m4_opam__c__1_opam_override/package.json
@@ -0,0 +1,6 @@
+{
+ "build": "true",
+ "dependencies": {
+ "esy-m4": "esy-packages/esy-m4#c7cf0ac9221be2b1f9d90e83559ca08397a629e7"
+ }
+}
diff --git a/esy.lock/overrides/opam__s__num_opam__c__1.4_opam_override/files/num-1.4.patch b/esy.lock/overrides/opam__s__num_opam__c__1.4_opam_override/files/num-1.4.patch
new file mode 100644
index 0000000000000000000000000000000000000000..dad75fa57231eeaea65400ee029a269e0c2636e1
--- /dev/null
+++ b/esy.lock/overrides/opam__s__num_opam__c__1.4_opam_override/files/num-1.4.patch
@@ -0,0 +1,58 @@
+diff --git a/src/Makefile b/src/Makefile
+index 8ad0e2c..d41d63c 100644
+--- a/src/Makefile
++++ b/src/Makefile
+@@ -1,16 +1,16 @@
+-OCAMLC=ocamlc
+-OCAMLOPT=ocamlopt
+-OCAMLDEP=ocamldep
+-OCAMLMKLIB=ocamlmklib
+-OCAMLFIND=ocamlfind
++OCAMLC=$(shell which ocamlc)
++OCAMLOPT=$(shell which ocamlopt)
++OCAMLDEP=$(shell which ocamldep)
++OCAMLMKLIB=$(shell which ocamlmklib)
++OCAMLFIND=$(shell which ocamlfind)
+ INSTALL_DATA=install -m 644
+ INSTALL_DLL=install
+ INSTALL_DIR=install -d
+ STDLIBDIR=$(shell $(OCAMLC) -where)
+ DESTDIR ?=
+
+-include $(STDLIBDIR)/Makefile.config
+
++include $(STDLIBDIR)/Makefile.config
+ ifeq "$(filter i386 amd64 arm64 power,$(ARCH))" ""
+ # Unsupported architecture
+ BNG_ARCH=generic
+@@ -86,14 +86,14 @@ endif
+ VERSION=$(shell sed -ne 's/^ *version *: *"\([^"]*\)".*$$/\1/p' ../num.opam)
+
+ install:
+- $(INSTALL_DIR) $(DESTDIR)$(STDLIBDIR)
++ $(INSTALL_DIR) $(LIBDIR)
+ sed -e 's/%%VERSION%%/$(VERSION)/g' META.in > META
+ $(OCAMLFIND) install num META
+ rm -f META
+- $(INSTALL_DATA) $(TOINSTALL) $(DESTDIR)$(STDLIBDIR)
++ $(INSTALL_DATA) $(TOINSTALL) $(LIBDIR)
+ ifeq "$(SUPPORTS_SHARED_LIBRARIES)" "true"
+- $(INSTALL_DIR) $(DESTDIR)$(STDLIBDIR)/stublibs
+- $(INSTALL_DLL) $(TOINSTALL_STUBS) $(DESTDIR)$(STDLIBDIR)/stublibs
++ $(INSTALL_DIR) $(LIBDIR)/stublibs
++ $(INSTALL_DLL) $(TOINSTALL_STUBS) $(LIBDIR)/stublibs
+ endif
+
+ findlib-install:
+@@ -105,9 +105,9 @@ findlib-uninstall:
+ $(OCAMLFIND) remove num
+
+ uninstall: findlib-uninstall
+- cd $(DESTDIR)$(STDLIBDIR) && rm -f $(TOINSTALL)
++ cd $(LIBDIR) && rm -f $(TOINSTALL)
+ ifeq "$(SUPPORTS_SHARED_LIBRARIES)" "true"
+- cd $(DESTDIR)$(STDLIBDIR)/stublibs && rm -f $(TOINSTALL_STUBS)
++ cd $(LIBDIR)/stublibs && rm -f $(TOINSTALL_STUBS)
+ endif
+
+ clean:
diff --git a/esy.lock/overrides/opam__s__num_opam__c__1.4_opam_override/package.json b/esy.lock/overrides/opam__s__num_opam__c__1.4_opam_override/package.json
new file mode 100644
index 0000000000000000000000000000000000000000..4199a64edd626211f1a5222b6b53450e6078cda1
--- /dev/null
+++ b/esy.lock/overrides/opam__s__num_opam__c__1.4_opam_override/package.json
@@ -0,0 +1,25 @@
+{
+ "buildsInSource": true,
+ "build": [
+ [
+ "make"
+ ]
+ ],
+ "install": [
+ [
+ "make",
+ "LIBDIR=#{self.install / 'lib'}",
+ "findlib-install"
+ ]
+ ],
+ "exportedEnv": {
+ "CAML_LD_LIBRARY_PATH": {
+ "val": "#{self.install / 'lib' / 'num' : $CAML_LD_LIBRARY_PATH}",
+ "scope": "global"
+ }
+ },
+ "dependencies": {
+ "ocaml": "*",
+ "@opam/ocamlfind": "*"
+ }
+}
diff --git a/esy.lock/overrides/opam__s__ocamlfind_opam__c__1.8.1_opam_override/files/findlib-1.8.1.patch b/esy.lock/overrides/opam__s__ocamlfind_opam__c__1.8.1_opam_override/files/findlib-1.8.1.patch
new file mode 100644
index 0000000000000000000000000000000000000000..3e3ee5a24f1ba4bac4c1f5aaf53dd9ab5012b6d4
--- /dev/null
+++ b/esy.lock/overrides/opam__s__ocamlfind_opam__c__1.8.1_opam_override/files/findlib-1.8.1.patch
@@ -0,0 +1,471 @@
+--- ./Makefile
++++ ./Makefile
+@@ -57,16 +57,16 @@
+ cat findlib.conf.in | \
+ $(SH) tools/patch '@SITELIB@' '$(OCAML_SITELIB)' >findlib.conf
+ if ./tools/cmd_from_same_dir ocamlc; then \
+- echo 'ocamlc="ocamlc.opt"' >>findlib.conf; \
++ echo 'ocamlc="ocamlc.opt$(EXEC_SUFFIX)"' >>findlib.conf; \
+ fi
+ if ./tools/cmd_from_same_dir ocamlopt; then \
+- echo 'ocamlopt="ocamlopt.opt"' >>findlib.conf; \
++ echo 'ocamlopt="ocamlopt.opt$(EXEC_SUFFIX)"' >>findlib.conf; \
+ fi
+ if ./tools/cmd_from_same_dir ocamldep; then \
+- echo 'ocamldep="ocamldep.opt"' >>findlib.conf; \
++ echo 'ocamldep="ocamldep.opt$(EXEC_SUFFIX)"' >>findlib.conf; \
+ fi
+ if ./tools/cmd_from_same_dir ocamldoc; then \
+- echo 'ocamldoc="ocamldoc.opt"' >>findlib.conf; \
++ echo 'ocamldoc="ocamldoc.opt$(EXEC_SUFFIX)"' >>findlib.conf; \
+ fi
+
+ .PHONY: install-doc
+--- ./src/findlib/findlib_config.mlp
++++ ./src/findlib/findlib_config.mlp
+@@ -24,3 +24,5 @@
+ | "MacOS" -> "" (* don't know *)
+ | _ -> failwith "Unknown Sys.os_type"
+ ;;
++
++let exec_suffix = "@EXEC_SUFFIX@";;
+--- ./src/findlib/findlib.ml
++++ ./src/findlib/findlib.ml
+@@ -28,15 +28,20 @@
+ let conf_ldconf = ref "";;
+ let conf_ignore_dups_in = ref ([] : string list);;
+
+-let ocamlc_default = "ocamlc";;
+-let ocamlopt_default = "ocamlopt";;
+-let ocamlcp_default = "ocamlcp";;
+-let ocamloptp_default = "ocamloptp";;
+-let ocamlmklib_default = "ocamlmklib";;
+-let ocamlmktop_default = "ocamlmktop";;
+-let ocamldep_default = "ocamldep";;
+-let ocamlbrowser_default = "ocamlbrowser";;
+-let ocamldoc_default = "ocamldoc";;
++let add_exec str =
++ match Findlib_config.exec_suffix with
++ | "" -> str
++ | a -> str ^ a ;;
++let ocamlc_default = add_exec "ocamlc";;
++let ocamlopt_default = add_exec "ocamlopt";;
++let ocamlcp_default = add_exec "ocamlcp";;
++let ocamloptp_default = add_exec "ocamloptp";;
++let ocamlmklib_default = add_exec "ocamlmklib";;
++let ocamlmktop_default = add_exec "ocamlmktop";;
++let ocamldep_default = add_exec "ocamldep";;
++let ocamlbrowser_default = add_exec "ocamlbrowser";;
++let ocamldoc_default = add_exec "ocamldoc";;
++
+
+
+ let init_manually
+--- ./src/findlib/fl_package_base.ml
++++ ./src/findlib/fl_package_base.ml
+@@ -133,7 +133,15 @@
+ List.find (fun def -> def.def_var = "exists_if") p.package_defs in
+ let files = Fl_split.in_words def.def_value in
+ List.exists
+- (fun file -> Sys.file_exists (Filename.concat d' file))
++ (fun file ->
++ let fln = Filename.concat d' file in
++ let e = Sys.file_exists fln in
++ (* necessary for ppx executables *)
++ if e || Sys.os_type <> "Win32" || Filename.check_suffix fln ".exe" then
++ e
++ else
++ Sys.file_exists (fln ^ ".exe")
++ )
+ files
+ with Not_found -> true in
+
+--- ./src/findlib/fl_split.ml
++++ ./src/findlib/fl_split.ml
+@@ -126,10 +126,17 @@
+ | '/' | '\\' -> true
+ | _ -> false in
+ let norm_dir_win() =
+- if l >= 1 && s.[0] = '/' then
+- Buffer.add_char b '\\' else Buffer.add_char b s.[0];
+- if l >= 2 && s.[1] = '/' then
+- Buffer.add_char b '\\' else Buffer.add_char b s.[1];
++ if l >= 1 then (
++ if s.[0] = '/' then
++ Buffer.add_char b '\\'
++ else
++ Buffer.add_char b s.[0] ;
++ if l >= 2 then
++ if s.[1] = '/' then
++ Buffer.add_char b '\\'
++ else
++ Buffer.add_char b s.[1];
++ );
+ for k = 2 to l - 1 do
+ let c = s.[k] in
+ if is_slash c then (
+--- ./src/findlib/frontend.ml
++++ ./src/findlib/frontend.ml
+@@ -31,10 +31,18 @@
+ else
+ Sys_error (arg ^ ": " ^ Unix.error_message code)
+
++let is_win = Sys.os_type = "Win32"
++
++let () =
++ match Findlib_config.system with
++ | "win32" | "win64" | "mingw" | "cygwin" | "mingw64" | "cygwin64" ->
++ (try set_binary_mode_out stdout true with _ -> ());
++ (try set_binary_mode_out stderr true with _ -> ());
++ | _ -> ()
+
+ let slashify s =
+ match Findlib_config.system with
+- | "mingw" | "mingw64" | "cygwin" ->
++ | "win32" | "win64" | "mingw" | "cygwin" | "mingw64" | "cygwin64" ->
+ let b = Buffer.create 80 in
+ String.iter
+ (function
+@@ -49,7 +57,7 @@
+
+ let out_path ?(prefix="") s =
+ match Findlib_config.system with
+- | "mingw" | "mingw64" | "cygwin" ->
++ | "win32" | "win64" | "mingw" | "mingw64" | "cygwin" ->
+ let u = slashify s in
+ prefix ^
+ (if String.contains u ' ' then
+@@ -273,11 +281,9 @@
+
+
+ let identify_dir d =
+- match Sys.os_type with
+- | "Win32" ->
+- failwith "identify_dir" (* not available *)
+- | _ ->
+- let s = Unix.stat d in
++ if is_win then
++ failwith "identify_dir"; (* not available *)
++ let s = Unix.stat d in
+ (s.Unix.st_dev, s.Unix.st_ino)
+ ;;
+
+@@ -459,6 +465,96 @@
+ )
+ packages
+
++let rewrite_cmd s =
++ if s = "" || not is_win then
++ s
++ else
++ let s =
++ let l = String.length s in
++ let b = Buffer.create l in
++ for i = 0 to pred l do
++ match s.[i] with
++ | '/' -> Buffer.add_char b '\\'
++ | x -> Buffer.add_char b x
++ done;
++ Buffer.contents b
++ in
++ if (Filename.is_implicit s && String.contains s '\\' = false) ||
++ Filename.check_suffix (String.lowercase s) ".exe" then
++ s
++ else
++ let s' = s ^ ".exe" in
++ if Sys.file_exists s' then
++ s'
++ else
++ s
++
++let rewrite_cmd s =
++ if s = "" || not is_win then s else
++ let s =
++ let l = String.length s in
++ let b = Buffer.create l in
++ for i = 0 to pred l do
++ match s.[i] with
++ | '/' -> Buffer.add_char b '\\'
++ | x -> Buffer.add_char b x
++ done;
++ Buffer.contents b
++ in
++ if (Filename.is_implicit s && String.contains s '\\' = false) ||
++ Filename.check_suffix (String.lowercase s) ".exe" then
++ s
++ else
++ let s' = s ^ ".exe" in
++ if Sys.file_exists s' then
++ s'
++ else
++ s
++
++let rewrite_pp cmd =
++ if not is_win then cmd else
++ let module T = struct exception Keep end in
++ let is_whitespace = function
++ | ' ' | '\011' | '\012' | '\n' | '\r' | '\t' -> true
++ | _ -> false in
++ (* characters that triggers special behaviour (cmd.exe, not unix shell) *)
++ let is_unsafe_char = function
++ | '(' | ')' | '%' | '!' | '^' | '<' | '>' | '&' -> true
++ | _ -> false in
++ let len = String.length cmd in
++ let buf = Buffer.create (len + 4) in
++ let buf_cmd = Buffer.create len in
++ let rec iter_ws i =
++ if i >= len then () else
++ let cur = cmd.[i] in
++ if is_whitespace cur then (
++ Buffer.add_char buf cur;
++ iter_ws (succ i)
++ )
++ else
++ iter_cmd i
++ and iter_cmd i =
++ if i >= len then add_buf_cmd () else
++ let cur = cmd.[i] in
++ if is_unsafe_char cur || cur = '"' || cur = '\'' then
++ raise T.Keep;
++ if is_whitespace cur then (
++ add_buf_cmd ();
++ Buffer.add_substring buf cmd i (len - i)
++ )
++ else (
++ Buffer.add_char buf_cmd cur;
++ iter_cmd (succ i)
++ )
++ and add_buf_cmd () =
++ if Buffer.length buf_cmd > 0 then
++ Buffer.add_string buf (rewrite_cmd (Buffer.contents buf_cmd))
++ in
++ try
++ iter_ws 0;
++ Buffer.contents buf
++ with
++ | T.Keep -> cmd
+
+ let process_pp_spec syntax_preds packages pp_opts =
+ (* Returns: pp_command *)
+@@ -549,7 +645,7 @@
+ None -> []
+ | Some cmd ->
+ ["-pp";
+- cmd ^ " " ^
++ (rewrite_cmd cmd) ^ " " ^
+ String.concat " " (List.map Filename.quote pp_i_options) ^ " " ^
+ String.concat " " (List.map Filename.quote pp_archives) ^ " " ^
+ String.concat " " (List.map Filename.quote pp_opts)]
+@@ -625,9 +721,11 @@
+ in
+ try
+ let preprocessor =
++ rewrite_cmd (
+ resolve_path
+ ~base ~explicit:true
+- (package_property predicates pname "ppx") in
++ (package_property predicates pname "ppx") )
++ in
+ ["-ppx"; String.concat " " (preprocessor :: options)]
+ with Not_found -> []
+ )
+@@ -895,6 +993,14 @@
+ switch (e.g. -L<path> instead of -L <path>)
+ *)
+
++(* We may need to remove files on which we do not have complete control.
++ On Windows, removing a read-only file fails so try to change the
++ mode of the file first. *)
++let remove_file fname =
++ try Sys.remove fname
++ with Sys_error _ when is_win ->
++ (try Unix.chmod fname 0o666 with Unix.Unix_error _ -> ());
++ Sys.remove fname
+
+ let ocamlc which () =
+
+@@ -1022,9 +1128,12 @@
+
+ "-intf",
+ Arg.String (fun s -> pass_files := !pass_files @ [ Intf(slashify s) ]);
+-
++
+ "-pp",
+- Arg.String (fun s -> pp_specified := true; add_spec_fn "-pp" s);
++ Arg.String (fun s -> pp_specified := true; add_spec_fn "-pp" (rewrite_pp s));
++
++ "-ppx",
++ Arg.String (fun s -> add_spec_fn "-ppx" (rewrite_pp s));
+
+ "-thread",
+ Arg.Unit (fun _ -> threads := threads_default);
+@@ -1237,7 +1346,7 @@
+ with
+ any ->
+ close_out initl;
+- Sys.remove initl_file_name;
++ remove_file initl_file_name;
+ raise any
+ end;
+
+@@ -1245,9 +1354,9 @@
+ at_exit
+ (fun () ->
+ let tr f x = try f x with _ -> () in
+- tr Sys.remove initl_file_name;
+- tr Sys.remove (Filename.chop_extension initl_file_name ^ ".cmi");
+- tr Sys.remove (Filename.chop_extension initl_file_name ^ ".cmo");
++ tr remove_file initl_file_name;
++ tr remove_file (Filename.chop_extension initl_file_name ^ ".cmi");
++ tr remove_file (Filename.chop_extension initl_file_name ^ ".cmo");
+ );
+
+ let exclude_list = [ stdlibdir; threads_dir; vmthreads_dir ] in
+@@ -1493,7 +1602,9 @@
+ [ "-v", Arg.Unit (fun () -> verbose := Verbose);
+ "-pp", Arg.String (fun s ->
+ pp_specified := true;
+- options := !options @ ["-pp"; s]);
++ options := !options @ ["-pp"; rewrite_pp s]);
++ "-ppx", Arg.String (fun s ->
++ options := !options @ ["-ppx"; rewrite_pp s]);
+ ]
+ )
+ )
+@@ -1672,7 +1783,9 @@
+ Arg.String (fun s -> add_spec_fn "-I" (slashify (resolve_path s)));
+
+ "-pp", Arg.String (fun s -> pp_specified := true;
+- add_spec_fn "-pp" s);
++ add_spec_fn "-pp" (rewrite_pp s));
++ "-ppx", Arg.String (fun s -> add_spec_fn "-ppx" (rewrite_pp s));
++
+ ]
+ )
+ )
+@@ -1830,7 +1943,10 @@
+ output_string ch_out append;
+ close_out ch_out;
+ close_in ch_in;
+- Unix.utimes outpath s.Unix.st_mtime s.Unix.st_mtime;
++ (try Unix.utimes outpath s.Unix.st_mtime s.Unix.st_mtime
++ with Unix.Unix_error(e,_,_) ->
++ prerr_endline("Warning: setting utimes for " ^ outpath
++ ^ ": " ^ Unix.error_message e));
+
+ prerr_endline("Installed " ^ outpath);
+ with
+@@ -1882,6 +1998,8 @@
+ Unix.openfile (Filename.concat dir owner_file) [Unix.O_RDONLY] 0 in
+ let f =
+ Unix.in_channel_of_descr fd in
++ if is_win then
++ set_binary_mode_in f false;
+ try
+ let line = input_line f in
+ let is_my_file = (line = pkg) in
+@@ -2208,7 +2326,7 @@
+ let lines = read_ldconf !ldconf in
+ let dlldir_norm = Fl_split.norm_dir dlldir in
+ let dlldir_norm_lc = string_lowercase_ascii dlldir_norm in
+- let ci_filesys = (Sys.os_type = "Win32") in
++ let ci_filesys = is_win in
+ let check_dir d =
+ let d' = Fl_split.norm_dir d in
+ (d' = dlldir_norm) ||
+@@ -2356,7 +2474,7 @@
+ List.iter
+ (fun file ->
+ let absfile = Filename.concat dlldir file in
+- Sys.remove absfile;
++ remove_file absfile;
+ prerr_endline ("Removed " ^ absfile)
+ )
+ dll_files
+@@ -2365,7 +2483,7 @@
+ (* Remove the files from the package directory: *)
+ if Sys.file_exists pkgdir then begin
+ let files = Sys.readdir pkgdir in
+- Array.iter (fun f -> Sys.remove (Filename.concat pkgdir f)) files;
++ Array.iter (fun f -> remove_file (Filename.concat pkgdir f)) files;
+ Unix.rmdir pkgdir;
+ prerr_endline ("Removed " ^ pkgdir)
+ end
+@@ -2415,7 +2533,9 @@
+
+
+ let print_configuration() =
++ let sl = slashify in
+ let dir s =
++ let s = sl s in
+ if Sys.file_exists s then
+ s
+ else
+@@ -2453,27 +2573,27 @@
+ if md = "" then "the corresponding package directories" else dir md
+ );
+ Printf.printf "The standard library is assumed to reside in:\n %s\n"
+- (Findlib.ocaml_stdlib());
++ (sl (Findlib.ocaml_stdlib()));
+ Printf.printf "The ld.conf file can be found here:\n %s\n"
+- (Findlib.ocaml_ldconf());
++ (sl (Findlib.ocaml_ldconf()));
+ flush stdout
+ | Some "conf" ->
+- print_endline (Findlib.config_file())
++ print_endline (sl (Findlib.config_file()))
+ | Some "path" ->
+- List.iter print_endline (Findlib.search_path())
++ List.iter ( fun x -> print_endline (sl x)) (Findlib.search_path())
+ | Some "destdir" ->
+- print_endline (Findlib.default_location())
++ print_endline ( sl (Findlib.default_location()))
+ | Some "metadir" ->
+- print_endline (Findlib.meta_directory())
++ print_endline ( sl (Findlib.meta_directory()))
+ | Some "metapath" ->
+ let mdir = Findlib.meta_directory() in
+ let ddir = Findlib.default_location() in
+- print_endline
+- (if mdir <> "" then mdir ^ "/META.%s" else ddir ^ "/%s/META")
++ print_endline ( sl
++ (if mdir <> "" then mdir ^ "/META.%s" else ddir ^ "/%s/META"))
+ | Some "stdlib" ->
+- print_endline (Findlib.ocaml_stdlib())
++ print_endline ( sl (Findlib.ocaml_stdlib()))
+ | Some "ldconf" ->
+- print_endline (Findlib.ocaml_ldconf())
++ print_endline ( sl (Findlib.ocaml_ldconf()))
+ | _ ->
+ assert false
+ ;;
+@@ -2481,7 +2601,7 @@
+
+ let ocamlcall pkg cmd =
+ let dir = package_directory pkg in
+- let path = Filename.concat dir cmd in
++ let path = rewrite_cmd (Filename.concat dir cmd) in
+ begin
+ try Unix.access path [ Unix.X_OK ]
+ with
+@@ -2647,6 +2767,10 @@
+ | Sys_error f ->
+ prerr_endline ("ocamlfind: " ^ f);
+ exit 2
++ | Unix.Unix_error (e, fn, f) ->
++ prerr_endline ("ocamlfind: " ^ fn ^ " " ^ f
++ ^ ": " ^ Unix.error_message e);
++ exit 2
+ | Findlib.No_such_package(pkg,info) ->
+ prerr_endline ("ocamlfind: Package `" ^ pkg ^ "' not found" ^
+ (if info <> "" then " - " ^ info else ""));
+--- ./src/findlib/Makefile
++++ ./src/findlib/Makefile
+@@ -90,6 +90,7 @@
+ cat findlib_config.mlp | \
+ $(SH) $(TOP)/tools/patch '@CONFIGFILE@' '$(OCAMLFIND_CONF)' | \
+ $(SH) $(TOP)/tools/patch '@STDLIB@' '$(OCAML_CORE_STDLIB)' | \
++ $(SH) $(TOP)/tools/patch '@EXEC_SUFFIX@' '$(EXEC_SUFFIX)' | \
+ sed -e 's;@AUTOLINK@;$(OCAML_AUTOLINK);g' \
+ -e 's;@SYSTEM@;$(SYSTEM);g' \
+ >findlib_config.ml
diff --git a/esy.lock/overrides/opam__s__ocamlfind_opam__c__1.8.1_opam_override/package.json b/esy.lock/overrides/opam__s__ocamlfind_opam__c__1.8.1_opam_override/package.json
new file mode 100644
index 0000000000000000000000000000000000000000..9314f870880865a95d7dddaabda53b89b5a0fa94
--- /dev/null
+++ b/esy.lock/overrides/opam__s__ocamlfind_opam__c__1.8.1_opam_override/package.json
@@ -0,0 +1,61 @@
+{
+ "build": [
+ [
+ "bash",
+ "-c",
+ "#{os == 'windows' ? 'patch -p1 < findlib-1.8.1.patch' : 'true'}"
+ ],
+ [
+ "./configure",
+ "-bindir",
+ "#{self.bin}",
+ "-sitelib",
+ "#{self.lib}",
+ "-mandir",
+ "#{self.man}",
+ "-config",
+ "#{self.lib}/findlib.conf",
+ "-no-custom",
+ "-no-topfind"
+ ],
+ [
+ "make",
+ "all"
+ ],
+ [
+ "make",
+ "opt"
+ ]
+ ],
+ "install": [
+ [
+ "make",
+ "install"
+ ],
+ [
+ "install",
+ "-m",
+ "0755",
+ "ocaml-stub",
+ "#{self.bin}/ocaml"
+ ],
+ [
+ "mkdir",
+ "-p",
+ "#{self.toplevel}"
+ ],
+ [
+ "install",
+ "-m",
+ "0644",
+ "src/findlib/topfind",
+ "#{self.toplevel}/topfind"
+ ]
+ ],
+ "exportedEnv": {
+ "OCAML_TOPLEVEL_PATH": {
+ "val": "#{self.toplevel}",
+ "scope": "global"
+ }
+ }
+}
diff --git a/esy.lock/overrides/opam__s__zarith_opam__c__1.12_opam_override/package.json b/esy.lock/overrides/opam__s__zarith_opam__c__1.12_opam_override/package.json
new file mode 100644
index 0000000000000000000000000000000000000000..5500d0c94174d1fcfaa6e066ce69c751a00d3c98
--- /dev/null
+++ b/esy.lock/overrides/opam__s__zarith_opam__c__1.12_opam_override/package.json
@@ -0,0 +1,19 @@
+{
+ "build": [
+ "#{os == 'windows' ? 'env CC=x86_64-w64-mingw32-gcc ': ''}./configure",
+ "make"
+ ],
+ "install": [
+ "make install"
+ ],
+ "exportedEnv": {
+ "CAML_LD_LIBRARY_PATH": {
+ "val": "#{self.lib / 'zarith' : $CAML_LD_LIBRARY_PATH}",
+ "scope": "global"
+ }
+ },
+ "dependencies": {
+ "ocaml": "*",
+ "@opam/conf-gmp": "*"
+ }
+}
diff --git a/package.json b/package.json
new file mode 100644
index 0000000000000000000000000000000000000000..7cbec8fc4bc3e7429c3ccdacdff3beb80ededb0d
--- /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" ]
+ ]
+ }
+ }
+ }
+}