Added some details to the first few sections of auto-docs#12
Open
LennartATSkylabsAI wants to merge 3 commits intomainfrom
Open
Added some details to the first few sections of auto-docs#12LennartATSkylabsAI wants to merge 3 commits intomainfrom
LennartATSkylabsAI wants to merge 3 commits intomainfrom
Conversation
LennartATSkylabsAI
added
the
documentation
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | e8e81bb |
| fmdeps/BRiCk/ | main | 902bdd0 |
| fmdeps/auto/ | main | 33373ac |
| bluerock/NOVA/ | skylabs-proof | 6cbef03 |
| bluerock/bhv/ | skylabs-main | 448828c |
| fmdeps/brick-libcpp/ | main | 302bf88 |
| fmdeps/ci/ | main | 6dff30c |
| 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.04% | 124531.2 | 124481.3 | -49.9 | total |
| -0.04% | 49.8 | - | -49.8 | ├ disappeared files (2) |
| -0.00% | 124481.3 | 124481.3 | -0.0 | └ common files |
| +0.00% | 22655.0 | 22655.0 | +0.0 | ├ translation units |
| -0.00% | 101826.2 | 101826.3 | -0.1 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -0.04% | 124531.2 | 124481.3 | -49.9 | total |
| -0.04% | 49.8 | - | -49.8 | ├ disappeared files (2) |
| -0.00% | 124481.3 | 124481.3 | -0.0 | └ common files |
| +0.00% | 22655.0 | 22655.0 | +0.0 | ├ translation units |
| -0.00% | 101826.2 | 101826.3 | -0.1 | └ proofs and tests |
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | e8e81bb |
| fmdeps/BRiCk/ | main | 902bdd0 |
| fmdeps/auto/ | main | 33373ac |
| bluerock/NOVA/ | skylabs-proof | 6cbef03 |
| bluerock/bhv/ | skylabs-main | 448828c |
| fmdeps/brick-libcpp/ | main | 302bf88 |
| fmdeps/ci/ | main | 6dff30c |
| 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.01% | 124531.2 | 124518.1 | -13.1 | total |
| -0.01% | 17.3 | - | -17.3 | ├ disappeared files (1) |
| +0.00% | 124518.1 | 124513.8 | +4.2 | └ common files |
| -0.00% | 22655.0 | 22655.0 | -0.0 | ├ translation units |
| +0.00% | 101863.0 | 101858.8 | +4.2 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +11.20% | 32.5 | 36.2 | +3.6 | fmdeps/auto-docs/content/docs/functions/verification.v |
| -0.01% | 124531.2 | 124518.1 | -13.1 | total |
| -0.01% | 17.3 | - | -17.3 | ├ disappeared files (1) |
| +0.00% | 124518.1 | 124513.8 | +4.2 | └ common files |
| -0.00% | 22655.0 | 22655.0 | -0.0 | ├ translation units |
| +0.00% | 101863.0 | 101858.8 | +4.2 | └ proofs and tests |
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | e8e81bb |
| fmdeps/BRiCk/ | main | 902bdd0 |
| fmdeps/auto/ | main | b45c3e8 |
| bluerock/NOVA/ | skylabs-proof | 6cbef03 |
| bluerock/bhv/ | skylabs-main | 448828c |
| fmdeps/brick-libcpp/ | main | 302bf88 |
| fmdeps/ci/ | main | 6dff30c |
| 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 | 0b5fea6 |
| 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.01% | 124547.9 | 124555.9 | +8.0 | total |
| -0.00% | 22655.3 | 22655.3 | -0.0 | ├ translation units |
| +0.01% | 101900.6 | 101892.6 | +8.0 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +11.20% | 32.5 | 36.2 | +3.6 | fmdeps/auto-docs/content/docs/functions/verification.v |
| +21.80% | 17.3 | 21.1 | +3.8 | fmdeps/auto-docs/content/docs/control_flow/loop.v |
| +0.01% | 124547.9 | 124555.9 | +8.0 | total |
| -0.00% | 22655.3 | 22655.3 | -0.0 | ├ translation units |
| +0.01% | 101900.6 | 101892.6 | +8.0 | └ proofs and tests |
Comment on lines
+15
to
+17
| /* void ref_arg(int& r) { r++; }; | ||
|
|
||
| void rv_ref_arg(int&& r); | ||
| void rv_ref_arg(int&& r);*/ |
Collaborator
There was a problem hiding this comment.
If they are not relevant, let's remove them entirely.
| ## By-reference arguments | ||
|
|
||
| Formal parameters that are passed by reference, e.g. `int&` can be specified using `\arg` with the `Vref` value constructor, | ||
| thus making explicit that the value is a proper non-null reference. |
Collaborator
There was a problem hiding this comment.
Vref is just a notation for Vptr, so nothing is really made explicit here.
gmalecha-at-skylabs
approved these changes
May 6, 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
2 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.
Sections covered: initial sections up to (including) 'Learn - Classes - Class Representation Predicates"