Good First Issues in Ocaml

See #1674 for an initial attempt. Thanks to @sims1253 for the suggestion There are several functions that historically duplicated work and now can be done in a single call returning a tuple. These were primarily added in stan-dev/math#2931: qr: replaces calls to qr_Q/qr_R qr_thin: replaces calls to qr_thin_Q/qr_thin_R eigendecompose_sym: replaces calls to eigenvalues_sym/eigenvectors_sym eigendecompose: replaces calls to eigenvalues/eigenvectors complex_schur_decompose: replaces calls to complex_schur_decompose_t/complex_schur_decompose_u svd: replaces calls to svd_U/svd_V csr_extract : replaces calls to csr_extract_u/csr_extract_v/csr_extract_w The proposal is to add a small optimization which detects cases where these are called one after the other and rewrite them to use the combined version. It may also be useful to separately flag a warning for models where the older functions are both called on the same thing.

A comment on Hacker News I agree with the OP here. Rather than blindly following Rust, I strongly believe that having a unique error handling system that goes well with the ideologies of wyzer will make it a more fun language to work with.

While reviewing https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1686, I did runs with sem.malloc.fail enabled and found differences in memory leak analysis. For example, the result for sv-benchmarks/c/ldv-memsafety/memleaks_test1-3.i changes. In particular, it seems that calling free on a pointer, which can be known or NULL is less precise than just with the known pointer in the memLeak analysis. However, that shouldn't be the case: free(NULL) is fine and a no-op. This also seems to affect at least 1175 tasks in sv-benchmarks/Juliet_Test/.

While reviewing https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1686, I did runs with sem.malloc.fail enabled and found differences in tasks using alloca. According to the man page, alloca can never return NULL: RETURN VALUE The alloca() function returns a pointer to the beginning of the allocated space. If the allocation causes stack overflow, program behavior is undefined.

Currently I believe C-c C-y (split) doesn't work if a window modality would be required. Ideally it should just work if the term is a modally annotated free variable, since the window can be guessed to be its annotation, and should also allow the user to input a term behind a modal annotation to specify the window.

What to build The generated coverage report (packages/css-grammar/data/coverage.md, make css-oracle) lists 185 missing standard properties, 47 legacy aliases, and 80 missing functions, each with its spec id and value-definition syntax. This is the umbrella issue for burning that list down. Work through it by spec module (e.g. css-borders-4, css-overflow-4, css-rhythm-1), not property-by-property, so shared value types land once. A contributor guide describing the end-to-end recipe for adding a property (spec dialect, runtime witnesses, testing, oracle regeneration) lives at documents/adding-css-properties.md. Important caveats: The syntax strings in the report come from the specs and are not paste-ready: styled-ppx's spec dialect diverges (interpolation alternatives, runtime witnesses in the hand-maintained type modules). Auto-generation of specs has been evaluated and rejected. Every addition must update the coverage report (make css-oracle) — CI gates on staleness. Acceptance cri

