Good First Issues in Ocaml

Problem Right now each of our optimization passes uses the same symbol generator which builds sym1__, sym2__, sym3__, symN__. When there is a change in the optimizer you end up with a bunch of sym*__ changes and it is very hard to grep and grock when and why those changes happened. Possible Answer We should have a symbol name generator that operates per optimization. So for each pass we would generate sym{PASS_NAME}1__, ..., sym{PASS_NAME}N__. I think this will make it easier to read what caused a change and where.

Astrée apparently found it to be useful to use the constants (minus 1) in assignments such as x = x % 10 (here: 10) as additional widening thresholds. We should consider this also in our autotuner. They did not mention a specific example, but here is a simple example: int x = 0; while (nondet()) { x = (x + 1) % 10; } assert(x <= 10); In the example above, narrowing recovers precision, but here it wouldn't: int x = 1; while (nondet()) { if (x % 10 == 0) x = 1; else x++; } assert(x <= 10); In more realistic examples, this would probably be related to something such as a ring buffer maintaining the last k entries. Given this is only one additional line of code, I think it's worth trying.

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.

I think it can be beneficial for the markdown backend to support line tags (https://ocaml.github.io/odoc/odoc/odoc_for_authors.html#line-tags), and it currently fits the design of frontmatter data. I wonder whether we should make it a setting or set it as the default. What would you say? From jonludlam/parseff@7d0cd4e#diff-346adc8f62cbd27737f177027dba7b4a9bb7d64d9c48f6738624a88281949e36R1-R2 @short_title Quick start @children_order primitives combinators repetition convenience errors diagnostics zero-copy streaming binary utf8 guides/ parseff/ src/ --- short_title: "Quick start" children_order: ["primitives", "combinators", "repetition", "convenience", "errors", "diagnostics", "zero-copy", "streaming", "binary", "utf8", "guides/", "parseff/", "src/"] --- # Article Content Begins Here Something worth pointing out is that "children_order" won't be used in the markdown case, and the list is viable fields is limited, wonder if this is by design and there's a solid reason behind.

Since OCaml 5.4, one can annotate a mutable record field to have atomic getters and setters. This information should be reflected in odoc's display of the field!

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!