max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: replace sed with perl in test driver

Browse source 
Consistent across all three platforms
This commit is contained in:
Sebastian Ullrich 2021-09-16 17:58:50 +02:00
parent a7b044b80b
commit d65871241d
2 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
nix/bootstrap.nix
View file

@ -1,5 +1,5 @@
{ debug ? false, stage0debug ? false, extraCMakeFlags ? [],
stdenv, lib, cmake, gmp, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir,
stdenv, lib, cmake, gmp, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl,
... } @ args:
with builtins;
rec {
@ -122,6 +122,7 @@ rec {
test = buildCMake {
name = "lean-test-${desc}";
realSrc = lib.sourceByRegex ../. [ "src.*" "tests.*" ];
buildInputs = [ gmp perl ];
preConfigure = ''
cd src
'';

2
tests/common.sh
View file

@ -27,7 +27,7 @@ function compile_lean {
function exec_capture {
# mvar suffixes like in `?m.123` are deterministic but prone to change on minor changes, so strip them
"$@" 2>&1 | sed -E 's/(\?\w)\.[0-9]+/\1/g' > "$f.produced.out"
"$@" 2>&1 | perl -pe 's/(\?\w)\.[0-9]+/\1/g' > "$f.produced.out"
}
# Remark: `${var+x}` is a parameter expansion which evaluates to nothing if `var` is unset, and substitutes the string `x` otherwise.