c4patino/nixpkgs
1
0
Fork 0
mirror of https://github.com/NixOS/nixpkgs.git synced 2026-07-06 17:13:24 -05:00
Code Issues Projects Releases Packages Wiki Activity

hol_light: unstable-2024-07-07 -> 0-unstable-2026-05-19

Browse source 
Build against the default OCaml (5.4) set instead of the 5.3 pin, using the
module-mode launcher (ocaml-hol). Carries a patch so the pa_j chooser
accepts camlp5 8.05, links findlib into ocaml-hol, and sets up the runtime
OCAMLPATH/CAML_LD_LIBRARY_PATH. Drops the camlp5 8.03.2 downgrade.

(cherry picked from commit 7579aa2942)
This commit is contained in:
Matthias J. Kannwischer 2026-05-30 18:52:00 +08:00 • committed by github-actions[bot]
commit ba488fa795
6 changed files with 114 additions and 116 deletions
Download patch file Download diff file Expand all files Collapse all files

22
pkgs/applications/science/logic/hol_light/0001-pa_j-accept-camlp5-8.05-for-OCaml-5.4.patch Normal file
View file

@ -0,0 +1,22 @@
From: "Matthias J. Kannwischer" <matthias@zerorisc.com>
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 <matthias@zerorisc.com>
---
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"

12
pkgs/applications/science/logic/hol_light/0002-link-findlib-into-ocaml-hol.patch Normal file
View file

@ -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 ; \

66
pkgs/applications/science/logic/hol_light/0004-Fix-compilation-with-camlp5-7.11.patch
View file

@ -1,66 +0,0 @@
From: Stephane Glondu <steph@glondu.net>
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

117
pkgs/applications/science/logic/hol_light/default.nix
View file

@ -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
];
};
}

2
pkgs/top-level/all-packages.nix
View file

@ -11141,7 +11141,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 { });

11
pkgs/top-level/ocaml-packages.nix
View file

@ -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 ###