companion_cube changed the topic of #ocaml to: Discussion about the OCaml programming language | http://www.ocaml.org | OCaml 4.12 released: https://ocaml.org/releases/4.12.0.html | Try OCaml in your browser: https://try.ocamlpro.com | Public channel logs at https://libera.irclog.whitequark.org/ocaml/
zebrag has quit [Quit: Konversation terminated!]
Skyfire has quit [Quit: WeeChat 3.2]
average_ has joined #ocaml
mosterdt_ has joined #ocaml
Absalom has quit [Quit: Ping timeout (120 seconds)]
dwt_ has quit [Remote host closed the connection]
average has quit [Ping timeout: 272 seconds]
favonia has quit [Ping timeout: 272 seconds]
mosterdt has quit [Ping timeout: 272 seconds]
infinity0 has quit [Ping timeout: 272 seconds]
average_ is now known as average
Absalom has joined #ocaml
infinity0 has joined #ocaml
favonia has joined #ocaml
dwt_ has joined #ocaml
Skyfire has joined #ocaml
mbuf has joined #ocaml
tizoc has quit [Quit: Coyote finally caught me]
tizoc has joined #ocaml
malc has joined #ocaml
gravicappa has joined #ocaml
mro has joined #ocaml
mro has quit [Remote host closed the connection]
mro has joined #ocaml
bartholin has joined #ocaml
chrisz has joined #ocaml
chrisz has quit [Client Quit]
nd__ has quit [Ping timeout: 272 seconds]
Haudegen has joined #ocaml
malc has quit [Remote host closed the connection]
neiluj has joined #ocaml
neiluj has quit [Remote host closed the connection]
neiluj has joined #ocaml
nd__ has joined #ocaml
neiluj has quit [Ping timeout: 248 seconds]
olle has joined #ocaml
eight has joined #ocaml
glassofethanol has joined #ocaml
mro_ has joined #ocaml
mro has quit [Ping timeout: 272 seconds]
yoctocell has joined #ocaml
kakadu has joined #ocaml
<hannes> I'm aware there are likely billions of HTTP clients in OCaml, but I developed a new one -- https://github.com/roburio/httpaf-lwt-client -- with the purpose of being lightweight, in the lwt monad, supporting HTTP + HTTPS (1.0/1.1), validating TLS certificates from the server, following redirects.
<hannes> feedback and suggestions is welcome -- at the moment the only exposed API is a single HTTP request :)
wingsorc__ has quit [Quit: Leaving]
<hannes> design goal is also unsurprising and minimalistic (i.e. no conduit/gluten/... in the dependency cone), no exceptions (instead proper errors with the result type)
nd__ has quit [Ping timeout: 248 seconds]
mro_ has quit [Ping timeout: 272 seconds]
mro has joined #ocaml
mro has quit [Ping timeout: 245 seconds]
<lobo> i like the name of the cli tool :-)
nd__ has joined #ocaml
<d_bot> <Kakadu> I few weeks ago I though about creating **minimal** http cilent and which Unix calls I need to implement it...
nd__ has quit [Ping timeout: 272 seconds]
<hannes> Kakadu: I guess https://github.com/cfcs/ofetch/ is more minimal tbh..
<d_bot> <Kakadu> Thanks!
chrisz has joined #ocaml
chrisz has quit [Client Quit]
terrorjack4 has joined #ocaml
johnel_ has joined #ocaml
PinealGl1ndOptic has joined #ocaml
gahr_ has joined #ocaml
micro has joined #ocaml
chrisz has joined #ocaml
hannes__ has joined #ocaml
daimrod1 has joined #ocaml
terrorjack4 has quit [Quit: The Lounge - https://thelounge.chat]
hannes has quit [Killed (NickServ (GHOST command used by hannes__))]
hannes__ is now known as hannes
nd__ has joined #ocaml
asm has quit [*.net *.split]
dinosaure has quit [*.net *.split]
nyuhu has quit [*.net *.split]
Nahra has quit [*.net *.split]
Serpent7776 has quit [*.net *.split]
kvik has quit [*.net *.split]
bartholin has quit [*.net *.split]
berberman_ has quit [*.net *.split]
leah2 has quit [*.net *.split]
krnkktz has quit [*.net *.split]
PinealGlandOptic has quit [*.net *.split]
johnel has quit [*.net *.split]
gahr has quit [*.net *.split]
daimrod has quit [*.net *.split]
Guest7430 has quit [*.net *.split]
kevinsjoberg has quit [*.net *.split]
Tardigreat[m] has quit [*.net *.split]
energizer has quit [*.net *.split]
engil1 has quit [*.net *.split]
mewfree[m] has quit [*.net *.split]
marinelli[m] has quit [*.net *.split]
Ekho has quit [*.net *.split]
micro_ has quit [*.net *.split]
Armael has quit [*.net *.split]
cbarrett has quit [*.net *.split]
ski has quit [*.net *.split]
brettgilio has quit [*.net *.split]
troydm has quit [*.net *.split]
andreypopp has quit [*.net *.split]
tomku has quit [*.net *.split]
terrorjack has joined #ocaml
dinosaure has joined #ocaml
asm has joined #ocaml
Nahra has joined #ocaml
nyuhu has joined #ocaml
kvik has joined #ocaml
Serpent7776 has joined #ocaml
chrisz has joined #ocaml
smondet[m] has quit [Ping timeout: 240 seconds]
schube[m] has quit [Ping timeout: 252 seconds]
labor[m] has quit [Ping timeout: 252 seconds]
nd__ has quit [Ping timeout: 272 seconds]
troydm has joined #ocaml
andreypopp has joined #ocaml
tomku has joined #ocaml
brettgilio has joined #ocaml
ks_ has joined #ocaml
Exa has joined #ocaml
remexre has joined #ocaml
kevinsjoberg has joined #ocaml
leah2 has joined #ocaml
Guest7430 has joined #ocaml
riverdc has joined #ocaml
bartholin has joined #ocaml
berberman_ has joined #ocaml
ccx_ has joined #ocaml
mewfree[m] has joined #ocaml
Ekho has joined #ocaml
marinelli[m] has joined #ocaml
Armael has joined #ocaml
bronsen has joined #ocaml
ski has joined #ocaml
Chouhartem has joined #ocaml
copy has joined #ocaml
cbarrett has joined #ocaml
waleee has quit [Ping timeout: 268 seconds]
engil1 has joined #ocaml
Tardigreat[m] has joined #ocaml
catern has joined #ocaml
drakonis has joined #ocaml
thvnx has joined #ocaml
arg_ has joined #ocaml
energizer has joined #ocaml
tristanC has joined #ocaml
octachron has joined #ocaml
notnotdan has joined #ocaml
greenbagels has joined #ocaml
mewfree[m] has quit [Ping timeout: 252 seconds]
marinelli[m] has quit [Ping timeout: 252 seconds]
Tardigreat[m] has quit [Ping timeout: 272 seconds]
fluxm has quit [Ping timeout: 276 seconds]
krnkktz has joined #ocaml
Haudegen has quit [Quit: Bin weg.]
labor[m] has joined #ocaml
schube[m] has joined #ocaml
smondet[m] has joined #ocaml
gahr_ is now known as gahr
mro has joined #ocaml
Tardigreat[m] has joined #ocaml
nd__ has joined #ocaml
mbuf has quit [Quit: Leaving]
fluxm has joined #ocaml
Haudegen has joined #ocaml
marinelli[m] has joined #ocaml
mewfree[m] has joined #ocaml
mro has quit [Remote host closed the connection]
mro has joined #ocaml
mro_ has joined #ocaml
mro has quit [Ping timeout: 256 seconds]
mro_ has quit [Ping timeout: 252 seconds]
zebrag has joined #ocaml
mattil has joined #ocaml
mattil has quit [Remote host closed the connection]
mattil has joined #ocaml
neiluj has joined #ocaml
glassofethanol has quit [Remote host closed the connection]
<neiluj> how would you describe the architecture of you library, beyond listing the modules themselves?
<neiluj> I tried to draw a graph of the dependencies between the modules but it gets messy and doesn't bring much
<companion_cube> with dune I tend to make a lot of small sub-libraries
<companion_cube> with `foo.bar` naming, all in package `foo`
<companion_cube> that gives more structure
nd___ has joined #ocaml
nd__ has quit [Ping timeout: 272 seconds]
<neiluj> good idea, thanks!
<neiluj> in my case, it might be too extreme, so I'll explain with a few words how modules are put together
nd___ has quit [Ping timeout: 248 seconds]
<companion_cube> another way is, if you use dune with wrapped modules, to have the main module be the entry point where you can write a lot of stuff
<companion_cube> you can expose the actual sub-modules in any order, with doc in the middle…
yoctocell has quit [Read error: Connection reset by peer]
<neiluj> by reexporting modules in the main module?
zebrag has quit [Quit: Konversation terminated!]
favonia has quit [Ping timeout: 272 seconds]
favonia has joined #ocaml
<companion_cube> yes
<companion_cube> if you write a main module explicitly, then you need to reexport
<companion_cube> (otherwise dune makes a main module for you)
<neiluj> perfect!
berberman has joined #ocaml
berberman_ has quit [Ping timeout: 256 seconds]
mro has joined #ocaml
Haudegen has quit [Quit: Bin weg.]
mro has quit [Quit: Leaving...]
zebrag has joined #ocaml
<d_bot> <carmysilna> I'm having a little trouble knowing how to create a Map. I have a module `Word`, a type `Word.t`, and a `Word.Comparator : Base.Comparator.S_fc with comparable_t = t`, but I can't figure out how to define a `type env = (Word.t, Ast.term list, ???) Map.t`. It needs a module but when I try to put `Word.Comparator` there, the compiler complains that its not a type constructor.
waleee has joined #ocaml
<Corbin> `module Env = Map.Make (Word)` will create the module you want, I think. There's a lot to say about functors but I'm not sure where to start.
<d_bot> <octachron> The `Base` library has a completely different implementations of `Map` based on first class modules.
<d_bot> <carmysilna> yeah, I'm using `Base.Map`, should have specified
<d_bot> <octachron> Once you have a comparator function and type, it should be something akin to `Map.empty (module Word)`
<d_bot> <monk> not like i would ever find the time or mental fortitude for getting around to this, but where would one look for learning how to make a basic formal verification of a modest protocol written in ocaml
<d_bot> <monk> i would assume coq is the tool to use here in some way or form
<d_bot> <carmysilna> I think I get this, I'm wondering how to define a type alias for the type of `Map.empty (module Word)`
<d_bot> <octachron> Coq is generally more used to write the specification and protocol in Coq and then extract it in OCaml. If you want to verify OCaml code I think that CFML or Gospel might be the simpler path. See https://github.com/ocaml-gospel/vocal for a verified ocaml library.
<d_bot> <monk> thank you for the discernment between the two for me
<d_bot> <octachron> @carmysilna : `type 'data map = (t, 'data, Word.comparator_witness) Map.t` ?
<d_bot> <monk> so is the former more akin to "describing" the protocol in coq or do you actually implement it before it gets extracted to the ocaml equivalent
<d_bot> <monk> context here is that i am completely ignorant of coq, so i don't know the semantics of a coq specification relative to a proven program
<neiluj> monk: note that you can import ocaml code to coq https://github.com/clarus/coq-of-ocaml, with some caveats tho
<d_bot> <carmysilna> thanks
kakadu has quit [Quit: Konversation terminated!]
<d_bot> <octachron> @monk :If I am not mistaken, you also implement the protocol (or parts of it), which is useful to proving some of its properties (beware that I am not really familiar with Coq).
<d_bot> <monk> i greatly appreciate the info all the same 🙏
Haudegen has joined #ocaml
<companion_cube> I hope gospel will get to a robust usable state :3
<neiluj> If you don't want to prove the properties manually in Coq, have a look at FStar
<companion_cube> I'd love to use it
<neiluj> ah you've already written the protocol in ocaml
average has quit [Ping timeout: 268 seconds]
Tuplanolla has joined #ocaml
average has joined #ocaml
<d_bot> <monk> neiluj: well, the idea was i would write the protocol in ocaml and then verify it.
<d_bot> <monk> which i already assumed would involve some code contortion as i learned what program constructs don't play nicely (read: easily submit to) with formal methods via coq
<d_bot> <monk> so it is interesting that coq-of-ocaml has the entire alpha tezos protocol extracted, but doesn't look like they have any proofs written out from the extracted coq code
<neiluj> yeah it's still a work in progress
<d_bot> <monk> companion_cube: yeah gospel is super interesting since, from what i understand, do the coq legwork in the documentation of your already-written-and-actively used ocaml code
<d_bot> <monk> i really like the idea
<d_bot> <monk> yeah the more i look at gospel, the more i like it
<d_bot> <carmysilna> How can I stop Menhir from depending on my toplevel library module? I'm getting an error that it depends on `Mlatu.ml` which isn't allowed, but I'm not referencing `Mlatu.*` at all in `Mlatu__Parser.mly`
<d_bot> <carmysilna> Hm. `dune clean` fixed it. weird
mattil has quit [Quit: Leaving]
gravicappa has quit [Ping timeout: 272 seconds]
average has quit [Quit: Connection closed for inactivity]
chrisz has quit [Quit: Changing server]
chrisz has joined #ocaml
neiluj has quit [Quit: Leaving]
arbipher has quit [Quit: Konversation terminated!]
<d_bot> <leviroth> You probably want `type env = Ast.term list Map.M(Word).t`.
<d_bot> <carmysilna> thanks for the answer, I got it though with `type env = (Word.t, Term.t list, Word.comparator_witness) Map.t`
<d_bot> <carmysilna> I think your answer is using the stdlib Map? I'm using Base.Map, I should have specified
<d_bot> <leviroth> For sure. `Map.M` is supposed to be a more ergonomic version of the same, though its poor discoverability makes the ergonomics a bit moot.
<d_bot> <leviroth> No, I'm talking about Base.
<d_bot> <carmysilna> oh, that is a lot easier. thanks
<d_bot> <carmysilna> I think the whole module could be a lot better documented though
bartholin has quit [Quit: Leaving]
<d_bot> <carmysilna> So `dune install` installs in `~/.opam/default/` at least for me. Is there a function in `Core` or `Caml` that will return this path, so I can access the path of data files that are also installed there?
olle has quit [Ping timeout: 268 seconds]
Tuplanolla has quit [Quit: Leaving.]
sleepydog has joined #ocaml
PinealGl1ndOptic has quit [Quit: leaving]
Haudegen has quit [Ping timeout: 268 seconds]