Repository navigation
spec for thread creation with pthread.h - #186
Open
simon-skylabs wants to merge 31 commits into
Open
simon-skylabs wants to merge 31 commits into
simon-skylabs wants to merge 31 commits into
Conversation
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | f6f58f7 |
| fmdeps/BRiCk/ | main | 8986f99 |
| fmdeps/auto/ | main | c586fe2 |
| fmdeps/auto-docs/ | main | 8b76de6 |
| bluerock/NOVA/ | skylabs-proof | 906d2ed |
| bluerock/bhv/ | skylabs-main | 38a3f03 |
| 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 |
| fmdeps/skylabs-fm/ | main | 2bd0ed5 |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
Changes in Warnings or Errors
| Before | New | Fixed | After | |
|---|---|---|---|---|
| Errors | 0 | 0 | 1 | |
| Warnings | 78 | 0 | 0 | 78 |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +1.87% | 198892.1 | 202611.3 | +3719.2 | total |
| +1.84% | - | 3719.2 | +3719.2 | ├ newly appeared files (4) |
| -0.00% | 198892.1 | 198892.1 | -0.0 | └ common files |
| -0.00% | 53317.9 | 53317.9 | -0.0 | ├ translation units |
| +0.00% | 145574.3 | 145574.3 | +0.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +1.87% | 198892.1 | 202611.3 | +3719.2 | total |
| +1.84% | - | 3719.2 | +3719.2 | ├ newly appeared files (4) |
| -0.00% | 198892.1 | 198892.1 | -0.0 | └ common files |
| -0.00% | 53317.9 | 53317.9 | -0.0 | ├ translation units |
| +0.00% | 145574.3 | 145574.3 | +0.0 | └ proofs and tests |
pgiarrusso-sl
requested changes
Sep 22, 2026
pgiarrusso-sl
left a comment
pgiarrusso-sl
left a comment
Contributor
There was a problem hiding this comment.
Here is an incomplete review. But TLDR: this isn't ready yet to read.
added 16 commits
October 4, 2026 01:22
simon-skylabs
force-pushed
the
simon/thread-spec
branch
from
October 5, 2026 05:56
74023cc to
1014f2a
Compare
simon-skylabs
changed the title
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | d480d67 |
| fmdeps/auto-docs/ | main | 41a7a97 |
| bluerock/NOVA/ | skylabs-proof | b83447d |
| bluerock/bhv/ | skylabs-main | 48a669b |
| fmdeps/brick-libgtest/ | main | aeeddad |
| fmdeps/ci/ | main | 7d6ce12 |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| vendored/rocq/ | skylabs-master | fcb26f5 |
| fmdeps/rocq-agent-toolkit/ | main | f8a45cb |
| 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 |
| fmdeps/skylabs-fm/ | main | 457ecfd |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
Changes in Warnings or Errors
| Before | New | Fixed | After | |
|---|---|---|---|---|
| Errors | 0 | 0 | 4 | |
| Warnings | 73 | 73 |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -0.19% | 193903.1 | 193528.1 | -375.0 | total |
| -0.27% | 515.0 | - | -515.0 | ├ disappeared files (5) |
| +0.10% | - | 189.1 | +189.1 | ├ newly appeared files (9) |
| -0.03% | 193388.1 | 193339.0 | -49.1 | └ common files |
| +0.01% | 53049.8 | 53054.7 | +4.9 | ├ translation units |
| -0.04% | 140338.3 | 140284.3 | -54.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -16.78% | 371.9 | 309.5 | -62.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arith_bug.v |
| -10.66% | 18.5 | 16.5 | -2.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/fixed-regression-tests/type_ptr_size_ref/ref_prim_size.v |
| -4.99% | 23.2 | 22.1 | -1.2 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/cstring/spec.v |
| -4.69% | 212.3 | 202.4 | -10.0 | fmdeps/auto/rocq-skylabs-auto-core/tests/subgoals.v |
| -4.53% | 60.3 | 57.6 | -2.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/micromega/micromega1.v |
| -0.91% | 146.5 | 145.2 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/atomic_exchange_void/atomic_exchange_void.v |
| -0.86% | 244.7 | 242.6 | -2.1 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/SubArrays.v |
| -0.60% | 243.7 | 242.3 | -1.5 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_While.v |
| -0.48% | 242.5 | 241.3 | -1.2 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays.v |
| -0.46% | 230.8 | 229.7 | -1.1 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_WhileTrueWithBreak.v |
| -0.18% | 709.3 | 708.0 | -1.3 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/cctype/proof.v |
| -0.17% | 1345.7 | 1343.5 | -2.2 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/MultipleLoops.v |
| +0.33% | 340.0 | 341.1 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist/merge_cpp_proof.v |
| +0.50% | 202.4 | 203.4 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep_spec.v |
| +0.79% | 165.5 | 166.8 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_main_proof.v |
| +0.83% | 166.9 | 168.3 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/splice_cpp_spec.v |
| +0.88% | 137.6 | 138.9 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_main_proof.v |
| +0.97% | 140.2 | 141.6 | +1.4 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/defs.v |
| +0.99% | 109.2 | 110.3 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_main_proof.v |
| +1.01% | 143.5 | 145.0 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_main_proof.v |
| +1.15% | 116.2 | 117.5 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/unit_tests.v |
| +1.26% | 116.6 | 118.1 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_main_proof.v |
| +1.36% | 74.6 | 75.6 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/inheritance_if_style_hpp_spec.v |
| +1.37% | 74.2 | 75.2 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/nrvo_elision/nrvo_elision.v |
| +1.52% | 68.0 | 69.1 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/pure_virtual_dispatch/pure_virtual_dispatch.v |
| +1.53% | 67.2 | 68.2 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/simple_if_style_hpp_spec.v |
| +1.61% | 62.6 | 63.6 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array_string_init/main_cpp_proof.v |
| +1.61% | 64.0 | 65.1 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/x86_64/inheritance_arch_hpp_spec.v |
| +1.80% | 58.7 | 59.7 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/aarch64/inheritance_arch_hpp_spec.v |
| +1.82% | 70.5 | 71.8 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0084_cpp_main_proof.v |
| +1.86% | 60.0 | 61.1 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f2_proof.v |
| +1.87% | 55.2 | 56.3 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0088_cpp_main_proof.v |
| +1.88% | 69.9 | 71.2 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/conditional/bit_cast_nan/bit_cast_nan.v |
| +2.25% | 46.1 | 47.1 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/auto_frac/anyR_proof.v |
| +2.26% | 49.1 | 50.3 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0076_cpp_f0_proof.v |
| +2.43% | 46.3 | 47.4 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/data_class/dataclass_hpp_proof.v |
| +2.47% | 45.6 | 46.7 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/packed_alignment/packed_align_unsound.v |
| +2.64% | 39.5 | 40.6 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/int128/test.v |
| +2.65% | 51.1 | 52.4 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/assign_raw_uchar/wp_lval_assign_raw.v |
| +2.73% | 40.5 | 41.6 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/char_conv/char_conv.v |
| +2.74% | 43.7 | 44.9 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/control_flow/main_cpp_spec.v |
| +2.79% | 40.8 | 42.0 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/conditional/array_type_ptr/array_type_ptr.v |
| +2.81% | 42.9 | 44.1 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/x86_64/simple_arch_hpp_spec.v |
| +2.89% | 44.8 | 46.1 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/inits/main_cpp_spec.v |
| +3.17% | 44.0 | 45.4 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/tblockr_array/witness.v |
| +3.23% | 39.7 | 40.9 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/clz_value/clz_value.v |
| +3.25% | 34.7 | 35.8 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/for_condition_decl/for_condition_decl.v |
| +3.34% | 37.9 | 39.1 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/anyR_proof.v |
| +3.36% | 41.1 | 42.5 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f2_proof.v |
| +3.45% | 37.6 | 38.9 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/aarch64/simple_arch_hpp_spec.v |
| +3.67% | 44.0 | 45.7 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/tblockr_array_better/witness.v |
| +4.02% | 33.5 | 34.9 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_f0_proof.v |
| +4.32% | 31.9 | 33.2 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/sem_const/constructor.v |
| +4.58% | 29.5 | 30.8 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f3_proof.v |
| +4.60% | 31.0 | 32.4 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0098_cpp_f0_proof.v |
| +4.65% | 26.8 | 28.0 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f0_proof.v |
| +4.73% | 27.3 | 28.6 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/factor.v |
| +4.77% | 27.8 | 29.1 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f1_proof.v |
| +4.98% | 29.1 | 30.5 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0099_cpp_f0_proof.v |
| +5.15% | 25.8 | 27.1 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/constructor.v |
| +5.34% | 25.6 | 27.0 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f0_proof.v |
| +5.38% | 24.3 | 25.6 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f3_proof.v |
| +5.42% | 18.6 | 19.6 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f1_proof.v |
| +5.48% | 24.5 | 25.9 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f0_proof.v |
| +5.68% | 19.5 | 20.6 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/normalization/test.v |
| +5.69% | 22.7 | 23.9 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/sub_const.v |
| +5.94% | 18.2 | 19.2 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f1_proof.v |
| +6.00% | 64.2 | 68.1 | +3.9 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/cast.v |
| +6.17% | 17.7 | 18.8 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_f0_proof.v |
| +6.24% | 22.2 | 23.6 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/virtual/virtual_cpp_proof.v |
| +6.49% | 24.6 | 26.2 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f0_proof.v |
| +6.55% | 21.0 | 22.4 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/fixed-regression-tests/type_ptr_size_ref/references.v |
| +7.63% | 20.4 | 21.9 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f0_proof.v |
| +14.20% | 14.5 | 16.5 | +2.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f1_proof.v |
| -0.19% | 193903.1 | 193528.1 | -375.0 | total |
| -0.27% | 515.0 | - | -515.0 | ├ disappeared files (5) |
| +0.10% | - | 189.1 | +189.1 | ├ newly appeared files (9) |
| -0.03% | 193388.1 | 193339.0 | -49.1 | └ common files |
| +0.01% | 53049.8 | 53054.7 | +4.9 | ├ translation units |
| -0.04% | 140338.3 | 140284.3 | -54.0 | └ proofs and tests |
|
| Repo | Job Branch | Job Commit | Branch Tip | Base branch | Base commit | PR |
|---|---|---|---|---|---|---|
| fmdeps/brick-libcpp/ | simon/thread-spec | cb823f1 | 2755e24 | main | 96b8c50 | #186 |
| fmdeps/BRiCk/ | simon/thread-spec | 44f7ad6 | c95c128 | main | 697dd58 ( |
#353 |
| fmdeps/auto/ | simon/thread-spec | 160cf74 | 160cf74 | main | ade879c ( |
#527 |
Passive Repos
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | d480d67 |
| fmdeps/auto-docs/ | main | 7934ebb |
| bluerock/NOVA/ | skylabs-proof | b83447d |
| bluerock/bhv/ | skylabs-main | 9484328 |
| fmdeps/brick-libgtest/ | main | aeeddad |
| fmdeps/ci/ | main | 7d6ce12 |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| vendored/rocq/ | skylabs-master | fcb26f5 |
| fmdeps/rocq-agent-toolkit/ | main | 5f3e808 |
| 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 |
| fmdeps/skylabs-fm/ | main | 457ecfd |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
Changes in Warnings or Errors
| Before | New | Fixed | After | |
|---|---|---|---|---|
| Errors | 1 | 0 | 5 | |
| Warnings | 73 | 73 |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -0.21% | 193683.8 | 193272.0 | -411.8 | total |
| -0.27% | 515.0 | - | -515.0 | ├ disappeared files (5) |
| +0.08% | - | 153.1 | +153.1 | ├ newly appeared files (9) |
| -0.03% | 193168.9 | 193118.9 | -50.0 | └ common files |
| +0.01% | 53049.8 | 53053.8 | +4.1 | ├ translation units |
| -0.04% | 140119.1 | 140065.0 | -54.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -16.78% | 371.9 | 309.5 | -62.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arith_bug.v |
| -10.66% | 18.5 | 16.5 | -2.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/fixed-regression-tests/type_ptr_size_ref/ref_prim_size.v |
| -4.99% | 23.2 | 22.1 | -1.2 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/cstring/spec.v |
| -4.69% | 212.3 | 202.4 | -10.0 | fmdeps/auto/rocq-skylabs-auto-core/tests/subgoals.v |
| -4.53% | 60.3 | 57.6 | -2.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/micromega/micromega1.v |
| -0.91% | 146.5 | 145.2 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/atomic_exchange_void/atomic_exchange_void.v |
| -0.86% | 244.7 | 242.6 | -2.1 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/SubArrays.v |
| -0.60% | 243.7 | 242.3 | -1.5 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_While.v |
| -0.48% | 242.5 | 241.3 | -1.2 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays.v |
| -0.46% | 230.8 | 229.7 | -1.1 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_WhileTrueWithBreak.v |
| -0.18% | 709.3 | 708.0 | -1.3 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/cctype/proof.v |
| -0.17% | 1345.7 | 1343.5 | -2.2 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/MultipleLoops.v |
| +0.33% | 340.0 | 341.1 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist/merge_cpp_proof.v |
| +0.50% | 202.4 | 203.4 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep_spec.v |
| +0.79% | 165.5 | 166.8 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_main_proof.v |
| +0.83% | 166.9 | 168.3 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/splice_cpp_spec.v |
| +0.88% | 137.6 | 138.9 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_main_proof.v |
| +0.97% | 140.2 | 141.6 | +1.4 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/defs.v |
| +0.99% | 109.2 | 110.3 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_main_proof.v |
| +1.01% | 143.5 | 145.0 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_main_proof.v |
| +1.15% | 116.2 | 117.5 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/unit_tests.v |
| +1.26% | 116.6 | 118.1 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_main_proof.v |
| +1.36% | 74.6 | 75.6 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/inheritance_if_style_hpp_spec.v |
| +1.37% | 74.2 | 75.2 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/nrvo_elision/nrvo_elision.v |
| +1.52% | 68.0 | 69.1 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/pure_virtual_dispatch/pure_virtual_dispatch.v |
| +1.53% | 67.2 | 68.2 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/simple_if_style_hpp_spec.v |
| +1.61% | 62.6 | 63.6 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array_string_init/main_cpp_proof.v |
| +1.61% | 64.0 | 65.1 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/x86_64/inheritance_arch_hpp_spec.v |
| +1.80% | 58.7 | 59.7 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/aarch64/inheritance_arch_hpp_spec.v |
| +1.82% | 70.5 | 71.8 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0084_cpp_main_proof.v |
| +1.86% | 60.0 | 61.1 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f2_proof.v |
| +1.87% | 55.2 | 56.3 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0088_cpp_main_proof.v |
| +1.88% | 69.9 | 71.2 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/conditional/bit_cast_nan/bit_cast_nan.v |
| +2.25% | 46.1 | 47.1 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/auto_frac/anyR_proof.v |
| +2.26% | 49.1 | 50.3 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0076_cpp_f0_proof.v |
| +2.43% | 46.3 | 47.4 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/data_class/dataclass_hpp_proof.v |
| +2.47% | 45.6 | 46.7 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/packed_alignment/packed_align_unsound.v |
| +2.64% | 39.5 | 40.6 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/int128/test.v |
| +2.65% | 51.1 | 52.4 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/assign_raw_uchar/wp_lval_assign_raw.v |
| +2.73% | 40.5 | 41.6 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/char_conv/char_conv.v |
| +2.74% | 43.7 | 44.9 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/control_flow/main_cpp_spec.v |
| +2.79% | 40.8 | 42.0 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/conditional/array_type_ptr/array_type_ptr.v |
| +2.81% | 42.9 | 44.1 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/x86_64/simple_arch_hpp_spec.v |
| +2.89% | 44.8 | 46.1 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/inits/main_cpp_spec.v |
| +3.17% | 44.0 | 45.4 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/tblockr_array/witness.v |
| +3.23% | 39.7 | 40.9 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/clz_value/clz_value.v |
| +3.25% | 34.7 | 35.8 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/for_condition_decl/for_condition_decl.v |
| +3.34% | 37.9 | 39.1 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/anyR_proof.v |
| +3.36% | 41.1 | 42.5 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f2_proof.v |
| +3.45% | 37.6 | 38.9 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/aarch64/simple_arch_hpp_spec.v |
| +3.67% | 44.0 | 45.7 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/tblockr_array_better/witness.v |
| +4.02% | 33.5 | 34.9 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_f0_proof.v |
| +4.32% | 31.9 | 33.2 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/sem_const/constructor.v |
| +4.58% | 29.5 | 30.8 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f3_proof.v |
| +4.60% | 31.0 | 32.4 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0098_cpp_f0_proof.v |
| +4.65% | 26.8 | 28.0 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f0_proof.v |
| +4.73% | 27.3 | 28.6 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/factor.v |
| +4.77% | 27.8 | 29.1 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f1_proof.v |
| +4.98% | 29.1 | 30.5 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0099_cpp_f0_proof.v |
| +5.15% | 25.8 | 27.1 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/constructor.v |
| +5.34% | 25.6 | 27.0 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f0_proof.v |
| +5.38% | 24.3 | 25.6 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f3_proof.v |
| +5.42% | 18.6 | 19.6 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f1_proof.v |
| +5.48% | 24.5 | 25.9 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f0_proof.v |
| +5.68% | 19.5 | 20.6 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/normalization/test.v |
| +5.69% | 22.7 | 23.9 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/sub_const.v |
| +5.94% | 18.2 | 19.2 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f1_proof.v |
| +6.00% | 64.2 | 68.1 | +3.9 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/cast.v |
| +6.17% | 17.7 | 18.8 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_f0_proof.v |
| +6.24% | 22.2 | 23.6 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/virtual/virtual_cpp_proof.v |
| +6.49% | 24.6 | 26.2 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f0_proof.v |
| +6.55% | 21.0 | 22.4 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/fixed-regression-tests/type_ptr_size_ref/references.v |
| +7.63% | 20.4 | 21.9 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f0_proof.v |
| +14.20% | 14.5 | 16.5 | +2.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f1_proof.v |
| -0.21% | 193683.8 | 193272.0 | -411.8 | total |
| -0.27% | 515.0 | - | -515.0 | ├ disappeared files (5) |
| +0.08% | - | 153.1 | +153.1 | ├ newly appeared files (9) |
| -0.03% | 193168.9 | 193118.9 | -50.0 | └ common files |
| +0.01% | 53049.8 | 53053.8 | +4.1 | ├ translation units |
| -0.04% | 140119.1 | 140065.0 | -54.0 | └ proofs and tests |
|
| Repo | Job Branch | Job Commit | Branch Tip | Base branch | Base commit | PR |
|---|---|---|---|---|---|---|
| fmdeps/brick-libcpp/ | simon/thread-spec | 8dcd047 | 8915086 | main | 96b8c50 | #186 |
| fmdeps/BRiCk/ | simon/thread-spec | 44f7ad6 | c95c128 | main | 697dd58 ( |
#353 |
| fmdeps/auto/ | simon/thread-spec | f2b43b7 | 160cf74 | main | ade879c ( |
#527 |
Passive Repos
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | d480d67 |
| fmdeps/auto-docs/ | main | 7934ebb |
| bluerock/NOVA/ | skylabs-proof | b83447d |
| bluerock/bhv/ | skylabs-main | 9484328 |
| fmdeps/brick-libgtest/ | main | aeeddad |
| fmdeps/ci/ | main | 7d6ce12 |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| vendored/rocq/ | skylabs-master | fcb26f5 |
| fmdeps/rocq-agent-toolkit/ | main | 5f3e808 |
| 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 |
| fmdeps/skylabs-fm/ | main | 457ecfd |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
Changes in Warnings or Errors
| Before | New | Fixed | After | |
|---|---|---|---|---|
| Errors | 1 | 0 | 5 | |
| Warnings | 73 | 73 |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -0.22% | 193683.8 | 193255.6 | -428.2 | total |
| -0.27% | 515.0 | - | -515.0 | ├ disappeared files (5) |
| +0.07% | - | 135.9 | +135.9 | ├ newly appeared files (9) |
| -0.03% | 193168.9 | 193119.7 | -49.2 | └ common files |
| +0.01% | 53049.8 | 53054.7 | +4.9 | ├ translation units |
| -0.04% | 140119.1 | 140065.0 | -54.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -16.78% | 371.9 | 309.5 | -62.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arith_bug.v |
| -10.66% | 18.5 | 16.5 | -2.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/fixed-regression-tests/type_ptr_size_ref/ref_prim_size.v |
| -4.99% | 23.2 | 22.1 | -1.2 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/cstring/spec.v |
| -4.69% | 212.3 | 202.4 | -10.0 | fmdeps/auto/rocq-skylabs-auto-core/tests/subgoals.v |
| -4.53% | 60.3 | 57.6 | -2.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/micromega/micromega1.v |
| -0.91% | 146.5 | 145.2 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/atomic_exchange_void/atomic_exchange_void.v |
| -0.86% | 244.7 | 242.6 | -2.1 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/SubArrays.v |
| -0.60% | 243.7 | 242.3 | -1.5 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_While.v |
| -0.48% | 242.5 | 241.3 | -1.2 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays.v |
| -0.46% | 230.8 | 229.7 | -1.1 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_WhileTrueWithBreak.v |
| -0.18% | 709.3 | 708.0 | -1.3 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/cctype/proof.v |
| -0.17% | 1345.7 | 1343.5 | -2.2 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/MultipleLoops.v |
| +0.33% | 340.0 | 341.1 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist/merge_cpp_proof.v |
| +0.50% | 202.4 | 203.4 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep_spec.v |
| +0.79% | 165.5 | 166.8 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_main_proof.v |
| +0.83% | 166.9 | 168.3 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/splice_cpp_spec.v |
| +0.88% | 137.6 | 138.9 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_main_proof.v |
| +0.97% | 140.2 | 141.6 | +1.4 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/defs.v |
| +0.99% | 109.2 | 110.3 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_main_proof.v |
| +1.01% | 143.5 | 145.0 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_main_proof.v |
| +1.15% | 116.2 | 117.5 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/unit_tests.v |
| +1.26% | 116.6 | 118.1 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_main_proof.v |
| +1.36% | 74.6 | 75.6 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/inheritance_if_style_hpp_spec.v |
| +1.37% | 74.2 | 75.2 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/nrvo_elision/nrvo_elision.v |
| +1.52% | 68.0 | 69.1 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/pure_virtual_dispatch/pure_virtual_dispatch.v |
| +1.53% | 67.2 | 68.2 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/simple_if_style_hpp_spec.v |
| +1.61% | 62.6 | 63.6 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array_string_init/main_cpp_proof.v |
| +1.61% | 64.0 | 65.1 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/x86_64/inheritance_arch_hpp_spec.v |
| +1.80% | 58.7 | 59.7 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/aarch64/inheritance_arch_hpp_spec.v |
| +1.82% | 70.5 | 71.8 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0084_cpp_main_proof.v |
| +1.86% | 60.0 | 61.1 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f2_proof.v |
| +1.87% | 55.2 | 56.3 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0088_cpp_main_proof.v |
| +1.88% | 69.9 | 71.2 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/conditional/bit_cast_nan/bit_cast_nan.v |
| +2.25% | 46.1 | 47.1 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/auto_frac/anyR_proof.v |
| +2.26% | 49.1 | 50.3 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0076_cpp_f0_proof.v |
| +2.43% | 46.3 | 47.4 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/data_class/dataclass_hpp_proof.v |
| +2.47% | 45.6 | 46.7 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/packed_alignment/packed_align_unsound.v |
| +2.64% | 39.5 | 40.6 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/int128/test.v |
| +2.65% | 51.1 | 52.4 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/assign_raw_uchar/wp_lval_assign_raw.v |
| +2.73% | 40.5 | 41.6 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/char_conv/char_conv.v |
| +2.74% | 43.7 | 44.9 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/control_flow/main_cpp_spec.v |
| +2.79% | 40.8 | 42.0 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/conditional/array_type_ptr/array_type_ptr.v |
| +2.81% | 42.9 | 44.1 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/x86_64/simple_arch_hpp_spec.v |
| +2.89% | 44.8 | 46.1 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/inits/main_cpp_spec.v |
| +3.17% | 44.0 | 45.4 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/tblockr_array/witness.v |
| +3.23% | 39.7 | 40.9 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/clz_value/clz_value.v |
| +3.25% | 34.7 | 35.8 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/for_condition_decl/for_condition_decl.v |
| +3.34% | 37.9 | 39.1 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/anyR_proof.v |
| +3.36% | 41.1 | 42.5 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f2_proof.v |
| +3.45% | 37.6 | 38.9 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/aarch64/simple_arch_hpp_spec.v |
| +3.67% | 44.0 | 45.7 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/tblockr_array_better/witness.v |
| +4.02% | 33.5 | 34.9 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_f0_proof.v |
| +4.32% | 31.9 | 33.2 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/sem_const/constructor.v |
| +4.58% | 29.5 | 30.8 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f3_proof.v |
| +4.60% | 31.0 | 32.4 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0098_cpp_f0_proof.v |
| +4.65% | 26.8 | 28.0 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f0_proof.v |
| +4.73% | 27.3 | 28.6 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/factor.v |
| +4.77% | 27.8 | 29.1 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f1_proof.v |
| +4.98% | 29.1 | 30.5 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0099_cpp_f0_proof.v |
| +5.15% | 25.8 | 27.1 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/constructor.v |
| +5.34% | 25.6 | 27.0 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f0_proof.v |
| +5.38% | 24.3 | 25.6 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f3_proof.v |
| +5.42% | 18.6 | 19.6 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f1_proof.v |
| +5.48% | 24.5 | 25.9 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f0_proof.v |
| +5.68% | 19.5 | 20.6 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/normalization/test.v |
| +5.69% | 22.7 | 23.9 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/sub_const.v |
| +5.94% | 18.2 | 19.2 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f1_proof.v |
| +6.00% | 64.2 | 68.1 | +3.9 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/cast.v |
| +6.17% | 17.7 | 18.8 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_f0_proof.v |
| +6.24% | 22.2 | 23.6 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/virtual/virtual_cpp_proof.v |
| +6.49% | 24.6 | 26.2 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f0_proof.v |
| +6.55% | 21.0 | 22.4 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/fixed-regression-tests/type_ptr_size_ref/references.v |
| +7.63% | 20.4 | 21.9 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f0_proof.v |
| +14.20% | 14.5 | 16.5 | +2.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f1_proof.v |
| -0.22% | 193683.8 | 193255.6 | -428.2 | total |
| -0.27% | 515.0 | - | -515.0 | ├ disappeared files (5) |
| +0.07% | - | 135.9 | +135.9 | ├ newly appeared files (9) |
| -0.03% | 193168.9 | 193119.7 | -49.2 | └ common files |
| +0.01% | 53049.8 | 53054.7 | +4.9 | ├ translation units |
| -0.04% | 140119.1 | 140065.0 | -54.0 | └ proofs and tests |
simon-skylabs
force-pushed
the
simon/thread-spec
branch
from
October 5, 2026 20:54
6c41dbb to
0712d95
Compare
|
| Repo | Job Branch | Job Commit | Branch Tip | Base branch | Base commit | PR |
|---|---|---|---|---|---|---|
| fmdeps/brick-libcpp/ | simon/thread-spec | 4d89417 | 0712d95 | main | 96b8c50 | #186 |
| fmdeps/BRiCk/ | simon/thread-spec | 44f7ad6 | c95c128 | main | 697dd58 ( |
#353 |
| fmdeps/auto/ | simon/thread-spec | f2b43b7 | 160cf74 | main | ade879c ( |
#527 |
Passive Repos
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | d480d67 |
| fmdeps/auto-docs/ | main | 7934ebb |
| bluerock/NOVA/ | skylabs-proof | b83447d |
| bluerock/bhv/ | skylabs-main | 9484328 |
| fmdeps/brick-libgtest/ | main | aeeddad |
| fmdeps/ci/ | main | 7d6ce12 |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| vendored/rocq/ | skylabs-master | fcb26f5 |
| fmdeps/rocq-agent-toolkit/ | main | 5f3e808 |
| 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 |
| fmdeps/skylabs-fm/ | main | 457ecfd |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
Changes in Warnings or Errors
| Before | New | Fixed | After | |
|---|---|---|---|---|
| Errors | 1 | 0 | 5 | |
| Warnings | 73 | 73 |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -0.22% | 193683.8 | 193253.2 | -430.6 | total |
| -0.27% | 515.0 | - | -515.0 | ├ disappeared files (5) |
| +0.07% | - | 133.5 | +133.5 | ├ newly appeared files (9) |
| -0.03% | 193168.9 | 193119.7 | -49.2 | └ common files |
| +0.01% | 53049.8 | 53054.7 | +4.9 | ├ translation units |
| -0.04% | 140119.1 | 140065.0 | -54.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -16.78% | 371.9 | 309.5 | -62.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arith_bug.v |
| -10.66% | 18.5 | 16.5 | -2.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/fixed-regression-tests/type_ptr_size_ref/ref_prim_size.v |
| -4.99% | 23.2 | 22.1 | -1.2 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/cstring/spec.v |
| -4.69% | 212.3 | 202.4 | -10.0 | fmdeps/auto/rocq-skylabs-auto-core/tests/subgoals.v |
| -4.53% | 60.3 | 57.6 | -2.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/micromega/micromega1.v |
| -0.91% | 146.5 | 145.2 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/atomic_exchange_void/atomic_exchange_void.v |
| -0.86% | 244.7 | 242.6 | -2.1 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/SubArrays.v |
| -0.60% | 243.7 | 242.3 | -1.5 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_While.v |
| -0.48% | 242.5 | 241.3 | -1.2 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays.v |
| -0.46% | 230.8 | 229.7 | -1.1 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_WhileTrueWithBreak.v |
| -0.18% | 709.3 | 708.0 | -1.3 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/cctype/proof.v |
| -0.17% | 1345.7 | 1343.5 | -2.2 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/MultipleLoops.v |
| +0.33% | 340.0 | 341.1 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist/merge_cpp_proof.v |
| +0.50% | 202.4 | 203.4 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep_spec.v |
| +0.79% | 165.5 | 166.8 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_main_proof.v |
| +0.83% | 166.9 | 168.3 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/splice_cpp_spec.v |
| +0.88% | 137.6 | 138.9 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_main_proof.v |
| +0.97% | 140.2 | 141.6 | +1.4 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/defs.v |
| +0.99% | 109.2 | 110.3 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_main_proof.v |
| +1.01% | 143.5 | 145.0 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_main_proof.v |
| +1.15% | 116.2 | 117.5 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/unit_tests.v |
| +1.26% | 116.6 | 118.1 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_main_proof.v |
| +1.36% | 74.6 | 75.6 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/inheritance_if_style_hpp_spec.v |
| +1.37% | 74.2 | 75.2 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/nrvo_elision/nrvo_elision.v |
| +1.52% | 68.0 | 69.1 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/pure_virtual_dispatch/pure_virtual_dispatch.v |
| +1.53% | 67.2 | 68.2 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/simple_if_style_hpp_spec.v |
| +1.61% | 62.6 | 63.6 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array_string_init/main_cpp_proof.v |
| +1.61% | 64.0 | 65.1 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/x86_64/inheritance_arch_hpp_spec.v |
| +1.80% | 58.7 | 59.7 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/aarch64/inheritance_arch_hpp_spec.v |
| +1.82% | 70.5 | 71.8 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0084_cpp_main_proof.v |
| +1.86% | 60.0 | 61.1 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f2_proof.v |
| +1.87% | 55.2 | 56.3 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0088_cpp_main_proof.v |
| +1.88% | 69.9 | 71.2 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/conditional/bit_cast_nan/bit_cast_nan.v |
| +2.25% | 46.1 | 47.1 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/auto_frac/anyR_proof.v |
| +2.26% | 49.1 | 50.3 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0076_cpp_f0_proof.v |
| +2.43% | 46.3 | 47.4 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/data_class/dataclass_hpp_proof.v |
| +2.47% | 45.6 | 46.7 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/packed_alignment/packed_align_unsound.v |
| +2.64% | 39.5 | 40.6 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/int128/test.v |
| +2.65% | 51.1 | 52.4 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/assign_raw_uchar/wp_lval_assign_raw.v |
| +2.73% | 40.5 | 41.6 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/char_conv/char_conv.v |
| +2.74% | 43.7 | 44.9 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/control_flow/main_cpp_spec.v |
| +2.79% | 40.8 | 42.0 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/conditional/array_type_ptr/array_type_ptr.v |
| +2.81% | 42.9 | 44.1 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/x86_64/simple_arch_hpp_spec.v |
| +2.89% | 44.8 | 46.1 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/inits/main_cpp_spec.v |
| +3.17% | 44.0 | 45.4 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/tblockr_array/witness.v |
| +3.23% | 39.7 | 40.9 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/clz_value/clz_value.v |
| +3.25% | 34.7 | 35.8 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/for_condition_decl/for_condition_decl.v |
| +3.34% | 37.9 | 39.1 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/anyR_proof.v |
| +3.36% | 41.1 | 42.5 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f2_proof.v |
| +3.45% | 37.6 | 38.9 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/aarch64/simple_arch_hpp_spec.v |
| +3.67% | 44.0 | 45.7 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/tblockr_array_better/witness.v |
| +4.02% | 33.5 | 34.9 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_f0_proof.v |
| +4.32% | 31.9 | 33.2 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/sem_const/constructor.v |
| +4.58% | 29.5 | 30.8 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f3_proof.v |
| +4.60% | 31.0 | 32.4 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0098_cpp_f0_proof.v |
| +4.65% | 26.8 | 28.0 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f0_proof.v |
| +4.73% | 27.3 | 28.6 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/factor.v |
| +4.77% | 27.8 | 29.1 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f1_proof.v |
| +4.98% | 29.1 | 30.5 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0099_cpp_f0_proof.v |
| +5.15% | 25.8 | 27.1 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/constructor.v |
| +5.34% | 25.6 | 27.0 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f0_proof.v |
| +5.38% | 24.3 | 25.6 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f3_proof.v |
| +5.42% | 18.6 | 19.6 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f1_proof.v |
| +5.48% | 24.5 | 25.9 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f0_proof.v |
| +5.68% | 19.5 | 20.6 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/normalization/test.v |
| +5.69% | 22.7 | 23.9 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/sub_const.v |
| +5.94% | 18.2 | 19.2 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f1_proof.v |
| +6.00% | 64.2 | 68.1 | +3.9 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/cast.v |
| +6.17% | 17.7 | 18.8 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_f0_proof.v |
| +6.24% | 22.2 | 23.6 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/virtual/virtual_cpp_proof.v |
| +6.49% | 24.6 | 26.2 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f0_proof.v |
| +6.55% | 21.0 | 22.4 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/fixed-regression-tests/type_ptr_size_ref/references.v |
| +7.63% | 20.4 | 21.9 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f0_proof.v |
| +14.20% | 14.5 | 16.5 | +2.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f1_proof.v |
| -0.22% | 193683.8 | 193253.2 | -430.6 | total |
| -0.27% | 515.0 | - | -515.0 | ├ disappeared files (5) |
| +0.07% | - | 133.5 | +133.5 | ├ newly appeared files (9) |
| -0.03% | 193168.9 | 193119.7 | -49.2 | └ common files |
| +0.01% | 53049.8 | 53054.7 | +4.9 | ├ translation units |
| -0.04% | 140119.1 | 140065.0 | -54.0 | └ proofs and tests |
simon-skylabs
force-pushed
the
simon/thread-spec
branch
from
October 7, 2026 00:19
6b900af to
9c10518
Compare
|
| Repo | Job Branch | Job Commit | Branch Tip | Base branch | Base commit | PR |
|---|---|---|---|---|---|---|
| fmdeps/brick-libcpp/ | simon/thread-spec | a535443 | 9c10518 | main | 96b8c50 | #186 |
| fmdeps/BRiCk/ | simon/thread-spec | da6eb58 | da6eb58 | main | da6eb58 | - |
| fmdeps/auto/ | simon/thread-spec | 3d63b8f | 7f69463 | main | 80eee7c ( |
#527 |
Passive Repos
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | d480d67 |
| fmdeps/auto-docs/ | main | 7934ebb |
| bluerock/NOVA/ | skylabs-proof | b83447d |
| bluerock/bhv/ | skylabs-main | 7c39db3 |
| fmdeps/brick-libgtest/ | main | aeeddad |
| fmdeps/ci/ | main | cab6c53 |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| vendored/rocq/ | skylabs-master | fcb26f5 |
| fmdeps/rocq-agent-toolkit/ | main | 5f3e808 |
| 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 |
| fmdeps/skylabs-fm/ | main | 457ecfd |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
Changes in Warnings or Errors
| Before | New | Fixed | After | |
|---|---|---|---|---|
| Errors | 11 | 2 | ||
| Warnings | 74 | 0 | 7 |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -67.57% | 188891.3 | 61256.0 | -127635.3 | total |
| -67.57% | 127645.0 | - | -127645.0 | ├ disappeared files (1804) |
| +0.01% | - | 9.8 | +9.8 | ├ newly appeared files (1) |
| -0.00% | 61246.2 | 61246.2 | -0.0 | └ common files |
| -0.00% | 48432.8 | 48432.8 | -0.0 | ├ translation units |
| +0.00% | 12813.4 | 12813.4 | +0.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -67.57% | 188891.3 | 61256.0 | -127635.3 | total |
| -67.57% | 127645.0 | - | -127645.0 | ├ disappeared files (1804) |
| +0.01% | - | 9.8 | +9.8 | ├ newly appeared files (1) |
| -0.00% | 61246.2 | 61246.2 | -0.0 | └ common files |
| -0.00% | 48432.8 | 48432.8 | -0.0 | ├ translation units |
| +0.00% | 12813.4 | 12813.4 | +0.0 | └ proofs and tests |
|
| Repo | Job Branch | Job Commit | Branch Tip | Base branch | Base commit | PR |
|---|---|---|---|---|---|---|
| fmdeps/brick-libcpp/ | simon/thread-spec | 8ae97d4 | b7656cf | main | 96b8c50 | #186 |
| fmdeps/BRiCk/ | simon/thread-spec | da6eb58 | da6eb58 | main | da6eb58 | - |
| fmdeps/auto/ | simon/thread-spec | 3d63b8f | 7f69463 | main | 80eee7c ( |
#527 |
Passive Repos
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | d480d67 |
| fmdeps/auto-docs/ | main | 7934ebb |
| bluerock/NOVA/ | skylabs-proof | b83447d |
| bluerock/bhv/ | skylabs-main | 7c39db3 |
| fmdeps/brick-libgtest/ | main | aeeddad |
| fmdeps/ci/ | main | cab6c53 |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| vendored/rocq/ | skylabs-master | fcb26f5 |
| fmdeps/rocq-agent-toolkit/ | main | 5f3e808 |
| 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 |
| fmdeps/skylabs-fm/ | main | 457ecfd |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
Changes in Warnings or Errors
| Before | New | Fixed | After | |
|---|---|---|---|---|
| Errors | 11 | 2 | ||
| Warnings | 74 | 0 | 7 |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -62.87% | 188891.3 | 70130.0 | -118761.3 | total |
| -62.88% | 118784.7 | - | -118784.7 | ├ disappeared files (1760) |
| +0.01% | - | 23.4 | +23.4 | ├ newly appeared files (3) |
| -0.00% | 70106.6 | 70106.5 | -0.0 | └ common files |
| -0.00% | 53139.3 | 53139.3 | -0.0 | ├ translation units |
| +0.00% | 16967.3 | 16967.3 | +0.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -62.87% | 188891.3 | 70130.0 | -118761.3 | total |
| -62.88% | 118784.7 | - | -118784.7 | ├ disappeared files (1760) |
| +0.01% | - | 23.4 | +23.4 | ├ newly appeared files (3) |
| -0.00% | 70106.6 | 70106.5 | -0.0 | └ common files |
| -0.00% | 53139.3 | 53139.3 | -0.0 | ├ translation units |
| +0.00% | 16967.3 | 16967.3 | +0.0 | └ proofs and tests |
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | d480d67 |
| fmdeps/auto-docs/ | main | 7934ebb |
| bluerock/NOVA/ | skylabs-proof | b83447d |
| bluerock/bhv/ | skylabs-main | 7c39db3 |
| fmdeps/brick-libgtest/ | main | aeeddad |
| fmdeps/ci/ | main | cab6c53 |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| vendored/rocq/ | skylabs-master | fcb26f5 |
| fmdeps/rocq-agent-toolkit/ | main | 5f3e808 |
| 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 |
| fmdeps/skylabs-fm/ | main | 457ecfd |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
No Changes in Warnings or Errors
| Before | New | Fixed | After | |
|---|---|---|---|---|
| Errors | 0 | 0 | 0 | 0 |
| Warnings | 74 | 0 | 0 | 74 |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.06% | 189047.3 | 189167.7 | +120.5 | total |
| +0.07% | - | 124.5 | +124.5 | ├ newly appeared files (8) |
| -0.00% | 189047.3 | 189043.2 | -4.0 | └ common files |
| -0.00% | 53139.3 | 53139.3 | -0.0 | ├ translation units |
| -0.00% | 135908.0 | 135904.0 | -4.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -2.16% | 59.8 | 58.5 | -1.3 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/proof/unique_lock.v |
| -1.94% | 60.4 | 59.2 | -1.2 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/proof/unique_lock_recursive_mutex.v |
| -1.80% | 62.2 | 61.1 | -1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/demo_cpp_proof.v |
| -0.93% | 112.9 | 111.8 | -1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/mutex/guard_recursive_cpp_proof.v |
| +0.06% | 189047.3 | 189167.7 | +120.5 | total |
| +0.07% | - | 124.5 | +124.5 | ├ newly appeared files (8) |
| -0.00% | 189047.3 | 189043.2 | -4.0 | └ common files |
| -0.00% | 53139.3 | 53139.3 | -0.0 | ├ translation units |
| -0.00% | 135908.0 | 135904.0 | -4.0 | └ proofs and tests |
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | d480d67 |
| fmdeps/BRiCk/ | main | da6eb58 |
| fmdeps/auto/ | main | d905259 |
| fmdeps/auto-docs/ | main | 7934ebb |
| bluerock/NOVA/ | skylabs-proof | b83447d |
| bluerock/bhv/ | skylabs-main | 7c39db3 |
| fmdeps/brick-libgtest/ | main | aeeddad |
| fmdeps/ci/ | main | cab6c53 |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| vendored/rocq/ | skylabs-master | fcb26f5 |
| fmdeps/rocq-agent-toolkit/ | main | 5f3e808 |
| 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 |
| fmdeps/skylabs-fm/ | main | 457ecfd |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
No Changes in Warnings or Errors
| Before | New | Fixed | After | |
|---|---|---|---|---|
| Errors | 0 | 0 | 0 | 0 |
| Warnings | 74 | 0 | 0 | 74 |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.06% | 189047.3 | 189167.7 | +120.5 | total |
| +0.07% | - | 124.5 | +124.5 | ├ newly appeared files (8) |
| -0.00% | 189047.3 | 189043.2 | -4.0 | └ common files |
| +0.00% | 53139.3 | 53139.3 | +0.0 | ├ translation units |
| -0.00% | 135908.0 | 135904.0 | -4.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -2.16% | 59.8 | 58.5 | -1.3 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/proof/unique_lock.v |
| -1.94% | 60.4 | 59.2 | -1.2 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/proof/unique_lock_recursive_mutex.v |
| -1.80% | 62.2 | 61.1 | -1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/demo_cpp_proof.v |
| -0.93% | 112.9 | 111.8 | -1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/mutex/guard_recursive_cpp_proof.v |
| +0.06% | 189047.3 | 189167.7 | +120.5 | total |
| +0.07% | - | 124.5 | +124.5 | ├ newly appeared files (8) |
| -0.00% | 189047.3 | 189043.2 | -4.0 | └ common files |
| +0.00% | 53139.3 | 53139.3 | +0.0 | ├ translation units |
| -0.00% | 135908.0 | 135904.0 | -4.0 | └ proofs and tests |
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | d480d67 |
| fmdeps/BRiCk/ | main | daefab6 |
| fmdeps/auto/ | main | 0ac4e93 |
| fmdeps/auto-docs/ | main | 7934ebb |
| bluerock/NOVA/ | skylabs-proof | 8fff234 |
| bluerock/bhv/ | skylabs-main | 7c39db3 |
| fmdeps/brick-libgtest/ | main | aeeddad |
| fmdeps/ci/ | main | cab6c53 |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| vendored/rocq/ | skylabs-master | fcb26f5 |
| fmdeps/rocq-agent-toolkit/ | main | 5f3e808 |
| 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 |
| fmdeps/skylabs-fm/ | main | 457ecfd |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
No Changes in Warnings or Errors
| Before | New | Fixed | After | |
|---|---|---|---|---|
| Errors | 0 | 0 | 0 | 0 |
| Warnings | 74 | 0 | 0 | 74 |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.07% | 188939.7 | 189069.8 | +130.2 | total |
| +0.07% | - | 124.7 | +124.7 | ├ newly appeared files (8) |
| +0.00% | 188939.7 | 188945.1 | +5.5 | └ common files |
| -0.00% | 53138.8 | 53138.8 | -0.0 | ├ translation units |
| +0.00% | 135800.8 | 135806.3 | +5.5 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +1.08% | 111.7 | 112.9 | +1.2 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/mutex/guard_recursive_cpp_proof.v |
| +1.86% | 61.1 | 62.2 | +1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/demo_cpp_proof.v |
| +1.99% | 59.2 | 60.4 | +1.2 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/proof/unique_lock_recursive_mutex.v |
| +2.20% | 58.5 | 59.8 | +1.3 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/proof/unique_lock.v |
| +0.07% | 188939.7 | 189069.8 | +130.2 | total |
| +0.07% | - | 124.7 | +124.7 | ├ newly appeared files (8) |
| +0.00% | 188939.7 | 188945.1 | +5.5 | └ common files |
| -0.00% | 53138.8 | 53138.8 | -0.0 | ├ translation units |
| +0.00% | 135800.8 | 135806.3 | +5.5 | └ proofs and tests |
added 2 commits
October 7, 2026 15:12
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | d480d67 |
| fmdeps/BRiCk/ | main | 64ef0d8 |
| fmdeps/auto/ | main | fc8ca04 |
| fmdeps/auto-docs/ | main | ef5d538 |
| bluerock/NOVA/ | skylabs-proof | 9a965ca |
| bluerock/bhv/ | skylabs-main | 7c39db3 |
| fmdeps/brick-libgtest/ | main | aeeddad |
| fmdeps/ci/ | main | cab6c53 |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| vendored/rocq/ | skylabs-master | fcb26f5 |
| fmdeps/rocq-agent-toolkit/ | main | 5f3e808 |
| 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 |
| fmdeps/skylabs-fm/ | main | 457ecfd |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
No Changes in Warnings or Errors
| Before | New | Fixed | After | |
|---|---|---|---|---|
| Errors | 0 | 0 | 0 | 0 |
| Warnings | 74 | 0 | 0 | 74 |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.06% | 188891.7 | 189012.8 | +121.1 | total |
| +0.07% | - | 123.8 | +123.8 | ├ newly appeared files (8) |
| -0.00% | 188891.7 | 188889.0 | -2.7 | └ common files |
| +0.00% | 53134.8 | 53134.8 | +0.0 | ├ translation units |
| -0.00% | 135757.0 | 135754.2 | -2.7 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -1.91% | 60.4 | 59.3 | -1.2 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/proof/unique_lock_recursive_mutex.v |
| -1.78% | 62.3 | 61.1 | -1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/demo_cpp_proof.v |
| -0.91% | 113.0 | 111.9 | -1.0 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/mutex/guard_recursive_cpp_proof.v |
| +0.06% | 188891.7 | 189012.8 | +121.1 | total |
| +0.07% | - | 123.8 | +123.8 | ├ newly appeared files (8) |
| -0.00% | 188891.7 | 188889.0 | -2.7 | └ common files |
| +0.00% | 53134.8 | 53134.8 | +0.0 | ├ translation units |
| -0.00% | 135757.0 | 135754.2 | -2.7 | └ proofs and tests |
pgiarrusso-sl
approved these changes
Oct 9, 2026
| @@ -0,0 +1,70 @@ | |||
| (* | |||
| * Copyright (c) 2025 SkyLabs AI, Inc. | |||
Contributor
There was a problem hiding this comment.
Suggested change
| * Copyright (c) 2025 SkyLabs AI, Inc. | |
| * Copyright (c) 2026 SkyLabs AI, Inc. |
| \with this_thread | ||
| \prepost current_thread this_thread | ||
| \require LocalWith procTI (Pre argp arg) | ||
| \require forall tid, LocalWith procTI (Post argp arg tid) |
Contributor
There was a problem hiding this comment.
Discussion with the UIC folks suggested this extension:
Suggested change
| \require forall tid, LocalWith procTI (Post argp arg tid) | |
| \require forall tid, LocalWith procTI (Post argp arg tid) | |
| \pre{Q_all_threads} AC | |
| << ∀ tids, all_threads tids >> ⊤, ... | |
| << ∃ tid, all_threads (tids ∪ { tid }) ** a_thread tid ** [| tid ∉ tids |] COMM Q_all_threads tid >> |
together with Observe2 [| tid ∈ tids |] (all_threads tids) (a_thread tid) and other natural rules.
And all_threads uses a auth (gset_disjR thread_id) algebra probably?
Then, our example user in #173 keeps exists tids, all_threads tids ** mutex_set_map tids in an invariant.
Finally, Q_all_threads tid is returned in the success case.
Contributor
There was a problem hiding this comment.
- Masks:
top \setminus upclose pthread.namespace, \emptymaybe? Just to reserve namespacepthread.namespacefor the pthread internals. all_threadsshould be process-local.
Contributor
There was a problem hiding this comment.
(This isn't essential for the thread spec, it's a follow-up).
| \through [| existT (P := P0) argT Pre = existT argT' Pre' |] | ||
| \through [| existT (P := P1) argT Post = existT argT' Post' |] | ||
| \end. | ||
| Admit Obligations. |
Contributor
There was a problem hiding this comment.
Hopefully an LLM can fill these in?
Comment on lines
+53
to
+55
| Definition learn_eq_dep {T U V} : Learning V → Learning (forall x : T, U x → V) := | ||
| fun '{|unLearning := k|} => | ||
| {|unLearning := fun L R ls => forall a a' b b', k (L a b) (R a' b') ((existT a b = existT a' b') :: ls) |}. |
Contributor
There was a problem hiding this comment.
This might be worth upstreaming but it might not be used.
| Context `{Σ : cpp_logic, σ : genv}. | ||
| Context `{!HasStdThreads Σ}. | ||
|
|
||
| Class ThreadFunction (nm : globname) (P : mpred) |
Contributor
There was a problem hiding this comment.
Suggested change
| Class ThreadFunction (nm : globname) (P : mpred) | |
| (** | |
| Automation to unify [starter_spec] obligations with spec assumptions. | |
| TODO: revisit how we should specify higher-order functions. | |
| *) | |
| Class ThreadFunction (nm : globname) (P : mpred) |
| if bool_decide (err = 0) then | ||
| ∃ γt tid, | ||
| pthread.handle γt this_thread tid (Post argp arg tid) ∗ | ||
| idp |-> pthread.R 1$m tid |
Contributor
There was a problem hiding this comment.
Suggested change
| idp |-> pthread.R 1$m tid | |
| idp |-> pthread.R 1$m tid ** Q_all_threads tid |
pgiarrusso-sl
approved these changes
Oct 9, 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
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.