adrien changed the topic of #ocaml to: Discussions about the OCaml programming language | http://www.ocaml.org | OCaml 4.08 release notes: https://caml.inria.fr/pub/distrib/ocaml-4.08/notes/Changes | Try OCaml in your browser: http://try.ocamlpro.com | Public channel logs at http://irclog.whitequark.org/ocaml
sagax has quit [Remote host closed the connection]
sagax has joined #ocaml
ygrek has joined #ocaml
RalfJ has quit [Ping timeout: 276 seconds]
_5HT has quit [Remote host closed the connection]
_5HT has joined #ocaml
RalfJ has joined #ocaml
stylewarning has quit [Excess Flood]
stylewarning has joined #ocaml
ygrek has quit [Ping timeout: 240 seconds]
mfp has quit [Ping timeout: 276 seconds]
jao has quit [Ping timeout: 265 seconds]
mbac has joined #ocaml
liberiga has joined #ocaml
<mbac> so the libraries base64 and extlib both have modules in them called base64. for some files in my project dune links base64.encode to the one in base64 and for others it links it to extlib, which is causing a compile failure
<mbac> wat
<mbac> i specifically list base64 in the libraries stanza and don't mention extlib at all
<companion_cube> extlib is probably pulled by a dependency?
<mbac> uh. and core_extended has a base64 module too
<mbac> yay
<companion_cube> but it's not at toplevel, shouldn't pose linking issues
<mbac> doing opam remove extlib and taking a reference to Base64.encode before i open Core seems to solve my woes
<mbac> that is my project builds now. whatever
haskell_enthusia has quit [Ping timeout: 245 seconds]
haskell_enthusia has joined #ocaml
analogue has joined #ocaml
sarahzrf has left #ocaml ["WeeChat 2.6"]
flux has quit [Ping timeout: 276 seconds]
analogue has quit [Quit: Leaving]
zolk3ri has quit [Remote host closed the connection]
tormen has joined #ocaml
amosbird_ is now known as amosbird
tormen_ has quit [Ping timeout: 268 seconds]
kvda has joined #ocaml
gravicappa has joined #ocaml
_5HT has quit [Remote host closed the connection]
_5HT has joined #ocaml
_5HT has quit [Remote host closed the connection]
_5HT has joined #ocaml
bbbold has joined #ocaml
_whitelogger has joined #ocaml
bbbold has quit [Quit: My Mac Mini has gone to sleep. ZZZzzz…]
bbbold has joined #ocaml
bbbold has quit [Client Quit]
bbbold has joined #ocaml
bbbold has quit [Client Quit]
_5HT has quit [Remote host closed the connection]
_5HT has joined #ocaml
Haudegen has joined #ocaml
narimiran has joined #ocaml
gravicappa has quit [Ping timeout: 240 seconds]
amiloradovsky has joined #ocaml
mal`` has quit [Quit: Leaving]
mbuf has joined #ocaml
liberiga has quit [Ping timeout: 260 seconds]
mal`` has joined #ocaml
bbbold has joined #ocaml
amiloradovsky has quit [Ping timeout: 265 seconds]
Nikkel has quit [Ping timeout: 246 seconds]
Nikkel has joined #ocaml
barockobamo has joined #ocaml
kvda has quit [Quit: Textual IRC Client: www.textualapp.com]
Serpent7776 has joined #ocaml
barockobamo2 has joined #ocaml
eagleflo has quit [Remote host closed the connection]
barockobamo has quit [Ping timeout: 264 seconds]
eagleflo has joined #ocaml
liberiga has joined #ocaml
bitwinery has quit [Quit: Leaving]
ggole has joined #ocaml
eagleflo has quit [Remote host closed the connection]
eagleflo has joined #ocaml
nullifidian_ has joined #ocaml
malina has joined #ocaml
nullifidian has quit [Ping timeout: 265 seconds]
eagleflo has quit [Remote host closed the connection]
eagleflo has joined #ocaml
eagleflo has quit [Remote host closed the connection]
eagleflo has joined #ocaml
_5HT has quit [Ping timeout: 240 seconds]
gravicappa has joined #ocaml
kakadu has joined #ocaml
mfp has joined #ocaml
gravicappa has quit [Ping timeout: 265 seconds]
nullifidian_ has quit [Read error: Connection reset by peer]
nullifidian has joined #ocaml
nahra` has joined #ocaml
Netsu has joined #ocaml
jack5638 has quit [Ping timeout: 246 seconds]
nahra has quit [Ping timeout: 245 seconds]
jack5638 has joined #ocaml
jbrown has quit [Quit: Leaving]
jbrown has joined #ocaml
zolk3ri has joined #ocaml
Netsu has quit [Ping timeout: 260 seconds]
jao has joined #ocaml
gravicappa has joined #ocaml
jao has quit [Ping timeout: 265 seconds]
haskell_enthusia has quit [Ping timeout: 276 seconds]
haskell_enthusia has joined #ocaml
jbrown has quit [Ping timeout: 276 seconds]
spew has joined #ocaml
jbrown has joined #ocaml
jao has joined #ocaml
bbbold has quit [Ping timeout: 276 seconds]
_5HT has joined #ocaml
picolino has quit [Ping timeout: 258 seconds]
_5HT has quit [Client Quit]
picolino has joined #ocaml
silver has joined #ocaml
Haudegen has quit [Quit: Bin weg.]
liberiga has quit [Ping timeout: 260 seconds]
jao has quit [Ping timeout: 240 seconds]
ohama has quit [Ping timeout: 245 seconds]
pino|work has quit [Quit: brb]
pino|work has joined #ocaml
ohama has joined #ocaml
narimiran_ has joined #ocaml
narimiran has quit [Remote host closed the connection]
gareppa has joined #ocaml
Haudegen has joined #ocaml
FreeBirdLjj has joined #ocaml
FreeBirdLjj has quit [Ping timeout: 265 seconds]
ravenous_ has joined #ocaml
ravenous_ has quit [Ping timeout: 252 seconds]
picolino has quit [Ping timeout: 276 seconds]
picolino has joined #ocaml
Serpent7776 has quit [Quit: Leaving]
zolk3ri has quit [Quit: leaving]
zolk3ri has joined #ocaml
gareppa has quit [Quit: Leaving]
pino|work has quit [Quit: brb]
pino|work has joined #ocaml
narimiran_ has quit [Ping timeout: 245 seconds]
smazga has joined #ocaml
malina has quit [Remote host closed the connection]
ygrek has joined #ocaml
malina has joined #ocaml
laudecay has joined #ocaml
nahra` has quit [Quit: ERC (IRC client for Emacs 26.2)]
nahra has joined #ocaml
jaar has joined #ocaml
ziyourenxiang has quit [Ping timeout: 268 seconds]
<laudecay> yeehaw
<laudecay> hey i think i found the issue from my code the other day
<laudecay> line 23, caml_sodium_init
<laudecay> if i call just that and then do a full major garbage collection i get the segfault again
<laudecay> does anyone see anything wrong with that code? like what's wrong :/
<def`> laudecay: look at PR and Issues of your github project
Netsu has joined #ocaml
<laudecay> wait
<Netsu> Hi there. Could anybody suggest me, please, what is the common way to verify an OCaml sources? E.g. is there any dependent annotations like Liquid Haskell?
<laudecay> holy shit there are 21 stars on it
<laudecay> i'm
<laudecay> holy shit
<hannes> laudecay: no pressure
FreeBirdLjj has joined #ocaml
<def`> Netsu: CFML is the only tool I know to do that, http://www.chargueraud.org/softs/cfml/ . Armael can tell you more about it :)
jaar has quit [Ping timeout: 276 seconds]
<Netsu> def`: oh, thanks, that's already something
<companion_cube> or writing in why3, and extracting the code afterwards
<Armael> Netsu: I'm indeed using CFML and I would be happy to provide guidance, but you should keep in mind that it is still a "research prototype" :)
<Armael> companion_cube was faster; indeed, an other (more pragmatic) option is to write your code in why3 (whyML is essentially a subset of OCaml) and then translate it to OCaml
FreeBirdLjj has quit [Ping timeout: 265 seconds]
<companion_cube> I imagine the extraction could even be done purely on the dev side, so there's no dep when installing a pacakge
<companion_cube> with dune + promote
<Armael> the logic of why3 is less general than CFML's, but if your program is in the supported subset then why3 is most likely more convenient to use (and benefits a lot from automation using SMT solvers, which CFML does not)
<Netsu> Armael: thanks a lot. Just collect necessary information now. How can I contact you in case I have questions on that moment?
<Armael> IRC / xmpp (armael@isomorphis.me) / email (same as xmpp)
<companion_cube> the best domain name 💞
<Armael> btw I don't know if you have some experience with Coq already, but CFML is basically embedded into Coq
<def`> companion_cube: what about iso.mor.phis.me :P
<Armael> learning Coq and CFML at the same time is likely quite hard
barockobamo2 has quit [Remote host closed the connection]
<companion_cube> def`: sorry but no, you can't compete
<Netsu> Armael: have no Coq experience yet. So looks like for me it would be necessary to learn it. BTW Can I refer CFML-related questions only, or Coq/why3 as well?
<Armael> I can answer questions about Coq and CFML, but not really for why3 (they have a website with lots of examples though IIRC)
<Armael> (they also probably have a mailing list)
<Netsu> Thanks for advice, I have a lot new to investigate now :)
<Armael> out of curiosity, what kind of program/library do you want to verify?
<Netsu> companion_cube: is Idris export to OCaml can be compared to why3?
<Netsu> Armael: blockchain consensus algorithm implementation
<companion_cube> I have no idea
<Armael> btw, I forgot to state the obvious, but if your code (or the core logic) can be written as something purely functional, just implement and verify it in Coq
<Armael> well, it's an other option at least
<Armael> well ok, I have no clue what this kind of code would look like :)
<Netsu> Armael: the main problem here actually that will be no formal proof that verified and final code are practically isomorphic.
<Armael> what do you mean?
picolino has quit [Ping timeout: 265 seconds]
picolino has joined #ocaml
<Netsu> that's why looked for kinda annotations to verify OCaml code itself, not "the same code written in other pure language", to avoid transition mistakes.
<Netsu> Or I miss smg?
<Armael> Coq has a mechanism for "compiling" (it's called "extraction") Coq functions as OCaml programs
<Armael> so then you obtain code that you can run directly
<Armael> (you usually have to write some glue code to make your verified code talk to the outside world, that you try to keep small and simple)
<Netsu> Armael: would that code be fast and readable enough than? Sorry, had no experience here yet, that's why asking.
<Netsu> *then
<Armael> you can make it reasonably fast; as for "readable", well, it should be treated as a product of compilation
<Armael> so not something that you should read directly
<Armael> (instead one should read the Coq implementation from which it is obtained)
<Armael> (I think in practice the OCaml code can be quite close to the Coq code, depending on how you write it, but there will be some noise due to the translation)
darktenaibre has joined #ocaml
Anarchos has joined #ocaml
AtumT has joined #ocaml
<laudecay> have yall seen iris
<laudecay> the safe rust concurrency thing
<laudecay> like proof based
<laudecay> the guy who wrote it came and talked at jane street tuesday, it was cool af
<Armael> yes, impressive work :)
<Netsu> laudecay: is there video available from talk?
vicfred has joined #ocaml
<laudecay> i think online maybe
<laudecay> idk
<laudecay> def js internal but confession: tomorrow is the last day of my 14 week internship and idk how to access the talk videos yet
<Netsu> maybe notes?
<laudecay> the website for the thing he presented is at http://plv.mpi-sws.org/rustbelt
<laudecay> talk notes aren't up anywhere i see
<laudecay> the video also isn't up on the internal videos page
AtumT has quit [Quit: AtumT]
AtumT has joined #ocaml
jnavila has joined #ocaml
picolino has quit [Ping timeout: 268 seconds]
picolino has joined #ocaml
vicfred has quit [Quit: Leaving]
vicfred has joined #ocaml
<laudecay> the video also isn't up on the internal videos page
<laudecay> er whoops sorry
zolk3ri has quit [Remote host closed the connection]
zolk3ri has joined #ocaml
mbuf has quit [Ping timeout: 240 seconds]
jnavila has quit [Ping timeout: 276 seconds]
vicfred has quit [Quit: Leaving]
Anarchos has quit [Quit: Vision[0.10.3]: i've been blurred!]
ggole has quit [Quit: Leaving]
unyu has quit [Quit: unyu~]
unyu has joined #ocaml
Serpent7776 has joined #ocaml
jim7j1ajh has joined #ocaml
jimt has quit [Ping timeout: 265 seconds]
interruptinuse is now known as inty
analogue has joined #ocaml
inty is now known as interruptinuse
Asmadeus has left #ocaml ["moo"]
Guest67709 has joined #ocaml
Guest67709 has quit [Remote host closed the connection]
jao- has joined #ocaml
analogue has quit [Quit: Leaving]
jao- is now known as jao
qwebirc97033 has joined #ocaml
<qwebirc97033> hey all
<qwebirc97033> when I try to run `opam init` it errors with the message
<qwebirc97033> `bwrap: No permissions to creating new namespace, likely because the kernel does not allow non-privileged user namespaces. On e.g. debian this can be enabled with 'sysctl kernel.unprivileged_userns_clone=1'`
<qwebirc97033> when I run that I get `sysctl: cannot stat /proc/sys/kernel/unprivileged_userns_clone: No such file or directory`
<qwebirc97033> I'm on ubuntu 18.04
<qwebirc97033> I can't figure out how to enable this option
<qwebirc97033> is there a way to initialize opam that doesn't require user namespaces or something like that?
sheijk_ has quit [Ping timeout: 258 seconds]
gareppa has joined #ocaml
sheijk has joined #ocaml
malina has quit [Remote host closed the connection]
jnavila has joined #ocaml
ygrek has quit [Ping timeout: 276 seconds]
ygrek has joined #ocaml
gravicappa has quit [Ping timeout: 245 seconds]
jnavila has quit [Ping timeout: 276 seconds]
jnavila has joined #ocaml
nullifidian_ has joined #ocaml
nullifidian has quit [Ping timeout: 265 seconds]
bitwinery has joined #ocaml
nullifidian_ is now known as nullifidian
malina has joined #ocaml
qwebirc97033 has quit [Remote host closed the connection]
gravicappa has joined #ocaml
malina has quit [Remote host closed the connection]
ygrek_ has joined #ocaml
ygrek has quit [Remote host closed the connection]
jnavila has quit [Ping timeout: 246 seconds]
jao has quit [Remote host closed the connection]
jao has joined #ocaml
gravicappa has quit [Ping timeout: 245 seconds]
laudecay has quit [Ping timeout: 265 seconds]
kakadu_ has joined #ocaml
jnavila has joined #ocaml
<Netsu> I have a question :) Can module-level have Upper Type Bounds? https://gist.github.com/Pitometsu/1fa440a0461697d8ad0fc6e406a5f765
<Netsu> e.g. declare that some module type is abstract, but include some other module type?
<Netsu> btw can it be done in some form for types there as well?
<Netsu> I guess, open variants and objects only, right?
laudecay has joined #ocaml
laudecay has quit [Ping timeout: 258 seconds]
spew has quit [Quit: Connection closed for inactivity]
ravenous_ has joined #ocaml
ravenous_ has quit [Ping timeout: 246 seconds]
gareppa has quit [Quit: Leaving]
Serpent7776 has quit [Quit: leaving]
nullifidian has quit [Ping timeout: 240 seconds]
jnavila has quit [Remote host closed the connection]
<Netsu> Still curious is it pollible to collect open variant type by functors...
<Netsu> or extensible variants..
nullifidian has joined #ocaml
zolk3ri has quit [Remote host closed the connection]
silver has quit [Read error: Connection reset by peer]
silver_ has joined #ocaml
laudecay has joined #ocaml
laudecay has quit [Ping timeout: 240 seconds]
ygrek_ has quit [Ping timeout: 245 seconds]
kakadu_ has quit [Remote host closed the connection]
<Netsu> e.g. let a : [> ] = let b : [> `A ] = `A in b;; work
<Netsu> but not: include(struct type 'a t = [> `A ] as 'a end : sig type 'a t = [> ] as 'a end);;
<Netsu> Even include(struct type 'a t = [> `A ] as 'a end : sig type 'a t = [> ] as 'a end with type 'a t = [> `A ] as 'a);;
<Netsu> Problem here: sig type 'a t = [> ] as 'a end with type 'a t = [> `A ] as 'a
<Netsu> ah, sorry, dumb question though
unyu has quit [Ping timeout: 276 seconds]
ziyourenxiang has joined #ocaml
smazga has quit [Quit: leaving]
analogue has joined #ocaml
bitwinery has quit [Remote host closed the connection]
bitwinery has joined #ocaml