Skip to content

refactor(ocaml-jsonrpc-tp/python): use pydantic BaseModel for Err + Resp types#282

Open
jhaag-skylabs-ai wants to merge 18 commits into
mainfrom
ocaml-jsonrpc-tp/python/use-pydantic
Open

refactor(ocaml-jsonrpc-tp/python): use pydantic BaseModel for Err + Resp types#282
jhaag-skylabs-ai wants to merge 18 commits into
mainfrom
ocaml-jsonrpc-tp/python/use-pydantic

Conversation

@jhaag-skylabs-ai
Copy link
Copy Markdown
Contributor

@jhaag-skylabs-ai jhaag-skylabs-ai commented Mar 4, 2026

Background

Note: depends on #282

Preferring pydantic BaseModels simplifies (de)serialization logic & downstream client code.

Closing Conditions

Engineering

  • ocaml-jsonrpc-tp:
    • update code generator for pydantic BaseModels in APIs:
      • @final
      • model_config:
        • frozen=True
        • extra="forbid"
    • prefer pydantic BaseModels for Err+Resp types
  • rocq-doc-manager:
  • porting of (downstream) clients

Testing

@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented Mar 4, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base commit PR
fmdeps/rocq-agent-toolkit/ ocaml-jsonrpc-tp/python/use-pydantic 104b88b b19cff9 #282

Passive Repos

Repo Job Branch Job Commit
./ main e5c342a
fmdeps/BRiCk/ main b79c734
fmdeps/auto/ main ffda14f
fmdeps/auto-docs/ main 9f57097
bluerock/NOVA/ skylabs-proof 996d600
bluerock/bhv/ skylabs-main b1ca30d
fmdeps/brick-libcpp/ main dc9818e
fmdeps/ci/ main 7712f8c
vendored/elpi/ skylabs-master aa4475f
fmdeps/fm-ci/ main 262fb04
fmdeps/fm-tools/ main 430933c
psi/protos/ main 8fe3e7c
psi/backend/ main 2a8240c
psi/ide/ main 6b596cf
psi/data/ main 62ed81e
vendored/rocq/ skylabs-master 2ede3c9
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 7d620c1
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
-0.00% 122840.0 122840.0 -0.0 total
-0.00% 22632.7 22632.7 -0.0 ├ translation units
+0.00% 100207.4 100207.4 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
-0.00% 122840.0 122840.0 -0.0 total
-0.00% 22632.7 22632.7 -0.0 ├ translation units
+0.00% 100207.4 100207.4 +0.0 └ proofs and tests

Comment thread ocaml-jsonrpc-tp/python/src/jsonrpc_tp/jsonrpc_tp_types.py
Comment thread ocaml-jsonrpc-tp/python/src/jsonrpc_tp/jsonrpc_tp_types.py Outdated
Copy link
Copy Markdown
Contributor

@Janno Janno left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nothing much to add to Gregory's comments. The overall change looks good to me.

