Test cbn delayed subst#14
Draft
Janno wants to merge 1 commit into
Draft
Conversation
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | 7d2ee30 |
| fmdeps/BRiCk/ | main | e64ccd1 |
| fmdeps/auto/ | main | a3a993e |
| fmdeps/auto-docs/ | main | d4c3641 |
| bluerock/NOVA/ | skylabs-proof | 8d011de |
| bluerock/bhv/ | skylabs-main | 6a61dd6 |
| fmdeps/brick-libcpp/ | main | a20f555 |
| fmdeps/ci/ | main | e54841c |
| vendored/elpi/ | skylabs-master | aa4475f |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| fmdeps/fm-tools/ | main | c1e387f |
| psi/protos/ | main | 8fe3e7c |
| psi/backend/ | main | 0b5fea6 |
| psi/ide/ | main | 6b596cf |
| psi/data/ | main | 42bb988 |
| fmdeps/rocq-agent-toolkit/ | main | 3eed23a |
| vendored/rocq-elpi/ | skylabs-master | 103a742 |
| vendored/rocq-equations/ | skylabs-main | a8c4832 |
| vendored/rocq-ext-lib/ | skylabs-master | 94a6630 |
| vendored/rocq-iris/ | skylabs-master | 3ad4ddd |
| vendored/rocq-lsp/ | skylabs-main | a8b7272 |
| vendored/rocq-stdlib/ | skylabs-master | bc07423 |
| vendored/rocq-stdpp/ | skylabs-master | e01d802 |
| fmdeps/skylabs-fm/ | main | 6ca56d6 |
| vendored/vsrocq/ | skylabs-main | 5b4527e |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -0.34% | 134466.5 | 134005.2 | -461.4 | total |
| -0.01% | 27548.3 | 27551.8 | -3.5 | ├ translation units |
| -0.43% | 106456.9 | 106914.7 | -457.8 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -45.10% | 17.9 | 9.8 | -8.1 | fmdeps/auto/rocq-skylabs-auto-core/theories/internal/ltac2_dnet.v |
| -18.86% | 56.5 | 45.8 | -10.7 | fmdeps/auto/rocq-skylabs-auto-core/tests/cancelx_tactic.v |
| -8.72% | 50.4 | 46.0 | -4.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep_spec.v |
| -8.63% | 65.4 | 59.8 | -5.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/pair_hpp_spec.v |
| -7.94% | 16.6 | 15.3 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/includes/A_cpp_proof.v |
| -7.82% | 21.8 | 20.1 | -1.7 | bluerock/bhv/zeta/lib/alloc/proof/core_proof_utils.v |
| -7.64% | 46.9 | 43.3 | -3.6 | bluerock/bhv/apps/vswitch/proof/model/ethernet.v |
| -7.29% | 89.7 | 83.2 | -6.5 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/send.v |
| -6.79% | 27.6 | 25.7 | -1.9 | bluerock/bhv/zeta/lib/lang/proof/page_hpp_proof.v |
| -6.73% | 59.0 | 55.1 | -4.0 | bluerock/bhv/zeta/lib/lang/proof/errno_hpp_proof.v |
| -6.33% | 16.4 | 15.4 | -1.0 | bluerock/bhv/zeta/lib/lang/proof/util.v |
| -5.49% | 145.2 | 137.2 | -8.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/splice_cpp_spec.v |
| -5.29% | 1243.9 | 1178.1 | -65.8 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/sync_impl.v |
| -5.07% | 52.2 | 49.5 | -2.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/initlist_cpp_proof.v |
| -4.92% | 30.2 | 28.7 | -1.5 | bluerock/bhv/zeta/lib/cxx/proof/range_hpp_spec.v |
| -3.61% | 35.2 | 33.9 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/default_specs_1.v |
| -3.56% | 42.4 | 40.9 | -1.5 | bluerock/bhv/zeta/lib/cxx/proof/sys/lock_guard_hpp_proof.v |
| -3.37% | 81.2 | 78.4 | -2.7 | bluerock/bhv/apps/umx/proof/main_cpp_proof/setup_sigs.v |
| -3.27% | 529.5 | 512.1 | -17.3 | bluerock/bhv/lib/drivers/serial/pl011/proof/pl011_cpp_proof.v |
| -3.26% | 85.3 | 82.5 | -2.8 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/drop.v |
| -3.11% | 138.5 | 134.2 | -4.3 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/proof.v |
| -2.85% | 231.5 | 224.9 | -6.6 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/data_abort_to_vbus.v |
| -2.60% | 189.4 | 184.4 | -4.9 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/initialize_dataplane.v |
| -2.57% | 340.9 | 332.2 | -8.8 | bluerock/bhv/apps/umx/proof/main_cpp_proof/setup.v |
| -2.46% | 103.6 | 101.0 | -2.5 | bluerock/bhv/lib/vrl/proof/vrl/port_hpp_proof.v |
| -2.28% | 492.5 | 481.3 | -11.2 | bluerock/bhv/apps/vmm/vml/devices/vpl011/proof/pl011_proof/access.v |
| -2.24% | 151.8 | 148.4 | -3.4 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/compute_gpa_fault_addr.v |
| -2.22% | 49.1 | 48.0 | -1.1 | bluerock/bhv/apps/umx/proof/main_cpp_proof/setup_output_loop_thread.v |
| -2.14% | 191.0 | 186.9 | -4.1 | bluerock/bhv/apps/umx/proof/main_cpp_proof/parse_connect_args.v |
| -2.12% | 1701.0 | 1665.0 | -36.1 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_glue.v |
| -2.10% | 99.8 | 97.7 | -2.1 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/start_cpu.v |
| -2.08% | 114.9 | 112.5 | -2.4 | bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_rich_proof.v |
| -2.08% | 486.4 | 476.3 | -10.1 | bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/zynqmp_dma_ver_cpp_proof.v |
| -2.06% | 862.6 | 844.8 | -17.8 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/proof.v |
| -1.94% | 476.9 | 467.7 | -9.3 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/msr_framework.v |
| -1.89% | 1865.1 | 1829.8 | -35.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/copy_frame.v |
| -1.86% | 690.0 | 677.1 | -12.8 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/virtual_interface.v |
| -1.81% | 90.7 | 89.0 | -1.6 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/ctor.v |
| -1.69% | 1158.9 | 1139.3 | -19.6 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/route.v |
| -1.67% | 192.2 | 189.0 | -3.2 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/create_forwarding_plane.v |
| -1.62% | 728.5 | 716.7 | -11.8 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/misc.v |
| -1.56% | 194.1 | 191.1 | -3.0 | bluerock/bhv/apps/vmm/lib/dynamic_as/proof/space_view_cpp_proof/space_sel.v |
| -1.55% | 191.3 | 188.4 | -3.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/set_virtio_net_header.v |
| -1.53% | 361.4 | 355.9 | -5.5 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/handle_data_abort.v |
| -1.52% | 108.9 | 107.2 | -1.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist/list_cpp_proof.v |
| -1.51% | 117.0 | 115.3 | -1.8 | bluerock/bhv/lib/socket/proof/socket_defs_hpp_proof.v |
| -1.49% | 82.2 | 81.0 | -1.2 | bluerock/bhv/zeta/lib/cxx/proof/sys/mutex_hpp_proof.v |
| -1.49% | 170.9 | 168.4 | -2.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/fields/test_cpp_proof.v |
| -1.45% | 156.9 | 154.6 | -2.3 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_roundedup.v |
| -1.41% | 104.2 | 102.7 | -1.5 | bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_proof.v |
| -1.38% | 394.9 | 389.4 | -5.5 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/extract_frame_header.v |
| -1.30% | 359.4 | 354.7 | -4.7 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/data_abort.v |
| -1.29% | 349.9 | 345.4 | -4.5 | bluerock/bhv/apps/vswitch/lib/vsmp/proof/msg_queue_hpp/proof.v |
| -1.29% | 96.1 | 94.9 | -1.2 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/get_fdt_from_uuid.v |
| -1.27% | 178.1 | 175.9 | -2.3 | bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_base_proof.v |
| -1.20% | 146.9 | 145.1 | -1.8 | bluerock/bhv/zeta/lib/zeta/proof/semaphore_hpp_proof.v |
| -1.08% | 498.3 | 492.9 | -5.4 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/vector/test_cpp_proof.v |
| -0.98% | 277.6 | 274.9 | -2.7 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create.v |
| -0.97% | 261.3 | 258.8 | -2.5 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_sm.v |
| -0.93% | 171.0 | 169.4 | -1.6 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers_other.v |
| -0.89% | 515.1 | 510.5 | -4.6 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/run_vm.v |
| -0.87% | 202.1 | 200.3 | -1.8 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/elpi/enums/variant_cpp_proof.v |
| -0.85% | 201.8 | 200.1 | -1.7 | bluerock/NOVA/build-proof/proof/sc_cpp_proof/create.v |
| -0.84% | 259.5 | 257.3 | -2.2 | bluerock/bhv/apps/vmm/lib/bluerock/proof/aarch64/reg_accessor_hpp_proof.v |
| -0.82% | 226.5 | 224.7 | -1.9 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers_read_console_id.v |
| -0.82% | 1970.9 | 1954.8 | -16.2 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/init_vcpus.v |
| -0.81% | 240.7 | 238.7 | -1.9 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/flood.v |
| -0.80% | 140.9 | 139.7 | -1.1 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_off.v |
| -0.76% | 365.9 | 363.1 | -2.8 | bluerock/bhv/zeta/lib/lang/proof/atomic_hpp_proof.v |
| -0.73% | 1093.2 | 1085.2 | -8.0 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/zeta_main.v |
| -0.71% | 180.8 | 179.5 | -1.3 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/spec.v |
| -0.71% | 179.3 | 178.1 | -1.3 | bluerock/bhv/zeta/lib/msc/proof/sys/rwlock_hpp_proof.v |
| -0.70% | 212.3 | 210.8 | -1.5 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/ctor.v |
| -0.70% | 176.9 | 175.7 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/data_class/class_32_cpp_proof.v |
| -0.69% | 464.7 | 461.5 | -3.2 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_pd.v |
| -0.68% | 198.2 | 196.8 | -1.3 | bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_public.v |
| -0.68% | 389.9 | 387.3 | -2.6 | bluerock/bhv/lib/vrl/proof/vrl/dataplane_hpp_proof.v |
| -0.66% | 347.8 | 345.5 | -2.3 | bluerock/bhv/apps/umx/proof/main_cpp_proof/input_loop.v |
| -0.63% | 1530.2 | 1520.6 | -9.6 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/prepare_address_space.v |
| -0.61% | 326.6 | 324.6 | -2.0 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/resume.v |
| -0.59% | 492.6 | 489.7 | -2.9 | bluerock/bhv/apps/vswitch/lib/port/proof/port/proof.v |
| -0.56% | 239.6 | 238.2 | -1.3 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/read_line.v |
| -0.56% | 555.1 | 552.0 | -3.1 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_sc.v |
| -0.56% | 196.4 | 195.3 | -1.1 | bluerock/bhv/zeta/lib/intrusive/proof/shared_pointer_hpp_proof.v |
| -0.55% | 1695.8 | 1686.5 | -9.3 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/reset.v |
| -0.53% | 202.2 | 201.1 | -1.1 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/queue/misc.v |
| -0.52% | 196.8 | 195.8 | -1.0 | bluerock/bhv/apps/vswitch/lib/port/include/port/aarch64_port_hpp.v |
| -0.52% | 943.3 | 938.4 | -4.9 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/setup.v |
| -0.51% | 276.5 | 275.0 | -1.4 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_on.v |
| -0.51% | 267.5 | 266.2 | -1.4 | bluerock/bhv/apps/vswitch/lib/vswitch/src/aarch64_vswitch_cpp.v |
| -0.50% | 651.4 | 648.2 | -3.3 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/misc.v |
| -0.49% | 222.6 | 221.5 | -1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/include/forwarding/aarch64_forwarding_plane_hpp.v |
| -0.48% | 977.2 | 972.5 | -4.7 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/portal_cpp_proof.v |
| -0.47% | 465.8 | 463.6 | -2.2 | bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_private.v |
| -0.44% | 231.7 | 230.7 | -1.0 | bluerock/bhv/apps/umx/proof/main_cpp_proof/user_handler.v |
| -0.43% | 306.2 | 304.9 | -1.3 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_pt.v |
| -0.42% | 561.3 | 558.9 | -2.4 | bluerock/bhv/apps/vmm/lib/board/src/x86/board_cpp.v |
| -0.41% | 760.4 | 757.3 | -3.1 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/setup.v |
| -0.40% | 632.6 | 630.1 | -2.5 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/vector/test_cpp.v |
| -0.38% | 362.2 | 360.8 | -1.4 | bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/schedule.v |
| -0.32% | 534.1 | 532.4 | -1.7 | bluerock/bhv/apps/vmm/vml/devices/vpl011/proof/pl011_proof/recv.v |
| -0.30% | 782.1 | 779.8 | -2.3 | bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/vcpu_roundup_proof.v |
| -0.29% | 381.0 | 379.9 | -1.1 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_sm.v |
| -0.26% | 676.1 | 674.3 | -1.8 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist_cpp/forward_list_hpp_proof.v |
| -0.23% | 539.5 | 538.3 | -1.2 | bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/ready_queues.v |
| -0.17% | 619.9 | 618.8 | -1.1 | bluerock/bhv/apps/umx/proof/main_cpp_proof/scanner_state.v |
| +0.12% | 896.4 | 897.5 | +1.1 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/atomic/test_cpp_proof.v |
| +0.17% | 906.0 | 907.5 | +1.6 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_default_impl.v |
| +0.25% | 669.6 | 671.3 | +1.7 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/copy.v |
| +0.30% | 686.3 | 688.4 | +2.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/call_cpp_proof.v |
| +0.38% | 431.1 | 432.8 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/arith_cpp_proof.v |
| +0.44% | 410.5 | 412.3 | +1.8 | bluerock/bhv/apps/vmm/lib/board/include/model/aarch64_board_common_hpp.v |
| +0.50% | 264.6 | 266.0 | +1.3 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/src/aarch64_vcpu_base_cpp.v |
| +0.65% | 163.0 | 164.0 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_binary_operators.v |
| +0.75% | 281.0 | 283.1 | +2.1 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/delegate.v |
| +0.90% | 127.4 | 128.5 | +1.2 | bluerock/bhv/apps/vmm/vml/devices/vuart/include/vuart/aarch64_vuart_hpp.v |
| +1.01% | 148.4 | 149.9 | +1.5 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/misc_hints.v |
| +1.02% | 112.6 | 113.8 | +1.2 | bluerock/bhv/apps/vmm/lib/bluerock/include/bluerock/platform/aarch64_memory_hpp.v |
| +1.11% | 170.8 | 172.7 | +1.9 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_rounding_mode.v |
| +1.15% | 88.3 | 89.3 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_main_proof.v |
| +1.25% | 303.7 | 307.5 | +3.8 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_main_proof.v |
| +1.38% | 212.7 | 215.7 | +2.9 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0098_cpp_main_proof.v |
| +1.45% | 81.3 | 82.5 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0099_cpp_main_proof.v |
| +1.70% | 112.7 | 114.6 | +1.9 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_main_proof.v |
| +1.70% | 82.7 | 84.2 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_main_proof.v |
| +1.70% | 156.9 | 159.5 | +2.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_main_proof.v |
| +1.83% | 123.1 | 125.3 | +2.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_main_proof.v |
| +1.84% | 76.2 | 77.6 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0076_cpp_main_proof.v |
| +1.88% | 62.0 | 63.2 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/read_prim/read_cpp_proof.v |
| +1.92% | 144.5 | 147.2 | +2.8 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_main_proof.v |
| +1.98% | 74.9 | 76.3 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0084_cpp_main_proof.v |
| +2.01% | 64.5 | 65.8 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/x86_64/inheritance_arch_hpp_spec.v |
| +2.08% | 117.7 | 120.1 | +2.4 | bluerock/bhv/apps/umx/include/aarch64_umx_hpp.v |
| +2.09% | 141.6 | 144.5 | +3.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_main_proof.v |
| +2.29% | 58.7 | 60.0 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/aarch64/inheritance_arch_hpp_spec.v |
| +2.37% | 59.3 | 60.7 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0088_cpp_main_proof.v |
| +2.38% | 43.0 | 44.1 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/auto_frac/anyR_proof.v |
| +2.38% | 49.0 | 50.1 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/data_class/dataclass_hpp_proof.v |
| +2.82% | 57.7 | 59.4 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f2_proof.v |
| +2.89% | 42.9 | 44.1 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/control_flow/main_cpp_spec.v |
| +2.98% | 44.8 | 46.1 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/inits/main_cpp_spec.v |
| +2.99% | 34.6 | 35.7 | +1.0 | bluerock/NOVA/build-proof/proof/iface/predicates/ec.v |
| +3.02% | 36.5 | 37.6 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/smoke.v |
| +3.13% | 34.4 | 35.5 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/sizeof_alignof.v |
| +3.37% | 54.8 | 56.7 | +1.8 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0076_cpp_f0_proof.v |
| +3.62% | 37.3 | 38.6 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/anyR_proof.v |
| +3.69% | 30.6 | 31.8 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0099_cpp_f0_proof.v |
| +3.71% | 30.2 | 31.3 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f1_proof.v |
| +3.77% | 43.3 | 44.9 | +1.6 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/utility/test_cpp_proof.v |
| +3.88% | 41.8 | 43.4 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f2_proof.v |
| +3.93% | 32.5 | 33.8 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/sem_const/constructor.v |
| +4.08% | 33.1 | 34.4 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/control_logical_forms.v |
| +4.13% | 34.1 | 35.5 | +1.4 | fmdeps/auto-docs/content/docs/functions/verification.v |
| +4.15% | 24.1 | 25.1 | +1.0 | bluerock/NOVA/build-proof/proof/iface/predicates/dma.v |
| +4.31% | 27.1 | 28.3 | +1.2 | bluerock/NOVA/build-proof/proof/iface/predicates/sc.v |
| +4.38% | 26.5 | 27.7 | +1.2 | bluerock/NOVA/build-proof/proof/iface/predicates/mem.v |
| +4.41% | 30.5 | 31.8 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/implicit_array_initialization.v |
| +4.43% | 31.5 | 32.9 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/arrays.v |
| +4.48% | 31.7 | 33.1 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f3_proof.v |
| +4.48% | 25.7 | 26.9 | +1.2 | bluerock/NOVA/build-proof/proof/iface/predicates/pd.v |
| +4.52% | 26.4 | 27.6 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f0_proof.v |
| +4.63% | 31.7 | 33.1 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0098_cpp_f0_proof.v |
| +5.01% | 33.6 | 35.3 | +1.7 | bluerock/NOVA/build-proof/proof/kmem_hpp_spec.v |
| +5.13% | 21.3 | 22.4 | +1.1 | fmdeps/auto-docs/content/docs/class_reps/alt.v |
| +5.22% | 26.1 | 27.5 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/factor.v |
| +5.26% | 25.8 | 27.2 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f3_proof.v |
| +5.38% | 19.1 | 20.1 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f1_proof.v |
| +5.40% | 19.3 | 20.4 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_f0_proof.v |
| +5.45% | 27.4 | 28.9 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f0_proof.v |
| +5.47% | 19.5 | 20.6 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f2_proof.v |
| +5.48% | 19.3 | 20.4 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f1_proof.v |
| +5.51% | 23.8 | 25.1 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/constructor.v |
| +5.58% | 26.2 | 27.6 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f0_proof.v |
| +5.66% | 20.2 | 21.4 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/normalization/test.v |
| +5.73% | 18.6 | 19.7 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_f0_proof.v |
| +6.06% | 23.1 | 24.5 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/virtual/virtual_cpp_proof.v |
| +6.22% | 18.4 | 19.5 | +1.1 | fmdeps/auto-docs/content/docs/control_flow/loop.v |
| +6.41% | 18.4 | 19.6 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f1_proof.v |
| +6.54% | 22.3 | 23.7 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/sub_const.v |
| +6.78% | 25.2 | 26.9 | +1.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f0_proof.v |
| +6.85% | 21.4 | 22.8 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f0_proof.v |
| +7.03% | 22.4 | 24.0 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/allocation_lambda_forms.v |
| +7.93% | 20.1 | 21.7 | +1.6 | fmdeps/auto-docs/content/docs/debugging/main.v |
| +7.96% | 18.2 | 19.6 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/assignment_operators_min_bool.v |
| +9.00% | 21.4 | 23.3 | +1.9 | bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/mutex_hpp_proof.v |
| +10.37% | 16.3 | 18.0 | +1.7 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/member_pointer_operators.v |
| +10.38% | 15.6 | 17.3 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f1_proof.v |
| -0.34% | 134466.5 | 134005.2 | -461.4 | total |
| -0.01% | 27548.3 | 27551.8 | -3.5 | ├ translation units |
| -0.43% | 106456.9 | 106914.7 | -457.8 | └ proofs and tests |
8 tasks
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
1 participant
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.
Github won't let me re-open the old PR because I force-pushed to the branch.
Fixes / closes #????
make doc_gram_rsts.