00:09 <dh`> I would expect that you can try, and get back text, and have it be vaguely right some of the time

01:25 <discocaml> <diligentclerk> yeah I'm wondering whether that's better than nothing or not

01:33 <discocaml> <darrenldl> i guess depends on whether you want your analysis to be at least sound or at least complete

01:33 <discocaml> <darrenldl> maybe coverage is the better word

01:34 <discocaml> <darrenldl> anyhow, AI does neither, so not really sure what's the right measure of success

01:45 <discocaml> <diligentclerk> correctness is only important here to the degree that incorrectness is going to waste my time by sending me on a wild goose chase, I think.

01:45 <discocaml> <diligentclerk> I'll give it a shot

01:52 <discocaml> <darrenldl> then LLM is pretty much guaranteed to waste your time then, especially with OCaml code

01:54 <discocaml> <darrenldl> i would personally just try putting together (haphazardly) a function call graph extraction tool, if one does not exist yet

02:02 <discocaml> <darrenldl> the tool itself doesn't even need to do the plotting, with d2, mermaid, plantml, and graphviz dot around

02:04 <discocaml> <darrenldl> proponents of LLM have been quite vocal about "only need to double check LLM's work manually is still faster than doing it by hand", but in this case it feels like to be able to double check, you'd need to read all the code anyway

03:18 <dh`> a module dependency graph is probably more useful

03:18 <dh`> call graphs are awkwardly large for something the size of rocq

03:18 <dh`> also surprisingly hard to extract reliably

03:32 <discocaml> <darrenldl> good point

03:32 <discocaml> <darrenldl> yeah, easier to parse and extract just module usage

05:20 <discocaml> <bluddy5> LLMs are often better at reading and explaining code than they are at creating code that considers all the subtleties of a large codebase. I know that in C++ they can be spectacular at diving in and giving you a good overview. But there's a huge disparity between models, to the point that you'll get entirely different experiences. Claude sonnet and chatgpt 5 will probably give you the best information. With sonnet, I was even able to essential

05:20 <discocaml> <bluddy5> I have no idea if they're anywhere close to this in ocaml, but it's worth a shot.

08:53 <discocaml> <charstring.> When generating Python code, I've had it create better code by asking it to solve the problem in Haskell or OCaml and only then make the Python function.

08:54 <discocaml> <diligentclerk> alright claude's website mentions a tool that does what I was talking about, you can just feed the whole Coq repo in and ask it a couple questions

23:33 <discocaml> <diligentclerk> I tried Flix and it seems interesting. In OCaml algebraic effects are handled kind of "individually" - one "exception" corresponds to a single exception handler. But in Flix effects are whole namespaces with grouped/related functionality, there is a `Console` effect and you can do `Console.write`, `Console.read`, etc; it looks almost like dynamically scoped *modules*. In the the "Hello world" wordcount program on their website, the main

23:33 <discocaml> <diligentclerk> `def wc(file: String): Unit \ {Console, FileReadWithResult} = {...}`

23:33 <discocaml> <diligentclerk> and it seems like the read is that `Console` and `FileReadWithResult` should be here understood as something like module types / interfaces, where we require that at the call site of `wc` there should be dynamically installed "handlers" which specify modules implementing the effect `Console` and `FileReadWithResults`.

23:35 <discocaml> <diligentclerk> This is complicated and novel to me so I'm trying to better understand it. Can we make this precise, has anyone written down an ML with "dynamically scoped modules", in which, like Flix, a function requires static annotations as to what modules are in scope? In what ways would this be more expressive/less expressive than modular implicits? It seems like in some ways the functionality would overlap.

23:42 <discocaml> <diligentclerk> https://blog.ezyang.com/2020/08/dynamic-scoping-is-an-effect-implicit-parameters-are-a-coeffect/

23:42 <discocaml> <diligentclerk> This seems relevant. Modular implicits are implicit parameters, after all, so I might be mixing some things up.

23:45 <discocaml> <diligentclerk> Although I am never quite sure whether a distinction between A and co-A is really meaningful or a matter of perspective. For example, by currying a function A x B -> C is equivalent to a function B -> C^A. But (A x -) is a co-monad and (-)^A is a monad. The difference between "this is a comonad" and "this is a monad" is just a matter of perspective here. So saying "ah, this is really a co-monadic phenomon rather than a monadic one" doesn