04:39 <discocaml> <functionalprogramming> is it recommended to use local switches or global ones

04:40 <discocaml> <.korven.> local ones per project are usually the way to go

06:54 <reynir> local switches has the benefit that dependency constraints in different projects don't interfere. The downside is that each opam switch can be gigabytes in size.

06:55 <discocaml> <.korven.> and it takes time to build the dependencies over and over for new switches. I think there's opam-bin to alleviate that problem? not sure. But something like `pnpm` global cache would be neat

09:00 <discocaml> <._null._> I wouldn't consider local switches as the universal solution, you can often do just fine with a global switch

09:06 <reynir> you can also link switches (opam switch link) so you can reuse local switches between projects for example

10:55 <Leonidas> korven: you can have sth a bit like this by enabling the dune cache

21:46 <Anarchos> weird test in the ocaml/testsuite/tests/lib-format/mx_pr586_par2 : it fails randomly

21:47 <Anarchos> 99.39% ot ifs output is 42.0f and others are 42.f+01

23:30 <discocaml> <contextfreebeer> I only use local switch for Coq and fstar that rely heavily on a specific version of the compiler, otherwise I just use the global switch and there are pretty much no issues

23:31 <discocaml> <contextfreebeer> well they don't require a specific version per se but only support a fairly narrow spectrum AFAIK, and don't support 5 yet

23:49 <discocaml> <tornato> Unrelated, but have you ever used idris, it looks pretty neat and has dependent types

23:50 <discocaml> <tornato> Trying to figure out which dependently typed language is worth learning

23:52 <discocaml> <Kali> learn both or all three honestly

23:58 <discocaml> <Kali> - the documentation for F\* is pretty sparse and just straight-up broken in some places, but it's got an smt solver so it makes some programs far easier to prove, and also uses *very* ocaml-like syntax

23:58 <discocaml> <Kali> - idris has the nicest documentation but does not use an smt solver and has a haskell-style syntax

23:58 <discocaml> <Kali> - coq is typically much more proof-oriented than programming-oriented, so you'll get more exposure to actual proofs rather than programming with a side of proofs; its documentation is fairly good but too technical sometimes (use the Software Foundations book instead) and its syntax is vaguely like ocaml's—for expressions anyway

23:59 <discocaml> <tornato> Interesting, I'm dumb and don't know what an SMT solver is, time to Google that😆