CI: Code quality #45

Janno · 2025-11-05T12:59:30Z

Examples (from test cases; absolute counts are not correct):

No Changes in Warnings or Errors

Changes in Warnings or Errors

	Before	New	Fixed	After
Errors	0	1	0	1
Warnings	0	1	0	1

❌ New Errors (1)

File "test.v", line 44, characters 19-20:
Error: Syntax error: '.' expected after [command] (in [vernac_aux]).

⚠️ New Warnings (1)

File "test.v", line 0, characters 0-0:
Warning: Non-empty stdout when building using coqc:
dangling text!
[non-empty-stdout,dummy]

Changes in Warnings or Errors

	Before	New	Fixed	After
Errors	1	0	1	0
Warnings	1	0	1	0

❎ Fixed Errors (1)

File "test.v", line 44, characters 19-20:
Error: Syntax error: '.' expected after [command] (in [vernac_aux]).

💚 Fixed Warnings (1)

File "test.v", line 0, characters 0-0:
Warning: Non-empty stdout when building using coqc:
dangling text!
[non-empty-stdout,dummy]

github-actions · 2025-11-05T13:27:25Z

Performance summary for https://github.com/SkylabsAI/workspace/actions/runs/19102842187

Relative	Master	MR	Change	Filename
+0.00%	116922.2	116922.2	+0.0	total
+0.00%	22019.8	22019.8	+0.0	├ translation units
+0.00%	94902.3	94902.3	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename

+0.00%	116922.2	116922.2	+0.0	total
+0.00%	22019.8	22019.8	+0.0	├ translation units
+0.00%	94902.3	94902.3	+0.0	└ proofs and tests

github-actions · 2025-11-06T13:00:26Z

Performance summary for https://github.com/SkylabsAI/workspace/actions/runs/19134908446

Relative	Master	MR	Change	Filename
+0.01%	116952.4	116968.5	+16.1	total
-0.01%	22013.8	22016.4	-2.6	├ translation units
+0.02%	94954.7	94936.0	+18.7	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-13.58%	57.8	49.9	-7.8	fmdeps/auto/coq-bluerock-auto-cpp/tests/micromega/micromega1.v
+0.44%	391.1	392.8	+1.7	bluerock/bhv/apps/vmm/proof/main_cpp_proof.v
+0.67%	338.4	340.7	+2.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/transaction_protocol/hints.v
+3.94%	41.1	42.7	+1.6	bluerock/bhv/apps/vswitch/proof/upstream/hints.v

+0.01%	116952.4	116968.5	+16.1	total
-0.01%	22013.8	22016.4	-2.6	├ translation units
+0.02%	94954.7	94936.0	+18.7	└ proofs and tests

github-actions · 2025-11-06T13:17:11Z

Performance summary for https://github.com/SkylabsAI/workspace/actions/runs/19134908446

Relative	Master	MR	Change	Filename
+0.01%	116952.4	116968.5	+16.1	total
-0.01%	22013.8	22016.4	-2.6	├ translation units
+0.02%	94954.7	94936.0	+18.7	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-13.58%	57.8	49.9	-7.8	fmdeps/auto/coq-bluerock-auto-cpp/tests/micromega/micromega1.v
+0.44%	391.1	392.8	+1.7	bluerock/bhv/apps/vmm/proof/main_cpp_proof.v
+0.67%	338.4	340.7	+2.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/transaction_protocol/hints.v
+3.94%	41.1	42.7	+1.6	bluerock/bhv/apps/vswitch/proof/upstream/hints.v

+0.01%	116952.4	116968.5	+16.1	total
-0.01%	22013.8	22016.4	-2.6	├ translation units
+0.02%	94954.7	94936.0	+18.7	└ proofs and tests

github-actions · 2025-11-06T13:34:04Z

Performance summary for https://github.com/SkylabsAI/workspace/actions/runs/19137074957