It might make sense to make the two classes final so that we can more easily switch to ty if we ever want to do that. (See https://skylabs-ai.atlassian.net/wiki/spaces/FM/pages/639336451/Python+Type+Checkers#Correct-isinstance()-behavior)

Comment thread ocaml-jsonrpc-tp/python/src/jsonrpc_tp/jsonrpc_tp_types.py
@jhaag-skylabs-ai jhaag-skylabs-ai force-pushed the ocaml-jsonrpc-tp/python/use-pydantic branch from df6602f to ac7a598 Compare March 5, 2026 17:30
@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented Mar 5, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base commit PR
fmdeps/rocq-agent-toolkit/ ocaml-jsonrpc-tp/python/use-pydantic fcaaa2e 56e7017 #282

Passive Repos

Repo Job Branch Job Commit
./ main e5c342a
fmdeps/BRiCk/ main b79c734
fmdeps/auto/ main ffda14f
fmdeps/auto-docs/ main 9f57097
bluerock/NOVA/ skylabs-proof 996d600
bluerock/bhv/ skylabs-main b1ca30d
fmdeps/brick-libcpp/ main dc9818e
fmdeps/ci/ main 7712f8c
vendored/elpi/ skylabs-master aa4475f
fmdeps/fm-ci/ main 262fb04
fmdeps/fm-tools/ main 430933c
psi/protos/ main 8fe3e7c
psi/backend/ main 196a186
psi/ide/ main 6b596cf
psi/data/ main 62ed81e
vendored/rocq/ skylabs-master 2ede3c9
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 7d620c1
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
-0.00% 122840.0 122840.0 -0.0 total
-0.00% 22632.7 22632.7 -0.0 ├ translation units
+0.00% 100207.4 100207.4 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
-0.00% 122840.0 122840.0 -0.0 total
-0.00% 22632.7 22632.7 -0.0 ├ translation units
+0.00% 100207.4 100207.4 +0.0 └ proofs and tests

@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented Mar 5, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base commit PR
fmdeps/rocq-agent-toolkit/ ocaml-jsonrpc-tp/python/use-pydantic b89ca34 56e7017 #282

Passive Repos

Repo Job Branch Job Commit
./ main e5c342a
fmdeps/BRiCk/ main b79c734
fmdeps/auto/ main ffda14f
fmdeps/auto-docs/ main 9f57097
bluerock/NOVA/ skylabs-proof 996d600
bluerock/bhv/ skylabs-main 8d08b1c
fmdeps/brick-libcpp/ main dc9818e
fmdeps/ci/ main 7712f8c
vendored/elpi/ skylabs-master aa4475f
fmdeps/fm-ci/ main 262fb04
fmdeps/fm-tools/ main 430933c
psi/protos/ main 8fe3e7c
psi/backend/ main 196a186
psi/ide/ main 6b596cf
psi/data/ main 62ed81e
vendored/rocq/ skylabs-master 2ede3c9
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 7d620c1
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
+0.00% 122903.6 122903.6 +0.0 total
+0.00% 22632.5 22632.5 +0.0 ├ translation units
+0.00% 100271.1 100271.1 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
+0.00% 122903.6 122903.6 +0.0 total
+0.00% 22632.5 22632.5 +0.0 ├ translation units
+0.00% 100271.1 100271.1 +0.0 └ proofs and tests

@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented Mar 5, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base commit PR
fmdeps/rocq-agent-toolkit/ ocaml-jsonrpc-tp/python/use-pydantic ec362f9 56e7017 #282
psi/backend/ ocaml-jsonrpc-tp/python/use-pydantic af89a42 196a186 #1259

Passive Repos

Repo Job Branch Job Commit
./ main e5c342a
fmdeps/BRiCk/ main b79c734
fmdeps/auto/ main ffda14f
fmdeps/auto-docs/ main 9f57097
bluerock/NOVA/ skylabs-proof 996d600
bluerock/bhv/ skylabs-main 8d08b1c
fmdeps/brick-libcpp/ main dc9818e
fmdeps/ci/ main 7712f8c
vendored/elpi/ skylabs-master aa4475f
fmdeps/fm-ci/ main 262fb04
fmdeps/fm-tools/ main 430933c
psi/protos/ main 8fe3e7c
psi/ide/ main 6b596cf
psi/data/ main 62ed81e
vendored/rocq/ skylabs-master 2ede3c9
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 7d620c1
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
+0.00% 122903.6 122903.6 +0.0 total
+0.00% 22632.5 22632.5 +0.0 ├ translation units
+0.00% 100271.1 100271.1 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
+0.00% 122903.6 122903.6 +0.0 total
+0.00% 22632.5 22632.5 +0.0 ├ translation units
+0.00% 100271.1 100271.1 +0.0 └ proofs and tests

Comment thread rocq-doc-manager/python/src/rocq_doc_manager/microrpc/deserialize.py Outdated
@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented Mar 5, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base commit PR
fmdeps/rocq-agent-toolkit/ ocaml-jsonrpc-tp/python/use-pydantic 6ef2266 56e7017 #282
psi/backend/ ocaml-jsonrpc-tp/python/use-pydantic af89a42 196a186 #1259

Passive Repos

Repo Job Branch Job Commit
./ main e5c342a
fmdeps/BRiCk/ main b79c734
fmdeps/auto/ main ffda14f
fmdeps/auto-docs/ main 9f57097
bluerock/NOVA/ skylabs-proof 996d600
bluerock/bhv/ skylabs-main 8d08b1c
fmdeps/brick-libcpp/ main dc9818e
fmdeps/ci/ main 7712f8c
vendored/elpi/ skylabs-master aa4475f
fmdeps/fm-ci/ main 262fb04
fmdeps/fm-tools/ main 430933c
psi/protos/ main 8fe3e7c
psi/ide/ main 6b596cf
psi/data/ main 62ed81e
vendored/rocq/ skylabs-master 2ede3c9
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 7d620c1
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
+0.00% 122903.5 122903.5 +0.0 total
+0.00% 22632.4 22632.4 +0.0 ├ translation units
+0.00% 100271.1 100271.1 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
+0.00% 122903.5 122903.5 +0.0 total
+0.00% 22632.4 22632.4 +0.0 ├ translation units
+0.00% 100271.1 100271.1 +0.0 └ proofs and tests

@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented Mar 5, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base commit PR
fmdeps/rocq-agent-toolkit/ ocaml-jsonrpc-tp/python/use-pydantic e723c73 56e7017 #282
psi/backend/ ocaml-jsonrpc-tp/python/use-pydantic af89a42 196a186 #1259

Passive Repos

Repo Job Branch Job Commit
./ main e5c342a
fmdeps/BRiCk/ main b79c734
fmdeps/auto/ main ffda14f
fmdeps/auto-docs/ main 9f57097
bluerock/NOVA/ skylabs-proof 996d600
bluerock/bhv/ skylabs-main 8d08b1c
fmdeps/brick-libcpp/ main dc9818e
fmdeps/ci/ main 7712f8c
vendored/elpi/ skylabs-master aa4475f
fmdeps/fm-ci/ main 262fb04
fmdeps/fm-tools/ main 430933c
psi/protos/ main 8fe3e7c
psi/ide/ main 6b596cf
psi/data/ main 62ed81e
vendored/rocq/ skylabs-master 2ede3c9
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 7d620c1
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
-0.00% 122903.6 122903.5 -0.0 total
-0.00% 22632.4 22632.5 -0.0 ├ translation units
+0.00% 100271.1 100271.1 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
-0.00% 122903.6 122903.5 -0.0 total
-0.00% 22632.4 22632.5 -0.0 ├ translation units
+0.00% 100271.1 100271.1 +0.0 └ proofs and tests

@jhaag-skylabs-ai
Copy link
Copy Markdown
Contributor Author

jhaag-skylabs-ai commented Mar 5, 2026

@gmalecha-at-skylabs this is ready for another review. Please take a close look at rocq_doc_manager/microrpc/deserialize.py to ensure that the revised Exception (de)serialization logic is safe+secure :~)

