00:16 <discocaml> <contextfreebeer> companion_cube: nope, nothing like that. I am pretty sure sorted vs unsorted just has a massive effect on the algorithmic behavior in some cases which is why I noticed a discrepancy between the two versions. It's a SAT solver so sorting the clauses vs not sorting them changes which literals are chosen to be watched (I just choose the first nonfalse ones I find) and it might also change how long it takes to find new watched literals etc

00:17 <companion_cube> Oh I see

00:17 <discocaml> <contextfreebeer> The performance seems completely identical between sorted array and set

00:17 <companion_cube> Yeah but arrays ought to be way faster in that context

00:17 <companion_cube> Cache effects and all that

00:18 <discocaml> <contextfreebeer> For sure, that's why I want to switch. I'm not sure if sorting the clauses even makes sense, there's no reason why that should be better

00:19 <discocaml> <contextfreebeer> Using sets made sense at the start because I implemented assignments in the worst possible way by removing literals from the clause, which completely tanks the performance, the clauses have been static for a long time now but I haven't gotten around to changing the representation

00:23 <companion_cube> You can sort clauses, I do it

00:23 <companion_cube> It's also part or simplifying

00:23 <discocaml> <contextfreebeer> by "the performance is identical" I meant the performance is on the same level, not wildly different, the performance is of course strictly better

00:24 <discocaml> <contextfreebeer> companion_cube: oh, really? I see

00:30 <discocaml> <contextfreebeer> Guess I can just sort them then. Just out of curiosity I'm running the solver on all the formulas that I have locally with both versions. probably it will just end up evening out.

00:36 <discocaml> <contextfreebeer> not going to dwell on that too much since I have yet to implement garbage collection of learned clauses, I think I will get more mileage out of that, hope so anyway

00:50 <companion_cube> Is it for learning? Are you following a paper?

01:07 <discocaml> <contextfreebeer> companion_cube: yeah, for learning, I find SAT solvers absolutely fascinating. I'm not exactly following a paper per se but I have probably read most of the classic papers by now during the course of implementing this solver

01:08 <companion_cube> I guess you read the minisat paper? :)

01:09 <discocaml> <contextfreebeer> Ofc

01:31 <companion_cube> very cool

01:32 <companion_cube> btw implementing proof production can be a useful tool when debugging

04:58 <discocaml> <darrenldl> is there a file globbing library around that does the traversal smartly for me instead of just providing a test predicate?

06:00 <discocaml> <darrenldl> can't seem to spot any, will just have to write one myself ig

06:28 <discocaml> <barconstruction> Has OCaml ever been spelled O'Caml in any official OCaml documentation, ever?

06:28 <discocaml> <barconstruction> Even like 20 years ago

07:49 <adrien> I think so

07:49 <adrien> 20+ years ago it was a mess

07:49 <adrien> ocaml, O'Caml, OCAML, and probably every other formatting you can come up with

07:57 <discocaml> <peuk> Occam's Hell

08:58 <masterbuilder> companion_cube: Yeah, already doing that, you mean emitting the satisfying assignment or an UNSAT proof, right? I have my test suite hooked up to GRAT for verification. my test suite has 50 thousand formulas and only 3000 of those time out after 10 seconds, so that makes me fairly confident the solver is correct by now :) integrating an external verifier into the project did indeed really help with debugging the watched literals implementation

08:58 <masterbuilder> which had a subtle bug in the first attempt

09:04 <masterbuilder> only 100 time outs after switching to an array representation for the clauses

11:30 <companion_cube> Very cool

19:56 <discocaml> <saiiiniii> Is there a native windows installer for OCaml yet?

19:57 <discocaml> <saiiiniii> Ocamls website doesn’t point me in any direction really

19:57 <discocaml> <saiiiniii> Ocamls website doesn’t point me in any direction really so I was wondering if anyone is aware of any third parties

20:04 <discocaml> <Kali> "native" no, "windows" yes

20:07 <dh`> uninstall windows, you'll thank yourself laer

20:07 <dh`> er later

20:44 <Anarchos> Is there an easy way to debug the runtime when doing 'dune runtest' ?I need to inspect what happens inside unix_kill()

22:57 <Anarchos> Are there janestreet people here ?

22:57 <Anarchos> I need advice on a unit test in spawn