add explicit goal selector (downstream from https://github.com/SkyLabsAI/auto/pull/445) - #175
Merged
Merged
Conversation
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | db1581e |
| fmdeps/BRiCk/ | main | e819c36 |
| fmdeps/auto-docs/ | main | 6490c5f |
| bluerock/NOVA/ | skylabs-proof | f3533d2 |
| bluerock/bhv/ | skylabs-main | e37df58 |
| fmdeps/ci/ | main | e1ec839 |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| vendored/rocq/ | skylabs-master | bef7df5 |
| fmdeps/rocq-agent-toolkit/ | main | 227bb83 |
| vendored/rocq-elpi/ | skylabs-master | 7dee592 |
| vendored/rocq-equations/ | skylabs-main | 9cf8471 |
| vendored/rocq-iris/ | skylabs-master | a7af9f7 |
| vendored/rocq-lsp/ | skylabs-main | 64ef78a |
| vendored/rocq-stdlib/ | skylabs-master | 00897b3 |
| vendored/rocq-stdpp/ | skylabs-master | 0c5e505 |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
Changes in Warnings or Errors
| Before | New | Fixed | After | |
|---|---|---|---|---|
| Errors | 0 | 0 | 1 | |
| Warnings | 91 | 0 | 0 | 91 |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -0.27% | 198220.5 | 197686.4 | -534.1 | total |
| -0.16% | 322.2 | - | -322.2 | ├ disappeared files (8) |
| -0.11% | 197898.3 | 197686.4 | -211.9 | └ common files |
| -0.00% | 53108.6 | 53108.6 | -0.0 | ├ translation units |
| -0.15% | 144789.8 | 144577.9 | -211.9 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -35.20% | 52.7 | 34.1 | -18.5 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/IntegerDivide_WhileTrueWithBreak.v |
| -12.38% | 17.0 | 14.9 | -2.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f1_proof.v |
| -11.95% | 19.0 | 16.7 | -2.3 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/member_pointer_operators.v |
| -11.94% | 19.0 | 16.7 | -2.3 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/variable_length_arrays.v |
| -7.05% | 20.6 | 19.2 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/assignment_operators_min_bool.v |
| -6.53% | 22.4 | 20.9 | -1.5 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/cstring/spec.v |
| -6.43% | 22.6 | 21.1 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f0_proof.v |
| -6.22% | 24.0 | 22.5 | -1.5 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/semaphore/test_cpp_proof.v |
| -6.08% | 18.9 | 17.8 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f1_proof.v |
| -5.83% | 22.3 | 21.0 | -1.3 | fmdeps/auto-docs/content/docs/debugging/main.v |
| -5.79% | 17.9 | 16.9 | -1.0 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/semaphore/spec.v |
| -5.73% | 24.8 | 23.4 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/sub_const.v |
| -5.40% | 26.9 | 25.4 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f3_proof.v |
| -5.38% | 19.4 | 18.3 | -1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_f0_proof.v |
| -5.36% | 27.3 | 25.8 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/constructor.v |
| -5.34% | 27.0 | 25.6 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f0_proof.v |
| -5.31% | 30.4 | 28.8 | -1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f1_proof.v |
| -5.28% | 19.9 | 18.8 | -1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f1_proof.v |
| -5.25% | 21.8 | 20.7 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/inherited_constructor.v |
| -5.25% | 28.1 | 26.6 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f0_proof.v |
| -5.18% | 20.1 | 19.0 | -1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_f0_proof.v |
| -5.16% | 20.4 | 19.3 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f2_proof.v |
| -5.13% | 20.9 | 19.8 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/normalization/test.v |
| -5.12% | 20.2 | 19.2 | -1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f1_proof.v |
| -5.11% | 20.6 | 19.5 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_f1_proof.v |
| -5.10% | 28.0 | 26.6 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/factor.v |
| -5.10% | 30.8 | 29.2 | -1.6 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/test_ssridents.v |
| -4.87% | 27.0 | 25.7 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f0_proof.v |
| -4.80% | 35.4 | 33.7 | -1.7 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/Fibonacci.v |
| -4.77% | 33.4 | 31.8 | -1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/xval_init_lval.v |
| -4.70% | 31.1 | 29.6 | -1.5 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/SumLocalArrayUsingRangeloop.v |
| -4.65% | 24.6 | 23.5 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/allocation_lambda_forms.v |
| -4.60% | 29.6 | 28.2 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f0_proof.v |
| -4.53% | 32.6 | 31.1 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/implicit_array_initialization.v |
| -4.49% | 32.5 | 31.0 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f3_proof.v |
| -4.42% | 32.2 | 30.7 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0099_cpp_f0_proof.v |
| -4.38% | 33.9 | 32.5 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/arrays.v |
| -4.07% | 34.3 | 32.9 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0098_cpp_f0_proof.v |
| -4.02% | 36.1 | 34.7 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/sem_const/constructor.v |
| -3.98% | 34.9 | 33.5 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/control_logical_forms.v |
| -3.83% | 37.3 | 35.8 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_f0_proof.v |
| -3.63% | 35.0 | 33.7 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/sizeof_alignof.v |
| -3.43% | 37.1 | 35.8 | -1.3 | fmdeps/auto-docs/content/docs/functions/verification.v |
| -3.43% | 44.5 | 43.0 | -1.5 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/SumUpToN_WhileTrueWithBreak.v |
| -3.34% | 32.0 | 31.0 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/destructuring/test.v |
| -3.31% | 37.8 | 36.6 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/smoke.v |
| -3.14% | 41.9 | 40.6 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/anyR_proof.v |
| -3.12% | 46.8 | 45.3 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f2_proof.v |
| -3.11% | 52.2 | 50.5 | -1.6 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayZeroInitialization.v |
| -3.07% | 46.7 | 45.2 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/inits/main_cpp_spec.v |
| -3.05% | 48.8 | 47.3 | -1.5 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/Power.v |
| -3.02% | 48.9 | 47.4 | -1.5 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/Factorial.v |
| -2.81% | 45.8 | 44.5 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/control_flow/main_cpp_spec.v |
| -2.80% | 40.3 | 39.2 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_casts.v |
| -2.76% | 41.8 | 40.7 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/int128/test.v |
| -2.69% | 43.3 | 42.1 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/bitwise_operators.v |
| -2.66% | 41.1 | 40.0 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/integral_casts.v |
| -2.65% | 50.5 | 49.2 | -1.3 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/SumUpToN.v |
| -2.54% | 451.3 | 439.9 | -11.4 | fmdeps/auto/brick_groundtruth/examples/loopsynth/downward_loop.v |
| -2.53% | 46.2 | 45.1 | -1.2 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/utility/test_cpp_proof.v |
| -2.38% | 48.3 | 47.1 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/auto_frac/anyR_proof.v |
| -2.29% | 50.4 | 49.3 | -1.2 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/proof/unique_lock.v |
| -2.28% | 49.0 | 47.9 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_unary_operators.v |
| -2.23% | 63.4 | 62.0 | -1.4 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/IntegerDivide.v |
| -2.22% | 58.8 | 57.5 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0076_cpp_f0_proof.v |
| -2.15% | 52.6 | 51.5 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/if_switch_initializers.v |
| -2.15% | 51.6 | 50.5 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/arithmetic_operators.v |
| -1.94% | 57.4 | 56.2 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/comma_operator.v |
| -1.93% | 59.1 | 58.0 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0088_cpp_main_proof.v |
| -1.91% | 57.3 | 56.2 | -1.1 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayZeroInitialization_DoWhile.v |
| -1.83% | 72.2 | 70.9 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_f3_proof.v |
| -1.77% | 65.0 | 63.8 | -1.2 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/DynamicArrayInitialization.v |
| -1.77% | 63.3 | 62.2 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/relational_operators.v |
| -1.76% | 60.4 | 59.3 | -1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/new/demo_cpp_proof.v |
| -1.75% | 61.7 | 60.6 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/wp_lval_op_assign_variants.v |
| -1.72% | 62.9 | 61.8 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/read_prim/read_cpp_proof.v |
| -1.69% | 139.5 | 137.2 | -2.4 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayReverseCopy.v |
| -1.57% | 71.1 | 70.0 | -1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/demo_cpp_proof.v |
| -1.51% | 68.8 | 67.8 | -1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f2_proof.v |
| -1.46% | 88.8 | 87.5 | -1.3 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/FindFirst_EarlyExit.v |
| -1.45% | 80.6 | 79.4 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0084_cpp_main_proof.v |
| -1.44% | 75.8 | 74.7 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/primitive_initialization.v |
| -1.43% | 95.4 | 94.0 | -1.4 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/Gcd.v |
| -1.42% | 78.4 | 77.3 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array_string_init/main_cpp_proof.v |
| -1.40% | 75.9 | 74.8 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0076_cpp_main_proof.v |
| -1.40% | 76.4 | 75.4 | -1.1 | fmdeps/auto-docs/content/demo/linked_list/linked_list_cpp_proof.v |
| -1.39% | 88.8 | 87.5 | -1.2 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/FindFirst_EarlyExitFromWhile.v |
| -1.34% | 78.9 | 77.9 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/pair_hpp_spec.v |
| -1.33% | 114.0 | 112.5 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/initialization_forms.v |
| -1.31% | 89.4 | 88.3 | -1.2 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/CountPositives.v |
| -1.30% | 905.1 | 893.3 | -11.8 | fmdeps/auto/brick_groundtruth/examples/loopsynth/za18_2.v |
| -1.30% | 86.1 | 85.0 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0099_cpp_main_proof.v |
| -1.26% | 79.4 | 78.4 | -1.0 | fmdeps/auto-docs/content/demo/forward_list_v1/test_cpp_proof.v |
| -1.26% | 86.4 | 85.3 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_main_proof.v |
| -1.18% | 92.3 | 91.2 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_binary_operators.v |
| -1.18% | 91.7 | 90.6 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_relational_operators.v |
| -1.17% | 138.4 | 136.8 | -1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_main_proof.v |
| -1.15% | 99.4 | 98.3 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/destructuring_declarations.v |
| -1.14% | 95.8 | 94.7 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/lambda_captures.v |
| -1.12% | 99.1 | 98.0 | -1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/mutex/guard_recursive_cpp_proof.v |
| -1.10% | 103.5 | 102.4 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/compound_assignment_increments.v |
| -1.01% | 112.6 | 111.5 | -1.1 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/FindMax.v |
| -1.00% | 135.7 | 134.3 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/unit_tests.v |
| -0.95% | 110.4 | 109.3 | -1.0 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayCopy_WhileTrueWithBreak.v |
| -0.91% | 171.0 | 169.4 | -1.6 | fmdeps/auto/brick_groundtruth/examples/loopsynth/replicate_example_0.v |
| -0.86% | 131.9 | 130.8 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_main_proof.v |
| -0.86% | 173.2 | 171.7 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_main_proof.v |
| -0.81% | 163.0 | 161.7 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_main_proof.v |
| -0.80% | 143.1 | 141.9 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/destructuring/test_pair.v |
| -0.76% | 191.6 | 190.1 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_main_proof.v |
| -0.70% | 152.3 | 151.2 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/splice_cpp_spec.v |
| -0.67% | 182.5 | 181.2 | -1.2 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/Factorial_longlong.v |
| -0.49% | 1808.1 | 1799.3 | -8.8 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/MultipleLoops.v |
| -0.49% | 234.0 | 232.9 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep_spec.v |
| -0.43% | 244.5 | 243.4 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0098_cpp_main_proof.v |
| -0.37% | 293.8 | 292.7 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arith_bug.v |
| -0.36% | 399.8 | 398.4 | -1.4 | fmdeps/auto/brick_groundtruth/examples/loopsynth/qtest_5_failure.v |
| -0.35% | 304.6 | 303.5 | -1.1 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_While.v |
| -0.32% | 349.6 | 348.5 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist/merge_cpp_proof.v |
| -0.32% | 397.6 | 396.4 | -1.3 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/joinpoint_tests.v |
| -0.29% | 511.6 | 510.2 | -1.5 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v |
| -0.28% | 503.1 | 501.7 | -1.4 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/vector/test_cpp_proof.v |
| -0.16% | 802.4 | 801.1 | -1.3 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/compare/test_cpp_proof.v |
| -0.15% | 831.9 | 830.7 | -1.2 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/compare/test_cpp_proof.v |
| -0.13% | 884.9 | 883.7 | -1.2 | fmdeps/auto/brick_groundtruth/examples/loopsynth/Exp1_0_failure.v |
| +0.22% | 873.5 | 875.4 | +1.9 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/identityloop.v |
| +0.47% | 309.5 | 311.0 | +1.5 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_zip.v |
| +0.58% | 289.7 | 291.4 | +1.7 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_WhileTrueWithBreak.v |
| +0.93% | 110.6 | 111.6 | +1.0 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayCopy.v |
| -0.27% | 198220.5 | 197686.4 | -534.1 | total |
| -0.16% | 322.2 | - | -322.2 | ├ disappeared files (8) |
| -0.11% | 197898.3 | 197686.4 | -211.9 | └ common files |
| -0.00% | 53108.6 | 53108.6 | -0.0 | ├ translation units |
| -0.15% | 144789.8 | 144577.9 | -211.9 | └ proofs and tests |
simon-skylabs
force-pushed
the
simon/prelude-goal-selector
branch
from
September 11, 2026 18:20
1016546 to
659ec59
Compare
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | db1581e |
| fmdeps/BRiCk/ | main | e819c36 |
| fmdeps/auto-docs/ | main | 6490c5f |
| bluerock/NOVA/ | skylabs-proof | f3533d2 |
| bluerock/bhv/ | skylabs-main | e37df58 |
| fmdeps/ci/ | main | e1ec839 |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| vendored/rocq/ | skylabs-master | bef7df5 |
| fmdeps/rocq-agent-toolkit/ | main | 227bb83 |
| vendored/rocq-elpi/ | skylabs-master | 7dee592 |
| vendored/rocq-equations/ | skylabs-main | 9cf8471 |
| vendored/rocq-iris/ | skylabs-master | a7af9f7 |
| vendored/rocq-lsp/ | skylabs-main | 64ef78a |
| vendored/rocq-stdlib/ | skylabs-master | 00897b3 |
| vendored/rocq-stdpp/ | skylabs-master | 0c5e505 |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
No Changes in Warnings or Errors
| Before | New | Fixed | After | |
|---|---|---|---|---|
| Errors | 0 | 0 | 0 | 0 |
| Warnings | 91 | 0 | 0 | 91 |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -0.11% | 198220.5 | 198008.6 | -211.9 | total |
| +0.00% | 53108.6 | 53108.6 | +0.0 | ├ translation units |
| -0.15% | 145111.9 | 144900.0 | -211.9 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -35.20% | 52.7 | 34.1 | -18.5 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/IntegerDivide_WhileTrueWithBreak.v |
| -12.38% | 17.0 | 14.9 | -2.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f1_proof.v |
| -11.95% | 19.0 | 16.7 | -2.3 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/member_pointer_operators.v |
| -11.94% | 19.0 | 16.7 | -2.3 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/variable_length_arrays.v |
| -7.05% | 20.6 | 19.2 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/assignment_operators_min_bool.v |
| -6.53% | 22.4 | 20.9 | -1.5 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/cstring/spec.v |
| -6.43% | 22.6 | 21.1 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f0_proof.v |
| -6.22% | 24.0 | 22.5 | -1.5 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/semaphore/test_cpp_proof.v |
| -6.08% | 18.9 | 17.8 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f1_proof.v |
| -5.83% | 22.3 | 21.0 | -1.3 | fmdeps/auto-docs/content/docs/debugging/main.v |
| -5.79% | 17.9 | 16.9 | -1.0 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/semaphore/spec.v |
| -5.73% | 24.8 | 23.4 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/sub_const.v |
| -5.40% | 26.9 | 25.4 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f3_proof.v |
| -5.38% | 19.4 | 18.3 | -1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_f0_proof.v |
| -5.36% | 27.3 | 25.8 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/constructor.v |
| -5.34% | 27.0 | 25.6 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f0_proof.v |
| -5.31% | 30.4 | 28.8 | -1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f1_proof.v |
| -5.28% | 19.9 | 18.8 | -1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f1_proof.v |
| -5.25% | 21.8 | 20.7 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/inherited_constructor.v |
| -5.25% | 28.1 | 26.6 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f0_proof.v |
| -5.18% | 20.1 | 19.0 | -1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_f0_proof.v |
| -5.16% | 20.4 | 19.3 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f2_proof.v |
| -5.13% | 20.9 | 19.8 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/normalization/test.v |
| -5.12% | 20.2 | 19.2 | -1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f1_proof.v |
| -5.11% | 20.6 | 19.5 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_f1_proof.v |
| -5.10% | 28.0 | 26.6 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/factor.v |
| -5.10% | 30.8 | 29.2 | -1.6 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/test_ssridents.v |
| -4.87% | 27.0 | 25.7 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f0_proof.v |
| -4.80% | 35.4 | 33.7 | -1.7 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/Fibonacci.v |
| -4.77% | 33.4 | 31.8 | -1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/xval_init_lval.v |
| -4.70% | 31.1 | 29.6 | -1.5 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/SumLocalArrayUsingRangeloop.v |
| -4.65% | 24.6 | 23.5 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/allocation_lambda_forms.v |
| -4.60% | 29.6 | 28.2 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f0_proof.v |
| -4.53% | 32.6 | 31.1 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/implicit_array_initialization.v |
| -4.49% | 32.5 | 31.0 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f3_proof.v |
| -4.42% | 32.2 | 30.7 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0099_cpp_f0_proof.v |
| -4.38% | 33.9 | 32.5 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/arrays.v |
| -4.07% | 34.3 | 32.9 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0098_cpp_f0_proof.v |
| -4.02% | 36.1 | 34.7 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/sem_const/constructor.v |
| -3.98% | 34.9 | 33.5 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/control_logical_forms.v |
| -3.83% | 37.3 | 35.8 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_f0_proof.v |
| -3.63% | 35.0 | 33.7 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/sizeof_alignof.v |
| -3.43% | 37.1 | 35.8 | -1.3 | fmdeps/auto-docs/content/docs/functions/verification.v |
| -3.43% | 44.5 | 43.0 | -1.5 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/SumUpToN_WhileTrueWithBreak.v |
| -3.34% | 32.0 | 31.0 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/destructuring/test.v |
| -3.31% | 37.8 | 36.6 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/smoke.v |
| -3.14% | 41.9 | 40.6 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/anyR_proof.v |
| -3.12% | 46.8 | 45.3 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f2_proof.v |
| -3.11% | 52.2 | 50.5 | -1.6 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayZeroInitialization.v |
| -3.07% | 46.7 | 45.2 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/inits/main_cpp_spec.v |
| -3.05% | 48.8 | 47.3 | -1.5 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/Power.v |
| -3.02% | 48.9 | 47.4 | -1.5 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/Factorial.v |
| -2.81% | 45.8 | 44.5 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/control_flow/main_cpp_spec.v |
| -2.80% | 40.3 | 39.2 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_casts.v |
| -2.76% | 41.8 | 40.7 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/int128/test.v |
| -2.69% | 43.3 | 42.1 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/bitwise_operators.v |
| -2.66% | 41.1 | 40.0 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/integral_casts.v |
| -2.65% | 50.5 | 49.2 | -1.3 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/SumUpToN.v |
| -2.54% | 451.3 | 439.9 | -11.4 | fmdeps/auto/brick_groundtruth/examples/loopsynth/downward_loop.v |
| -2.53% | 46.2 | 45.1 | -1.2 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/utility/test_cpp_proof.v |
| -2.38% | 48.3 | 47.1 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/auto_frac/anyR_proof.v |
| -2.29% | 50.4 | 49.3 | -1.2 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/proof/unique_lock.v |
| -2.28% | 49.0 | 47.9 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_unary_operators.v |
| -2.23% | 63.4 | 62.0 | -1.4 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/IntegerDivide.v |
| -2.22% | 58.8 | 57.5 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0076_cpp_f0_proof.v |
| -2.15% | 52.6 | 51.5 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/if_switch_initializers.v |
| -2.15% | 51.6 | 50.5 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/arithmetic_operators.v |
| -1.94% | 57.4 | 56.2 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/comma_operator.v |
| -1.93% | 59.1 | 58.0 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0088_cpp_main_proof.v |
| -1.91% | 57.3 | 56.2 | -1.1 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayZeroInitialization_DoWhile.v |
| -1.83% | 72.2 | 70.9 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_f3_proof.v |
| -1.77% | 65.0 | 63.8 | -1.2 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/DynamicArrayInitialization.v |
| -1.77% | 63.3 | 62.2 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/relational_operators.v |
| -1.76% | 60.4 | 59.3 | -1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/new/demo_cpp_proof.v |
| -1.75% | 61.7 | 60.6 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/wp_lval_op_assign_variants.v |
| -1.72% | 62.9 | 61.8 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/read_prim/read_cpp_proof.v |
| -1.69% | 139.5 | 137.2 | -2.4 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayReverseCopy.v |
| -1.57% | 71.1 | 70.0 | -1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/demo_cpp_proof.v |
| -1.51% | 68.8 | 67.8 | -1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f2_proof.v |
| -1.46% | 88.8 | 87.5 | -1.3 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/FindFirst_EarlyExit.v |
| -1.45% | 80.6 | 79.4 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0084_cpp_main_proof.v |
| -1.44% | 75.8 | 74.7 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/primitive_initialization.v |
| -1.43% | 95.4 | 94.0 | -1.4 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/Gcd.v |
| -1.42% | 78.4 | 77.3 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array_string_init/main_cpp_proof.v |
| -1.40% | 75.9 | 74.8 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0076_cpp_main_proof.v |
| -1.40% | 76.4 | 75.4 | -1.1 | fmdeps/auto-docs/content/demo/linked_list/linked_list_cpp_proof.v |
| -1.39% | 88.8 | 87.5 | -1.2 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/FindFirst_EarlyExitFromWhile.v |
| -1.34% | 78.9 | 77.9 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/pair_hpp_spec.v |
| -1.33% | 114.0 | 112.5 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/initialization_forms.v |
| -1.31% | 89.4 | 88.3 | -1.2 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/CountPositives.v |
| -1.30% | 905.1 | 893.3 | -11.8 | fmdeps/auto/brick_groundtruth/examples/loopsynth/za18_2.v |
| -1.30% | 86.1 | 85.0 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0099_cpp_main_proof.v |
| -1.26% | 79.4 | 78.4 | -1.0 | fmdeps/auto-docs/content/demo/forward_list_v1/test_cpp_proof.v |
| -1.26% | 86.4 | 85.3 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_main_proof.v |
| -1.18% | 92.3 | 91.2 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_binary_operators.v |
| -1.18% | 91.7 | 90.6 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_relational_operators.v |
| -1.17% | 138.4 | 136.8 | -1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_main_proof.v |
| -1.15% | 99.4 | 98.3 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/destructuring_declarations.v |
| -1.14% | 95.8 | 94.7 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/lambda_captures.v |
| -1.12% | 99.1 | 98.0 | -1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/mutex/guard_recursive_cpp_proof.v |
| -1.10% | 103.5 | 102.4 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/compound_assignment_increments.v |
| -1.01% | 112.6 | 111.5 | -1.1 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/FindMax.v |
| -1.00% | 135.7 | 134.3 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/unit_tests.v |
| -0.95% | 110.4 | 109.3 | -1.0 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayCopy_WhileTrueWithBreak.v |
| -0.91% | 171.0 | 169.4 | -1.6 | fmdeps/auto/brick_groundtruth/examples/loopsynth/replicate_example_0.v |
| -0.86% | 131.9 | 130.8 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_main_proof.v |
| -0.86% | 173.2 | 171.7 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_main_proof.v |
| -0.81% | 163.0 | 161.7 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_main_proof.v |
| -0.80% | 143.1 | 141.9 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/destructuring/test_pair.v |
| -0.76% | 191.6 | 190.1 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_main_proof.v |
| -0.70% | 152.3 | 151.2 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/splice_cpp_spec.v |
| -0.67% | 182.5 | 181.2 | -1.2 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/Factorial_longlong.v |
| -0.49% | 1808.1 | 1799.3 | -8.8 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/MultipleLoops.v |
| -0.49% | 234.0 | 232.9 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep_spec.v |
| -0.43% | 244.5 | 243.4 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0098_cpp_main_proof.v |
| -0.37% | 293.8 | 292.7 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arith_bug.v |
| -0.36% | 399.8 | 398.4 | -1.4 | fmdeps/auto/brick_groundtruth/examples/loopsynth/qtest_5_failure.v |
| -0.35% | 304.6 | 303.5 | -1.1 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_While.v |
| -0.32% | 349.6 | 348.5 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist/merge_cpp_proof.v |
| -0.32% | 397.6 | 396.4 | -1.3 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/joinpoint_tests.v |
| -0.29% | 511.6 | 510.2 | -1.5 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v |
| -0.28% | 503.1 | 501.7 | -1.4 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/vector/test_cpp_proof.v |
| -0.16% | 802.4 | 801.1 | -1.3 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/compare/test_cpp_proof.v |
| -0.15% | 831.9 | 830.7 | -1.2 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/compare/test_cpp_proof.v |
| -0.13% | 884.9 | 883.7 | -1.2 | fmdeps/auto/brick_groundtruth/examples/loopsynth/Exp1_0_failure.v |
| +0.22% | 873.5 | 875.4 | +1.9 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/identityloop.v |
| +0.47% | 309.5 | 311.0 | +1.5 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_zip.v |
| +0.58% | 289.7 | 291.4 | +1.7 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_WhileTrueWithBreak.v |
| +0.93% | 110.6 | 111.6 | +1.0 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayCopy.v |
| -0.11% | 198220.5 | 198008.6 | -211.9 | total |
| +0.00% | 53108.6 | 53108.6 | +0.0 | ├ translation units |
| -0.15% | 145111.9 | 144900.0 | -211.9 | └ proofs and tests |
simon-skylabs
force-pushed
the
simon/prelude-goal-selector
branch
from
September 16, 2026 20:16
659ec59 to
dcbfbdf
Compare
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | d0ca455 |
| fmdeps/BRiCk/ | main | 73a6aa6 |
| fmdeps/auto-docs/ | main | 9914064 |
| bluerock/NOVA/ | skylabs-proof | 948378b |
| bluerock/bhv/ | skylabs-main | 3506c0b |
| fmdeps/ci/ | main | c25c8df |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| vendored/rocq/ | skylabs-master | bef7df5 |
| fmdeps/rocq-agent-toolkit/ | main | 1e0e853 |
| vendored/rocq-elpi/ | skylabs-master | 7dee592 |
| vendored/rocq-equations/ | skylabs-main | 9cf8471 |
| vendored/rocq-iris/ | skylabs-master | a7af9f7 |
| vendored/rocq-lsp/ | skylabs-main | 64ef78a |
| vendored/rocq-stdlib/ | skylabs-master | 00897b3 |
| vendored/rocq-stdpp/ | skylabs-master | 0c5e505 |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
No Changes in Warnings or Errors
| Before | New | Fixed | After | |
|---|---|---|---|---|
| Errors | 0 | 0 | 0 | 0 |
| Warnings | 81 | 0 | 0 | 81 |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -0.10% | 199148.4 | 198945.4 | -202.9 | total |
| +0.00% | 53307.9 | 53307.9 | +0.0 | ├ translation units |
| -0.14% | 145840.5 | 145637.6 | -202.9 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -12.24% | 17.0 | 14.9 | -2.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f1_proof.v |
| -11.91% | 19.0 | 16.7 | -2.3 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/member_pointer_operators.v |
| -11.88% | 19.0 | 16.8 | -2.3 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/variable_length_arrays.v |
| -6.86% | 20.6 | 19.2 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/assignment_operators_min_bool.v |
| -6.52% | 22.4 | 20.9 | -1.5 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/cstring/spec.v |
| -6.36% | 22.7 | 21.3 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f0_proof.v |
| -6.19% | 23.7 | 22.3 | -1.5 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/g4g/N4_sum.v |
| -6.14% | 24.1 | 22.6 | -1.5 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/semaphore/test_cpp_proof.v |
| -6.10% | 22.7 | 21.4 | -1.4 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/g4g_trace/N4_sum.v |
| -6.03% | 19.0 | 17.8 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f1_proof.v |
| -5.81% | 17.9 | 16.9 | -1.0 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/semaphore/spec.v |
| -5.75% | 24.9 | 23.5 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/sub_const.v |
| -5.57% | 298.5 | 281.9 | -16.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arith_bug.v |
| -5.38% | 27.5 | 26.0 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/constructor.v |
| -5.36% | 27.0 | 25.6 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f3_proof.v |
| -5.33% | 19.4 | 18.4 | -1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_f0_proof.v |
| -5.28% | 27.2 | 25.8 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f0_proof.v |
| -5.25% | 21.9 | 20.7 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/inherited_constructor.v |
| -5.24% | 30.6 | 29.0 | -1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f1_proof.v |
| -5.22% | 28.3 | 26.8 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f0_proof.v |
| -5.19% | 19.9 | 18.9 | -1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f1_proof.v |
| -5.15% | 21.0 | 19.9 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/normalization/test.v |
| -5.13% | 20.4 | 19.4 | -1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f2_proof.v |
| -5.10% | 20.1 | 19.1 | -1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_f0_proof.v |
| -5.09% | 20.3 | 19.3 | -1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f1_proof.v |
| -5.07% | 20.6 | 19.6 | -1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_f1_proof.v |
| -4.92% | 29.6 | 28.1 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/factor.v |
| -4.83% | 27.1 | 25.8 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f0_proof.v |
| -4.75% | 33.7 | 32.1 | -1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/xval_init_lval.v |
| -4.61% | 32.3 | 30.8 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/implicit_array_initialization.v |
| -4.54% | 32.1 | 30.6 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0099_cpp_f0_proof.v |
| -4.51% | 29.3 | 27.9 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f0_proof.v |
| -4.47% | 32.7 | 31.3 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f3_proof.v |
| -4.37% | 33.7 | 32.2 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/arrays.v |
| -4.32% | 34.1 | 32.6 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0098_cpp_f0_proof.v |
| -4.18% | 29.5 | 28.3 | -1.2 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/test_ssridents.v |
| -4.14% | 36.0 | 34.5 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_f0_proof.v |
| -4.03% | 36.1 | 34.6 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/sem_const/constructor.v |
| -4.03% | 30.1 | 28.9 | -1.2 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/SumLocalArrayUsingRangeloop.v |
| -3.97% | 30.9 | 29.6 | -1.2 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/g4g/N4_sum_a.v |
| -3.91% | 35.3 | 33.9 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/control_logical_forms.v |
| -3.89% | 29.6 | 28.5 | -1.2 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/g4g_trace/N4_sum_a.v |
| -3.74% | 35.1 | 33.8 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/sizeof_alignof.v |
| -3.38% | 41.0 | 39.6 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/anyR_proof.v |
| -3.37% | 38.2 | 36.9 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/smoke.v |
| -3.34% | 32.3 | 31.2 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/destructuring/test.v |
| -3.29% | 469.7 | 454.3 | -15.5 | fmdeps/auto/brick_groundtruth/examples/loopsynth/downward_loop.v |
| -3.06% | 47.5 | 46.0 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/inits/main_cpp_spec.v |
| -2.90% | 45.5 | 44.2 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f2_proof.v |
| -2.85% | 46.3 | 45.0 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/control_flow/main_cpp_spec.v |
| -2.82% | 41.6 | 40.4 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/integral_casts.v |
| -2.81% | 40.9 | 39.8 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_casts.v |
| -2.74% | 42.2 | 41.0 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/int128/test.v |
| -2.66% | 43.7 | 42.5 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/bitwise_operators.v |
| -2.63% | 44.6 | 43.4 | -1.2 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/SumUpToN_WhileTrueWithBreak.v |
| -2.58% | 43.7 | 42.5 | -1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/g4g_trace/N12_area.v |
| -2.54% | 56.4 | 55.0 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0076_cpp_f0_proof.v |
| -2.53% | 46.8 | 45.6 | -1.2 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/utility/test_cpp_proof.v |
| -2.45% | 46.9 | 45.7 | -1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/g4g/N12_area.v |
| -2.43% | 50.7 | 49.5 | -1.2 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/proof/unique_lock.v |
| -2.38% | 48.7 | 47.5 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/auto_frac/anyR_proof.v |
| -2.35% | 50.5 | 49.3 | -1.2 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/SumUpToN.v |
| -2.29% | 49.6 | 48.4 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_unary_operators.v |
| -2.21% | 49.0 | 47.9 | -1.1 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/Power.v |
| -2.17% | 52.1 | 51.0 | -1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/g4g_trace/N5_swap.v |
| -2.16% | 53.2 | 52.1 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/if_switch_initializers.v |
| -2.12% | 53.2 | 52.1 | -1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/g4g_trace/N5_swap_a.v |
| -2.07% | 52.2 | 51.1 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/arithmetic_operators.v |
| -2.05% | 60.6 | 59.4 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/wp_lval_op_assign_variants.v |
| -2.03% | 51.6 | 50.6 | -1.0 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/proof/unique_lock_recursive_mutex.v |
| -1.96% | 57.4 | 56.3 | -1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/g4g_trace/N6_print_sizeof.v |
| -1.94% | 58.1 | 56.9 | -1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/g4g/N5_swap.v |
| -1.92% | 59.9 | 58.8 | -1.2 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/new/demo_cpp_proof.v |
| -1.89% | 71.9 | 70.5 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_f3_proof.v |
| -1.88% | 59.7 | 58.6 | -1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/g4g/N5_swap_a.v |
| -1.87% | 60.2 | 59.1 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0088_cpp_main_proof.v |
| -1.86% | 58.1 | 57.0 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/comma_operator.v |
| -1.79% | 62.9 | 61.8 | -1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/g4g/N6_print_sizeof.v |
| -1.78% | 65.2 | 64.0 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f2_proof.v |
| -1.77% | 64.2 | 63.1 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/relational_operators.v |
| -1.71% | 64.2 | 63.1 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/read_prim/read_cpp_proof.v |
| -1.56% | 71.6 | 70.5 | -1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/demo_cpp_proof.v |
| -1.52% | 77.6 | 76.4 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array_string_init/main_cpp_proof.v |
| -1.43% | 77.3 | 76.2 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0076_cpp_main_proof.v |
| -1.42% | 78.0 | 76.9 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/primitive_initialization.v |
| -1.38% | 76.8 | 75.8 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0084_cpp_main_proof.v |
| -1.38% | 87.4 | 86.2 | -1.2 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/initializer_list/test_cpp_proof.v |
| -1.35% | 850.1 | 838.6 | -11.5 | fmdeps/auto/brick_groundtruth/examples/loopsynth/za18_2.v |
| -1.33% | 82.7 | 81.6 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0099_cpp_main_proof.v |
| -1.32% | 79.5 | 78.4 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/pair_hpp_spec.v |
| -1.31% | 117.7 | 116.1 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/initialization_forms.v |
| -1.25% | 88.1 | 87.0 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_main_proof.v |
| -1.21% | 121.1 | 119.6 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_main_proof.v |
| -1.17% | 93.1 | 92.0 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_relational_operators.v |
| -1.17% | 93.5 | 92.5 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_binary_operators.v |
| -1.17% | 99.9 | 98.7 | -1.2 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/mutex/guard_recursive_cpp_proof.v |
| -1.16% | 90.2 | 89.2 | -1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_main_proof.v |
| -1.14% | 130.6 | 129.1 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_main_proof.v |
| -1.14% | 97.1 | 96.0 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/lambda_captures.v |
| -1.12% | 98.9 | 97.8 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/destructuring_declarations.v |
| -1.07% | 155.5 | 153.8 | -1.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_main_proof.v |
| -1.03% | 132.9 | 131.6 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/unit_tests.v |
| -1.02% | 104.1 | 103.1 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/compound_assignment_increments.v |
| -0.83% | 179.2 | 177.7 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_main_proof.v |
| -0.81% | 162.7 | 161.3 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_main_proof.v |
| -0.79% | 144.5 | 143.4 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/destructuring/test_pair.v |
| -0.77% | 154.9 | 153.7 | -1.2 | fmdeps/auto/brick_groundtruth/examples/loopsynth/replicate_example_0.v |
| -0.71% | 153.9 | 152.8 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/splice_cpp_spec.v |
| -0.64% | 220.2 | 218.8 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0098_cpp_main_proof.v |
| -0.53% | 273.4 | 271.9 | -1.4 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/SubArrays.v |
| -0.47% | 233.9 | 232.8 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep_spec.v |
| -0.37% | 330.3 | 329.1 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_main_proof.v |
| -0.34% | 353.3 | 352.1 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist/merge_cpp_proof.v |
| -0.32% | 513.9 | 512.2 | -1.6 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v |
| -0.27% | 506.8 | 505.4 | -1.3 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/vector/test_cpp_proof.v |
| -0.25% | 528.2 | 526.9 | -1.3 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/cstring/proof.v |
| -0.19% | 1585.3 | 1582.4 | -2.9 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/MultipleLoops.v |
| -0.17% | 819.3 | 817.9 | -1.4 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/compare/test_cpp_proof.v |
| -0.16% | 848.8 | 847.5 | -1.3 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/compare/test_cpp_proof.v |
| +0.48% | 280.5 | 281.9 | +1.4 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_zip.v |
| +1.21% | 123.8 | 125.3 | +1.5 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/CountPositives_DoWhile.v |
| +2.30% | 47.5 | 48.6 | +1.1 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/Power_WhileTrueWithBreak.v |
| -0.10% | 199148.4 | 198945.4 | -202.9 | total |
| +0.00% | 53307.9 | 53307.9 | +0.0 | ├ translation units |
| -0.14% | 145840.5 | 145637.6 | -202.9 | └ proofs and tests |
rlepigre-skylabs-ai
approved these changes
Sep 17, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.