Skip to content

hol_light: build against the default OCaml (5.4)#525966

Merged
vbgl merged 2 commits into
NixOS:masterfrom
mkannwischer:hol-light-update
Jun 1, 2026
Merged

hol_light: build against the default OCaml (5.4)#525966
vbgl merged 2 commits into
NixOS:masterfrom
mkannwischer:hol-light-update

Conversation

@mkannwischer
Copy link
Copy Markdown
Contributor

@mkannwischer mkannwischer commented May 30, 2026 •
edited
Loading

This PR updates HOL-Light to the latest upstream version and switches it to the default OCaml (5.4) on the way.
I had to also propagate pcre2 and fmt in camlp5 as the newer version's findlib META requires it.

I've aligned the hol_light package a bit with other packages. I have tested that downstream HOL-Light proofs in mlkem-native work fine with the new package: pq-code-package/mlkem-native#1712.

Things done

@nixpkgs-ci nixpkgs-ci Bot added 8.has: package (update) This PR updates a package to a newer version 10.rebuild-linux: 11-100 This PR causes between 11 and 100 packages to rebuild on Linux. 10.rebuild-darwin: 11-100 This PR causes between 11 and 100 packages to rebuild on Darwin. 6.topic: ocaml OCaml is a general-purpose, high-level, multi-paradigm programming language. labels May 30, 2026
@mkannwischer
camlp5: propagate findlib deps pcre2 and fmt
74a82cc 
camlp5's META requires pcre2 and fmt, but they were only buildInputs, so
findlib consumers of camlp5 could not resolve them. Move them to
propagatedBuildInputs.
@mkannwischer
hol_light: unstable-2024-07-07 -> 0-unstable-2026-05-19
7579aa2 
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.
@mkannwischer mkannwischer mentioned this pull request May 30, 2026
Closed
@mkannwischer
Copy link
Copy Markdown
Contributor Author

mkannwischer commented May 30, 2026

nixpkgs-review result

Generated using nixpkgs-review.

Command: nixpkgs-review pr 525966
Commit: 7579aa29421e7fb5d2ed7da97040ed9448d1e10a

x86_64-linux

✅ 14 packages built:
  • haxe (haxe_4_3)
  • haxePackages.format
  • haxePackages.heaps
  • haxePackages.hlopenal
  • haxePackages.hlsdl
  • hxcpp (haxePackages.hxcpp)
  • haxePackages.hxcs
  • haxePackages.hxjava
  • haxePackages.hxnodejs_4
  • hol_light (ocamlPackages.hol_light, ocamlPackages_latest.hol_light)
  • ledit
  • ocamlPackages.camlp5 (ocamlPackages.camlp5_strict, ocamlPackages_latest.camlp5, ocamlPackages_latest.camlp5_strict)
  • orpie
  • prooftree

@mkannwischer
Copy link
Copy Markdown
Contributor Author

mkannwischer commented May 30, 2026

nixpkgs-review result

Generated using nixpkgs-review.

Command: nixpkgs-review pr 525966
Commit: 7579aa29421e7fb5d2ed7da97040ed9448d1e10a

aarch64-darwin

❌ 1 package failed to build:
  • prooftree
✅ 13 packages built:
  • haxe (haxe_4_3)
  • haxePackages.format
  • haxePackages.heaps
  • haxePackages.hlopenal
  • haxePackages.hlsdl
  • hxcpp (haxePackages.hxcpp)
  • haxePackages.hxcs
  • haxePackages.hxjava
  • haxePackages.hxnodejs_4
  • hol_light (ocamlPackages.hol_light, ocamlPackages_latest.hol_light)
  • ledit
  • ocamlPackages.camlp5 (ocamlPackages.camlp5_strict, ocamlPackages_latest.camlp5, ocamlPackages_latest.camlp5_strict)
  • orpie

@mkannwischer
Copy link
Copy Markdown
Contributor Author

mkannwischer commented May 30, 2026 •
edited
Loading

The prooftree build on aarch64-darwin fails due to the ocaml-4.12.1 and gtksourceview-2.10.5 builds failing - so that's unrelated to this PR.

@mkannwischer mkannwischer marked this pull request as ready for review May 30, 2026 14:40
@mkannwischer
Copy link
Copy Markdown
Contributor Author

mkannwischer commented May 30, 2026

@vbgl, could you take a look please?

@nixpkgs-ci nixpkgs-ci Bot requested review from thoughtpolice and vbgl May 30, 2026 15:00
@vbgl vbgl added the backport release-26.05 Backport PR automatically label Jun 1, 2026
@vbgl vbgl added this pull request to the merge queue Jun 1, 2026
Merged via the queue into NixOS:master with commit 2ed4e1d Jun 1, 2026
31 of 34 checks passed
@nixpkgs-ci nixpkgs-ci Bot mentioned this pull request Jun 1, 2026
Merged
@nixpkgs-ci
Copy link
Copy Markdown
Contributor

nixpkgs-ci Bot commented Jun 1, 2026

Successfully created backport PR for release-26.05:

@github-actions github-actions Bot added the 8.has: port to stable This PR already has a backport to the stable release. label Jun 1, 2026
@vbgl vbgl mentioned this pull request Jun 2, 2026
Open
14 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@thoughtpolice thoughtpolice Awaiting requested review from thoughtpolice

@vbgl vbgl Awaiting requested review from vbgl

Assignees

No one assigned

Labels

6.topic: ocaml OCaml is a general-purpose, high-level, multi-paradigm programming language. 8.has: package (update) This PR updates a package to a newer version 8.has: port to stable This PR already has a backport to the stable release. 10.rebuild-darwin: 11-100 This PR causes between 11 and 100 packages to rebuild on Darwin. 10.rebuild-linux: 11-100 This PR causes between 11 and 100 packages to rebuild on Linux. backport release-26.05 Backport PR automatically

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@mkannwischer @vbgl