From 22f4a7a1806d624e5a2cfd072c711fba981632a4 Mon Sep 17 00:00:00 2001 From: Gaetan Lepage Date: Fri, 12 Jun 2026 09:35:54 +0000 Subject: [PATCH 1/3] ocamlPackages.easy_logging: init at 0.8.2 --- .../ocaml-modules/easy_logging/default.nix | 49 +++++++++++++++++++ pkgs/top-level/ocaml-packages.nix | 2 + 2 files changed, 51 insertions(+) create mode 100644 pkgs/development/ocaml-modules/easy_logging/default.nix diff --git a/pkgs/development/ocaml-modules/easy_logging/default.nix b/pkgs/development/ocaml-modules/easy_logging/default.nix new file mode 100644 index 000000000000..463c3f654a0f --- /dev/null +++ b/pkgs/development/ocaml-modules/easy_logging/default.nix @@ -0,0 +1,49 @@ +{ + lib, + buildDunePackage, + fetchFromGitHub, + + # propagatedBuildInputs, + calendar, + + nix-update-script, +}: + +buildDunePackage (finalAttrs: { + pname = "easy_logging"; + version = "0.8.2"; + __structuredAttrs = true; + + src = fetchFromGitHub { + owner = "sapristi"; + repo = "easy_logging"; + tag = "v${finalAttrs.version}"; + hash = "sha256-Xy6Rfef7r2K8DTok7AYa/9m3ZEV07LlUeMQSRayLBco="; + }; + + propagatedBuildInputs = [ + calendar + ]; + + doCheck = true; + # Only run the tests for the `easy_logging` package itself. + # The other directories belong to the separate `easy_logging_yojson` package, which is not built + # here and pulls in additional dependencies. + checkPhase = '' + runHook preCheck + + dune runtest easy_logging ''${enableParallelBuilding:+-j $NIX_BUILD_CORES} + + runHook postCheck + ''; + + passthru.updateScript = nix-update-script { }; + + meta = { + description = "Logging module for OCaml"; + homepage = "https://github.com/sapristi/easy_logging"; + license = lib.licenses.mpl20; + maintainers = with lib.maintainers; [ GaetanLepage ]; + platforms = lib.platforms.all; + }; +}) diff --git a/pkgs/top-level/ocaml-packages.nix b/pkgs/top-level/ocaml-packages.nix index 6802e6228f46..fe300b2eeac4 100644 --- a/pkgs/top-level/ocaml-packages.nix +++ b/pkgs/top-level/ocaml-packages.nix @@ -541,6 +541,8 @@ let easy-format = callPackage ../development/ocaml-modules/easy-format { }; + easy_logging = callPackage ../development/ocaml-modules/easy_logging { }; + eigen = callPackage ../development/ocaml-modules/eigen { stdenv = pkgs.gcc14Stdenv; }; From be1266bb43fc41c6faef49607d9a95b959df78bb Mon Sep 17 00:00:00 2001 From: Gaetan Lepage Date: Fri, 12 Jun 2026 09:37:04 +0000 Subject: [PATCH 2/3] ocamlPackages.charon: init at 2026.06.12 --- .../ocaml-modules/charon/default.nix | 54 +++++++++++++++++++ .../name_matcher_parser/default.nix | 42 +++++++++++++++ pkgs/top-level/ocaml-packages.nix | 4 ++ 3 files changed, 100 insertions(+) create mode 100644 pkgs/development/ocaml-modules/charon/default.nix create mode 100644 pkgs/development/ocaml-modules/name_matcher_parser/default.nix diff --git a/pkgs/development/ocaml-modules/charon/default.nix b/pkgs/development/ocaml-modules/charon/default.nix new file mode 100644 index 000000000000..a1f4604666b1 --- /dev/null +++ b/pkgs/development/ocaml-modules/charon/default.nix @@ -0,0 +1,54 @@ +{ + lib, + buildDunePackage, + fetchFromGitHub, + + # propagatedBuildInputs, + easy_logging, + name_matcher_parser, + ppx_deriving, + unionFind, + visitors, + yojson, + + nix-update-script, +}: + +buildDunePackage (finalAttrs: { + pname = "charon"; + version = "2026.06.12"; + __structuredAttrs = true; + + src = fetchFromGitHub { + owner = "AeneasVerif"; + repo = "charon"; + tag = "nightly-${finalAttrs.version}"; + hash = "sha256-XCNDFJ8HakRBQ68rWB29R5RF7zhmqmNMna098SvXDE0="; + }; + + propagatedBuildInputs = [ + easy_logging + name_matcher_parser + ppx_deriving + unionFind + visitors + yojson + ]; + + # The charon-ml test suite requires pre-generated `.llbc` fixtures produced by + # running the (Rust) charon binary, which are not part of the OCaml source + # distribution, so the tests cannot run here. + doCheck = false; + + passthru.updateScript = nix-update-script { + extraArgs = [ "--version=unstable" ]; + }; + + meta = { + description = "Analyze Rust crates without touching compiler internals"; + homepage = "https://github.com/AeneasVerif/charon"; + license = lib.licenses.asl20; + maintainers = with lib.maintainers; [ GaetanLepage ]; + platforms = lib.platforms.all; + }; +}) diff --git a/pkgs/development/ocaml-modules/name_matcher_parser/default.nix b/pkgs/development/ocaml-modules/name_matcher_parser/default.nix new file mode 100644 index 000000000000..e9763adadd8a --- /dev/null +++ b/pkgs/development/ocaml-modules/name_matcher_parser/default.nix @@ -0,0 +1,42 @@ +{ + lib, + buildDunePackage, + charon, + + # nativeBuildInputs, + menhir, + + # propagatedBuildInputs, + menhirLib, + ppx_deriving, + visitors, + zarith, +}: + +buildDunePackage (finalAttrs: { + pname = "name_matcher_parser"; + inherit (charon) version; + __structuredAttrs = true; + + inherit (charon) src; + + nativeBuildInputs = [ menhir ]; + + propagatedBuildInputs = [ + menhirLib + ppx_deriving + visitors + zarith + ]; + + # No test suite is defined for this package. + doCheck = false; + + meta = { + description = "Parser to define name matchers"; + homepage = "https://github.com/AeneasVerif/charon"; + license = lib.licenses.asl20; + maintainers = with lib.maintainers; [ GaetanLepage ]; + platforms = lib.platforms.all; + }; +}) diff --git a/pkgs/top-level/ocaml-packages.nix b/pkgs/top-level/ocaml-packages.nix index fe300b2eeac4..5d4f8316a419 100644 --- a/pkgs/top-level/ocaml-packages.nix +++ b/pkgs/top-level/ocaml-packages.nix @@ -247,6 +247,8 @@ let checkseum = callPackage ../development/ocaml-modules/checkseum { }; + charon = callPackage ../development/ocaml-modules/charon { }; + chrome-trace = callPackage ../development/ocaml-modules/chrome-trace { }; cil = callPackage ../development/ocaml-modules/cil { }; @@ -1423,6 +1425,8 @@ let ### N ### + name_matcher_parser = callPackage ../development/ocaml-modules/name_matcher_parser { }; + nbd = pkgs.libnbd.override { ocamlPackages = self; buildOcamlBindings = true; From ce4a299968e0e3586ddcd36fac626b8464e3a2bd Mon Sep 17 00:00:00 2001 From: Gaetan Lepage Date: Fri, 12 Jun 2026 09:37:21 +0000 Subject: [PATCH 3/3] ocamlPackages.aeneas: init at 2026.06.12 --- .../ocaml-modules/aeneas/default.nix | 58 +++++++++++++++++++ pkgs/top-level/ocaml-packages.nix | 2 + 2 files changed, 60 insertions(+) create mode 100644 pkgs/development/ocaml-modules/aeneas/default.nix diff --git a/pkgs/development/ocaml-modules/aeneas/default.nix b/pkgs/development/ocaml-modules/aeneas/default.nix new file mode 100644 index 000000000000..ea17be64e274 --- /dev/null +++ b/pkgs/development/ocaml-modules/aeneas/default.nix @@ -0,0 +1,58 @@ +{ + lib, + buildDunePackage, + fetchFromGitHub, + + # propagatedBuildInputs, + charon, + core_unix, + domainslib, + ocamlgraph, + progress, + visitors, + + nix-update-script, +}: + +buildDunePackage (finalAttrs: { + pname = "aeneas"; + version = "2026.06.12"; + __structuredAttrs = true; + + minimalOCamlVersion = "5.1"; + + src = fetchFromGitHub { + owner = "AeneasVerif"; + repo = "aeneas"; + tag = "nightly-${finalAttrs.version}"; + hash = "sha256-loTnCy4lNJki+dSShZ35jKyOWIh1XcPwN7oY7CyFa04="; + }; + + sourceRoot = "${finalAttrs.src.name}/src"; + + propagatedBuildInputs = [ + charon + core_unix + domainslib + ocamlgraph + progress + visitors + ]; + + # The test suite consists of heavy integration tests that require the full + # toolchain (Rust, charon and the F*/Coq/Lean backends), so it is not run here. + doCheck = false; + + passthru.updateScript = nix-update-script { + extraArgs = [ "--version=unstable" ]; + }; + + meta = { + description = "Verification toolchain for Rust programs"; + homepage = "https://github.com/AeneasVerif/aeneas"; + license = lib.licenses.asl20; + maintainers = with lib.maintainers; [ GaetanLepage ]; + mainProgram = "aeneas"; + platforms = lib.platforms.all; + }; +}) diff --git a/pkgs/top-level/ocaml-packages.nix b/pkgs/top-level/ocaml-packages.nix index 5d4f8316a419..8913bb36c421 100644 --- a/pkgs/top-level/ocaml-packages.nix +++ b/pkgs/top-level/ocaml-packages.nix @@ -22,6 +22,8 @@ let afl-persistent = callPackage ../development/ocaml-modules/afl-persistent { }; + aeneas = callPackage ../development/ocaml-modules/aeneas { }; + alcotest = callPackage ../development/ocaml-modules/alcotest { }; alcotest-lwt = callPackage ../development/ocaml-modules/alcotest/lwt.nix { };