companion_cube changed the topic of #ocaml to: Discussion about the OCaml programming language | http://www.ocaml.org | OCaml 4.14.0 released: https://ocaml.org/releases/4.14.0.html | Try OCaml in your browser: https://try.ocamlpro.com | Public channel logs at https://libera.irclog.whitequark.org/ocaml/
<pgiarrusso> anmonteiro: do you know if F* proofs cover these problems? Many proof techniques wouldn't, since it isn't an implementation error
xgqt has quit [Ping timeout: 268 seconds]
Tuplanolla has quit [Quit: Leaving.]
xgqt has joined #ocaml
kurfen has quit [Ping timeout: 268 seconds]
kurfen has joined #ocaml
sagax has quit [Excess Flood]
sagax has joined #ocaml
<d_bot> <darrenldl> mirage is using fiat crypto (coq) code rather than hacl star (F*) though?
<d_bot> <darrenldl> (or am i being very silly again
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
raskol has joined #ocaml
terrorjack has quit [Quit: The Lounge - https://thelounge.chat]
waleee has quit [Ping timeout: 272 seconds]
terrorjack has joined #ocaml
gopiandcode has quit [Read error: Connection reset by peer]
Haudegen has joined #ocaml
gopiandcode has joined #ocaml
wingsorc has quit [Ping timeout: 255 seconds]
spip has quit [Ping timeout: 240 seconds]
spip has joined #ocaml
hsw_ has joined #ocaml
hsw has quit [Remote host closed the connection]
hsw_ is now known as hsw
raskol has quit [Ping timeout: 268 seconds]
gopiandcode has quit [Ping timeout: 264 seconds]
gopiandcode has joined #ocaml
sagax has quit [Excess Flood]
mbuf has joined #ocaml
andrzejku has joined #ocaml
andrzejku2 has joined #ocaml
andrzejku has quit [Ping timeout: 268 seconds]
<d_bot> <dinosaure> I can confirm that mirage-crypto uses fiat indeed
<d_bot> <dinosaure> We gave a try to f* and hacl but we got several issue mainly from the OCaml ecosystem and Hannes decided to use only fiat then
<d_bot> <dinosaure> (And we definitely decided to archived what we did about hacl)
<d_bot> <darrenldl> i just realised i misread what pgiarusso was asking
azimut has joined #ocaml
Tuplanolla has joined #ocaml
neiluj has joined #ocaml
bartholin has joined #ocaml
<neiluj> Hi! Wanted to know if it is possible to have one module with a generic type 'a t as a GADT to restrict 'a to two types and then have functions doing different things depending on the type of 'a. It is not possible since OCaml doesn't support ad hoc polymorphism.
<neiluj> Is there a way to do something like it: one module that can be instantiated with only two modules (instead of two types) and have the functions of the module behave differently depending on the input module?
<neiluj> or maybe the solution is to have simply two modules...
mro has joined #ocaml
mro has quit [Remote host closed the connection]
neiluj has quit [Remote host closed the connection]
neiluj has joined #ocaml
mro has joined #ocaml
mro has quit [Quit: Leaving...]
jpds has quit [Ping timeout: 268 seconds]
jpds has joined #ocaml
azimut has quit [Remote host closed the connection]
azimut has joined #ocaml
dextaa has quit [Read error: Connection reset by peer]
dextaa has joined #ocaml
Haudegen has quit [Quit: Bin weg.]
andrzejku2 has quit [Quit: Leaving]
motherfsck has quit [Ping timeout: 246 seconds]
motherfsck has joined #ocaml
neiluj has quit [Quit: Leaving]
waleee has joined #ocaml
Haudegen has joined #ocaml
motherfsck has quit [Ping timeout: 240 seconds]
motherfsck has joined #ocaml
waleee has quit [Ping timeout: 260 seconds]
rgrinberg has joined #ocaml
eax_ has joined #ocaml
dextaa has quit [Read error: Connection reset by peer]
dextaa has joined #ocaml
szkl has joined #ocaml
gopiandcode has quit [Ping timeout: 248 seconds]
gopiandcode has joined #ocaml
perrierjouet has quit [Quit: WeeChat 3.5]
perrierjouet has joined #ocaml
dstein64- has joined #ocaml
Haudegen has quit [Quit: Bin weg.]
dstein64 has quit [Ping timeout: 256 seconds]
dstein64- is now known as dstein64
perrierjouet has quit [Quit: WeeChat 3.5]
perrierjouet has joined #ocaml
rgrinberg has quit [Ping timeout: 268 seconds]
rgrinberg has joined #ocaml
mbuf has quit [Quit: Leaving]
spip has quit [Ping timeout: 255 seconds]
bobo_ has joined #ocaml
bartholin has quit [Quit: Leaving]
littlemike has joined #ocaml
<littlemike> how's it going ocaml folks
<littlemike> just stopping by
littlemike has quit [Quit: WeeChat 3.2.1]
Haudegen has joined #ocaml
raskol has joined #ocaml
gareppa has joined #ocaml
bgs has quit [Ping timeout: 248 seconds]
bgs has joined #ocaml
raskol has quit [Ping timeout: 272 seconds]
szkl has quit [Quit: Connection closed for inactivity]
spip has joined #ocaml
bobo_ has quit [Ping timeout: 255 seconds]
<d_bot> <Le condor du plateau> which is more idiomatic between `|>` and `@@`?
<d_bot> <Le condor du plateau> I rarely see `@@`
<d_bot> <geoff> I'm not sure about idiomatic, but I tend to use `@@` in non "pipeline" contexts, and `|>` if there are enough steps that it seems justified.
<d_bot> <geoff> usually wouldn't use `|>` if it is going to fit on one line
<d_bot> <Bluddy> People like `@@` less because it's a little less aesthetically pleasing. Both are fine though.
<companion_cube> depends on what you want to see first
<companion_cube> I use both
<rgrinberg> I use |> to get rid of useless bindings and @@ to get rid of useless parens
<rgrinberg> so they have different uses really
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
gareppa has quit [Quit: Leaving]
<d_bot> <Le condor du plateau> ok I see
<d_bot> <Le condor du plateau> I use personally `@@` to avoid parentheses and `|>` to chain operations which is consistent with your answers
<d_bot> <pseud> When writing filthy stateful code, do I have alternatives to `let _ = <side-effectful expr> in let _ = <side-effectful expr> in <expr>` ?
<sim642> If the side-effectful expr has type unit, then you can just use semicolons
<sim642> Or the standard ignore function to ignore any returned value from impure functions to still use semicolons
<companion_cube> `e1; e2; e3`
<companion_cube> but careful with ignore
<d_bot> <pseud> Ok, so I could do `<expr> |> ignore;` ?
<companion_cube> I always do: `ignore (<expr> : <ty>); …`
<companion_cube> because it's too easy to ignore a partial application without realizing it
<d_bot> <geoff> ahh that makes a lot of sense
<companion_cube> <ty> doesn't have to be fully detailed, but like `ignore (foo : _ list); …` or `ignore (foo : _ * _); …` to make sure it's not a function type
<sim642> Isn't there some kind of warning about partially applied functions being ignored?
<sim642> I guess it might be for let _, but not calls of ignore?
<sim642> Although ignore is an external, so maybe a bit of compiler special case magic could extend to it, if it doesn't already
<sim642> According to https://github.com/ocaml/ocaml/issues/10604 there is something for it
<d_bot> <Terence> hello, I'm using menhir and I saw in the examples it was using 2 parsers : one for fast parsing (code-backend) and then another slower one when the first one detects an error (table backend + incremental api).
<d_bot> <Terence> However, in the manual there is the following :
<d_bot> <Terence>
<d_bot> <Terence> > this approach to producing syntax error messages does not
<d_bot> <Terence> require using Menhir’s incremental API and table back-end. One can instead use Menhir’s code back-end with
<d_bot> <Terence> --exn-carries-state
<d_bot> <Terence>
<d_bot> <Terence>
<d_bot> <Terence> So I was wondering how this compares to the other approach
rgrinberg has joined #ocaml
Serpent7776 has quit [Quit: leaving]
waleee has joined #ocaml
bastienleonard has joined #ocaml
bastienleonard has quit [Client Quit]
bastienleonard has joined #ocaml
<d_bot> <deepspacejohn> I also have a Menhir question. It seems like it's not possible to add documentation comments that appear in the generated `.mli`, is that correct?
bastienleonard has quit [Client Quit]
bastienleonard has joined #ocaml
Haudegen has quit [Ping timeout: 268 seconds]
azimut has quit [Ping timeout: 268 seconds]
Tuplanolla has quit [Quit: Leaving.]