aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/nix
diff options
context:
space:
mode:
authorVincent Laporte2018-11-23 09:29:04 +0000
committerVincent Laporte2018-11-26 08:44:07 +0000
commit9335cc09090bfba1f81f81c35e0acb324bf6cba5 (patch)
tree7d61e6acbc084b16682c825cd7ac3ffbb9d42439 /dev/ci/nix
parent51ce6bf10be48a479d80978d6c1a517336aa3458 (diff)
[nix-ci] Add a README in dev/ci/nix
Diffstat (limited to 'dev/ci/nix')
-rw-r--r--dev/ci/nix/README.md19
1 files changed, 19 insertions, 0 deletions
diff --git a/dev/ci/nix/README.md b/dev/ci/nix/README.md
new file mode 100644
index 0000000000..1685b084e9
--- /dev/null
+++ b/dev/ci/nix/README.md
@@ -0,0 +1,19 @@
+# Working on third-party developments with *this* version of Coq
+
+Aim: getting an environment suitable for working on a third-party development
+using the current version of Coq (i.e., built from the current state of this
+repository).
+
+Dive into such an environment, for the project `example` by running, from the
+root of this repository:
+
+ ./dev/ci/nix/shell example
+
+This will build Coq and the other dependencies of the `example` project, then
+open a shell with all these dependencies available (e.g., `coqtop` is in path).
+
+Additionally, three environment variables are set, to abstract over the
+build-system of that project: `configure`, `make`, and `clean`. Therefore, after
+changing the working directory to the root of the sources of that project, the
+contents of these variables can be evaluated to respectively set-up, build, and
+clean the project.