Skip to content

Adapt to SkyLabsAI/auto#412 - #165

Merged
Janno merged 1 commit into
mainfrom
janno/close-admits
Sep 8, 2026
Merged

Adapt to SkyLabsAI/auto#412#165
Janno merged 1 commit into
mainfrom
janno/close-admits

Conversation

@Janno

@Janno Janno commented Sep 2, 2026

Copy link
Copy Markdown
Contributor

No description provided.

@skylabs-ai-ci

skylabs-ai-ci Bot commented Sep 2, 2026

Copy link
Copy Markdown

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Branch Tip Base branch Base commit PR
fmdeps/brick-libcpp/ janno/close-admits 8dfe94c b41894c main f757890 #165
fmdeps/auto/ janno/close-admits 1df291e eec59c3 main b86f915 #412
bluerock/NOVA/ janno/close-admits 6143004 fd56249 skylabs-proof eb2fd0d #21
bluerock/bhv/ janno/close-admits 665ecb3 da677b4 skylabs-main e6646bb #69

Passive Repos
Repo Job Branch Job Commit
./ main fc2860d
fmdeps/BRiCk/ main f8dc05c
fmdeps/auto-docs/ main 6490c5f
fmdeps/ci/ main 6a09c2f
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
fmdeps/skylabs-fm/ main 69d6d20
vendored/vsrocq/ skylabs-main ee79e7a

Changes in Warnings or Errors

Before New Fixed After
Errors 0 0 0 0
Warnings 118 ${\color{red}6}$ ${\color{green}8}$ 116
Code quality details

💚 Fixed Warnings (8)

 
File "./fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/edge_expression_forms.v", line 10, characters 0-1685:
Warning:
Invoking cpp2v produced the following warnings!
/tmp/build_ddb2d8_dune/ocaml_temp_659339.cpp:64:32: warning: left operand of comma operator has no effect
   64 |     int member_ignored = (pair.left, pair.right);
      |                           ~~~~ ^~~~
1 warning generated.

cpp2v command line:
  cpp2v -for-interactive source --no-sharing -o /tmp/build_ddb2d8_dune/_61b4e0.v /tmp/build_ddb2d8_dune/ocaml_temp_659339.cpp --no-elaborate --
 [cpp.prog,brick,default]

File "./fmdeps/auto/rocq-skylabs-auto-cpp/tests/fupd/inc_twice_hpp_spec.v", line 12, characters 0-456:
Warning:
Invoking cpp2v produced the following warnings!
/tmp/build_ddb2d8_dune/ocaml_temp_ae1f4e.cpp:8:9: warning: #pragma once in main file
    8 | #pragma once
      |         ^
1 warning generated.

cpp2v command line:
  cpp2v -for-interactive source --no-sharing -o /tmp/build_ddb2d8_dune/_8cac3f.v /tmp/build_ddb2d8_dune/ocaml_temp_ae1f4e.cpp --elaborate --
 [cpp.prog,brick,default]

File "./fmdeps/auto/rocq-skylabs-auto-cpp/tests/io/io_c_spec.v", line 12, characters 0-435:
Warning:
Invoking cpp2v produced the following warnings!
/tmp/build_ddb2d8_dune/ocaml_temp_d02a6c.cpp:10:16: warning: 'main' should not be 'extern "C"'
   10 | extern "C" int main(int argc, const char* argv[])
      |                ^
1 warning generated.

cpp2v command line:
  cpp2v -for-interactive source --no-sharing -o /tmp/build_ddb2d8_dune/_2b7e02.v /tmp/build_ddb2d8_dune/ocaml_temp_d02a6c.cpp --elaborate --
 [cpp.prog,brick,default]

File "./fmdeps/auto/rocq-skylabs-auto-cpp/theories/cpp/string.v", line 1662, characters 6-70:
Warning:
Use of the non-reference term UNSAFE_collect_string_lits_C
                                ["cstr''"%bs; "cstr"%bs] in "using" clauses is deprecated
[non-reference-hint-using,deprecated,default]

File "./fmdeps/auto/rocq-skylabs-auto-cpp/theories/cpp/string.v", line 1698, characters 6-68:
Warning:
Use of the non-reference term UNSAFE_collect_string_lits_C
                                ["cstr"%bs; "cstr'"%bs] in "using" clauses is deprecated
[non-reference-hint-using,deprecated,default]

