aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-09-06 21:31:09 +0200
committerEmilio Jesus Gallego Arias2018-09-06 21:34:33 +0200
commitc8cc7a6901edf80638e7fcb4a9d22173e9523c96 (patch)
treed567b540b601b26a393ebc3d7404b7cd2f74dcf2
parent51197c3b8b5a6f30397f0263e2e2f4461519c66e (diff)
[dune] [doc] Document `dune utop $lib`
-rw-r--r--.github/CODEOWNERS1
-rw-r--r--.ocamlinit1
-rw-r--r--dev/doc/build-system.dune.md11
3 files changed, 13 insertions, 0 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 65c971ce76..274a0001b1 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -258,6 +258,7 @@
########## Dune ##########
+/.ocamlinit @ejgallego
/Makefile.dune @ejgallego
/tools/coq_dune* @ejgallego
/dune* @ejgallego
diff --git a/.ocamlinit b/.ocamlinit
new file mode 100644
index 0000000000..3771334e12
--- /dev/null
+++ b/.ocamlinit
@@ -0,0 +1 @@
+#rectypes;;
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 0b3e414513..85aaf317ef 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -39,6 +39,17 @@ In order to build a single package, you can do `dune build
$PACKAGE.install`. Dune also provides targets for documentation and
testing, see below.
+## Developer shell
+
+You can create a developer shell with `dune utop $library`, where
+`$library` can be any directory in the current workspace. For example,
+`dune utop engine` or `dune utop plugins/ltac` will launch `utop` with
+the right libraries already loaded.
+
+Note that you must invoke the `#rectypes;;` toplevel flag in order to
+use Coq libraries. The provided `.ocamlinit` file does this
+automatically.
+
## Compositionality, developer and release modes.
By default [in "developer mode"], Dune will compose all the packages