Add tamarin-prover + its Maude runtime backend (5 packages) - #449
Conversation
tamarin-prover 1.12.0 (Haskell security-protocol verifier) built on minimal's GHC 9.10.3 — upstream pins 9.6, so we drive it with cabal + the system GHC, pin the solve to Stackage LTS 24.50, and carry three source-compat fixes: a fclabels template-haskell 2.22 shim, the LTS pin, and a GHC-61689 REPL.hs field-import fix. Plus its Maude 3.5.1 rewriting backend and Maude's C/C++ deps (libsigsegv, libtecla, buddy) linked dynamically against minimal's shared libs; libtecla vendors modern config.guess/config.sub (its 2003 copies predate aarch64). All five build + pass minimal check on aarch64; maude's build asserts it runs + finds its prelude. See pkgmgr-rs#528. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
Warning Review limit reachedYou’ve reached a temporary PR review limit under our Fair Usage Limits Policy. Next review available in: 32 minutes Enable usage-based reviews in Billing to review now. Otherwise, wait until the next included review is available. How can I continue?After more reviews become available, a review can be triggered using the To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based reviews. How do review limits work?CodeRabbit enforces per-developer PR review limits for each organization. Most developers receive the normal plan review availability. For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, additional reviews become available more gradually as earlier reviews age out of the rolling window. Please refer docs for additional details. Review details⚙️ Run configurationConfiguration used: Path: .coderabbit.yaml Review profile: CHILL Plan: Pro Run ID: 📒 Files selected for processing (6)
📝 WalkthroughWalkthroughAdds packaging definitions and reproducible build scripts for BuDDy, libsigsegv, libtecla, Maude, and tamarin-prover, including refreshed autotools detection scripts and GHC 9.10 compatibility patches. ChangesMaude and Tamarin packaging
Estimated code review effort: 4 (Complex) | ~60 minutes Possibly related issues
Suggested reviewers: 🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✨ Finishing Touches🧪 Generate unit tests (beta)
Comment |
Wat |
yeah, this is the haskell 'pin deps' file |
|
Can we fetch it? Just very aware that this repo is checked out by every consumer of pkgs so want to keep large files out if possible |
The Stackage LTS-24.50 cabal.config (~3.5k lines / 122 KB pinning the whole GHC-9.10.3 dependency set) was committed as a Local file, but the pkgs repo is cloned by every consumer, so large files bloat every checkout. Fetch it as a pinned `extract=false` Source (mirrored to gs://, sha256-locked) instead — the build already needs internet for Hackage and the LTS snapshot is immutable, so it stays reproducible. Rebuilt + smoke-tested green with the fetched config. Raised by @twitchyliquid64 on pkgs#449. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
done, moved it out of the repo into a fetched, sha-pinned gs:// source |
|
In dat silly voice Hell yeah brother |
| @@ -0,0 +1,1815 @@ | |||
| #! /bin/sh | |||
| @@ -0,0 +1,2354 @@ | |||
| #! /bin/sh | |||
There was a problem hiding this comment.
Actionable comments posted: 5
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@packages/buddy/build.sh`:
- Around line 1-4: Update the build scripts to use Bash strict mode: in
packages/buddy/build.sh, packages/libsigsegv/build.sh, and
packages/libtecla/build.sh, change the shebang to #!/bin/bash and set -euo
pipefail; in packages/maude/build.sh, retain the existing Bash shebang and
replace set -ex with set -euo pipefail.
In `@packages/maude/build.sh`:
- Around line 32-41: The smoke test in the build script must exercise prelude
loading rather than relying on maude --version. Replace the version invocation
and version grep with a small reduction command that requires the installed
prelude, capture its output and exit status, and assert the expected reduction
result so an incorrect MAUDE_LIB or missing prelude fails the build.
- Around line 10-30: Update packages/maude/build.sh (lines 10-30) to pass
--enable-deterministic-archives to configure and remove installed *.la files
after installation; update packages/libtecla/build.sh (lines 17-30) to pass the
same configure option. The sites packages/buddy/build.sh (lines 8-10) and
packages/libsigsegv/build.sh (lines 6-7) require no direct changes.
In `@packages/tamarin-prover/build.ncl`:
- Around line 1-7: Move the `let { Attrs, BuildSpec, Local, Needs, OutputBin,
Source, .. } = import "minimal.ncl" in` declaration to the first line of
`build.ncl`, before all header comments, while preserving the existing bindings
and import.
In `@packages/tamarin-prover/build.sh`:
- Around line 73-83: The build failure logging in the cabal build pipeline uses
the predictable /tmp/tam-build.log path, enabling symlink attacks. Update the
build flow around PIPESTATUS[0] to create a unique temporary log with mktemp,
use that path for tee, grep, and tail, and clean it up after the
failure-reporting logic completes.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: CHILL
Plan: Pro
Run ID: 86937223-5b18-4368-9880-c20bffc9ffc7
📒 Files selected for processing (13)
packages/buddy/build.nclpackages/buddy/build.shpackages/libsigsegv/build.nclpackages/libsigsegv/build.shpackages/libtecla/build.nclpackages/libtecla/build.shpackages/libtecla/config.guesspackages/libtecla/config.subpackages/maude/build.nclpackages/maude/build.shpackages/tamarin-prover/build.nclpackages/tamarin-prover/build.shpackages/tamarin-prover/fclabels-ghc910.patch
| #!/bin/sh | ||
| # BuDDy — standard automake, but the release tarball ships configure/install-sh | ||
| # WITHOUT the execute bit (noted in Maude's INSTALL), so restore it first. C++. | ||
| set -e |
There was a problem hiding this comment.
🩺 Stability & Availability | 🟡 Minor | ⚡ Quick win
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Inspect the relevant build scripts and any packaging guidance in the repo.
git ls-files 'packages/*/build.sh' 'README.md' '*.md' | sed -n '1,200p'
echo '--- buddy ---'
cat -n packages/buddy/build.sh
echo '--- libsigsegv ---'
cat -n packages/libsigsegv/build.sh
echo '--- libtecla ---'
cat -n packages/libtecla/build.sh
echo '--- maude ---'
cat -n packages/maude/build.shRepository: gominimal/pkgs
Length of output: 10540
Use Bash strict mode in these build scripts.
packages/buddy/build.sh#L1-L4,packages/libsigsegv/build.sh#L1-L4, andpackages/libtecla/build.sh#L1-L6: switch the shebang to#!/bin/bashand addset -euo pipefail.packages/maude/build.sh#L1-L8: keep Bash, but replaceset -exwithset -euo pipefail.
📍 Affects 4 files
packages/buddy/build.sh#L1-L4(this comment)packages/libsigsegv/build.sh#L1-L4packages/libtecla/build.sh#L1-L6packages/maude/build.sh#L1-L8
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@packages/buddy/build.sh` around lines 1 - 4, Update the build scripts to use
Bash strict mode: in packages/buddy/build.sh, packages/libsigsegv/build.sh, and
packages/libtecla/build.sh, change the shebang to #!/bin/bash and set -euo
pipefail; in packages/maude/build.sh, retain the existing Bash shebang and
replace set -ex with set -euo pipefail.
Source: Coding guidelines
| export CFLAGS="-O2 -pipe -fno-stack-protector -gno-record-gcc-switches -ffile-prefix-map=$(pwd)=/builddir" | ||
| export CXXFLAGS="$CFLAGS" | ||
| export LDFLAGS="-Wl,--build-id=none -L/usr/lib" | ||
| export CPPFLAGS="-I/usr/include" | ||
|
|
||
| # The tag archive has no generated ./configure — build it. | ||
| autoreconf -i | ||
|
|
||
| # Maude's configure defaults the link vars to the right DYNAMIC `-l` flags when | ||
| # they're unset — GMP_LIBS="-lgmpxx -lgmp", LIBSIGSEGV_LIB="-lsigsegv", | ||
| # BUDDY_LIB="-lbdd" — and AUTO-DETECTS TECLA_LIBS="-ltecla -lncurses" (tecla needs | ||
| # a terminfo lib; hardcoding "-ltecla" would drop it). So we pass none of them and | ||
| # just disable the SMT backends (not packaged). --enable-compiler is experimental | ||
| # and not needed for tamarin's use — leave it off (default). | ||
| ./configure \ | ||
| --prefix=/usr \ | ||
| --with-cvc4=no \ | ||
| --with-yices2=no | ||
|
|
||
| make -j"$(nproc)" | ||
| make DESTDIR="$OUTPUT_DIR" install |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟠 Major | ⚡ Quick win
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '\n== files ==\n'
git ls-files 'packages/*/build.sh' | sed -n '1,120p'
printf '\n== relevant snippets ==\n'
for f in packages/maude/build.sh packages/buddy/build.sh packages/libsigsegv/build.sh packages/libtecla/build.sh; do
echo "--- $f ---"
nl -ba "$f" | sed -n '1,120p'
done
printf '\n== search for ARFLAGS / deterministic archive settings ==\n'
rg -n "ARFLAGS|enable-deterministic-archives|\.la|DESTDIR|install_lib|install_inc" packages/{maude,buddy,libsigsegv,libtecla}/build.shRepository: gominimal/pkgs
Length of output: 3403
🏁 Script executed:
#!/bin/bash
set -euo pipefail
for f in packages/maude/build.sh packages/buddy/build.sh packages/libsigsegv/build.sh packages/libtecla/build.sh; do
echo "--- $f ---"
sed -n '1,140p' "$f" | cat -n
echo
done
printf '\n== matches ==\n'
rg -n "ARFLAGS|enable-deterministic-archives|\.la|DESTDIR|install_lib|install_inc" \
packages/maude/build.sh packages/buddy/build.sh packages/libsigsegv/build.sh packages/libtecla/build.shRepository: gominimal/pkgs
Length of output: 6239
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '\n== ARFLAGS usage in build scripts ==\n'
rg -n "ARFLAGS='Drc'|ARFLAGS=\"Drc\"|ARFLAGS=" packages/*/build.sh || true
printf '\n== deterministic archive flags in autotools builds ==\n'
rg -n --glob 'packages/*/build.sh' --glob '!packages/{maude,buddy,libsigsegv,libtecla}/build.sh' "enable-deterministic-archives" packages || trueRepository: gominimal/pkgs
Length of output: 1699
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '\n== ARFLAGS usage in build scripts ==\n'
rg -n "ARFLAGS='Drc'|ARFLAGS=\"Drc\"|ARFLAGS=" packages/*/build.sh || true
printf '\n== deterministic archive flags in autotools builds ==\n'
rg -n "enable-deterministic-archives" packages/*/build.sh || trueRepository: gominimal/pkgs
Length of output: 1830
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '\n== libtecla related files ==\n'
git ls-files 'packages/libtecla/*' | sed -n '1,120p'
printf '\n== maude / libtecla / buddy / libsigsegv build metadata ==\n'
for f in packages/maude/build.sh packages/libtecla/build.sh packages/buddy/build.sh packages/libsigsegv/build.sh; do
echo "--- $f ---"
rg -n "enable-deterministic-archives|ARFLAGS|\.la|install_lib|install_inc|libtool|shared|static" "$f" || true
doneRepository: gominimal/pkgs
Length of output: 1100
Add deterministic archive flags to the remaining autotools builds.
packages/maude/build.sh: pass--enable-deterministic-archivesand remove*.laafter install.packages/libtecla/build.sh: pass--enable-deterministic-archives.
📍 Affects 4 files
packages/maude/build.sh#L10-L30(this comment)packages/buddy/build.sh#L8-L10packages/libsigsegv/build.sh#L6-L7packages/libtecla/build.sh#L17-L30
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@packages/maude/build.sh` around lines 10 - 30, Update packages/maude/build.sh
(lines 10-30) to pass --enable-deterministic-archives to configure and remove
installed *.la files after installation; update packages/libtecla/build.sh
(lines 17-30) to pass the same configure option. The sites
packages/buddy/build.sh (lines 8-10) and packages/libsigsegv/build.sh (lines
6-7) require no direct changes.
Source: Coding guidelines
| # Smoke-test: maude's compiled-in prelude path is the runtime /usr/share (absent | ||
| # in the build sandbox), so point MAUDE_LIB at the freshly-installed share dir | ||
| # and REQUIRE a version print. The sandbox hides stdout, but a nonzero exit here | ||
| # fails the build — so this genuinely proves the binary links + finds its | ||
| # prelude, not just that `make install` ran. (#528) | ||
| export MAUDE_LIB="$OUTPUT_DIR/usr/share" | ||
| ver_out="$("$OUTPUT_DIR/usr/bin/maude" --version 2>&1 || true)" | ||
| echo "maude --version → $ver_out" | ||
| echo "$ver_out" | grep -qE "3\.5" \ | ||
| || { echo "smoke test FAILED: maude did not print its version (got: '$ver_out')" >&2; exit 1; } |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟠 Major | ⚡ Quick win
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
set -euo pipefail
printf '--- packages/maude/build.sh ---\n'
nl -ba packages/maude/build.sh | sed -n '1,120p'
printf '\n--- search for MAUDE_LIB / version smoke test references ---\n'
rg -n "MAUDE_LIB|--version|findPrelude|smoke test" packages/maude -S || trueRepository: gominimal/pkgs
Length of output: 243
🏁 Script executed:
#!/bin/bash
set -euo pipefail
echo '--- packages/maude/build.sh ---'
nl -ba packages/maude/build.sh | sed -n '1,140p'
echo
echo '--- search for MAUDE_LIB / version smoke test references ---'
rg -n "MAUDE_LIB|--version|findPrelude|smoke test" packages/maude -S || trueRepository: gominimal/pkgs
Length of output: 224
🌐 Web query:
Maude 3.5.1 src/Main/main.cc --version findPrelude MAUDE_LIB
💡 Result:
In Maude 3.5.1, the MAUDE_LIB environment variable is the standard mechanism used to specify the directory where the system searches for the prelude.maude file and other library files [1][2]. When the Maude interpreter starts, it searches for the required prelude file in the following locations, in order [1][3]: 1. The directories specified in the MAUDE_LIB environment variable [1][3]. 2. The directory containing the Maude executable [1]. 3. The current working directory [1]. If you are experiencing issues with finding the prelude, you can define MAUDE_LIB to point to the directory containing your prelude.maude file [2]. Regarding the command line syntax mentioned: - There is no standard command-line argument called --version or findPrelude in the Maude executable itself that outputs this information [4][1]. The Maude binary is typically invoked simply as maude [1][2]. - If you are writing C++ code and interacting with the Maude source code, the logic for locating the prelude is handled internally by the interpreter's initialization routines, which check these environment variables and directory paths [1][3]. - If you are using the Maude bindings (e.g., in Python), the library provides an init function where you can explicitly control whether the prelude is loaded using the loadPrelude parameter [5]. If you need to verify where your environment is looking, you can check the value of the environment variable in your terminal using the command echo $MAUDE_LIB [6]. If it is unset or incorrect, you can set it in your shell configuration (e.g., export MAUDE_LIB=/path/to/maude/lib) [2].
Citations:
- 1: https://maude.cs.illinois.edu/get-maude
- 2: https://lists.siebelschool.illinois.edu/lists/arc/maude-help/2007-09/msg00002.html
- 3: https://maude.lcc.uma.es/maude30-manual-html/maude-manualch2.html
- 4: https://maude.lcc.uma.es/maude-manual/
- 5: https://fadoss.github.io/maude-bindings/
- 6: https://lists.siebelschool.illinois.edu/lists/arc/maude-help/2020-03/msg00001.html
🏁 Script executed:
#!/bin/bash
set -euo pipefail
echo '--- packages/maude/build.sh ---'
cat -n packages/maude/build.sh | sed -n '1,160p'
echo
echo '--- search for MAUDE_LIB / version smoke test references ---'
rg -n "MAUDE_LIB|--version|findPrelude|smoke test|prelude" packages/maude -S || trueRepository: gominimal/pkgs
Length of output: 3140
🌐 Web query:
site:github.com/maude-lang/Maude main.cc --version findPrelude Maude3.5.1
💡 Result:
In the Maude source code, main.cc serves as the entry point for the Maude interpreter [1][2]. The internal function findPrelude is responsible for locating the standard prelude.maude file, which is essential for the initialization of the Maude environment. Regarding the command-line usage, Maude does not use the specific syntax main.cc --version to display version information. Instead, you can verify the version of the installed Maude interpreter by executing the maude command directly in your terminal, which typically displays the version banner upon startup, or by checking the release notes and documentation provided in the official repository [3][2][4]. Maude 3.5.1 is a released version of the software, as documented in the project's official GitHub repository [3][5].
Citations:
- 1: https://github.com/maude-lang/Maude/blob/master/INSTALL
- 2: https://github.com/maude-lang/Maude
- 3: https://github.com/maude-lang/Maude/releases/tag/Maude3.5.1
- 4: https://github.com/maude-lang/Maude/blob/master/README.md
- 5: https://github.com/maude-lang/Maude/blob/master/NEWS
🏁 Script executed:
#!/bin/bash
set -euo pipefail
sed -n '1,160p' packages/maude/build.shRepository: gominimal/pkgs
Length of output: 2119
Exercise a prelude-backed reduction here instead of --version. --version exits before the prelude lookup path, so MAUDE_LIB can be wrong and this smoke test can still pass. Run a small reduction that depends on the installed prelude and assert its output.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@packages/maude/build.sh` around lines 32 - 41, The smoke test in the build
script must exercise prelude loading rather than relying on maude --version.
Replace the version invocation and version grep with a small reduction command
that requires the installed prelude, capture its output and exit status, and
assert the expected reduction result so an incorrect MAUDE_LIB or missing
prelude fails the build.
| # Auto-bootstrapped from https://github.com/tamarin-prover/tamarin-prover. | ||
| # tamarin-prover is a Haskell binary (security-protocol verifier). Upstream pins | ||
| # GHC 9.6 (Stack LTS 22.x); minimal ships GHC 9.10.3. Its .cabal files carry NO | ||
| # upper version bounds, so we drive it with `cabal` + the system GHC and let the | ||
| # solver pick 9.10-compatible Hackage versions. Pioneering — upstream hasn't | ||
| # published a 9.10 build (pkgmgr-rs#528). | ||
| let { Attrs, BuildSpec, Local, Needs, OutputBin, Source, .. } = import "minimal.ncl" in |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win
Move the minimal.ncl import to the first line.
The required Nickel type import currently follows the header comments. As per coding guidelines, “Import Nickel types from minimal.ncl as the first line in build.ncl.”
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@packages/tamarin-prover/build.ncl` around lines 1 - 7, Move the `let { Attrs,
BuildSpec, Local, Needs, OutputBin, Source, .. } = import "minimal.ncl" in`
declaration to the first line of `build.ncl`, before all header comments, while
preserving the existing bindings and import.
Source: Coding guidelines
| set +e | ||
| cabal build exe:tamarin-prover \ | ||
| --with-compiler="$(command -v ghc)" \ | ||
| --jobs="$(nproc)" -v1 2>&1 | tee /tmp/tam-build.log | ||
| rc=${PIPESTATUS[0]} | ||
| set -e | ||
| if [ "$rc" -ne 0 ]; then | ||
| echo "===== cabal build failed (rc=$rc) — real error: =====" | ||
| grep -iE "\.hs:[0-9]+:[0-9]+: error|error:\s*\[GHC|undefined reference|cannot find -l|panic|internal error" /tmp/tam-build.log | tail -25 \ | ||
| || echo "(no error text captured)" | ||
| tail -25 /tmp/tam-build.log |
There was a problem hiding this comment.
🔒 Security & Privacy | 🟡 Minor | ⚡ Quick win
Use a unique build-log file.
A process able to create /tmp/tam-build.log before this pipeline can redirect tee through a symlink and overwrite a file writable by the build user. Use mktemp and clean up the generated log.
Proposed fix
+build_log="$(mktemp "${TMPDIR:-/tmp}/tam-build.XXXXXX")"
+trap 'rm -f "$build_log"' EXIT
set +e
cabal build exe:tamarin-prover \
--with-compiler="$(command -v ghc)" \
- --jobs="$(nproc)" -v1 2>&1 | tee /tmp/tam-build.log
+ --jobs="$(nproc)" -v1 2>&1 | tee "$build_log"
rc=${PIPESTATUS[0]}
set -e
if [ "$rc" -ne 0 ]; then
echo "===== cabal build failed (rc=$rc) — real error: ====="
- grep -iE "\.hs:[0-9]+:[0-9]+: error|error:\s*\[GHC|undefined reference|cannot find -l|panic|internal error" /tmp/tam-build.log | tail -25 \
+ grep -iE "\.hs:[0-9]+:[0-9]+: error|error:\s*\[GHC|undefined reference|cannot find -l|panic|internal error" "$build_log" | tail -25 \
|| echo "(no error text captured)"
- tail -25 /tmp/tam-build.log
+ tail -25 "$build_log"📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| set +e | |
| cabal build exe:tamarin-prover \ | |
| --with-compiler="$(command -v ghc)" \ | |
| --jobs="$(nproc)" -v1 2>&1 | tee /tmp/tam-build.log | |
| rc=${PIPESTATUS[0]} | |
| set -e | |
| if [ "$rc" -ne 0 ]; then | |
| echo "===== cabal build failed (rc=$rc) — real error: =====" | |
| grep -iE "\.hs:[0-9]+:[0-9]+: error|error:\s*\[GHC|undefined reference|cannot find -l|panic|internal error" /tmp/tam-build.log | tail -25 \ | |
| || echo "(no error text captured)" | |
| tail -25 /tmp/tam-build.log | |
| build_log="$(mktemp "${TMPDIR:-/tmp}/tam-build.XXXXXX")" | |
| trap 'rm -f "$build_log"' EXIT | |
| set +e | |
| cabal build exe:tamarin-prover \ | |
| --with-compiler="$(command -v ghc)" \ | |
| --jobs="$(nproc)" -v1 2>&1 | tee "$build_log" | |
| rc=${PIPESTATUS[0]} | |
| set -e | |
| if [ "$rc" -ne 0 ]; then | |
| echo "===== cabal build failed (rc=$rc) — real error: =====" | |
| grep -iE "\.hs:[0-9]+:[0-9]+: error|error:\s*\[GHC|undefined reference|cannot find -l|panic|internal error" "$build_log" | tail -25 \ | |
| || echo "(no error text captured)" | |
| tail -25 "$build_log" |
🧰 Tools
🪛 ast-grep (0.44.1)
[warning] 75-75: Writing to or reading from a hardcoded, predictable path under /tmp is vulnerable to symlink and TOCTOU attacks: a local attacker can pre-create the file (or a symlink pointing elsewhere) and hijack or corrupt the contents. Generate a unique, unpredictable temporary file with mktemp instead, e.g. tmpfile="$(mktemp)" (or mktemp -d for directories) and reference "$tmpfile".
Context: /tmp/tam-build.log
Note: [CWE-377] Insecure Temporary File.
(predictable-tmp-file-bash)
[warning] 80-80: Writing to or reading from a hardcoded, predictable path under /tmp is vulnerable to symlink and TOCTOU attacks: a local attacker can pre-create the file (or a symlink pointing elsewhere) and hijack or corrupt the contents. Generate a unique, unpredictable temporary file with mktemp instead, e.g. tmpfile="$(mktemp)" (or mktemp -d for directories) and reference "$tmpfile".
Context: /tmp/tam-build.log
Note: [CWE-377] Insecure Temporary File.
(predictable-tmp-file-bash)
[warning] 82-82: Writing to or reading from a hardcoded, predictable path under /tmp is vulnerable to symlink and TOCTOU attacks: a local attacker can pre-create the file (or a symlink pointing elsewhere) and hijack or corrupt the contents. Generate a unique, unpredictable temporary file with mktemp instead, e.g. tmpfile="$(mktemp)" (or mktemp -d for directories) and reference "$tmpfile".
Context: /tmp/tam-build.log
Note: [CWE-377] Insecure Temporary File.
(predictable-tmp-file-bash)
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@packages/tamarin-prover/build.sh` around lines 73 - 83, The build failure
logging in the cabal build pipeline uses the predictable /tmp/tam-build.log
path, enabling symlink attacks. Update the build flow around PIPESTATUS[0] to
create a unique temporary log with mktemp, use that path for tee, grep, and
tail, and clean it up after the failure-reporting logic completes.
Source: Linters/SAST tools
…x/ prefix PR review round on #449: - Fetch libtecla's config.guess/config.sub (2024 GNU config, ~4k lines) as sha256-pinned Sources instead of vendoring them — keeps the pair out of every consumer's checkout (@twitchyliquid64). Moved them + the Stackage LTS pin under a build-aux/ prefix in the mirror bucket so they don't clutter source tarballs. - Bash strict mode (#!/bin/bash + set -euo pipefail) across buddy, libsigsegv, libtecla, maude build.sh (CodeRabbit); maude drops set -ex. Maude chain rebuilds green with the fetched config + strict mode. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
|
What
Packages the Tamarin security-protocol verifier (
tamarin-prover1.12.0) andthe Maude rewriting engine it shells out to at runtime, plus Maude's three
C/C++ library dependencies. Five new packages:
tamarin-provermaudelibteclalibsigsegvbuddyRequested by Bryan (formal-methods tooling in minimal). See pkgmgr-rs#528.
tamarin-prover on GHC 9.10.3
Upstream pins GHC 9.6 (Stack LTS 22.x); minimal ships GHC 9.10.3, and
upstream has no published 9.10 build. Tamarin's
.cabalfiles carry no upperversion bounds, so we drive it with cabal + the system GHC and pin the whole
dependency solve to Stackage LTS 24.50 (= GHC 9.10.3 exactly) via an
imported
cabal.config. Three source-compat fixes were needed:(dormant since 2021, dropped from Stackage at 9.8→9.10).
Data/Label/Derive.hshits the template-haskell 2.22
TyVarBndrflag change (() → BndrVis); fixedwith a 6-line
dropBndrVisshim (fclabels-ghc910.patch), vendored viacabal get+ a localpackages:entry.import:ed as a Local file so the solver picks thecurated 9.10.3-compatible versions, rather than
allow-newer: all(whichgrabs incompatible bleeding-edge combos, e.g. yesod-static's crypton/memory).
src/Main/REPL.hs— a bare record-field import (maudePath) rejected byGHC 9.10 (GHC-61689); fixed to import via the type. Tamarin's
developbranch already made this exact change.
Maude backend
Maude (C++) is the rewriting-logic engine that is Tamarin's backend. It links
its library deps dynamically (minimal ships gmp/libsigsegv/libtecla/buddy
--disable-static, whereas Maude's INSTALL assumes static). gmp is already inminimal (
--enable-cxxprovideslibgmpxx). Notable per-dep bits:config.guess/config.sub— its bundled 2003copies predate aarch64 ("cannot guess build type").
autoreconfs the git tag archive (no generated./configure); needsm4in build_deps. SMT backends (CVC4/Yices2) disabled to start.Verification
minimal checkon aarch64 (parse / import-line / output-types/ enumerate-bins / missing-runtime_deps / standalone-tests / fmt).
maude --versionto print + find its prelude (a nonzero exit fails the build).--versionbanner).Reviewer notes (unresolved / deliberate)
source_provenance— upstream is an academic site(sites.astro.caltech.edu) with no git host or canonical release archive; the
tarball is mirrored to
gs://minimal-staging-archives. TODO if we want aprovenance category for it.
ftp.gnu.org / some codeload paths, so libsigsegv/buddy/libtecla/maude fetch
from
gs://minimal-staging-archives(same convention as the other ~319 pkgs).needs = { internet, dns }) — the Haskell build resolves deps from Hackage live, so thesource stays on the GitHub tag archive (pinned sha) rather than a mirror.
Tamarin doesn't require them for its core Maude path.
🤖 Generated with Claude Code
Summary by CodeRabbit