diff --git a/pkgs/applications/science/logic/hol_light/0001-pa_j-accept-camlp5-8.05-for-OCaml-5.4.patch b/pkgs/applications/science/logic/hol_light/0001-pa_j-accept-camlp5-8.05-for-OCaml-5.4.patch new file mode 100644 index 0000000000000..b47e4a62c486b --- /dev/null +++ b/pkgs/applications/science/logic/hol_light/0001-pa_j-accept-camlp5-8.05-for-OCaml-5.4.patch @@ -0,0 +1,22 @@ +From: "Matthias J. Kannwischer" +Date: Sat, 30 May 2026 16:37:44 +0800 +Subject: pa_j: accept camlp5 8.05 for OCaml 5.4 + +Signed-off-by: Matthias J. Kannwischer +--- + pa_j/chooser.sh | 2 +- + 1 file changed, 1 insertion(+), 1 deletion(-) + +diff --git a/pa_j/chooser.sh b/pa_j/chooser.sh +index 5ec8d00..de5c8c8 100755 +--- a/pa_j/chooser.sh ++++ b/pa_j/chooser.sh +@@ -20,7 +20,7 @@ CAMLP5_FULL_VERSION=`camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 + + if test ${OCAML_BINARY_VERSION} = "3.0" + then echo "pa_j_${OCAML_VERSION}.ml" +-elif test ${CAMLP5_FULL_VERSION} = "8.04.00" ++elif test ${CAMLP5_BINARY_VERSION} = "8.04" -o ${CAMLP5_BINARY_VERSION} = "8.05" + then + if test ${OCAML_BINARY_VERSION} = "5.4" + then echo "pa_j_5.4_8.04.00.ml" diff --git a/pkgs/applications/science/logic/hol_light/0002-link-findlib-into-ocaml-hol.patch b/pkgs/applications/science/logic/hol_light/0002-link-findlib-into-ocaml-hol.patch new file mode 100644 index 0000000000000..688f2e0506feb --- /dev/null +++ b/pkgs/applications/science/logic/hol_light/0002-link-findlib-into-ocaml-hol.patch @@ -0,0 +1,12 @@ +diff --git a/Makefile b/Makefile +--- a/Makefile ++++ b/Makefile +@@ -128,7 +128,7 @@ + hol.sh: pa_j.cmo ${HOLSRC} bignum.cmo hol_loader.cmo update_database.ml + if [ `uname` = "Linux" ] || [ `uname` = "Darwin" ] ; then \ + if [ ${OCAML_UNARY_VERSION} = "5" ] || [ ${OCAML_VERSION} = "4.14" ] ; then \ +- ocamlfind ocamlmktop -package zarith -o ocaml-hol zarith.cma bignum.cmo hol_loader.cmo ; \ ++ ocamlfind ocamlmktop -package zarith,findlib -o ocaml-hol zarith.cma bignum.cmo hol_loader.cmo ; \ + sed "s^__DIR__^`pwd`^g; s^__USE_MODULE__^$(HOLLIGHT_USE_MODULE)^g" hol_4.14.sh > hol.sh ; \ + else \ + ocamlmktop -o ocaml-hol nums.cma bignum.cmo hol_loader.cmo ; \ diff --git a/pkgs/applications/science/logic/hol_light/0004-Fix-compilation-with-camlp5-7.11.patch b/pkgs/applications/science/logic/hol_light/0004-Fix-compilation-with-camlp5-7.11.patch deleted file mode 100644 index 2fc2b1544c442..0000000000000 --- a/pkgs/applications/science/logic/hol_light/0004-Fix-compilation-with-camlp5-7.11.patch +++ /dev/null @@ -1,66 +0,0 @@ -From: Stephane Glondu -Date: Wed, 12 Feb 2020 05:42:32 +0100 -Subject: Fix compilation with camlp5 7.11 - ---- - pa_j_4.xx_7.xx.ml | 17 +++++++++++------ - 1 file changed, 11 insertions(+), 6 deletions(-) - -diff --git a/pa_j_4.xx_7.xx.ml b/pa_j_4.xx_7.xx.ml -index 4f7ed60..e834058 100755 ---- a/pa_j/pa_j_4.xx_7.xx.ml -+++ b/pa_j/pa_j_4.xx_7.xx.ml -@@ -410,9 +410,10 @@ and reloc_module_type floc sh = - | MtApp loc x1 x2 → - let loc = floc loc in - MtApp loc (self x1) (self x2) -- | MtFun loc x1 x2 x3 → -+ | MtFun loc x x3 → - let loc = floc loc in -- MtFun loc x1 (self x2) (self x3) -+ let x = vala_map (option_map (fun (x1, x2) -> (x1, self x2))) x in -+ MtFun loc x (self x3) - | MtLid loc x1 → - let loc = floc loc in - MtLid loc x1 -@@ -507,9 +508,10 @@ and reloc_module_expr floc sh = - | MeApp loc x1 x2 → - let loc = floc loc in - MeApp loc (self x1) (self x2) -- | MeFun loc x1 x2 x3 → -+ | MeFun loc x x3 → - let loc = floc loc in -- MeFun loc x1 (reloc_module_type floc sh x2) (self x3) -+ let x = vala_map (option_map (fun (x1, x2) -> (x1, reloc_module_type floc sh x2))) x in -+ MeFun loc x (self x3) - | MeStr loc x1 → - let loc = floc loc in - MeStr loc (vala_map (List.map (reloc_str_item floc sh)) x1) -@@ -2007,7 +2009,7 @@ EXTEND - | -> <:vala< [] >> ] ] - ; - mod_binding: -- [ [ i = V UIDENT; me = mod_fun_binding -> (i, me) ] ] -+ [ [ i = V uidopt "uidopt"; me = mod_fun_binding -> (i, me) ] ] - ; - mod_fun_binding: - [ RIGHTA -@@ -2070,7 +2072,7 @@ EXTEND - <:sig_item< value $lid:i$ : $t$ >> ] ] - ; - mod_decl_binding: -- [ [ i = V UIDENT; mt = module_declaration -> (i, mt) ] ] -+ [ [ i = V uidopt "uidopt"; mt = module_declaration -> (i, mt) ] ] - ; - module_declaration: - [ RIGHTA -@@ -2092,6 +2094,9 @@ EXTEND - | "module"; i = V mod_ident ""; ":="; me = module_expr -> - <:with_constr< module $_:i$ := $me$ >> ] ] - ; -+ uidopt: -+ [ [ m = V UIDENT -> Some m ] ] -+ ; - (* Core expressions *) - expr: - [ "top" RIGHTA diff --git a/pkgs/applications/science/logic/hol_light/default.nix b/pkgs/applications/science/logic/hol_light/default.nix index c0b7ebbc03776..5c10c8e1a1841 100644 --- a/pkgs/applications/science/logic/hol_light/default.nix +++ b/pkgs/applications/science/logic/hol_light/default.nix @@ -1,61 +1,51 @@ { lib, stdenv, - runtimeShell, fetchFromGitHub, + makeBinaryWrapper, + writeText, ocaml, findlib, - num, zarith, camlp5, camlp-streams, + fmt, pcre2, + ledit, bash, }: let - use_zarith = lib.versionAtLeast ocaml.version "4.14"; - load_num = - if use_zarith then - '' - -I ${zarith}/lib/ocaml/${ocaml.version}/site-lib/zarith \ - -I ${zarith}/lib/ocaml/${ocaml.version}/site-lib/stublibs \ - -I ${pcre2}/lib/ocaml/${ocaml.version}/site-lib/stublibs \ - '' - else - lib.optionalString (num != null) '' - -I ${num}/lib/ocaml/${ocaml.version}/site-lib/num \ - -I ${num}/lib/ocaml/${ocaml.version}/site-lib/top-num \ - -I ${num}/lib/ocaml/${ocaml.version}/site-lib/stublibs - ''; - - start_script = '' - #!${runtimeShell} - cd $out/lib/hol_light - export OCAMLPATH="''${OCAMLPATH-}''${OCAMLPATH:+:}${camlp5}/lib/ocaml/${ocaml.version}/site-lib/" - exec ${ocaml}/bin/ocaml \ - -I \`${camlp5}/bin/camlp5 -where\` \ - ${load_num} \ - -I ${findlib}/lib/ocaml/${ocaml.version}/site-lib/ \ - -I ${camlp-streams}/lib/ocaml/${ocaml.version}/site-lib/camlp-streams camlp_streams.cma \ - -init make.ml - ''; + ocamlPath = lib.makeSearchPath "/lib/ocaml/${ocaml.version}/site-lib" [ + camlp5 + camlp-streams + fmt + pcre2 + zarith + ]; + stublibsPath = lib.makeSearchPath "/lib/ocaml/${ocaml.version}/site-lib/stublibs" [ + zarith + pcre2 + ]; in stdenv.mkDerivation { pname = "hol_light"; - version = "unstable-2024-07-07"; + version = "0-unstable-2026-05-19"; src = fetchFromGitHub { owner = "jrh13"; repo = "hol-light"; - rev = "16b184e30e7e3fe9add7d1ee93242323ed2e1726"; - hash = "sha256-V0OtsmX5pa+CH3ZXmNG3juXwXZ5+A0k13eMCAfaRziQ="; + rev = "9b510bc76da4cecf6e509be44d327c9236ec273f"; + hash = "sha256-QaTDrGHpHvEde2AK/SD7eM+bAC9vN5o+dQqW1oau1Yo="; }; - patches = [ ./0004-Fix-compilation-with-camlp5-7.11.patch ]; - - buildInputs = [ bash ]; + patches = [ + # Accept camlp5 8.05 in the pa_j chooser; submitted upstream. + ./0001-pa_j-accept-camlp5-8.05-for-OCaml-5.4.patch + # Link findlib into ocaml-hol so `#use "topfind"` works in the sandbox. + ./0002-link-findlib-into-ocaml-hol.patch + ]; strictDeps = true; @@ -63,28 +53,77 @@ stdenv.mkDerivation { ocaml findlib camlp5 + makeBinaryWrapper + ]; + buildInputs = [ + bash + ocaml + findlib + camlp5 + ledit ]; propagatedBuildInputs = [ camlp-streams + fmt pcre2 - (if use_zarith then zarith else num) + zarith ]; + setupHook = writeText "hol-light-setup-hook.sh" '' + addHolLight () { + if test -d "''$1/lib/hol_light"; then + export HOLLIGHT_DIR="''$1/lib/hol_light" + fi + } + addEnvHooks "$targetOffset" addHolLight + ''; + + buildPhase = '' + runHook preBuild + patchShebangs . + HOLLIGHT_USE_MODULE=1 make hol.sh + HOLLIGHT_USE_MODULE=1 make + runHook postBuild + ''; + installPhase = '' - mkdir -p "$out/lib/hol_light" "$out/bin" - cp -a . $out/lib/hol_light - echo "${start_script}" > "$out/bin/hol_light" - chmod a+x "$out/bin/hol_light" + runHook preInstall + mkdir -p "$out/lib/hol_light" + cp -a . "$out/lib/hol_light" + # The Makefile bakes the build directory into hol.sh; regenerate it + # pointing at the install location. + sed "s^__DIR__^$out/lib/hol_light^g; s^__USE_MODULE__^1^g" hol_4.14.sh \ + > "$out/lib/hol_light/hol.sh" + chmod +x "$out/lib/hol_light/hol.sh" + # Add the findlib site-lib so the toplevel can `#use "topfind"`. + substituteInPlace "$out/lib/hol_light/hol.sh" \ + --replace-fail '-init ''${HOL_ML_PATH} -I ''${HOLLIGHT_DIR}' \ + '-init ''${HOL_ML_PATH} -I ''${HOLLIGHT_DIR} -I ${findlib}/lib/ocaml/${ocaml.version}/site-lib' + makeWrapper "$out/lib/hol_light/hol.sh" "$out/bin/hol_light" \ + --prefix PATH : ${ + lib.makeBinPath [ + ocaml + findlib + camlp5 + ledit + ] + } \ + --set OCAMLPATH "${ocamlPath}" \ + --prefix CAML_LD_LIBRARY_PATH : "${stublibsPath}" + ln -s hol_light "$out/bin/hol.sh" + runHook postInstall ''; meta = { description = "Interactive theorem prover based on Higher-Order Logic"; homepage = "http://www.cl.cam.ac.uk/~jrh13/hol-light/"; + mainProgram = "hol_light"; license = lib.licenses.bsd2; platforms = lib.platforms.unix; maintainers = with lib.maintainers; [ thoughtpolice vbgl + mkannwischer ]; }; } diff --git a/pkgs/development/tools/ocaml/camlp5/default.nix b/pkgs/development/tools/ocaml/camlp5/default.nix index 4a8cd807a53f9..e2931d73ddc39 100644 --- a/pkgs/development/tools/ocaml/camlp5/default.nix +++ b/pkgs/development/tools/ocaml/camlp5/default.nix @@ -8,6 +8,7 @@ makeWrapper, rresult, bos, + fmt, pcre2, re, camlp-streams, @@ -52,12 +53,15 @@ stdenv.mkDerivation ( buildInputs = lib.optionals recent [ bos - pcre2 re rresult ]; - propagatedBuildInputs = lib.optional recent camlp-streams; + propagatedBuildInputs = lib.optionals recent [ + camlp-streams + pcre2 + fmt + ]; strictDeps = true; diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 3b9a43a312e0f..9fedba178df52 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -11091,7 +11091,7 @@ with pkgs; enableUnfree = true; }; - inherit (ocaml-ng.ocamlPackages_5_3) hol_light; + inherit (ocamlPackages) hol_light; isabelle-components = recurseIntoAttrs (callPackage ../by-name/is/isabelle/components { }); diff --git a/pkgs/top-level/ocaml-packages.nix b/pkgs/top-level/ocaml-packages.nix index c9c9f327a0f7a..6416a7daf1ff2 100644 --- a/pkgs/top-level/ocaml-packages.nix +++ b/pkgs/top-level/ocaml-packages.nix @@ -2336,16 +2336,7 @@ let google-drive-ocamlfuse = callPackage ../applications/networking/google-drive-ocamlfuse { }; - hol_light = callPackage ../applications/science/logic/hol_light { - camlp5 = - if lib.versionAtLeast camlp5.version "8.04.00" then - camlp5.overrideAttrs { - version = "8.03.2"; - __intentionallyOverridingVersion = true; - } - else - camlp5; - }; + hol_light = callPackage ../applications/science/logic/hol_light { }; ### End ###