From 20c0e621a81c4751a7cfee225c57559831472332 Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Wed, 10 Jul 2024 15:07:05 +0100 Subject: [PATCH 1/8] update the Jasmin compiler --- scripts/ci/config/jasmin | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/ci/config/jasmin b/scripts/ci/config/jasmin index 670eaad6..c3c583fd 100644 --- a/scripts/ci/config/jasmin +++ b/scripts/ci/config/jasmin @@ -1 +1 @@ -7be631a8da1dc3f7c966681028138ae56d8e4610 +e4640e7dcdb01d1ba63617a5d78456e1209d699c From a42d4e095171d17e2a9ee7564e10832b68395951 Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Wed, 10 Jul 2024 15:07:05 +0100 Subject: [PATCH 2/8] update the Jasmin compiler 2 --- flake.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/flake.nix b/flake.nix index 68f67a54..006f8772 100644 --- a/flake.nix +++ b/flake.nix @@ -5,7 +5,7 @@ nixpkgs.url = "nixpkgs/release-23.11"; easycrypt.url = "github:EasyCrypt/easycrypt/4201fddc14b81d2a69a33f034c9c7db4dfd58d0e"; jasmin = { - url = "github:jasmin-lang/jasmin/e84c0c59b4f4e005f2be4de5fdfbcaf1e3e2f975"; + url = "github:jasmin-lang/jasmin/e4640e7dcdb01d1ba63617a5d78456e1209d699c"; flake = false; }; }; From de4f8391319cf7bcb47881578e800e60d315579c Mon Sep 17 00:00:00 2001 From: Tiago Oliveira Date: Wed, 10 Jul 2024 15:48:39 +0100 Subject: [PATCH 3/8] update the Jasmin compiler 3 --- flake.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/flake.nix b/flake.nix index 006f8772..ff5c2d5a 100644 --- a/flake.nix +++ b/flake.nix @@ -2,7 +2,7 @@ description = "Libjade"; inputs = { - nixpkgs.url = "nixpkgs/release-23.11"; + nixpkgs.url = "nixpkgs/release-24.05"; easycrypt.url = "github:EasyCrypt/easycrypt/4201fddc14b81d2a69a33f034c9c7db4dfd58d0e"; jasmin = { url = "github:jasmin-lang/jasmin/e4640e7dcdb01d1ba63617a5d78456e1209d699c"; From 2e61fc2c194e1bb9da6286337bd5072199d0b70c Mon Sep 17 00:00:00 2001 From: Aaron Kaiser Date: Wed, 10 Jul 2024 17:08:13 +0200 Subject: [PATCH 4/8] Update flake.lock --- flake.lock | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/flake.lock b/flake.lock index 53c68883..c5fb6d32 100644 --- a/flake.lock +++ b/flake.lock @@ -81,17 +81,17 @@ "jasmin": { "flake": false, "locked": { - "lastModified": 1712566927, - "narHash": "sha256-sRegD+ecNeKUf0STO/2WRST2+CoEqdBdCAd478/zI8o=", + "lastModified": 1720533296, + "narHash": "sha256-GKqk5pYrq9oz7njTpaASlA5JVIcf6RQYcsSc6X/y6NA=", "owner": "jasmin-lang", "repo": "jasmin", - "rev": "e84c0c59b4f4e005f2be4de5fdfbcaf1e3e2f975", + "rev": "e4640e7dcdb01d1ba63617a5d78456e1209d699c", "type": "github" }, "original": { "owner": "jasmin-lang", "repo": "jasmin", - "rev": "e84c0c59b4f4e005f2be4de5fdfbcaf1e3e2f975", + "rev": "e4640e7dcdb01d1ba63617a5d78456e1209d699c", "type": "github" } }, @@ -129,16 +129,16 @@ }, "nixpkgs_2": { "locked": { - "lastModified": 1713362983, - "narHash": "sha256-glRKaESbOIEQRU5aZZu/T18rNaqNnBKDVag1EsfylpQ=", + "lastModified": 1720621723, + "narHash": "sha256-cZKWxDhaoEZZa6VCXOGWA5A6OEqtzZ2O9veKW5XYjW4=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "8bc628c7d96aa5cf767bad443091f39aed0cbad0", + "rev": "89bc15e14e6d045136baf82b388af2986eaad1e9", "type": "github" }, "original": { "id": "nixpkgs", - "ref": "release-23.11", + "ref": "release-24.05", "type": "indirect" } }, From e309dd047d43ef9c921dc3ec5e2ac4d2232134d7 Mon Sep 17 00:00:00 2001 From: Aaron Kaiser Date: Wed, 10 Jul 2024 17:29:25 +0200 Subject: [PATCH 5/8] Refactor flake to build for differente architectures --- flake.lock | 21 ++++++++++++++++++ flake.nix | 64 +++++++++++++++++++++++++++++------------------------- 2 files changed, 55 insertions(+), 30 deletions(-) diff --git a/flake.lock b/flake.lock index c5fb6d32..04219d9b 100644 --- a/flake.lock +++ b/flake.lock @@ -45,6 +45,26 @@ "type": "github" } }, + "flake-parts": { + "inputs": { + "nixpkgs-lib": [ + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1719994518, + "narHash": "sha256-pQMhCCHyQGRzdfAkdJ4cIWiw+JNuWsTX7f0ZYSyz0VY=", + "owner": "hercules-ci", + "repo": "flake-parts", + "rev": "9227223f6d922fee3c7b190b2cc238a99527bbb7", + "type": "github" + }, + "original": { + "owner": "hercules-ci", + "repo": "flake-parts", + "type": "github" + } + }, "flake-utils": { "inputs": { "systems": "systems" @@ -274,6 +294,7 @@ "root": { "inputs": { "easycrypt": "easycrypt", + "flake-parts": "flake-parts", "jasmin": "jasmin", "nixpkgs": "nixpkgs_2" } diff --git a/flake.nix b/flake.nix index ff5c2d5a..c8a06f8f 100644 --- a/flake.nix +++ b/flake.nix @@ -3,42 +3,46 @@ inputs = { nixpkgs.url = "nixpkgs/release-24.05"; + easycrypt.url = "github:EasyCrypt/easycrypt/4201fddc14b81d2a69a33f034c9c7db4dfd58d0e"; jasmin = { url = "github:jasmin-lang/jasmin/e4640e7dcdb01d1ba63617a5d78456e1209d699c"; flake = false; }; + + flake-parts = { + url = "github:hercules-ci/flake-parts"; + inputs.nixpkgs-lib.follows = "nixpkgs"; + }; }; - outputs = { self, nixpkgs, easycrypt, jasmin, ... }: - let - system = "x86_64-linux"; - pkgs = nixpkgs.legacyPackages.${system}; - jasminc = pkgs.callPackage "${jasmin}/default.nix" { inherit pkgs; }; - ec = easycrypt.packages.${system}.default; - in - { - packages.${system}.default = pkgs.callPackage ./default.nix { inherit pkgs jasminc; }; - - devShells.${system}.default = pkgs.mkShell { - name = "libjade"; - src = self.packages.${system}.default.src; - - packages = self.packages.${system}.default.nativeBuildInputs ++ - [ - ec - pkgs.valgrind - pkgs.cvc4 - pkgs.cvc5 - pkgs.z3 - ]; - - EASYCRYPT = "${ec}/bin/easycrypt"; - ECARGS = "-I Jasmin:${jasmin}/eclib"; - - shellHook = '' - easycrypt why3config - ''; - }; + outputs = inputs@{ flake-parts, easycrypt, jasmin, ... }: + flake-parts.lib.mkFlake { inherit inputs; } { + imports = [ ]; + systems = [ "x86_64-linux" "aarch64-linux" "aarch64-darwin" "x86_64-darwin" ]; + perSystem = { pkgs, system, self', ... }: + let + ec = easycrypt.packages.${system}; + jasminc = pkgs.callPackage "${jasmin}/default.nix" { inherit pkgs; }; + in + { + packages.default = pkgs.callPackage ./default.nix { inherit pkgs jasminc; }; + + devShells.default = pkgs.mkShell { + name = "libjade"; + src = self'.packages.default.src; + + packages = [ + ec.with_provers + pkgs.why3 + ]; + + ECARGS = "-I Jasmin:${jasmin}/eclib"; + + shellHook = '' + easycrypt why3config + ''; + }; + }; }; } From 9df540b3d04fede01f48f6a3f2ea0e9ae05f0298 Mon Sep 17 00:00:00 2001 From: Aaron Kaiser Date: Wed, 10 Jul 2024 18:24:46 +0200 Subject: [PATCH 6/8] Reintroduce valgrind as a dependency --- flake.nix | 1 + 1 file changed, 1 insertion(+) diff --git a/flake.nix b/flake.nix index c8a06f8f..5b3574df 100644 --- a/flake.nix +++ b/flake.nix @@ -35,6 +35,7 @@ packages = [ ec.with_provers pkgs.why3 + pkgs.valgrind ]; ECARGS = "-I Jasmin:${jasmin}/eclib"; From 5a0a25bd097e6f7690d79a545f480e88ed9866f4 Mon Sep 17 00:00:00 2001 From: "Thing-han, Lim" <15379156+potsrevennil@users.noreply.github.com> Date: Thu, 11 Jul 2024 16:34:11 +0100 Subject: [PATCH 7/8] update easycrypt to the lastest version Signed-off-by: Thing-han, Lim <15379156+potsrevennil@users.noreply.github.com> --- flake.lock | 8 ++++---- flake.nix | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/flake.lock b/flake.lock index 04219d9b..095c1bfc 100644 --- a/flake.lock +++ b/flake.lock @@ -15,17 +15,17 @@ "stable": "stable" }, "locked": { - "lastModified": 1712580297, - "narHash": "sha256-3zpAbtDN7eFKjzCUExdl6lpidzprw5wzNEduQ1zGWHs=", + "lastModified": 1720168760, + "narHash": "sha256-tSUBdZmNeB1tURt7fqeH/xKArumzsE14PwsI8beDlro=", "owner": "EasyCrypt", "repo": "easycrypt", - "rev": "4201fddc14b81d2a69a33f034c9c7db4dfd58d0e", + "rev": "a9e31ff5f758ef62453d76de382a10ee718afc51", "type": "github" }, "original": { "owner": "EasyCrypt", "repo": "easycrypt", - "rev": "4201fddc14b81d2a69a33f034c9c7db4dfd58d0e", + "rev": "a9e31ff5f758ef62453d76de382a10ee718afc51", "type": "github" } }, diff --git a/flake.nix b/flake.nix index 5b3574df..10e35d24 100644 --- a/flake.nix +++ b/flake.nix @@ -4,7 +4,7 @@ inputs = { nixpkgs.url = "nixpkgs/release-24.05"; - easycrypt.url = "github:EasyCrypt/easycrypt/4201fddc14b81d2a69a33f034c9c7db4dfd58d0e"; + easycrypt.url = "github:EasyCrypt/easycrypt/a9e31ff5f758ef62453d76de382a10ee718afc51"; jasmin = { url = "github:jasmin-lang/jasmin/e4640e7dcdb01d1ba63617a5d78456e1209d699c"; flake = false; @@ -35,7 +35,7 @@ packages = [ ec.with_provers pkgs.why3 - pkgs.valgrind + (pkgs.lib.optional pkgs.stdenv.isLinux pkgs.valgrind) ]; ECARGS = "-I Jasmin:${jasmin}/eclib"; From fffa4d669c7b8a3a3f073b89f3913f9b1ecb0919 Mon Sep 17 00:00:00 2001 From: Aaron Kaiser Date: Fri, 12 Jul 2024 12:27:14 +0200 Subject: [PATCH 8/8] fix(nix): Add missing dependencies to flake --- flake.nix | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/flake.nix b/flake.nix index 10e35d24..cbbb2630 100644 --- a/flake.nix +++ b/flake.nix @@ -16,13 +16,13 @@ }; }; - outputs = inputs@{ flake-parts, easycrypt, jasmin, ... }: + outputs = inputs@{ self, flake-parts, easycrypt, jasmin, ... }: flake-parts.lib.mkFlake { inherit inputs; } { imports = [ ]; systems = [ "x86_64-linux" "aarch64-linux" "aarch64-darwin" "x86_64-darwin" ]; perSystem = { pkgs, system, self', ... }: let - ec = easycrypt.packages.${system}; + ec = easycrypt.packages.${system}.default; jasminc = pkgs.callPackage "${jasmin}/default.nix" { inherit pkgs; }; in { @@ -32,10 +32,15 @@ name = "libjade"; src = self'.packages.default.src; - packages = [ - ec.with_provers + packages = self.packages.${system}.default.nativeBuildInputs ++ [ + ec + pkgs.cvc4 + pkgs.cvc5 + pkgs.z3 pkgs.why3 (pkgs.lib.optional pkgs.stdenv.isLinux pkgs.valgrind) + pkgs.emacs + pkgs.emacsPackages.proof-general ]; ECARGS = "-I Jasmin:${jasmin}/eclib";