File "./fmdeps/auto/rocq-skylabs-auto-cpp/theories/cpp/string.v", line 1699, characters 6-62:
Warning:
Use of the non-reference term UNSAFE_collect_string_lits_C ["cstr''"%bs] in "using" clauses is deprecated
[non-reference-hint-using,deprecated,default]

File "./fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/aarch64/inheritance_arch_hpp_spec.v", line 83, characters 8-85:
Warning: Timeout (2.50s) exceeded: tactic ran for 2.51s [sl-work-timeout,sl]

File "./fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/x86_64/simple_arch_hpp_spec.v", line 34, characters 8-13:
Warning: Timeout (2.50s) exceeded: tactic ran for 3.09s [sl-work-timeout,sl]

⚠️ New Warnings (6)

 
File "./fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/edge_expression_forms.v", line 10, characters 0-1685:
Warning:
Invoking cpp2v produced the following warnings!
/tmp/build_2dab78_dune/ocaml_temp_c6a176.cpp:64:32: warning: left operand of comma operator has no effect
   64 |     int member_ignored = (pair.left, pair.right);
      |                           ~~~~ ^~~~
1 warning generated.

cpp2v command line:
  cpp2v -for-interactive source --no-sharing -o /tmp/build_2dab78_dune/_a35f8b.v /tmp/build_2dab78_dune/ocaml_temp_c6a176.cpp --no-elaborate --
 [cpp.prog,brick,default]

File "./fmdeps/auto/rocq-skylabs-auto-cpp/tests/fupd/inc_twice_hpp_spec.v", line 12, characters 0-456:
Warning:
Invoking cpp2v produced the following warnings!
/tmp/build_2dab78_dune/ocaml_temp_9d8889.cpp:8:9: warning: #pragma once in main file
    8 | #pragma once
      |         ^
1 warning generated.

cpp2v command line:
  cpp2v -for-interactive source --no-sharing -o /tmp/build_2dab78_dune/_c3f840.v /tmp/build_2dab78_dune/ocaml_temp_9d8889.cpp --elaborate --
 [cpp.prog,brick,default]

File "./fmdeps/auto/rocq-skylabs-auto-cpp/tests/io/io_c_spec.v", line 12, characters 0-435:
Warning:
Invoking cpp2v produced the following warnings!
/tmp/build_2dab78_dune/ocaml_temp_d033c5.cpp:10:16: warning: 'main' should not be 'extern "C"'
   10 | extern "C" int main(int argc, const char* argv[])
      |                ^
1 warning generated.

cpp2v command line:
  cpp2v -for-interactive source --no-sharing -o /tmp/build_2dab78_dune/_6d3aa1.v /tmp/build_2dab78_dune/ocaml_temp_d033c5.cpp --elaborate --
 [cpp.prog,brick,default]

File "./fmdeps/auto/rocq-skylabs-auto-cpp/theories/cpp/string.v", line 1715, characters 6-70:
Warning:
Use of the non-reference term UNSAFE_collect_string_lits_C
                                ["cstr''"%bs; "cstr"%bs] in "using" clauses is deprecated
[non-reference-hint-using,deprecated,default]

File "./fmdeps/auto/rocq-skylabs-auto-cpp/theories/cpp/string.v", line 1751, characters 6-68:
Warning:
Use of the non-reference term UNSAFE_collect_string_lits_C
                                ["cstr"%bs; "cstr'"%bs] in "using" clauses is deprecated
[non-reference-hint-using,deprecated,default]

File "./fmdeps/auto/rocq-skylabs-auto-cpp/theories/cpp/string.v", line 1752, characters 6-62:
Warning:
Use of the non-reference term UNSAFE_collect_string_lits_C ["cstr''"%bs] in "using" clauses is deprecated
[non-reference-hint-using,deprecated,default]

Performance