Relative	Master	MR	Change	Filename
+0.01%	116952.5	116968.6	+16.1	total
-0.01%	22013.9	22016.5	-2.5	├ translation units
+0.02%	94954.7	94936.0	+18.7	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-13.58%	57.8	49.9	-7.8	fmdeps/auto/coq-bluerock-auto-cpp/tests/micromega/micromega1.v
+0.44%	391.1	392.8	+1.7	bluerock/bhv/apps/vmm/proof/main_cpp_proof.v
+0.67%	338.4	340.7	+2.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/transaction_protocol/hints.v
+3.94%	41.1	42.7	+1.6	bluerock/bhv/apps/vswitch/proof/upstream/hints.v

+0.01%	116952.5	116968.6	+16.1	total
-0.01%	22013.9	22016.5	-2.5	├ translation units
+0.02%	94954.7	94936.0	+18.7	└ proofs and tests

github-actions · 2025-11-07T11:21:28Z

Performance summary for https://github.com/SkylabsAI/workspace/actions/runs/19166432732

Relative	Master	MR	Change	Filename
+0.01%	116952.4	116968.5	+16.1	total
-0.01%	22013.8	22016.4	-2.6	├ translation units
+0.02%	94954.7	94936.0	+18.7	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-13.58%	57.8	49.9	-7.8	fmdeps/auto/coq-bluerock-auto-cpp/tests/micromega/micromega1.v
+0.44%	391.1	392.8	+1.7	bluerock/bhv/apps/vmm/proof/main_cpp_proof.v
+0.67%	338.4	340.7	+2.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/transaction_protocol/hints.v
+3.94%	41.1	42.7	+1.6	bluerock/bhv/apps/vswitch/proof/upstream/hints.v

+0.01%	116952.4	116968.5	+16.1	total
-0.01%	22013.8	22016.4	-2.6	├ translation units
+0.02%	94954.7	94936.0	+18.7	└ proofs and tests

github-actions · 2025-11-07T11:36:29Z

Performance summary for https://github.com/SkylabsAI/workspace/actions/runs/19166874313

Relative	Master	MR	Change	Filename
+0.01%	116952.4	116968.6	+16.2	total
-0.01%	22014.0	22016.4	-2.4	├ translation units
+0.02%	94954.7	94936.0	+18.7	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-13.58%	57.8	49.9	-7.8	fmdeps/auto/coq-bluerock-auto-cpp/tests/micromega/micromega1.v
+0.44%	391.1	392.8	+1.7	bluerock/bhv/apps/vmm/proof/main_cpp_proof.v
+0.67%	338.4	340.7	+2.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/transaction_protocol/hints.v
+3.94%	41.1	42.7	+1.6	bluerock/bhv/apps/vswitch/proof/upstream/hints.v

+0.01%	116952.4	116968.6	+16.2	total
-0.01%	22014.0	22016.4	-2.4	├ translation units
+0.02%	94954.7	94936.0	+18.7	└ proofs and tests

github-actions · 2025-11-07T11:56:41Z

Performance summary for https://github.com/SkylabsAI/workspace/actions/runs/19167318227

Relative	Master	MR	Change	Filename
+0.01%	116952.4	116968.5	+16.1	total
-0.01%	22013.8	22016.4	-2.6	├ translation units
+0.02%	94954.7	94936.0	+18.7	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-13.58%	57.8	49.9	-7.8	fmdeps/auto/coq-bluerock-auto-cpp/tests/micromega/micromega1.v
+0.44%	391.1	392.8	+1.7	bluerock/bhv/apps/vmm/proof/main_cpp_proof.v
+0.67%	338.4	340.7	+2.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/transaction_protocol/hints.v
+3.94%	41.1	42.7	+1.6	bluerock/bhv/apps/vswitch/proof/upstream/hints.v

+0.01%	116952.4	116968.5	+16.1	total
-0.01%	22013.8	22016.4	-2.6	├ translation units
+0.02%	94954.7	94936.0	+18.7	└ proofs and tests

github-actions · 2025-11-07T12:22:12Z

