File tree Expand file tree Collapse file tree 1 file changed +2
-1
lines changed
1-runs/run-2024-03-31---06-37---tcg40 Expand file tree Collapse file tree 1 file changed +2
-1
lines changed Original file line number Diff line number Diff line change @@ -35,6 +35,7 @@ KINDS=("noreuse" "reuse")
35
35
36
36
for i in {0..1}; do
37
37
echo " @@@ ${KINDS[i]} BUILD @@@"
38
+ curl -d " Started[${KINDS[i]} ]. run:$EXPERIMENTDIR . machine:$( uname -a) ." ntfy.sh/xISSztEV8EoOchM2
38
39
mkdir -p builds/
39
40
git clone --depth 1 git@github.com:opencompl/lean4.git --branch ${COMMITS[i]} $EXPERIMENTDIR /builds/${KINDS[i]}
40
41
mkdir -p $EXPERIMENTDIR /builds/${KINDS[i]} /build/release/
@@ -53,6 +54,6 @@ for i in {0..1}; do
53
54
make -j10 stage2
54
55
touch $EXPERIMENTDIR /$CSVNAME && echo " " > $EXPERIMENTDIR /$CSVNAME
55
56
$TIME -v make -j10 stage3 2>&1 | tee " $EXPERIMENTDIR /time-${KINDS[i]} -stage3.txt"
56
- # cd stage3 && ctest -j32 --output-on-failure 2>&1 | tee "$EXPERIMENTDIR/ctest-${KINDS[i]}-stage3.txt" && cd ../
57
+ cd stage3 && ctest -E handleLocking -j32 --output-on-failure 2>&1 | tee " $EXPERIMENTDIR /ctest-${KINDS[i]} -stage3.txt" && cd ../
57
58
curl -d " Done[${KINDS[i]} ]. run:$EXPERIMENTDIR . machine:$( uname -a) ." ntfy.sh/xISSztEV8EoOchM2
58
59
done ;
You can’t perform that action at this time.
0 commit comments