@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented Mar 5, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base commit PR
fmdeps/rocq-agent-toolkit/ ocaml-jsonrpc-tp/python/use-pydantic c9f0c37 56e7017 #282
psi/backend/ ocaml-jsonrpc-tp/python/use-pydantic af89a42 196a186 #1259

Passive Repos

Repo Job Branch Job Commit
./ main e5c342a
fmdeps/BRiCk/ main b79c734
fmdeps/auto/ main ffda14f
fmdeps/auto-docs/ main 9f57097
bluerock/NOVA/ skylabs-proof 996d600
bluerock/bhv/ skylabs-main 8d08b1c
fmdeps/brick-libcpp/ main dc9818e
fmdeps/ci/ main 7712f8c
vendored/elpi/ skylabs-master aa4475f
fmdeps/fm-ci/ main 262fb04
fmdeps/fm-tools/ main 430933c
psi/protos/ main 8fe3e7c
psi/ide/ main 6b596cf
psi/data/ main 62ed81e
vendored/rocq/ skylabs-master 2ede3c9
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 7d620c1
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
+0.00% 122903.6 122903.6 +0.0 total
+0.00% 22632.5 22632.5 +0.0 ├ translation units
+0.00% 100271.1 100271.1 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
+0.00% 122903.6 122903.6 +0.0 total
+0.00% 22632.5 22632.5 +0.0 ├ translation units
+0.00% 100271.1 100271.1 +0.0 └ proofs and tests

@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented Mar 5, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base commit PR
fmdeps/rocq-agent-toolkit/ ocaml-jsonrpc-tp/python/use-pydantic 218fa41 56e7017 #282
psi/backend/ ocaml-jsonrpc-tp/python/use-pydantic af89a42 196a186 #1259

Passive Repos

Repo Job Branch Job Commit
./ main e5c342a
fmdeps/BRiCk/ main b79c734
fmdeps/auto/ main ffda14f
fmdeps/auto-docs/ main 9f57097
bluerock/NOVA/ skylabs-proof 996d600
bluerock/bhv/ skylabs-main 8d08b1c
fmdeps/brick-libcpp/ main dc9818e
fmdeps/ci/ main 7712f8c
vendored/elpi/ skylabs-master aa4475f
fmdeps/fm-ci/ main 262fb04
fmdeps/fm-tools/ main 430933c
psi/protos/ main 8fe3e7c
psi/ide/ main 6b596cf
psi/data/ main 62ed81e
vendored/rocq/ skylabs-master 2ede3c9
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 7d620c1
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
-0.00% 122903.5 122903.5 -0.0 total
-0.00% 22632.4 22632.4 -0.0 ├ translation units
+0.00% 100271.1 100271.1 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
-0.00% 122903.5 122903.5 -0.0 total
-0.00% 22632.4 22632.4 -0.0 ├ translation units
+0.00% 100271.1 100271.1 +0.0 └ proofs and tests

