07:06 <discocaml> <systems1965> any news on when the windows port might be available 🙂

11:31 <discocaml> <ada2k> windows port of what

13:20 <discocaml> <jmiven> if you're asking about opam, then last month 🙂 https://www.ocaml.org/changelog/2024-07-01-opam-2-2-0

16:23 <neiluj> hey

16:25 <neiluj> how do I force dune to use a specific C compiler?

16:25 <discocaml> <heyting> Hello all. I want to grasp basic to intermediate ocaml so I can navigate the source code of the Coq proof assistant. Which literature on ocaml would best suit me? I am familiar with haskell, coq, java, python

16:27 <neiluj> how do I force dune to use a specific C compiler?

16:38 <Anarchos> heyting free book : https://dev.realworldocaml.org/

16:40 <discocaml> <systems1965> https://ocaml.org/releases/5.2.0

16:40 <discocaml> <systems1965> Says

16:40 <discocaml> <systems1965> The Windows MSVC port is still unavailable.

16:41 <discocaml> <systems1965> I am under the impression, that this is the windows port, dont know how opam on windows work without it

17:07 <discocaml> <otini_> neijul: add `-cc <compiler>` to the flags

17:10 <discocaml> <otini_> i.e., the `(flags ...)` stanza in your dune file

18:23 <discocaml> <._null._> Anarchos: Coq doesn't use Base, so maybe not the most appropriate book

18:24 <discocaml> <._null._> If you're already familiar with both Haskell and Coq, you may get away with simply reading the online manual

22:57 <discocaml> <barconstruction> Can we think of effects as introducing a degree dynamic scoping into the language (in a controlled way)

22:58 <discocaml> <barconstruction> Is your goal to

22:58 <discocaml> <barconstruction> - convince yourself that Coq is rigorous

22:58 <discocaml> <barconstruction> - make changes to Coq that will eventually get upstreamed

22:58 <discocaml> <barconstruction> - write plugins for Coq that others can use

23:02 <discocaml> <barconstruction> If your goal is (3) I would caution you that Coq developers have expressed on numerous occasions that the public OCaml API of Coq is not stable and changes significantly between minor versions, so OCaml plugins require a lot of long term maintenance. For serious Coq automation it is perhaps better to learn Ltac2 or Elpi, because the code you write is much more stable (and eliminates some tedious aspects of manually manipulating Coq ter

23:02 <discocaml> <barconstruction>

23:02 <discocaml> <barconstruction> Anecdotally, people I think of as Coq "power users" (Jason Gross comes to mind) do not write much OCaml automation (at least not that I have seen them discuss publicly)

23:04 <discocaml> <barconstruction> "HierarchyBuilder", a serious new piece of automation for the Mathematical Components Coq library (math-comp), was written in Elpi rather than in OCaml

23:35 <companion_cube> I'm worried Coq is going to lose to Lean because of that, tbh