refactor: install python requirements.txt in shell.nix

[alexkeizer]

No description provided.

[github-actions]

Alive Statistics: 90 / 93 (3 failed)

[github-actions]

bitwuzla proved and bv_decide failed theorem 3 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gexact_proof
bitwuzla proved and bv_decide failed theorem 6 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gexact_proof
bitwuzla proved and bv_decide failed theorem 14 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gdivhshift_proof
bitwuzla proved and bv_decide failed theorem 19 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gdivhshift_proof
bitwuzla proved and bv_decide failed theorem 51 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gdivhshift_proof
bitwuzla proved and bv_decide failed theorem 53 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gdivhshift_proof
bitwuzla proved and bv_decide failed theorem 3 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gdistribute_proof
bitwuzla proved and bv_decide failed theorem 4 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gdistribute_proof
bitwuzla proved and bv_decide failed theorem 12 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gnarrowhmath_proof
bitwuzla proved and bv_decide failed theorem 9 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gapinthsub_proof
bitwuzla proved and bv_decide failed theorem 1 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gapinthrem2_proof
bitwuzla proved and bv_decide failed theorem 38 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/grem_proof
bitwuzla proved and bv_decide failed theorem 1 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gadd4_proof
bitwuzla proved and bv_decide failed theorem 7 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gtrunc_proof
bitwuzla proved and bv_decide failed theorem 0 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/g2008h02h23hMulSub_proof
bitwuzla proved and bv_decide failed theorem 0 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/g2010h11h23hDistributed_proof
bitwuzla proved and bv_decide failed theorem 4 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gadd_or_sub_proof
bitwuzla proved and bv_decide failed theorem 15 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gshifthshift_proof
bitwuzla proved and bv_decide failed theorem 7 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gtrunchinseltpoison_proof
bitwuzla proved and bv_decide failed theorem 14 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gshlhfactor_proof
bitwuzla proved and bv_decide failed theorem 21 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/greassociatehnuw_proof
bitwuzla proved and bv_decide failed theorem 22 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/greassociatehnuw_proof
bitwuzla proved and bv_decide failed theorem 23 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/greassociatehnuw_proof
bitwuzla proved and bv_decide failed theorem 24 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/greassociatehnuw_proof
bitwuzla proved and bv_decide failed theorem 6 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gadd2_proof
bitwuzla proved and bv_decide failed theorem 5 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/g2012h08h28hudiv_ashl_proof
bitwuzla proved and bv_decide failed theorem 13 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gsubhxorhcmp_proof
bv_decide solved 7925 theorems.
bitwuzla solved 7952 theorems.
bv_decide found 0 counterexamples.
bitwuzla found 0 counterexamples.
bv_decide only failed on 27 problems.
bitwuzla only failed on 0 problems.
both bitwuzla and bv_decide failed on 26 problems.
In total, bitwuzla saw 7978 problems.
In total, bv_decide saw 7978 problems.
ran rg 'LeanSAT provided a counter' | wc -l, this file found 0, rg found 0, SUCCESS
ran rg 'Bitwuzla provided a counter' | wc -l, this file found 0, rg found 0, SUCCESS
ran rg 'LeanSAT proved' | wc -l, this file found 7925, rg found 0, FAIL
ran rg 'Bitwuzla proved' | wc -l, this file found 7952, rg found 0, FAIL
The InstCombine benchmark contains 4520 theorems in total.
Saved dataframe at: /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/raw-data/InstCombine/instcombine_ceg_data.csv
Saved dataframe at: /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/raw-data/InstCombine/instcombine_solved_data.csv