From a6de94419ae97d9f5e0344b66a1d78a923df8d45 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 2 Jun 2026 13:46:09 +0200 Subject: [PATCH] hol_light: move to by-name/ (cherry picked from commit 58a1315c6188b0966b77700399614df7e3afd05d) --- ...a_j-accept-camlp5-8.05-for-OCaml-5.4.patch | 0 .../0002-link-findlib-into-ocaml-hol.patch | 0 .../ho/hol_light/package.nix} | 20 ++++++++++++------- pkgs/top-level/all-packages.nix | 2 -- pkgs/top-level/ocaml-packages.nix | 3 +-- 5 files changed, 14 insertions(+), 11 deletions(-) rename pkgs/{applications/science/logic => by-name/ho}/hol_light/0001-pa_j-accept-camlp5-8.05-for-OCaml-5.4.patch (100%) rename pkgs/{applications/science/logic => by-name/ho}/hol_light/0002-link-findlib-into-ocaml-hol.patch (100%) rename pkgs/{applications/science/logic/hol_light/default.nix => by-name/ho/hol_light/package.nix} (95%) diff --git a/pkgs/applications/science/logic/hol_light/0001-pa_j-accept-camlp5-8.05-for-OCaml-5.4.patch b/pkgs/by-name/ho/hol_light/0001-pa_j-accept-camlp5-8.05-for-OCaml-5.4.patch similarity index 100% rename from pkgs/applications/science/logic/hol_light/0001-pa_j-accept-camlp5-8.05-for-OCaml-5.4.patch rename to pkgs/by-name/ho/hol_light/0001-pa_j-accept-camlp5-8.05-for-OCaml-5.4.patch diff --git a/pkgs/applications/science/logic/hol_light/0002-link-findlib-into-ocaml-hol.patch b/pkgs/by-name/ho/hol_light/0002-link-findlib-into-ocaml-hol.patch similarity index 100% rename from pkgs/applications/science/logic/hol_light/0002-link-findlib-into-ocaml-hol.patch rename to pkgs/by-name/ho/hol_light/0002-link-findlib-into-ocaml-hol.patch diff --git a/pkgs/applications/science/logic/hol_light/default.nix b/pkgs/by-name/ho/hol_light/package.nix similarity index 95% rename from pkgs/applications/science/logic/hol_light/default.nix rename to pkgs/by-name/ho/hol_light/package.nix index 5c10c8e1a184..9cf947c92052 100644 --- a/pkgs/applications/science/logic/hol_light/default.nix +++ b/pkgs/by-name/ho/hol_light/package.nix @@ -4,17 +4,23 @@ fetchFromGitHub, makeBinaryWrapper, writeText, - ocaml, - findlib, - zarith, - camlp5, - camlp-streams, - fmt, - pcre2, + ocamlPackages, ledit, bash, }: +let + inherit (ocamlPackages) + ocaml + findlib + zarith + camlp5 + camlp-streams + fmt + pcre2 + ; +in + let ocamlPath = lib.makeSearchPath "/lib/ocaml/${ocaml.version}/site-lib" [ camlp5 diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 1adc70e3a7b5..46c45b52ff7f 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -11138,8 +11138,6 @@ with pkgs; enableUnfree = true; }; - inherit (ocamlPackages) hol_light; - isabelle-components = recurseIntoAttrs (callPackage ../by-name/is/isabelle/components { }); lean3 = lean; diff --git a/pkgs/top-level/ocaml-packages.nix b/pkgs/top-level/ocaml-packages.nix index 6416a7daf1ff..6802e6228f46 100644 --- a/pkgs/top-level/ocaml-packages.nix +++ b/pkgs/top-level/ocaml-packages.nix @@ -2336,8 +2336,6 @@ let google-drive-ocamlfuse = callPackage ../applications/networking/google-drive-ocamlfuse { }; - hol_light = callPackage ../applications/science/logic/hol_light { }; - ### End ### } @@ -2348,6 +2346,7 @@ let dune_2 = pkgs.dune_2; # Added 2025-12-08 dune_3 = pkgs.dune_3; # Added 2025-12-08 gd4o = throw "ocamlPackages.gd4o is not maintained, use ocamlPackages.gd instead"; + hol_light = pkgs.hol_light; # Added 2026-06-02 notty = throw "2026-05-05: notty is no longer maintained, use notty-community instead"; ocaml-freestanding = throw "ocamlPackages.ocaml-freestanding has been removed due to being broken for more than a year; see RFC 180"; # Added 2026-02-05 ocaml-vdom = throw "2023-10-09: ocamlPackages.ocaml-vdom was renamed to ocamlPackages.vdom";