Performance summary for https://github.com/SkylabsAI/workspace/actions/runs/19167890543

Relative	Master	MR	Change	Filename
+0.01%	116952.5	116968.6	+16.1	total
-0.01%	22014.0	22016.5	-2.5	├ translation units
+0.02%	94954.7	94936.0	+18.7	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-13.58%	57.8	49.9	-7.8	fmdeps/auto/coq-bluerock-auto-cpp/tests/micromega/micromega1.v
+0.44%	391.1	392.8	+1.7	bluerock/bhv/apps/vmm/proof/main_cpp_proof.v
+0.67%	338.4	340.7	+2.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/transaction_protocol/hints.v
+3.94%	41.1	42.7	+1.6	bluerock/bhv/apps/vswitch/proof/upstream/hints.v

+0.01%	116952.5	116968.6	+16.1	total
-0.01%	22014.0	22016.5	-2.5	├ translation units
+0.02%	94954.7	94936.0	+18.7	└ proofs and tests

rlepigre-skylabs-ai

That looks reasonable, but as we discussed earlier, it might be useful to rely on the dune-report tool to collect errors.

github-actions · 2025-11-11T16:58:53Z

Performance summary for https://github.com/SkylabsAI/workspace/actions/runs/19272519706

Relative	Master	MR	Change	Filename
-0.00%	116925.8	116925.3	-0.5	total
-0.01%	22013.8	22016.4	-2.6	├ translation units
+0.00%	94911.5	94909.4	+2.1	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-13.58%	57.8	49.9	-7.8	fmdeps/auto/coq-bluerock-auto-cpp/tests/micromega/micromega1.v
-4.67%	115.5	110.1	-5.4	bluerock/bhv/apps/umx/proof/main_cpp_proof/output_loop.v

-0.00%	116925.8	116925.3	-0.5	total
-0.01%	22013.8	22016.4	-2.6	├ translation units
+0.00%	94911.5	94909.4	+2.1	└ proofs and tests

github-actions · 2025-11-11T17:11:56Z

Performance summary for https://github.com/SkylabsAI/workspace/actions/runs/19272894508

Relative	Master	MR	Change	Filename
-0.00%	116925.8	116925.3	-0.5	total
-0.01%	22013.9	22016.5	-2.6	├ translation units
+0.00%	94911.5	94909.4	+2.1	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-13.58%	57.8	49.9	-7.8	fmdeps/auto/coq-bluerock-auto-cpp/tests/micromega/micromega1.v
-4.67%	115.5	110.1	-5.4	bluerock/bhv/apps/umx/proof/main_cpp_proof/output_loop.v

-0.00%	116925.8	116925.3	-0.5	total
-0.01%	22013.9	22016.5	-2.6	├ translation units
+0.00%	94911.5	94909.4	+2.1	└ proofs and tests

github-actions · 2025-11-12T11:43:50Z

Performance summary for https://github.com/SkylabsAI/workspace/actions/runs/19295970355

Relative	Master	MR	Change	Filename
-0.00%	116925.8	116925.3	-0.5	total
-0.01%	22013.8	22016.4	-2.6	├ translation units
+0.00%	94911.5	94909.4	+2.1	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-13.58%	57.8	49.9	-7.8	fmdeps/auto/coq-bluerock-auto-cpp/tests/micromega/micromega1.v
-4.67%	115.5	110.1	-5.4	bluerock/bhv/apps/umx/proof/main_cpp_proof/output_loop.v

-0.00%	116925.8	116925.3	-0.5	total
-0.01%	22013.8	22016.4	-2.6	├ translation units
+0.00%	94911.5	94909.4	+2.1	└ proofs and tests

github-actions · 2025-11-12T12:24:48Z

Performance summary for https://github.com/SkylabsAI/workspace/actions/runs/19295970355

