git: 311b26b38f32 - main - math/leangz: Add patches fixing 3 tests in math/lean4
- Go to: [ bottom of page ] [ top of archives ] [ this month ]
Date: Sun, 06 Sep 2026 06:19:01 UTC
The branch main has been updated by yuri:
URL: https://cgit.FreeBSD.org/ports/commit/?id=311b26b38f32c63ef9bed153d5b9f58ddac565c6
commit 311b26b38f32c63ef9bed153d5b9f58ddac565c6
Author: Yuri Victorovich <yuri@FreeBSD.org>
AuthorDate: 2026-09-05 20:16:11 +0000
Commit: Yuri Victorovich <yuri@FreeBSD.org>
CommitDate: 2026-09-06 06:18:25 +0000
math/leangz: Add patches fixing 3 tests in math/lean4
These patches will be upstreamed.
---
math/leangz/Makefile | 1 +
math/leangz/files/patch-src_lgz.rs | 39 +++++++++++++
math/leangz/files/patch-src_tar.rs | 116 +++++++++++++++++++++++++++++++++++++
math/leangz/pkg-descr | 4 ++
4 files changed, 160 insertions(+)
diff --git a/math/leangz/Makefile b/math/leangz/Makefile
index fc7cb45a7e10..a5cebf7945ac 100644
--- a/math/leangz/Makefile
+++ b/math/leangz/Makefile
@@ -1,6 +1,7 @@
PORTNAME= leangz
DISTVERSIONPREFIX= v
DISTVERSION= 0.1.20
+PORTREVISION= 1
CATEGORIES= math
MAINTAINER= yuri@FreeBSD.org
diff --git a/math/leangz/files/patch-src_lgz.rs b/math/leangz/files/patch-src_lgz.rs
new file mode 100644
index 000000000000..2589246a9581
--- /dev/null
+++ b/math/leangz/files/patch-src_lgz.rs
@@ -0,0 +1,39 @@
+-- Fix LGZ compression for Lean >= 4.33 non-8-byte-aligned constructor objects.
+-- Lean 4.33 introduced constructor objects with non-8-byte-aligned sizes (e.g.,
+-- a Bool field stored as 1 byte gives cs_sz=19 instead of the old 8-byte-rounded 24).
+-- The old code asserted cs_sz & 7 == 0, which panics on such objects.
+-- It also used (cs_sz >> 3) - 1 - num_fields to count scalar units, truncating to 0
+-- for non-aligned objects, silently dropping scalar bytes from the compressed stream.
+-- This patch removes the alignment assertion and fixes the scalar-field count to round
+-- UP to the nearest 8-byte unit so the decompressor emits the correct scalar data.
+-- The exprish path (Lean AST-specific encoding) keeps the legacy formula since those
+-- types always have 8-byte-aligned scalars and we must not accidentally match their
+-- hardcoded (ctor, num_fields, sfields) tuples.
+
+--- src/lgz.rs.orig 2026-06-27 14:23:24 UTC
++++ src/lgz.rs
+@@ -460,7 +460,7 @@ fn on_subobjs(cfg: Config, buf: &[u8], pos0: usize, mu
+ tag::RESERVED => panic!("reserved"),
+ _ctor => {
+ let len_except_sfields = 8 + 8 * header.num_fields as usize;
+- assert!(len_except_sfields <= header.cs_sz.get() as usize && header.cs_sz.get() & 7 == 0);
++ assert!(len_except_sfields <= header.cs_sz.get() as usize); // Lean >= 4.33 uses non-8-byte-aligned ctor sizes
+ on_array_subobjs(buf, header.num_fields.into(), pos, f);
+ pos0 + header.cs_sz.get() as usize
+ }
+@@ -1351,9 +1351,13 @@ impl<W: Write> LgzWriter<'_, W> {
+ }
+ tag::CLOSURE | tag::STRUCT_ARRAY | tag::EXTERNAL | tag::RESERVED => unreachable!(),
+ ctor => {
+- let sfields = (header.cs_sz.get() >> 3) - 1 - (header.num_fields as u16);
++ // Lean >= 4.33 uses non-8-byte-aligned scalar fields; use legacy formula for exprish
++ // path (Lean AST types always have 8-byte-aligned scalars), and round up for general path.
++ let sfields_legacy = (header.cs_sz.get() >> 3).saturating_sub(header.num_fields as u16 + 1);
++ let scalar_bytes = (header.cs_sz.get() as usize).saturating_sub(8 + 8 * header.num_fields as usize);
++ let sfields = ((scalar_bytes + 7) / 8) as u16;
+ if !ENABLE_EXPRISH
+- || self.try_write_exprish_ctor(pos, mode, ctor, header.num_fields, sfields).is_none()
++ || self.try_write_exprish_ctor(pos, mode, ctor, header.num_fields, sfields_legacy).is_none()
+ {
+ if let Some(packed) = pack_ctor(ctor, header.num_fields, sfields) {
+ self.write_op(mode, LgzMode::Normal, packed);
diff --git a/math/leangz/files/patch-src_tar.rs b/math/leangz/files/patch-src_tar.rs
new file mode 100644
index 000000000000..ef8c55d66a7c
--- /dev/null
+++ b/math/leangz/files/patch-src_tar.rs
@@ -0,0 +1,116 @@
+-- Fix leantar JSON stdin parsing to accept lake cache input format.
+-- lake sends `--stdin --json` entries as objects (for example
+-- `{"file":"...","hash":"..."}`), while older logic expected a positional
+-- tuple shape and failed to parse these records reliably.
+-- This patch accepts string, object, and legacy [hash,file] array entries.
+
+--- src/tar.rs.orig 2026-06-27 14:23:24 UTC
++++ src/tar.rs
+@@ -161,37 +161,77 @@ fn main() {
+ assert!(!from_stdin, "two stdin inputs");
+ from_stdin = true;
+ if json_stdin {
+- let str = std::io::read_to_string(std::io::stdin()).unwrap();
+- for j in serde_json::from_str::<Vec<serde_json::Value>>(&str).unwrap() {
+- args_vec.push(if let serde_json::Value::String(s) = j {
+- from_file(s)
+- } else {
+- let j = j.as_object().expect("expected object");
+- let file = j["file"].as_str().expect("expected string");
+- let base = match j.get("base") {
+- None => vec![],
+- Some(b) => match b.as_array() {
+- Some(arr) => arr
+- .iter()
+- .map(|v| {
+- if v.is_null() {
+- None::<PathBuf>
+- } else {
+- Some(v.as_str().expect("expected string or null").into())
+- }
+- })
+- .collect(),
+- None => vec![Some(b.as_str().expect("expected string or array").into())],
+- },
+- };
+- let hash = j.get("hash").filter(|v| !v.is_null()).map(|value| {
+- value
+- .as_str()
++ let s = std::io::read_to_string(std::io::stdin()).unwrap_or_else(|e| {
++ eprintln!("error reading stdin: {e}");
++ std::process::exit(1);
++ });
++ let v = match serde_json::from_str::<Vec<serde_json::Value>>(&s) {
++ Ok(v) => v,
++ Err(e) => {
++ eprintln!("error parsing JSON from stdin: {e}");
++ std::process::exit(1);
++ }
++ };
++ for j in v {
++ args_vec.push(match j {
++ serde_json::Value::String(s) => from_file(s),
++ // Accept [hash, file] two-element arrays produced by lake cache commands.
++ serde_json::Value::Array(ref arr) if arr.len() == 2 => {
++ let hash = arr[0].as_str()
+ .and_then(|s| u64::from_str_radix(s, 16).ok())
+- .expect("expected hex hash")
+- });
+- Arg { base, file: file.into(), hash }
+- })
++ .unwrap_or_else(|| {
++ eprintln!("json array: first element must be a hex hash string");
++ std::process::exit(1);
++ });
++ let file = arr[1].as_str().unwrap_or_else(|| {
++ eprintln!("json array: second element must be a file string");
++ std::process::exit(1);
++ });
++ Arg { base: vec![], file: file.into(), hash: Some(hash) }
++ }
++ serde_json::Value::Object(ref map) => {
++ let file = map.get("file").and_then(|v| v.as_str()).unwrap_or_else(|| {
++ eprintln!("json object missing 'file' string field");
++ std::process::exit(1);
++ });
++ let base = match map.get("base") {
++ None => vec![],
++ Some(b) => match b.as_array() {
++ Some(arr) => arr
++ .iter()
++ .map(|v| {
++ if v.is_null() {
++ None::<PathBuf>
++ } else {
++ Some(v.as_str().unwrap_or_else(|| {
++ eprintln!("json 'base' array element must be string or null");
++ std::process::exit(1);
++ }).into())
++ }
++ })
++ .collect(),
++ None => vec![Some(b.as_str().unwrap_or_else(|| {
++ eprintln!("json 'base' must be string or array");
++ std::process::exit(1);
++ }).into())],
++ },
++ };
++ let hash = map.get("hash").filter(|v| !v.is_null()).map(|value| {
++ value
++ .as_str()
++ .and_then(|s| u64::from_str_radix(s, 16).ok())
++ .unwrap_or_else(|| {
++ eprintln!("json 'hash' must be a hex string");
++ std::process::exit(1);
++ })
++ });
++ Arg { base, file: file.into(), hash }
++ }
++ _ => {
++ eprintln!("json stdin: expected string, [hash, file] array, or object");
++ std::process::exit(1);
++ }
++ });
+ }
+ } else {
+ for arg in std::io::stdin().lines().map(|arg| arg.unwrap()) {
diff --git a/math/leangz/pkg-descr b/math/leangz/pkg-descr
index 0edc7f1c4e45..2a656133cf48 100644
--- a/math/leangz/pkg-descr
+++ b/math/leangz/pkg-descr
@@ -1 +1,5 @@
Lean 4 .olean file (de)compressor.
+
+It is used in tests of math/lean4.
+leantar is developed by the community, not by the Lean4
+project iotself.