chore: Bump opam deps for new dune#144
Merged
rlepigre-skylabs-ai merged 8 commits intomainfrom May 7, 2026
Merged
Conversation
pgiarrusso-sl
changed the title
Contributor
rlepigre-skylabs-ai
left a comment
rlepigre-skylabs-ai
left a comment
There was a problem hiding this comment.
If we're bumping, it might make sense to bump all dependencies that can be bumped, including OCaml. I'm fine doing this in several steps though, my only concern is that it's more disruption to do it in several.
Contributor
Author
Oh agree — I bumped OCaml too by hand, but probably I should have removed all constraints, and didn't. |
pgiarrusso-sl
force-pushed
the
chore/bump
branch
from
a88ed8f to
96e84e8
Compare
Goal: let opam pick new versions.
Implementation: `s/ \{[^|&]*$//` regexp.
Because `opam install ../skylabs-deps.opam` doesn't pick the latest compiler.
This is based on the output of ``` opam install -y dev/opam-deps/skylabs-deps.opam -j5 && opam lock skylabs-deps ``` I readded conf-linux-libc-dev and ocaml-option-fp by hand.
pgiarrusso-sl
force-pushed
the
chore/bump
branch
from
96e84e8 to
bcc4cac
Compare
Contributor
|
Looks like |
Contributor
Author
|
The upstream issue is ocaml/dune#12904. |
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| fmdeps/BRiCk/ | main | 902bdd0 |
| fmdeps/auto/ | main | 33373ac |
| fmdeps/auto-docs/ | main | bfa8f2d |
| bluerock/NOVA/ | skylabs-proof | 6cbef03 |
| bluerock/bhv/ | skylabs-main | 448828c |
| fmdeps/brick-libcpp/ | main | 302bf88 |
| vendored/elpi/ | skylabs-master | aa4475f |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| fmdeps/fm-ci/ | main | 262fb04 |
| fmdeps/fm-tools/ | main | e17f6db |
| psi/protos/ | main | 8fe3e7c |
| psi/backend/ | main | a5fa400 |
| psi/ide/ | main | 6b596cf |
| psi/data/ | main | 76acc2f |
| vendored/rocq/ | skylabs-master | 2ede3c9 |
| fmdeps/rocq-agent-toolkit/ | main | ac7e4ec |
| 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 | 62d34c3 |
| vendored/vsrocq/ | skylabs-main | 5b4527e |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.00% | 125653.9 | 125653.9 | +0.0 | total |
| +0.00% | 22787.2 | 22787.1 | +0.0 | ├ translation units |
| +0.00% | 102866.8 | 102866.8 | +0.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.00% | 125653.9 | 125653.9 | +0.0 | total |
| +0.00% | 22787.2 | 22787.1 | +0.0 | ├ translation units |
| +0.00% | 102866.8 | 102866.8 | +0.0 | └ proofs and tests |
The script now additionally extracts data to jsonl format, using the provided [dune trace cat] command. This contains strictly more data than what we used to collect with [dune-report].
rlepigre-skylabs-ai
force-pushed
the
chore/bump
branch
from
c4eb9e6 to
0722e38
Compare
rlepigre-skylabs-ai
force-pushed
the
chore/bump
branch
from
0722e38 to
d78be06
Compare
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| fmdeps/BRiCk/ | main | 902bdd0 |
| fmdeps/auto/ | main | 33373ac |
| fmdeps/auto-docs/ | main | bfa8f2d |
| bluerock/NOVA/ | skylabs-proof | 6cbef03 |
| bluerock/bhv/ | skylabs-main | 448828c |
| fmdeps/brick-libcpp/ | main | 302bf88 |
| vendored/elpi/ | skylabs-master | aa4475f |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| fmdeps/fm-ci/ | main | 262fb04 |
| fmdeps/fm-tools/ | main | e17f6db |
| psi/protos/ | main | 8fe3e7c |
| psi/backend/ | main | a5fa400 |
| psi/ide/ | main | 6b596cf |
| psi/data/ | main | 76acc2f |
| vendored/rocq/ | skylabs-master | 2ede3c9 |
| fmdeps/rocq-agent-toolkit/ | main | ac7e4ec |
| 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 |
| vendored/vsrocq/ | skylabs-main | 5b4527e |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.00% | 125653.9 | 125653.9 | +0.0 | total |
| +0.00% | 22787.2 | 22787.1 | +0.0 | ├ translation units |
| +0.00% | 102866.8 | 102866.8 | +0.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.00% | 125653.9 | 125653.9 | +0.0 | total |
| +0.00% | 22787.2 | 22787.1 | +0.0 | ├ translation units |
| +0.00% | 102866.8 | 102866.8 | +0.0 | └ proofs and tests |
Janno
approved these changes
May 7, 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
3 participants
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.
Just a proposal for testing. This would let us solve the cram test issues at least.
This wasn't scheduled and finding compatible versions was more than the "5 minutes" I was hoping but still okayish.
Fix https://github.com/SkyLabsAI/skylabs-fm/issues/259.