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/
rgrinberg has joined #ocaml
waleee has quit [Ping timeout: 252 seconds]
rwmjones has quit [Ping timeout: 252 seconds]
rwmjones has joined #ocaml
vicfred has quit [Quit: Leaving]
favonia has joined #ocaml
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
rgrinberg has joined #ocaml
mbuf has joined #ocaml
zebrag has quit [Quit: Konversation terminated!]
gravicappa has joined #ocaml
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
rgrinberg has joined #ocaml
daachi has quit [Ping timeout: 252 seconds]
Johann has quit [*.net *.split]
tomku has quit [*.net *.split]
terrorjack has quit [*.net *.split]
daimrod1 has quit [*.net *.split]
tomku has joined #ocaml
daimrod1 has joined #ocaml
Johann has joined #ocaml
terrorjack has joined #ocaml
wagle has quit [*.net *.split]
reynir has quit [*.net *.split]
lobo has quit [*.net *.split]
octachron has quit [*.net *.split]
oisota has quit [*.net *.split]
johnel_ has quit [*.net *.split]
bacam has quit [*.net *.split]
theglass has quit [*.net *.split]
johnel has joined #ocaml
theglass has joined #ocaml
octachron has joined #ocaml
wagle has joined #ocaml
oisota has joined #ocaml
theglass has quit [Changing host]
theglass has joined #ocaml
lobo has joined #ocaml
lobo has joined #ocaml
lobo has quit [Changing host]
bacam has joined #ocaml
shawn has quit [Ping timeout: 250 seconds]
olle has joined #ocaml
<d_bot> <darrenldl> is proof general still the goto frontend for coq?
<vsiles> I'm using CoqTail+vim
<vsiles> that's nice if you are allergic to emacs
Haudegen has joined #ocaml
<Armael> i've heard that the vscode support is quite good as well
<Armael> (i'm using proof general myself, as i'm used to emacs)
wonko has joined #ocaml
xd1le has joined #ocaml
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
rgrinberg has joined #ocaml
hendursa1 has joined #ocaml
hendursaga has quit [Ping timeout: 276 seconds]
adanwan has joined #ocaml
<d_bot> <darrenldl> CoqTail looks neat, i'll give that a shot
<d_bot> <darrenldl> cheers
<d_bot> <darrenldl> Armael: thats curious, didnt realise vscode has support for coq, will have to try it out
bartholin has joined #ocaml
<Armael> https://github.com/coq-community/vscoq this is the relevant vscode extension
<vsiles> is it still maintained ? last I checked it was a bit of chaotic
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
<d_bot> <darrenldl> is the software foundations series by Pierce et al. the go to in terms of materials?
<d_bot> <darrenldl> still the go to*
<d_bot> <darrenldl> (for purpose of formalising systems)
<Armael> yes, probably
<Armael> it's somewhat biaised towards formalizing PL stuff, but it's a good introduction to coq in any case
<vsiles> +1
<Armael> my (biaised!) opinion is that Iris is what's hot right now, but that can come after learning SF ;-)
<vsiles> I'm reading about iris right now :p
<Armael> good.
<Armael> (:p)
<d_bot> <darrenldl> cheers : D
<d_bot> <darrenldl> hope this research direction works out for me (fingers crossed)
<d_bot> <Alistair> I’m a fairly big fan of Agda, also used for formalising PL stuff
<xd1le> yeah iris is great work
<Drup> Iris should definitely come after SF :p
<d_bot> <darrenldl> @TheBloodlessMan : ah, would you advise agda over coq?
lobo has quit [Quit: WeeChat 3.0]
lobo has joined #ocaml
<Drup> remind me the kind of things you want to formalize ?
<d_bot> <Alistair> I mean it depends what you’re looking for, as with anything there are trade offs between each language
<d_bot> <Alistair> But for PL stuff, both are pretty good, but I prefer Agda since tactics often decrease readability of proofs
<d_bot> <Alistair> Although for libraries Coq definitely wins
adanwan has quit [Ping timeout: 276 seconds]
<d_bot> <darrenldl> security protocols, so coq is probably safer bet cause crypto now that i think about it
<d_bot> <Alistair> e.g just set out on a new Agda project recently and ended up writing 2 libraries to do it 😂
<d_bot> <darrenldl> Drup: security protocols, so coq is probably safer bet cause crypto now that i think about it (forgot to tag name : D)
<d_bot> <darrenldl> @TheBloodlessMan i see, cheers!
<Drup> yeah, for that, definitely Coq over Agda. As cool as Agda is, you need tactics for this.
<Drup> (unless you want to get into very complex type systems to make your protocoles safe by construction, but that's a different domain :p)
<d_bot> <dinosaure> note that `mirage-crypto` already includes some cryptography primitives which comes from `coq` via the `fiat` project
<d_bot> <darrenldl> thanks for the reminder! will probably reference it when/if i get to the extraction part
<d_bot> <darrenldl> refer to it*
<d_bot> <Alistair> we'll get there one day, Agda's reflection library is starting to show promise for tactics
reynir has joined #ocaml
reynir has quit [Changing host]
reynir has joined #ocaml
adanwan has joined #ocaml
Haudegen has quit [Quit: Bin weg.]
reynir has quit [Quit: WeeChat 2.3]
reynir has joined #ocaml
<companion_cube> Drup: you mean TLA and no types, right?
<companion_cube> :p
adanwan has quit [Ping timeout: 276 seconds]
Haudegen has joined #ocaml
mro has joined #ocaml
daachi has joined #ocaml
hendursa1 has quit [Quit: hendursa1]
hendursaga has joined #ocaml
favonia has quit [Ping timeout: 256 seconds]
mro has quit [Remote host closed the connection]
mro has joined #ocaml
zebrag has joined #ocaml
mro has quit [Remote host closed the connection]
adanwan has joined #ocaml
waleee has joined #ocaml
mro has joined #ocaml
favonia has joined #ocaml
mro has quit [Ping timeout: 252 seconds]
vicfred has joined #ocaml
vicfred has quit [Client Quit]
favonia has quit [Ping timeout: 265 seconds]
adanwan has quit [Ping timeout: 276 seconds]
bartholin has quit [Quit: Leaving]
mro has joined #ocaml
mro has quit [Remote host closed the connection]
mro has joined #ocaml
mbuf has quit [Quit: Leaving]
xd1le has quit [Quit: xd1le]
landonf has quit [Ping timeout: 240 seconds]
favonia has joined #ocaml
favonia has quit [Ping timeout: 265 seconds]
Haudegen has quit [Quit: Bin weg.]
favonia has joined #ocaml
Geekingfrog is now known as the_blockchain
the_blockchain is now known as Geekingfrog
mro has quit [Remote host closed the connection]
Haudegen has joined #ocaml
rgrinberg has joined #ocaml
mro has joined #ocaml
mro has quit [Ping timeout: 252 seconds]
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
favonia has quit [Ping timeout: 265 seconds]
mro has joined #ocaml
favonia has joined #ocaml
rgrinberg has joined #ocaml
jcob has joined #ocaml
<jcob> Hello again everyone! I have a question on the following snippet of code:
<jcob> how come this is allowed when r is not let rec?
<jcob> and how come it terminates? That's what I'm confused by the most... x does not seem to decrease before r is called again, so how come r will eventually terminate rather than infinitely recursing?
<d_bot> <rgrinberg> you need let rec whenever you write `let rec foo = (* term with [foo] *) in ...`
<d_bot> <rgrinberg> In your example, you have `let r () = (* term without foo *)` in `(* term with [r] *)`. this doesn't require `rec`
<octachron> You might be misreading your code: the definition of `r` ends at line 2.
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
<jcob> octachron i see now. Thanks :D
<jcob> so r does not call itself
<jcob> i appreciate the help
zebrag has quit [Remote host closed the connection]
<olle> Indentation matter...
jess has joined #ocaml
mro has quit [Remote host closed the connection]
mro has joined #ocaml
jcob has quit [Quit: Client closed]
daachi has quit [Ping timeout: 252 seconds]
mro has quit [Remote host closed the connection]
<cemerick> so I just blew most of the afternoon because I didn't have an env var set, so Unix.get_env was raising a highly-uninformative Not_found ("Fatal error: exception Not_found; Raised by primitive operation at unknown location")
mro has joined #ocaml
<cemerick> I have -g on, I exported OCAMLRUNPARAM=b; what else could/should I have done to determine the source of the problem?
mro has quit [Ping timeout: 252 seconds]
rgrinberg has joined #ocaml
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
wonko has quit [Ping timeout: 265 seconds]
rgrinberg has joined #ocaml
adanwan has joined #ocaml
mro has joined #ocaml
<d_bot> <Et7f3> Use bytecode mode ?
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
<d_bot> <Et7f3> Strace/ltrace or just add print
rgrinberg has joined #ocaml
<d_bot> <EduardoRFS> should the discord channel be present here? https://github.com/ocaml/ocaml
<rgrinberg> cemerick the way we work around this in dune is to avoid/wrap all calls that return Not_found. I think that's the convention in core as well.
<d_bot> <cemerick> @Et7f3 suggesting strace for something this mundane is depressing af 🙃
<cemerick> rgrinberg: I mean, yeah, if I had foreseen the potential for the failure, I might have prevented it
gravicappa has quit [Ping timeout: 252 seconds]
mro_ has joined #ocaml
mro has quit [Ping timeout: 260 seconds]
shawn has joined #ocaml
zebrag has joined #ocaml
Serpent7776 has quit [Quit: leaving]
troydm has quit [Ping timeout: 252 seconds]
adanwan has quit [Ping timeout: 276 seconds]
Skyfire has quit [Quit: brb]
Skyfire has joined #ocaml
Tuplanolla has joined #ocaml
troydm has joined #ocaml
olle has quit [Ping timeout: 252 seconds]
rgrinberg has quit [Read error: Connection reset by peer]
Haudegen has quit [Quit: No Ping reply in 180 seconds.]
Haudegen has joined #ocaml
adanwan has joined #ocaml
Haudegen has quit [Quit: No Ping reply in 180 seconds.]
hendursaga has quit [Ping timeout: 276 seconds]
hendursaga has joined #ocaml
TheRuralJuror has joined #ocaml
mro_ has quit [Quit: Leaving...]
favonia has quit [Ping timeout: 252 seconds]
TheRuralJuror has quit [Ping timeout: 252 seconds]
favonia has joined #ocaml
favonia has quit [Ping timeout: 265 seconds]
Tuplanolla has quit [Quit: Leaving.]
vicfred has joined #ocaml
adanwan has quit [Ping timeout: 276 seconds]