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]
<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?
<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?
<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
<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]