Using awk to randomly sample a file

Create a file with 1000 lines:

for i in {1..1000};do echo $i; done > f


export P=0.5
cat f | awk -v p=$P 'BEGIN{srand()} {r = rand(); if (r <= p) print}'