Following some discussions at Gobcon, it seems that dominance elimination in the sense of Paznikov et al. (https://arxiv.org/abs/2512.05555, and also Flanagan & Freund and Choi et al. earlier) may also be useful for taming the number of race reports. It also seems that if one follows their definition, the property of being true/false alarms is preserved: If r1 dominates r2, r2 is a true race iff r1 is a true race.

The code that inspects the declared output type of a datatype constructor and extracts its indices assumes that its head is a constant. This means it is impossible to use explicit-output syntax in a local datatype defined with let rec, and hence also to define local indexed datatypes, since in that case the head is a metavariable. This should be a fairly simple fix, in Check.check_data add a clause testing equality of two metavariables with their environments alongside the one that tests equality of two constants.

Documented here: https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_selectionRange Demo of this feature using Rust's LSP: Screen.Recording.2026-07-08.at.16.28.52.mov A very simple first version could be to expand a selection to the entire sentence. This is exactly what rocq-lsp does. This would be very easy to implement. In the future, the implementation could be extended to increase selections based on the AST structure (especially in Gallina).

Repro case: module type A = sig type a end module type B = sig type b end module A : A = struct type a end module B : B = struct type b end module F (_ : A) (_ : B) = struct end module Test = F(B)(A) Merlin shows the following error message: 2. Modules do not match: A : sig type a = A.a end is not included in B (The exact same thing is in the *Messages* and *merlin-errors* buffer.) This is only the last line of the full error message shown by the compiler: Error: This application of the functor F is ill-typed. These arguments: B A do not match these parameters: (Arg : A) (Arg : B) -> ... 1. Modules do not match: B : sig type b = B.b end is not included in A The type a is required but not provided File "test.ml", line 1, characters 20-26: Expected declaration 2. Modules do not match: A : sig type a = A.a end is not included in B

The string type is still defined in the Structure module as a built in gospel type but it is not used as model for any OCaml type. Indeed, the model for OCaml strings is char sequence (which makes perfect sense). This can be a bit confusing for an unaware user as one will have some type checking errors when using Gospel strings to talk about OCaml ones. For instance, this piece of specification, though quite natural, won't type check, accepting the person type declaration but failing on the ensures clause: (*@ type person = { firstname: string; lastname: string } *) type t (*@ model : person *) val make : string -> string -> t (*@ t = make firstname lastname ensures t = { firstname; lastname } *) A possible bonus would be to parse "example" as a char sequence.

I had copy-pasted the theme setting that goes at the top from a pager which left a bunch of whitespace I hadn't seen. ---__________ theme: vanier ---__________ I was puzzled as to why it would display verbatim in the slides. I later worked out what the issue was. It might be useful to strip the whitespace after the --- or at least warn the user abuot it.

Implement the dead simple rule that catches x := x, because apparently some implementations of ST allow this.

For reviewing #1965, I read some documentation on signal handlers. There is in particular this rule An async-signal-safe function is one that can be safely called from within a signal handler. Many functions are not async-signal-safe. In particular, nonreentrant functions are generally unsafe to call from a signal handler. https://man7.org/linux/man-pages/man7/signal-safety.7.html and a list of such async-signal-safe functions. We may want to add an analysis that tracks whether the current thread is a signal handler, and warn whenever a library function that is not async-signal-safe is called. May be a good BSc project.

Some of the OCAMLRUNPARAM parameters (see documentation in the manual) denote memory space, and their units are typically in words. For example s=2M requests 2^20 words of minor heap size, that is 16 Mibibytes (MiB) on 64bits machines. I find this very confusing, and I always read those as MiB. I propose to add support for units w (words) and B (bytes), where bytes are translated back to words following the current machine word size. This would let users (optionally) be explicit and clear in their setting, s=2MB or s=2Mw. Note: I considered asking for using 2MiB as well, to be explicit that those are power-of-two units, but this introduces a risk of confusion as users might then assume that 2MB is in base ten (uncommon in computer science... except for disk space).

Hi team, as discussed in #general > Guidance on translating recursive code @ 💬 Zulip it should be possible to support early returns inside loops if they are equivalent to breaks. For instance (using Aeneas and Charon built from 39e3086), charon cargo --preset=aeneas runs successfully for the code below: fn my_fn(x: i32) -> Option<i32> { if x >= 0 { let mut y = x; loop { if y == 0 { return Some(y); } if y % 2 == 1 { y /= 2; } else { break; } } } None } fn main() { println!("{:?}", my_fn(42)); } And fails with aeneas -backend lean return_inside_loop.llbc with error: [�[92mInfo�[39m ] Imported: return_inside_loop.llbc �[?25lApplied prepasses: [----------------------------------------------------] 0/9 ⠋ Applied prepasses: [#####-----------------------------------------------] 1/9 ⠋ Applied prepasses: [#########################

This might be a thing of the past if we continue our encoding/decoding trajectory, however, if we do have a migration error I think we can do much better in terms of what the error actually says. For example, for many users it is not obvious that this even has anything to do with a ppx let along ppxlib! See: https://mathstodon.xyz/@jonmsterling/116085163003251340 I think we should mention more things and potentially point to ocaml-ppx/ppxlib/issues :)

See ocaml/ocaml-lsp#1586

Desired Behavior Imagine you have an editor extension enabled that can format your dune files (dune, dune-project, etc.) on save, using dune format-dune-file under the hood. I think now if you have a build running in watch mode in the project, this no longer works. The format command conflicts with the build locks. I think this use to work before dune.3.21 but I suspect something changed. Repro? I'd appreciate if someone else can confirm as I am not sure exactly sure from where this workflow comes from (dune.el?). I have noticed it via some other layer with the reformatter emacs package (using this setup). Not sure if this applies to other users. Thanks!

Following a conversation on the Zulip: the max length of a Vec is Isize::max, not Usize::max. Some proofs will likely need to be fixed (in particular the hashmap and the AVL tree).

Describe the bug I was debugging why some tests work when run on a single file, but not when run in batch on the whole directory with other rules and tests, as well as why I cannot limit semgrep not to take all available threads when running tests. It turned out, if run in a batch, the rule evaluation may be longer than expected. I actually expect it as the rule is quite complex and I adjust the timeout variable. However, it's turned out this configuration, as well as multiple others, are not propagated when using scan --test. To Reproduce You don't actually need to trigger the problem, the debug output is enough. So: Have any rules with tests Run semgrep scan --metrics=off -j 2 --disable-version-check --debug --max-memory=500 --timeout 10 --timeout-threshold=15 --test 2> out.txt After finishing, open out.txt and search for -timeout Find something like: [00.29][�[34mINFO�[0m]: Executed as: /home/..../semgrep/bin/semgrep-core -json -rules /tmp/tmp3stg9f5w.json -targets /tmp/tmpgd3

The mli file lacks the declaration. To be honest I find the addition of this Empty exception was a bad idea. The justification in #1080 was that it made the error less confusing and make Random.choice behave more like other modules. I disagree on both points: Random.choice on a empty enum is the poster child of "invalid argument". Do we believe that Invalid_arg should never be used at all and that we should have a distinct exception for every possible error path? Clearly, nobody really use exceptions like that, or I wouldn't be the first to notice this one not being catchable :) Also, other modules that raise Empty are containers (queues, stack...), and they raise Empty when the container is empty, which makes perfect sense. But what does it mean for a random generator to be empty? Have it reached the end of the random sequence or what? That's a bit confusing, while "invalid argument" points right at the culprit: the argument, which is invalid.