gentauro has quit [Read error: Connection reset by peer]
gentauro has joined #ocaml
CO2 has quit [Quit: WeeChat 4.1.1]
<discocaml>
<elliottcable> Hm. How y'all go about working on `dune-project`s that need more than one switch (e.g. some dependencies only work on OCaml 5, but the rest of the project also works on OCaml 4, or similar?)
src has quit [Quit: ---]
<discocaml>
<elliottcable> Multiple directory-local switches, a makefile to set them up, religiously use `eval $(opam env --switch=./_opam-4)` or whatever, or …
src has joined #ocaml
<discocaml>
<elliottcable> Ideally I'd like something fairly automated for contributors, but with the least possible fragile shell-scripting and makefile nonsense. )=
<discocaml>
<davesnx> dune workspaces to the rescue
<discocaml>
<elliottcable> hm. what about using that with local switches? i suppose I can use `(context (opam (switch ./_opam-4.08.1)))` or sth like that
<discocaml>
<elliottcable> just don't want to pollute a contributor's global `4.14.0` switch or whatever
Tuplanolla has quit [Quit: Leaving.]
<discocaml>
<elliottcable> Why does `Memtrace` no longer function past v5.0? I'm a little surprised, it looks like `Gc.Memprof` still exists?
discocaml has quit [Server closed connection]
discocaml has joined #ocaml
companion_cube has quit [Server closed connection]
companion_cube has joined #ocaml
palainp has quit [Ping timeout: 272 seconds]
palainp has joined #ocaml
edr has quit [Quit: Leaving]
euouae has joined #ocaml
<euouae>
Hello
<companion_cube>
👋
<euouae>
one of the things I'm enjoying a lot as I'm learning ocaml
<euouae>
is that ocaml separates structures from signatures
<euouae>
this is a bit genius, you can provide several "views" of a struct in this way
<euouae>
not sure if this is done often -- but it is cool nonetheless to decouple code from export options
<companion_cube>
it is nice to have .mli, yeah
<companion_cube>
gives a good higher level view of a module, it's a good place for documentation
chrisz has quit [Ping timeout: 255 seconds]
chrisz has joined #ocaml
waleee has quit [Ping timeout: 255 seconds]
<euouae>
does opam have a feature like "virtual environments" with python?
<discocaml>
<sim642> Opam switches are basically that
<Armael>
(if I understood correctly that you want to write an ocaml library then make it available to C as a C library)
<euouae>
Yes Armael
<euouae>
So don't use ctypes, right?
<Armael>
I've used both ways of doing FFI, these days I prefer to use the default ffi but ctypes is also fine
<euouae>
got it
<euouae>
so there's no automatic way of producing the C library
<Armael>
a few years ago, ctypes required arcane build system steps, but now I think there's dune integration, but I haven't tried it
<Armael>
no
<euouae>
I have to maintain both an .ml and a .c/.h file
<discocaml>
<darrenldl> ohhh load ocaml from c, sorry yeah i misunderstood
<euouae>
that makes sense, thanks
<euouae>
no worries darrenldl I think I was confusing with my explanation
<Armael>
i'd be hard to automatically bridge between ocaml and c in the general case
<Armael>
so the ffi provides you with some primitives but you need to write some "glue code" to do the bridging
<euouae>
I've been spoiled by certain things in Rust where it's possible
<euouae>
for a limited subset of types of Rust to automatically generate C bindings
<euouae>
(if I recall correctly)
<Armael>
yea I guess it's easier in rust beceause you have #repr(C) etc
<Armael>
more stuff could probably be automated for the ocaml-c ffi, but it hasn't been done afaik
<Armael>
fwiw, calling C from OCaml is much more common than the other direction, so I don't know of many examples doing what you want
<euouae>
Armael: I'm looking into Coq producing formally-verified OCaml code
<euouae>
and I thought it'd make sense to have it callable from C
<euouae>
Probably the way to go is to actually generate formally-verified C in the first place and compile with compcert
<Armael>
that'd be an other way to do it yes
<Armael>
likely more complicated on the coq side, because there's no generic mechanism to do coq->c like there is for coq->ocaml
<Armael>
it depends a bit on the code you're trying to produce
<Armael>
but there are examples of C code generated from coq, for example crypto primitives
<euouae>
I haven't yet gotten to the part of the books that describe C generation
<euouae>
but I did reach OCaml generation so I started studying OCaml after that... I figured I'd write at least one dune example of a simple formally verified OCaml lib interfacing with C before continuing in my study
<euouae>
anyway that's the plan for now. I was just wondering, where can I obtain the <caml/...> headers? do they come with ocaml?
<Armael>
:)
<Armael>
yes they do
<euouae>
aha! thanks
Serpent7776 has joined #ocaml
szkl has joined #ocaml
dnh has joined #ocaml
dnh_ has joined #ocaml
dnh has quit [Ping timeout: 264 seconds]
<euouae>
and using dune, what is the way to have the C library depend on the OCaml library?
<euouae>
maybe I'll do it with a makefile instead first
<discocaml>
<darrenldl> does coq have a C backend at any point?
dnh has joined #ocaml
<Anarchos>
darrenldl i do'nt think so, but i am in no way an expert in Coq. I would say the curry howard isomorphism to extract C code from the coq language must be…tedious …
<discocaml>
<.armael.> Yea there’s no easy systematic way to translate Coq to C.. I mean you’d have to emit a while GC etc
<discocaml>
<.armael.> What people have built is typically mechanisms where you write code in some specific Coq DSL and have a way to compile that DSL to C
<discocaml>
<.armael.> Yea there’s no easy systematic way to translate Coq to C.. I mean you’d have to emit a whole GC etc*
<_alix>
There is CertiCoq for compiling Coq into C (or a subset thereof) though I don't know how much of it really works https://github.com/CertiCoq/certicoq
vsiles_ is now known as vsiles
wingsorc has quit [Ping timeout: 258 seconds]
<discocaml>
<darrenldl> yeah i guess at that point itd be the nim route
Anarchos has quit [Quit: Vision[]: i've been blurred!]
szkl has quit [Quit: Connection closed for inactivity]
edr has joined #ocaml
Anarchos has joined #ocaml
Janni has joined #ocaml
Janni has quit [Client Quit]
Anarchos has quit [Ping timeout: 255 seconds]
waleee has joined #ocaml
Anarchos has joined #ocaml
mro has quit [Remote host closed the connection]
rak has quit [Server closed connection]
rak has joined #ocaml
slothby has quit [Ping timeout: 245 seconds]
slothby has joined #ocaml
Serpent7776 has quit [Read error: Connection reset by peer]
Serpent7776 has joined #ocaml
mro has joined #ocaml
Anarchos has quit [Quit: Vision[]: i've been blurred!]
mro has quit [Remote host closed the connection]
bartholin has joined #ocaml
waleee has quit [Ping timeout: 252 seconds]
jlrnick has quit [Ping timeout: 272 seconds]
bartholin has quit [Remote host closed the connection]
bartholin has joined #ocaml
ursa-major has joined #ocaml
justThanks is now known as justTesting
gahr has quit [Remote host closed the connection]
gahr has joined #ocaml
gahr has quit [Remote host closed the connection]
gahr has joined #ocaml
waleee has joined #ocaml
palainp has quit [Changing host]
palainp has joined #ocaml
Tuplanolla has joined #ocaml
thizanne has quit [Server closed connection]
thizanne has joined #ocaml
justTesting is now known as justThanks
jlrnick has joined #ocaml
jlrnick has quit [Ping timeout: 264 seconds]
Serpent7776 has quit [Ping timeout: 240 seconds]
Duns_Scrotus___ has quit [Server closed connection]
Duns_Scrotus___ has joined #ocaml
CO2 has joined #ocaml
<h0rror>
Error: Unbound module Nano_mutex, I've opened Core_unix and I have core_unix in my dune file, any idea?
dnh has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]