@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented Mar 5, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base commit PR
fmdeps/rocq-agent-toolkit/ ocaml-jsonrpc-tp/python/use-pydantic 5fced9d 56e7017 #282
psi/backend/ ocaml-jsonrpc-tp/python/use-pydantic af89a42 196a186 #1259

Passive Repos

Repo Job Branch Job Commit
./ main e5c342a
fmdeps/BRiCk/ main b79c734
fmdeps/auto/ main ffda14f
fmdeps/auto-docs/ main 9f57097
bluerock/NOVA/ skylabs-proof 996d600
bluerock/bhv/ skylabs-main 8d08b1c
fmdeps/brick-libcpp/ main dc9818e
fmdeps/ci/ main 7712f8c
vendored/elpi/ skylabs-master aa4475f
fmdeps/fm-ci/ main 262fb04
fmdeps/fm-tools/ main 430933c
psi/protos/ main 8fe3e7c
psi/ide/ main 6b596cf
psi/data/ main 62ed81e
vendored/rocq/ skylabs-master 2ede3c9
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 7d620c1
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
-0.00% 122903.6 122903.6 -0.0 total
-0.00% 22632.5 22632.5 -0.0 ├ translation units
+0.00% 100271.1 100271.1 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
-0.00% 122903.6 122903.6 -0.0 total
-0.00% 22632.5 22632.5 -0.0 ├ translation units
+0.00% 100271.1 100271.1 +0.0 └ proofs and tests

Comment thread rocq-doc-manager/python/src/rocq_doc_manager/microrpc/deserialize.py Outdated
Comment thread rocq-doc-manager/python/src/rocq_doc_manager/microrpc/deserialize.py Outdated
Copy link
Copy Markdown
Contributor

@gmalecha-at-skylabs gmalecha-at-skylabs left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My main concern right now is that this might be breaking the wire-protocol that we are talking between the client and the server. If so, then we need to do a release afterwards and that warrants more testing. If we can restrict these changes to only affect the logging infrastructure, then we would de-risk this.

While being explicit is a bit verbose, I'm actually thinking that maybe we should go and define very explicit protocol classes so that we can actually rigorously define all of the data types that are used and get all of these statically checked.

Copy link
Copy Markdown
Contributor

@rlepigre-skylabs-ai rlepigre-skylabs-ai left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Everything outside of deserialize.py looks good to me. I have not looked at that last file very much since there are open thread already.

result: T_resp


# Note: explicitly /not/ final because clients may want derived exception types
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not sure this comment is useful honestly.

Suggested change
# Note: explicitly /not/ final because clients may want derived exception types

@skylabs-ai-ci
Copy link
Copy Markdown

skylabs-ai-ci Bot commented Mar 6, 2026

CI summary (Details)

Active Repos

Repo Job Branch Job Commit Base branch Base commit PR
fmdeps/rocq-agent-toolkit/ ocaml-jsonrpc-tp/python/use-pydantic ebd311d main 56e7017 #282
psi/backend/ ocaml-jsonrpc-tp/python/use-pydantic af89a42 main 196a186 #1259

Passive Repos

Repo Job Branch Job Commit
./ main e5c342a
fmdeps/BRiCk/ main b79c734
fmdeps/auto/ main 61983bb
fmdeps/auto-docs/ main 9f57097
bluerock/NOVA/ skylabs-proof 996d600
bluerock/bhv/ skylabs-main 8d08b1c
fmdeps/brick-libcpp/ main dc9818e
fmdeps/ci/ main 4f94f40
vendored/elpi/ skylabs-master aa4475f
fmdeps/fm-ci/ main 262fb04
fmdeps/fm-tools/ main 430933c
psi/protos/ main 8fe3e7c
psi/ide/ main 6b596cf
psi/data/ main 62ed81e
vendored/rocq/ skylabs-master 2ede3c9
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 7d620c1
vendored/vsrocq/ skylabs-main 5b4527e

Performance

Relative Master MR Change Filename
-0.00% 122929.5 122929.5 -0.0 total
-0.00% 22632.7 22632.7 -0.0 ├ translation units
+0.00% 100296.8 100296.8 +0.0 └ proofs and tests
Full Results
Relative Master MR Change Filename
-0.00% 122929.5 122929.5 -0.0 total
-0.00% 22632.7 22632.7 -0.0 ├ translation units
+0.00% 100296.8 100296.8 +0.0 └ proofs and tests

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants