lean4/4.12.0 package update #29764
lean4/4.12.0 package update #29764
Conversation
![octo-sts[bot]](https://avatars.githubusercontent.com/in/801323?s=60&v=4){kind=small}
Signed-off-by: wolfi-bot <[email protected]>
octo-sts
bot
added
request-version-update
|
Open AI suggestions to solve the build error: |
Build errors are: Could not find LIBUV_LIBRARIES using the following names: uv, libuv Signed-off-by: Mark McCormick <[email protected]>
Signed-off-by: Mark McCormick <[email protected]>
|
Open AI suggestions to solve the build error: |
|
Open AI suggestions to solve the build error: |
…t version Signed-off-by: Mark McCormick <[email protected]>
|
Open AI suggestions to solve the build error: |
Signed-off-by: Mark McCormick <[email protected]>
|
Open AI suggestions to solve the build error: |
|
Open AI suggestions to solve the build error: |
|
Open AI suggestions to solve the build error: |
…ld error implies this may be the root cause. Signed-off-by: Mark McCormick <[email protected]>
Package lean4: Click to expand/collapsePackage lean4: Package lean4-static: Click to expand/collapsePackage lean4-static: Package lean4-dev: Click to expand/collapsePackage lean4-dev: malcontent found differences: Click to expand/collapseDeleted: lean4/var/lib/db/sbom/lean4-4.11.0-r0.spdx.json [
|
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| -MEDIUM | net/download | download files | downloadLocation |
| -LOW | ref/site/url | contains embedded HTTPS URLs | https://spdx.org/spdxdocs/chainguard/melange/c51ff545e23a4e427a1c68ae93c9 |
Deleted: lean4-static/var/lib/db/sbom/lean4-static-4.11.0-r0.spdx.json [⚠️ MEDIUM]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| -MEDIUM | net/download | download files | downloadLocation |
| -LOW | ref/site/url | contains embedded HTTPS URLs | https://spdx.org/spdxdocs/chainguard/melange/31e19c2e918170faeac9990e116b |
Added: lean4/usr/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | fs/file/write | writes to file | writeFile |
Added: lean4/usr/bin/cadical [⚠️ MEDIUM]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +MEDIUM | compression/xz | command shells out to xz | xz - |
| +MEDIUM | exec/program | executes external programs | execv |
| +MEDIUM | net/interface/list | list network interfaces | freeifaddrs getifaddrs |
| +MEDIUM | procfs/arbitrary/pid | access /proc for arbitrary pids | /proc/%ld/statm |
| +MEDIUM | shell/arbitrary_command/dev_null | runs commands, discards output | %s 2>/dev/null |
| +LOW | compression/bzip2 | Works with bzip2 files | bzip2 |
| +LOW | compression/gzip | works with gzip files | gzip |
| +LOW | exec/program/background | wait for process to exit | waitpid |
| +LOW | ref/path/var | path reference within /var | /var/lib/dbus/machine-id |
Added: lean4/usr/src/lean/Std/Sat/AIG/Cached.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | ref/site/url | contains embedded HTTPS URLs | https://fmv.jku.at/papers/BrummayerBiere-MEMICS06.pdf |
Added: lean4/usr/src/lean/Lean/Elab/Tactic/BVDecide.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | ref/site/url | contains embedded HTTPS URLs | https://github.com/bitwuzla/bitwuzla |
Added: lean4/usr/src/lean/Std/Tactic/BVDecide/Syntax.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | ref/site/url | contains embedded HTTPS URLs | https://smt-lib.org/logics-all.shtml |
Added: lean4/usr/src/lean/Init/Data/List/Sort/Impl.lean [⚠️ MEDIUM]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +MEDIUM | ref/words/heartbeat | references a 'heartbeat' | set_option maxHeartbeats 400000 |
Added: lean4/usr/src/lean/Std/Sat/AIG/Basic.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | ref/site/url | contains embedded HTTPS URLs | https://arxiv.org/pdf/1304.7861.pdf |
Added: lean4/usr/src/lean/Lean/Elab/Tactic/BVDecide/External.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | ref/site/url | contains embedded HTTPS URLs | https://github.com/bitwuzla/bitwuzla/blob/0e81e616af4d4421729884f01928b19 |
Added: lean4/usr/src/lean/lake/tests/reservoirConfig/lakefile.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | ref/site/url | contains embedded HTTPS URLs | https://example.com |
Added: lean4/usr/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean [⚠️ MEDIUM]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +MEDIUM | shell/pipe_sh | pipes to shell | [ |
Added: lean4-static/var/lib/db/sbom/lean4-static-4.12.0-r0.spdx.json [⚠️ MEDIUM]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +MEDIUM | net/download | download files | downloadLocation |
| +LOW | ref/site/url | contains embedded HTTPS URLs | https://spdx.org/spdxdocs/chainguard/melange/2bf62530df56e085dd1908cce021 |
Added: lean4/usr/src/lean/Std/Tactic/BVDecide/LRAT/Actions.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | ref/site/url | contains embedded HTTPS URLs | https://www.cs.utexas.edu/ |
Added: lean4/usr/src/lean/Lean/Elab/Tactic/BVDecide/LRAT/Trim.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | ref/site/url | contains embedded HTTPS URLs | https://drops.dagstuhl.de/storage/00lipics/lipics-vol271-sat2023/LIPIcs.S |
Added: lean4/usr/src/lean/Std/Tactic/BVDecide/LRAT/Parser.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | fs/file/write | writes to file | writeBinFile |
| +LOW | ref/site/url | contains embedded HTTPS URLs | https://github.com/arminbiere/lrat-trim/blob/80f22c57fb2d74cb72210f5b334a https://github.com/marijnheule/drat-trim?tab=readme-ov-file https://www.cs.cmu.edu/ |
Added: lean4/usr/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean [⚠️ MEDIUM]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +MEDIUM | shell/pipe_sh | pipes to shell | [ |
Added: lean4/usr/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | fs/file/write | writes to file | writeFile |
| +LOW | ref/site/url | contains embedded HTTPS URLs | arminbiere/cadical#112 |
Added: lean4/usr/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean [⚠️ MEDIUM]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +MEDIUM | shell/pipe_sh | pipes to shell | [ |
Changed: /tmp/wolfictl-apk-3982722326/lean4/usr/lib/lean/libleanshared.so
4 new behaviors
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +MEDIUM | ref/extensions/office | References multiple Office file extensions (possible exfil) | doc eml ppt pst xls |
| +MEDIUM | ref/path/tmp | path reference within /tmp | /tmp/tmp.XXXXXXXX |
| +LOW | env/TMPDIR | TMPDIR | TMPDIR getenv |
| +LOW | fs/tempdir | looks up location of temp directory | TMPDIR |
Moved: lean4-dev/var/lib/db/sbom/lean4-dev-4.11.0-r0.spdx.json -> /tmp/wolfictl-apk-3982722326/lean4-dev/var/lib/db/sbom/lean4-dev-4.12.0-r0.spdx.json (similarity: 0.99)
Moved: lean4-dev/var/lib/db/sbom/lean4-dev-4.11.0-r0.spdx.json -> /tmp/wolfictl-apk-3982722326/lean4/var/lib/db/sbom/lean4-4.12.0-r0.spdx.json (similarity: 0.90)
octo-sts
bot
added
the
bincapz/pass
Signed-off-by: Mark McCormick <[email protected]>
Package lean4: Click to expand/collapsePackage lean4: Package lean4-static: Click to expand/collapsePackage lean4-static: Package lean4-dev: Click to expand/collapsePackage lean4-dev: malcontent found differences: Click to expand/collapseDeleted: lean4/var/lib/db/sbom/lean4-4.11.0-r0.spdx.json [
|
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| -MEDIUM | net/download | download files | downloadLocation |
| -LOW | ref/site/url | contains embedded HTTPS URLs | https://spdx.org/spdxdocs/chainguard/melange/c51ff545e23a4e427a1c68ae93c9 |
Deleted: lean4-static/var/lib/db/sbom/lean4-static-4.11.0-r0.spdx.json [⚠️ MEDIUM]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| -MEDIUM | net/download | download files | downloadLocation |
| -LOW | ref/site/url | contains embedded HTTPS URLs | https://spdx.org/spdxdocs/chainguard/melange/31e19c2e918170faeac9990e116b |
Added: lean4/usr/src/lean/Std/Tactic/BVDecide/LRAT/Parser.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | fs/file/write | writes to file | writeBinFile |
| +LOW | ref/site/url | contains embedded HTTPS URLs | https://github.com/arminbiere/lrat-trim/blob/80f22c57fb2d74cb72210f5b334a https://github.com/marijnheule/drat-trim?tab=readme-ov-file https://www.cs.cmu.edu/ |
Added: lean4/usr/bin/cadical [⚠️ MEDIUM]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +MEDIUM | compression/xz | command shells out to xz | xz - |
| +MEDIUM | exec/program | executes external programs | execv |
| +MEDIUM | net/interface/list | list network interfaces | freeifaddrs getifaddrs |
| +MEDIUM | procfs/arbitrary/pid | access /proc for arbitrary pids | /proc/%ld/statm |
| +MEDIUM | shell/arbitrary_command/dev_null | runs commands, discards output | %s 2>/dev/null |
| +LOW | compression/bzip2 | Works with bzip2 files | bzip2 |
| +LOW | compression/gzip | works with gzip files | gzip |
| +LOW | exec/program/background | wait for process to exit | waitpid |
| +LOW | ref/path/var | path reference within /var | /var/lib/dbus/machine-id |
Added: lean4/usr/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean [⚠️ MEDIUM]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +MEDIUM | shell/pipe_sh | pipes to shell | [ |
Added: lean4/usr/src/lean/Std/Tactic/BVDecide/LRAT/Actions.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | ref/site/url | contains embedded HTTPS URLs | https://www.cs.utexas.edu/ |
Added: lean4/usr/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | fs/file/write | writes to file | writeFile |
Added: lean4/usr/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | fs/file/write | writes to file | writeFile |
| +LOW | ref/site/url | contains embedded HTTPS URLs | arminbiere/cadical#112 |
Added: lean4/usr/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean [⚠️ MEDIUM]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +MEDIUM | shell/pipe_sh | pipes to shell | [ |
Added: lean4/usr/src/lean/Lean/Elab/Tactic/BVDecide/LRAT/Trim.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | ref/site/url | contains embedded HTTPS URLs | https://drops.dagstuhl.de/storage/00lipics/lipics-vol271-sat2023/LIPIcs.S |
Added: lean4/usr/src/lean/lake/tests/reservoirConfig/lakefile.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | ref/site/url | contains embedded HTTPS URLs | https://example.com |
Added: lean4/usr/src/lean/Std/Sat/AIG/Basic.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | ref/site/url | contains embedded HTTPS URLs | https://arxiv.org/pdf/1304.7861.pdf |
Added: lean4/usr/src/lean/Std/Sat/AIG/Cached.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | ref/site/url | contains embedded HTTPS URLs | https://fmv.jku.at/papers/BrummayerBiere-MEMICS06.pdf |
Added: lean4-static/var/lib/db/sbom/lean4-static-4.12.0-r0.spdx.json [⚠️ MEDIUM]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +MEDIUM | net/download | download files | downloadLocation |
| +LOW | ref/site/url | contains embedded HTTPS URLs | https://spdx.org/spdxdocs/chainguard/melange/2bf62530df56e085dd1908cce021 |
Added: lean4/usr/src/lean/Lean/Elab/Tactic/BVDecide.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | ref/site/url | contains embedded HTTPS URLs | https://github.com/bitwuzla/bitwuzla |
Added: lean4/usr/src/lean/Lean/Elab/Tactic/BVDecide/External.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | ref/site/url | contains embedded HTTPS URLs | https://github.com/bitwuzla/bitwuzla/blob/0e81e616af4d4421729884f01928b19 |
Added: lean4/usr/src/lean/Init/Data/List/Sort/Impl.lean [⚠️ MEDIUM]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +MEDIUM | ref/words/heartbeat | references a 'heartbeat' | set_option maxHeartbeats 400000 |
Added: lean4/usr/src/lean/Std/Tactic/BVDecide/Syntax.lean [✅ LOW]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +LOW | ref/site/url | contains embedded HTTPS URLs | https://smt-lib.org/logics-all.shtml |
Added: lean4/usr/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean [⚠️ MEDIUM]
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +MEDIUM | shell/pipe_sh | pipes to shell | [ |
Changed: /tmp/wolfictl-apk-3892973299/lean4/usr/lib/lean/libleanshared.so
4 new behaviors
| RISK | KEY | DESCRIPTION | EVIDENCE |
|---|---|---|---|
| +MEDIUM | ref/extensions/office | References multiple Office file extensions (possible exfil) | doc eml ppt pst xls |
| +MEDIUM | ref/path/tmp | path reference within /tmp | /tmp/tmp.XXXXXXXX |
| +LOW | env/TMPDIR | TMPDIR | TMPDIR getenv |
| +LOW | fs/tempdir | looks up location of temp directory | TMPDIR |
Moved: lean4-dev/var/lib/db/sbom/lean4-dev-4.11.0-r0.spdx.json -> /tmp/wolfictl-apk-3892973299/lean4-dev/var/lib/db/sbom/lean4-dev-4.12.0-r0.spdx.json (similarity: 0.99)
Moved: lean4-dev/var/lib/db/sbom/lean4-dev-4.11.0-r0.spdx.json -> /tmp/wolfictl-apk-3892973299/lean4/var/lib/db/sbom/lean4-4.12.0-r0.spdx.json (similarity: 0.90)
Package update - which was also failing to build. Needed additional runtime dep, as well as enable the DBUILD_SHARED_LIBS cmake flag. This seems to be quite common in other wolfi packages.
Also adds some melange test coverage.