00:12 <d_bot> <stab> Anyone know of a good library for manipulating and interacting with smt that can be parameterized by the backend solver? Looks like alt-ergo may be my best bet without knowing anything about the space. Just want to implement some generic algorithms over the SAT portions of SMT formula without binding the user to a specific theory or solver

00:18 <companion_cube> if you want only SAT, there's more choice

00:18 <companion_cube> and the API is much smaller

00:18 <companion_cube> idk of anything generic though

00:18 <companion_cube> (maybe sattools?_

00:20 <d_bot> <stab> Well so what I want is to only interact with the SAT portions of the formula regardless of the theories my clients are using. Ie. treat (a < b /\ c > d) as (u1 /\ u2) Perform some reorganizing of the SAT formula then pass the new SMT to a solver get some results and do it all over again

00:21 <d_bot> <stab> Basically want to implement an algorithm that is useful regardless of the underlying theories and dont want to lock my clients of the lib into a theory or solver

00:21 <d_bot> <stab> i guess really i could implement this binding between u1 and a<b myself potentially

00:21 <companion_cube> you could functorize I guess

00:22 <companion_cube> SMT solvers already do that kind of stuff internally, the SAT solver doesn't know about theories

01:07 <d_bot> <stab> yeah it's more like i need to make a series of smt queries that are modifiable by only transforming the SAT which i guess is how SAT+SMT solving works anyways

01:07 <d_bot> <stab> lol

01:53 <companion_cube> hmmm

01:53 <companion_cube> typically you can't modify a formula once the SMT solver knows about it

01:53 <companion_cube> (not if it's incremental; otherwise if you just do n independent queries it's of course fine)

01:53 <companion_cube> you can use assumptions though

04:53 <d_bot> <gabenpls> i'm trying to run before i can walk, so i'm learning ocaml first before trying to create a compiler

04:53 <d_bot> <gabenpls> and i've got to say, i'm loving ocaml

04:53 <d_bot> <gabenpls> what a cool lang, sad i didn't discover it sooner

04:54 <d_bot> <gabenpls> can't wait to do rescript

05:05 <dmbaturin> Note that with reScript you will get stuck with an outdated OCaml backend.

05:07 <dmbaturin> If you want to target JS with actual, up-to-date OCaml, you can try js_of_ocaml. It's a trans-compiler from OCaml bytecode to JS.

05:12 <d_bot> <gabenpls> hmm i didn't plan on using rescript's ocaml backend, just rescript directly. do i have that right?

05:16 <dmbaturin> I mean, reScript is a fork of OCaml 4.06 (last I checked). It's effectively a hard fork, a different language by now, and it locks you out of all new OCaml features added since 4.06.

05:19 <d_bot> <gabenpls> got it

05:21 <d_bot> <gabenpls> so what's the purpose of reasonml? just to make the syntax more easy for people with js background?

05:21 <dmbaturin> ReasonML (now reScript) started as an alternative concrete syntax for OCaml, which created quite a bit of confusion among newcomers as to what it is and isn't. At some point its maintainers decided to position it as a standalone language, which I think is a right decision because it was never kept in sync with the OCaml compiler backend.

05:23 <dmbaturin> Well, the BuckleScript (JS backend) part wasn't kept in sync. ReasonML the concrete syntax itself does work with recent OCaml versions I believe, but almost no one ever used it outside of the BuckleScript/JS stack.

05:24 <dmbaturin> https://baturin.org/blog/if-you-think-reasonml-compiles-to-js-you-are-wrong/ This is a longer explanation, though I need to update it for the reScript situation.

05:33 <d_bot> <gabenpls> ok that makes more sense

05:34 <d_bot> <gabenpls> so what it comes down to is rescript vs js_of_ocaml, trying to figure out what's better. since i'm coming from a js/react background i'm guessing rescript

05:36 <dmbaturin> For me, js_of_ocaml is a great way to opt out of the NPM nightmare^W ecosystem and produce effectively eternal JS blobs.

05:39 <dmbaturin> If you want to use libraries from NPM a lot, you may want to use a tool that intentionally integrates with that ecosystem, like reScript. Or you may want to try js_of_ocaml as an alternative to that ecosystem.

05:40 <d_bot> <gabenpls> i see. thanks.

07:50 <d_bot> <zakkor> @gabenpls, dmbaturin: there is also the Melange project, which AFAIK tries to move away from rescript and wants to just make ReasonML an alternative syntax for OCaml, while leveraging the OCaml ecosystem going forward, instead of moving away from it

07:50 <d_bot> <zakkor> <https://anmonteiro.com/2021/03/on-ocaml-and-the-js-platform/>

09:39 <d_bot> <Et7f3> And someone forked the fork to bump to latest ocaml https://github.com/melange-re/melange @gabenpls

09:41 <d_bot> <Et7f3> Esy reason codebase use recent feature. Esy is a real binary so it is native reason

09:43 <d_bot> <Et7f3> (Oh Sorry for repost just so a different link but didn't opened it 🤦🏻)

09:44 <d_bot> <Et7f3> Why on IRC you have nickname: message does it kind of ping on discord or just conventions to know destination

12:58 <d_bot> <VPhantom> Melange isn't specific to ReasonML: it still supports the ReScript syntax (until ReScript moves too far away from OCaml in the future) and most importantly: up-to-date OCaml syntax which ReScript dropped support for. Melange is specifically for compiling any of the syntaxes into clean and light JS, without sacrificing the ability to keep up with the latest OCaml version. That means let bindings and all the modern OCaml goodness.

12:58 <d_bot> <VPhantom> Unlike ReScript however, Melange isn't sponsored at the moment, so progress is slow at best. Something I hope to help the author improve in the coming year.

14:46 <d_bot> <stab> yeah it's pretty annoying to get incremental solving to work with this since then I need to make some assumptions about how the client is representing formula. Right now im just assuming independent queries but obviously that's bad

14:46 <d_bot> <stab> Implementing a paper so im not completely off the reservation lol

16:26 <d_bot> <Kakadu> Do you know, was OCaml syntax has ever been patched to support JSX? AFAIK ReasonML one was patched. Wondering, which issues patching OCaml syntax could discover: tooo many conflicts or something else?...

16:39 <d_bot> <VPhantom> ReasonML has JSX, and I bet ReScript probably does as well. In OCaml there isn't a direct equivalent. There's some PPX floating around but they're for specific APIs.

16:48 <companion_cube> I don't think Xavier cares about JSX

16:49 <companion_cube> The syntax has not changed

17:18 <d_bot> <octachron> The ppx syntax has been amended to allow `{%jsx|...|}` as a shortcut for `[%jsx{|...|}]`.

17:27 <d_bot> <EduardoRFS> problem with ppx with string is that ocamlformat just doesn't care about them

17:29 <d_bot> <Kakadu> It would be great to have configurable parser where we can enable/disable JSX/metaOCaml/Reason syntaxes and metaOCaml would generate for us efficient recursive descent with error recovery

17:43 <d_bot> <VPhantom> I'll admit, if inline HTML could simply resolve to hyperscript type function calls I'd happily use it for templating. (As it is, I use said hyperscript technique with a base `h` function and derived curried `h tagname` functions.)

17:56 <d_bot> <VPhantom> Back in my JS days I created a compile-time templating scheme (<https://github.com/vphantom/node-jstc>) and I might be tempted to experiment with the concept with OCaml. In this old module each template file became a function which takes an environment object as its argument and returns a string of output. The basic idea of "string first, with OCaml interspersed" could be interesting, like PHP, ASP, JSP, etc. Of course I'd appen

17:58 <d_bot> <VPhantom> Hyperscript, on the other hand, has the advantage of being OCaml directly and of providing more guarantees about the quality of the output (tags get closed automatically, for one thing).

18:03 <d_bot> <VPhantom> (Huh, there was an Apache `mod_caml` around 2004. Loaded bytecode dynamically.)

18:12 <dmbaturin> VPhantom: I was much more intrigued by a browser that could run OCaml applets: https://caml.inria.fr/pub/old_caml_site/~rouaix/mmm/

18:14 <d_bot> <VPhantom> Nice! Though my heart still belongs to Oberon's "Juice" a.k.a. SLIM binaries (even though Java applets and now WASM won that race…)