Nix setup (#250)

Author: 4ever2

.github/coq-concert.opam.locked

@@ -34,7 +34,7 @@ pin-depends: [
   ["coq-metacoq-erasure.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
 ]
 build: [
-  [make]
+  [make "core"]
   [make "examples"] {with-test}
   [make "html"] {with-doc}
 ]

.github/workflows/build.yml

@@ -8,6 +8,7 @@ on:
     - '**.md'
     - '**.gitignore'
     - '**.opam'
+    - '**.nix'
     - '**.editorconfig'
     - 'LICENSE'
     - 'papers/**'
@@ -17,6 +18,7 @@ on:
     - '**.md'
     - '**.gitignore'
     - '**.opam'
+    - '**.nix'
     - '**.editorconfig'
     - 'LICENSE'
     - 'papers/**'

.github/workflows/nix-action-8.19.yml

@@ -2,6 +2,9 @@
 *.tmp
 .DS_Store
 
+# Nix outputs
+result
+
 # dpd-graph outputs
 *.dpd
 *.dot

.gitignore

@@ -0,0 +1,25 @@
+{
+  ## DO NOT CHANGE THIS
+  format = "1.0.0";
+  ## unless you made an automated or manual update
+  ## to another supported format.
+
+  attribute = "ConCert";
+
+  default-bundle = "8.19";
+
+  bundles."8.19" = {
+    coqPackages.coq.override.version = "8.19";
+    coqPackages.metacoq.override.version = "coq-8.19";
+    coqPackages.stdpp.override.version = "1.10.0";
+    coqPackages.QuickChick.override.version = "2.0.4";
+    coqPackages.RustExtraction.override.version = "0.1.0";
+    coqPackages.ElmExtraction.override.version = "0.1.0";
+  };
+
+  cachix.coq = {};
+  cachix.coq-community = {};
+  cachix.metacoq = {};
+
+  cachix.au-cobra.authToken = "CACHIX_AUTH_TOKEN";
+}

.nix/config.nix

@@ -0,0 +1 @@
+"a24e6f4fb01d4ca0811dc8d16246cfe36b37ac52"

.nix/coq-nix-toolbox.nix

@@ -0,0 +1,40 @@
+{ lib, mkCoqDerivation, which, coq
+  , metacoq, bignums, QuickChick, stdpp, RustExtraction, ElmExtraction
+  , version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "ConCert";
+  repo = "ConCert";
+  owner = "AU-COBRA";
+  domain = "github.com";
+
+  inherit version;
+  ## The `defaultVersion` attribute is important for nixpkgs but can be kept unchanged
+  ## for local usage since it will be ignored locally if
+  ## - this derivation corresponds to the main attribute,
+  ## - or its version is overridden (by a branch, PR, url or path) in `.nix/config.nix`.
+  defaultVersion = with versions; switch coq.coq-version [
+    ## Example of possible dependencies
+    # { case = range "8.13" "8.14"; out = "1.2.0"; }
+    ## other predicates are `isLe v`, `isLt v`, `isGe v`, `isGt v`, `isEq v` etc
+  ] null;
+
+  ## Declare existing releases
+  ## leave sha256 empty at first and then copy paste
+  ## the resulting sha given by the error message
+  # release."1.1.1".sha256 = "";
+  ## if the tag is not exactly the version number you can amend like this
+  # release."1.1.1".rev = "v1.1.1";
+  ## if a consistent scheme gives the tag from the release number, you can do like this:
+  # releaseRev = v: "v${v}";
+
+  propagatedBuildInputs = [ coq.ocamlPackages.findlib metacoq bignums QuickChick stdpp RustExtraction ElmExtraction ];
+
+  postPatch = ''patchShebangs ./extraction/process-extraction-examples.sh'';
+
+  meta = {
+    description = "A framework for smart contract verification in Coq";
+    maintainers = with maintainers; [ _4ever2 ];
+    license = licenses.mit;
+  };
+}

.nix/coq-overlays/ConCert/default.nix

@@ -1,6 +1,9 @@
-all: utils execution embedding extraction
+all: utils execution embedding extraction examples
 .PHONY: all
 
+core: utils execution embedding extraction
+.PHONY: core
+
 utils:
 	+make -C utils
 .PHONY: utils

Makefile

@@ -40,7 +40,7 @@ pin-depends: [
 ]
 
 build: [
-  [make]
+  [make "core"]
   [make "examples"] {with-test}
   [make "html"] {with-doc}
 ]

coq-concert.opam

@@ -0,0 +1,12 @@
+{ config ? {}, withEmacs ? false, print-env ? false, do-nothing ? false,
+  update-nixpkgs ? false, ci-matrix ? false,
+  override ? {}, ocaml-override ? {}, global-override ? {},
+  bundle ? null, job ? null, inNixShell ? null, src ? ./.,
+}@args:
+let auto = fetchGit {
+  url = "https://github.com/coq-community/coq-nix-toolbox.git";
+  ref = "master";
+  rev = import .nix/coq-nix-toolbox.nix;
+};
+in
+import auto ({inherit src;} // args)