Relative	Master	MR	Change	Filename
-0.00%	116925.8	116925.3	-0.5	total
-0.01%	22013.8	22016.4	-2.6	├ translation units
+0.00%	94911.5	94909.4	+2.1	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-13.58%	57.8	49.9	-7.8	fmdeps/auto/coq-bluerock-auto-cpp/tests/micromega/micromega1.v
-4.67%	115.5	110.1	-5.4	bluerock/bhv/apps/umx/proof/main_cpp_proof/output_loop.v

-0.00%	116925.8	116925.3	-0.5	total
-0.01%	22013.8	22016.4	-2.6	├ translation units
+0.00%	94911.5	94909.4	+2.1	└ proofs and tests

No longer relevant.

Janno changed the title ~~Code quality~~ CI: Code quality Nov 5, 2025

Janno force-pushed the janno/CI branch from 722cd07 to 378bb77 Compare November 5, 2025 13:01

Janno force-pushed the janno/CI branch from 987c5e0 to 4d1beec Compare November 6, 2025 12:00

Janno force-pushed the janno/CI branch from 4d1beec to 1c31217 Compare November 6, 2025 13:22

Janno force-pushed the janno/CI branch 2 times, most recently from 09cb862 to 1e550cb Compare November 7, 2025 11:04

Janno force-pushed the janno/CI branch from 1e550cb to 8e0a98b Compare November 7, 2025 11:22

Janno force-pushed the janno/CI branch from 8e0a98b to 0d7bf43 Compare November 7, 2025 11:41

Janno force-pushed the janno/CI branch from 4787c5b to 8467560 Compare November 7, 2025 12:08

Janno marked this pull request as ready for review November 7, 2025 12:24

Janno requested a review from rlepigre-skylabs-ai November 10, 2025 09:27

rlepigre-skylabs-ai previously requested changes Nov 10, 2025

View reviewed changes

Janno force-pushed the janno/CI branch from 8467560 to 9c1d39d Compare November 11, 2025 15:54

Janno added 7 commits November 12, 2025 12:29

Record code quality output in build artifact

fad44a3

Produce distinct summary and performance reports artifacts

9f221f4

Report code quality diffs

c1d422b

Add step name for gen-job's config step

aea858f

Avoid duplicate warnings about missing PRs; clarify refs versus commits

78612c8

Rename debug-level to log-level, set to WARN in CI

64eda56

Produce summaries for config action

135644e

Janno added 6 commits November 12, 2025 12:29

Reduce noise in summary

dce453c

Use dune logs

ac532e6

Rsync?

3b32897

Rsync!

cd9105c

Arguments!

cc0a0bd

Paths

5206a71

Janno force-pushed the janno/CI branch from 7d25af6 to 5206a71 Compare November 12, 2025 11:31

Janno merged commit e9796d0 into main Nov 12, 2025
27 checks passed

pgiarrusso-sl deleted the janno/CI branch November 12, 2025 13:56

CI: Code quality #45

CI: Code quality #45

Uh oh!

Conversation

Janno commented Nov 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

No Changes in Warnings or Errors

Changes in Warnings or Errors

❌ New Errors (1)

⚠️ New Warnings (1)

Changes in Warnings or Errors

❎ Fixed Errors (1)

💚 Fixed Warnings (1)

Uh oh!

github-actions bot commented Nov 5, 2025

Uh oh!

github-actions bot commented Nov 6, 2025

Uh oh!

github-actions bot commented Nov 6, 2025

Uh oh!

github-actions bot commented Nov 6, 2025

Uh oh!

github-actions bot commented Nov 7, 2025

Uh oh!

github-actions bot commented Nov 7, 2025

Uh oh!

github-actions bot commented Nov 7, 2025

Uh oh!

github-actions bot commented Nov 7, 2025

Uh oh!

rlepigre-skylabs-ai left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Nov 11, 2025

Uh oh!

github-actions bot commented Nov 11, 2025

Uh oh!

github-actions bot commented Nov 12, 2025

Uh oh!

github-actions bot commented Nov 12, 2025

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Janno commented Nov 5, 2025 •

edited

Loading