@@ -12,6 +12,7 @@ describes this development.
1212
1313## Installation
1414
15+ The plugin is available as an ` opam ` package. To install the version corresponding to this branch, use:
1516```
1617opam switch create coq-malfunction --packages="ocaml-variants.4.14.1+options,ocaml-option-flambda"
1718eval $(opam env --switch=coq-malfunction)
@@ -20,8 +21,38 @@ opam pin -n -y "https://github.com/MetaRocq/metarocq.git#v1.3.2-8.19"
2021opam pin -n -y "https://github.com/stedolan/malfunction.git#master"
2122opam install . --deps-only
2223make -j 4
24+ make install
2325```
2426
27+ ## Development
28+
29+ One can use ` nix ` to develop. After a successful [ installation] ( https://nixos.org/download/ ) of ` nix ` and ` cachix `
30+ (see [ instructions] ( https://metarocq.cachix.org ) ) use:
31+
32+ ``` bash
33+ nix-shell
34+ ```
35+
36+ This enters a shell environment with all the dependencies to build the plugin available.
37+ To check which libraries and versions are installed in the nix environment, use:
38+ ``` bash
39+ nixEnv
40+ ```
41+
42+ See ` nixHelp ` for the available commands in the ` nix-shell ` .
43+ To open the VSCode IDE to work on the Rocq files, call, under the ` nix-shell ` :
44+
45+ ``` bash
46+ code .vscode/rocq-verified-extraction.code-workspace
47+ ```
48+
49+ This workspace contains the necessary include flags to process the ` .v ` files.
50+ Note, when starting terminals from ` VSCode ` or elsewhere, you need to re-enter ` nix-shell ` to
51+ use the right environment for calling e.g. ` make ` .
52+
53+ To test the build as is done in the CI, you can (without even going under the ` nix-shell ` ), run ` nix-build ` at the root.
54+ To test with specific versions of dependencies, customize ` .nix/config.nix ` .
55+
2556## Usage
2657
2758After ` From VerifiedExtraction Require Import Extraction. `
0 commit comments