Sacha Ayoun

I think this is ready to be merged!

I think this is ready to be merged

Ah, this went out of sync :/

Interesting. I am not in control of the string that gets put there, only of the IrepId I choose: https://github.com/model-checking/kani/blob/main/cprover_bindings/src/irep/irep_id.rs#L905 We could maybe use "#annotation"? But I don't know its...

@danielsn proposed that we have our own kind of comments, such as `#kani_comment` or `#kani_meta`, which we could put anywhere we want on the Ireps Right now, the encoding of...

The file comes from here https://github.com/revery-ui/reason-harfbuzz/blob/master/src/harfbuzz.js If I was to guess, this looks like the output of a JS formatter like prettier. Trailing commas for multi-line function parameters are useful...

I didn't realise it was because of the trailing comma though, I created [a PR for reason-harfbuzz](https://github.com/revery-ui/reason-harfbuzz/pull/14) to remove the trailing comma

Yes, sorry the wording was unclear I am modifying the `@doc` alias to also generate LaTeX in addition to the HTML, it will be built in a `_latex` folder next...

I'm not really sure where to restrict the feature to dune > 3.1, where should I be adding a guard? In the `gen_rules` function?

Additionally, I'm trying to get things to work using directory targets, but I get ``` File "_doc/_html/scope1/_unknown_", line 1, characters 0-0: Error: Rules with directory targets must be sandboxed. ```...