Relative Master MR Change Filename
+0.09% 195010.7 195183.7 +173.0 total
+0.00% 52863.1 52863.1 +0.0 ├ translation units
+0.12% 142147.5 142320.6 +173.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
-5.71% 63.6 59.9 -3.6 fmdeps/auto/rocq-skylabs-auto-cpp/tests/micromega/micromega1.v
-3.00% 36.9 35.8 -1.1 fmdeps/auto-docs/content/docs/functions/verification.v
-1.71% 104.8 103.0 -1.8 fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayCopy_While.v
-1.55% 104.7 103.1 -1.6 fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayCopy_WhileTrueWithBreak.v
-1.53% 104.8 103.2 -1.6 fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayCopy.v
-1.33% 76.4 75.4 -1.0 fmdeps/auto-docs/content/demo/linked_list/linked_list_cpp_proof.v
-1.27% 86.8 85.7 -1.1 fmdeps/auto/brick_groundtruth/examples/loopcorpus/CountPositives.v
-1.16% 105.6 104.4 -1.2 fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayCopy_DownwardForLoop.v
-0.86% 134.2 133.0 -1.2 fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayReverseCopy.v
-0.83% 134.5 133.4 -1.1 fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayReverseCopy_WhileTrueWithBreak.v
-0.68% 271.5 269.7 -1.8 fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_WhileTrueWithBreak.v
-0.53% 283.3 281.8 -1.5 fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_While.v
-0.50% 291.2 289.8 -1.4 fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_zip.v
+0.31% 1964.9 1971.0 +6.0 bluerock/bhv/apps/vmm/proof/main_cpp_proof/init_vcpus.v
+0.32% 1598.4 1603.6 +5.1 fmdeps/auto/brick_groundtruth/examples/loopcorpus/MultipleLoops.v
+0.32% 844.7 847.4 +2.7 bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/proof.v
+0.32% 1132.4 1136.1 +3.7 bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/route.v
+0.36% 472.1 473.8 +1.7 fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v
+0.36% 324.0 325.2 +1.2 bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/async_copy_cookie.v
+0.47% 405.0 406.9 +1.9 bluerock/bhv/apps/vmm/vml/devices/vbus/proof/vbus_cpp_proof/access.v
+0.49% 392.3 394.3 +1.9 bluerock/bhv/lib/vrl/proof/vrl/dataplane_hpp_proof.v
+0.94% 128.1 129.3 +1.2 fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/inc_dec.v
+1.25% 91.0 92.2 +1.1 fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_binary_operators.v
+1.26% 90.4 91.5 +1.1 fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_relational_operators.v
+2.19% 55.4 56.7 +1.2 fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/g4g_trace/N6_print_sizeof.v
+2.36% 51.3 52.5 +1.2 fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/g4g_trace/N5_swap_a.v
+2.41% 50.2 51.4 +1.2 fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/g4g_trace/N5_swap.v
+2.43% 47.7 48.9 +1.2 fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_unary_operators.v
+2.67% 340.2 349.3 +9.1 fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist/merge_cpp_proof.v
+2.86% 38.6 39.7 +1.1 fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/aarch64/simple_arch_hpp_spec.v
+2.90% 41.8 43.0 +1.2 fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/g4g_trace/N12_area.v
+3.03% 39.1 40.2 +1.2 fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_casts.v
+3.62% 183.3 189.9 +6.6 fmdeps/auto/rocq-skylabs-auto-cpp/theories/cpp/string.v
+3.75% 105.0 109.0 +3.9 fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist/list_cpp_proof.v
+4.44% 28.1 29.3 +1.2 fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/g4g_trace/N4_sum_a.v
+6.83% 21.1 22.6 +1.4 fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/g4g_trace/N4_sum.v
+7.24% 20.6 22.1 +1.5 fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/destroy.v
+9.35% 41.1 45.0 +3.8 fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/new_delete.v
+11.99% 260.0 291.2 +31.2 fmdeps/auto/rocq-skylabs-auto-cpp/tests/arith_bug.v
+12.00% 436.1 488.4 +52.3 fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/cstring/proof.v
+12.12% 50.8 56.9 +6.2 fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/operators.v
+37.77% 48.8 67.2 +18.4 fmdeps/auto/rocq-skylabs-auto-cpp/tests/pretty/tests.v
+0.09% 195010.7 195183.7 +173.0 total
+0.00% 52863.1 52863.1 +0.0 ├ translation units
+0.12% 142147.5 142320.6 +173.0 └ proofs and tests

@pgiarrusso-sl

pgiarrusso-sl commented Sep 3, 2026

Copy link
Copy Markdown
Contributor

Overlaps with #143. Let's see if the same proofs work.

@pgiarrusso-sl

pgiarrusso-sl commented Sep 3, 2026

Copy link
Copy Markdown
Contributor

They don't, I needed simpl in *.

@Janno
Janno force-pushed the janno/close-admits branch from b41894c to ca88716 Compare September 8, 2026 09:55
@Janno
Janno merged commit be863c8 into main Sep 8, 2026
10 checks passed
@Janno
Janno deleted the janno/close-admits branch September 8, 2026 11:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@pgiarrusso-sl pgiarrusso-sl pgiarrusso-sl approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@Janno @pgiarrusso-sl