flake+opam-nix

.github/workflows/ci.yml

@@ -57,7 +57,7 @@ jobs:
         authToken: '${{ secrets.CACHIX_WRITE_TOKEN }}'
     - name: Build and cache EasyCrypt and dependencies
       run: |
-        nix-build
+        make nix-build-with-provers
 
   check:
     name: Check EasyCrypt Libraries

.gitignore

@@ -4,6 +4,7 @@
 *.pyo
 
 /_build
+/result
 /etc
 /theories/attic
 
@@ -19,3 +20,4 @@
 
 .merlin
 *.install
+*.log

Makefile

@@ -13,13 +13,15 @@ CHECK     += --bin=./ec.native --bin-args="$(ECARGS)"
 CHECK     += --bin-args="$(ECPROVERS:%=-p %)"
 CHECK     += --timeout="$(ECTOUT)" --jobs="$(ECJOBS)"
 CHECK     += $(ECEXTRA) config/tests.config
+NIX       ?= nix --extra-experimental-features "nix-command flakes"
 
 # --------------------------------------------------------------------
 UNAME_P = $(shell uname -p)
 UNAME_S = $(shell uname -s)
 
 # --------------------------------------------------------------------
 .PHONY: default build byte native tests check examples
+.PHONY: nix-build nix-build-with-provers nix-develop
 .PHONY: clean install uninstall
 
 default: build
@@ -51,6 +53,15 @@ examples: build
 check: unit stdlib examples
 	@true
 
+nix-build:
+	$(NIX) build
+
+nix-build-with-provers:
+	$(NIX) build .#with_provers
+
+nix-develop:
+	$(NIX) develop
+
 clean:
 	rm -f ec.native && $(DUNE) clean
 	find theories examples -name '*.eco' -exec rm '{}' ';'

README.md

@@ -183,17 +183,29 @@ following [these instructions](https://nixos.org/manual/nix/stable/#chap-install
 Then, at the root of the EasyCrypt source tree, type:
 
     ```
-    $> nix-shell
+    $> make nix-build
     ```
-    
-These should install all the required dependencies. From there, simply
-run:
+
+Once completed, you will find the EasyCrypt binary in `result/bin`.
+
+You can also run
 
     ```
-    $> make
+    $> make nix-build-with-provers
     ```
-    
-to compile EasyCrypt.
+
+to install EasyCrypt along with a set of provers.
+
+
+For getting a development environment, you can run:
+
+    ```
+    $> make nix-develop
+    ```
+
+These will install all the required dependencies, a set of provers and
+will then drop you into a shell. From there, simply run `make` to
+compile EasyCrypt.
 
 Note on Prover Versions
 --------------------------------------------------------------------