<discocaml>
<diligentclerk> Are you speaking of the difficulty of writing and maintaining OCaml plugins? Or the push towards the "sandboxed" tactic languages? or both?
neiluj has joined #ocaml
neiluj has quit [Ping timeout: 255 seconds]
waleee has quit [Ping timeout: 248 seconds]
<companion_cube>
The fact that to fully use and extend coq, you have to know 3 or 4 languages, including ocaml, whereas for lean it's exactly one language to use and extend it
<discocaml>
<diligentclerk> Ironically I remember that Tom Hales had the exact opposite criticism, haha.
<discocaml>
<diligentclerk> "The only way I can write Lean tactics is in Lean itself? Why can't I just write them in ML?"
<discocaml>
<diligentclerk>
<discocaml>
<diligentclerk> Isabelle seems in the same situation as Coq, it seems that they favor new automation to be written in the Eisbach "internal" language rather than in Isabelle/ML.
<companion_cube>
But lean is almost a ML at this point (although it's pure)
gdiazlo_caml has joined #ocaml
<companion_cube>
I guess some HOL veterans will want to keep the languages separate, but for most people it makes more sense to have only one language
<companion_cube>
Makes it easier to modify, extend, package, etc just like the reasons we typically bootstrap compilers
<discocaml>
<diligentclerk> Yeah I like that Lean is strict, makes me more sympathetic to it
gdiazlo_caml has quit [Ping timeout: 260 seconds]
<discocaml>
<._null._> What do you mean with strict ?
<discocaml>
<diligentclerk> Eager evaluation, as opposed to lazy
<discocaml>
<diligentclerk> c_cube said "it's almost an ML at this point" and this is one point of similarity
<discocaml>
<diligentclerk> The problem with the 3-4 languages seems to be a consequence of the broader issue of Coq having a diverse development team with people pursuing independent research projects and additions. In addition to having two potential successors for Ltac, there are both typeclasses and canonical structures to solve basically the same problems.
<discocaml>
<diligentclerk> There are "Sections" for organizing code + namespacing/encapsulation, and records that can have type-valued fields, and both of these have nontrivial overlap with the classical ML module system.
<discocaml>
<._null._> There are also bona fide modules and functors in Coq
gdiazlo_caml has joined #ocaml
gdiazlo_caml has quit [Ping timeout: 246 seconds]
<companion_cube>
yeah and in the end, functors are kind of a niche feature
neiluj has joined #ocaml
<discocaml>
<diligentclerk> Yes, that's what I meant, I was pointing out that there is an overlap between Coq's sections and records, and Coq's classical ML module system.
neiluj has quit [Ping timeout: 252 seconds]
<companion_cube>
ah, fair
gdiazlo_caml has joined #ocaml
gdiazlo_caml has quit [Ping timeout: 245 seconds]
neiluj has joined #ocaml
neiluj has quit [Ping timeout: 245 seconds]
gdiazlo_caml has joined #ocaml
gdiazlo_caml has quit [Ping timeout: 246 seconds]
twobitsp1ite has joined #ocaml
twobitsprite has quit [Ping timeout: 252 seconds]
twobitsprite has joined #ocaml
twobitsp1ite has quit [Ping timeout: 252 seconds]
gdiazlo_caml has joined #ocaml
infinity0 has quit [Ping timeout: 252 seconds]
landonf has quit [Ping timeout: 272 seconds]
GreaseMonkey has quit [Remote host closed the connection]
cbarrett has quit [Read error: Connection reset by peer]
caasih has quit [Read error: Connection reset by peer]
buoy49__ has quit [Read error: Connection reset by peer]
jbowen has quit [Write error: Connection reset by peer]
Duns_Scrotus____ has quit [Read error: Connection reset by peer]
delyan_ has quit [Read error: Connection reset by peer]
jyc has quit [Read error: Connection reset by peer]
seeg has quit [Read error: Connection reset by peer]
richardhuxton has quit [Read error: Connection reset by peer]
b0o has quit [Read error: Connection reset by peer]
ymherklotz has quit [Read error: Connection reset by peer]
lane has quit [Read error: Connection reset by peer]
patrick_ has quit [Read error: Connection reset by peer]
whereiseveryone has quit [Write error: Connection reset by peer]
Ankhers has quit [Read error: Connection reset by peer]
pmk has quit [Read error: Connection reset by peer]
henrytill has quit [Read error: Connection reset by peer]
pluviaq has quit [Read error: Connection reset by peer]
gdiazlo_caml has joined #ocaml
caasih has joined #ocaml
delyan_ has joined #ocaml
cbarrett has joined #ocaml
Duns_Scrotus____ has joined #ocaml
landonf has joined #ocaml
terrorjack40 has joined #ocaml
buoy49__ has joined #ocaml
terrorjack4 has quit [Ping timeout: 248 seconds]
terrorjack40 is now known as terrorjack4
jyc has joined #ocaml
jbowen has joined #ocaml
noddy has quit [Ping timeout: 252 seconds]
terrorjack4 has quit [Client Quit]
noddy has joined #ocaml
m5zs7k has quit [Read error: Connection reset by peer]
terrorjack4 has joined #ocaml
m5zs7k has joined #ocaml
terrorjack4 has quit [*.net *.split]
gdiazlo_caml has quit [*.net *.split]
kurfen has quit [*.net *.split]
noddy has quit [*.net *.split]
jbowen has quit [*.net *.split]
buoy49__ has quit [*.net *.split]
landonf has quit [*.net *.split]
Duns_Scrotus____ has quit [*.net *.split]
delyan_ has quit [*.net *.split]
lain` has quit [*.net *.split]
bacam has quit [*.net *.split]
dme2_ has quit [*.net *.split]
nore has quit [*.net *.split]
wagle has quit [*.net *.split]
quernd80 has quit [*.net *.split]
nore has joined #ocaml
lane has joined #ocaml
jbowen has joined #ocaml
buoy49__ has joined #ocaml
landonf has joined #ocaml
delyan_ has joined #ocaml
Duns_Scrotus____ has joined #ocaml
lain` has joined #ocaml
dme2_ has joined #ocaml
wagle has joined #ocaml
pmk has joined #ocaml
quernd80 has joined #ocaml
berberman has joined #ocaml
kurfen has joined #ocaml
077AAIWHV has joined #ocaml
bacam has joined #ocaml
gdiazlo_caml has joined #ocaml
kurfen has quit [Max SendQ exceeded]
kurfen has joined #ocaml
pluviaq has joined #ocaml
whereiseveryone has joined #ocaml
Ankhers has joined #ocaml
henrytill has joined #ocaml
b0o has joined #ocaml
seeg has joined #ocaml
ymherklotz has joined #ocaml
richardhuxton has joined #ocaml
welterde has joined #ocaml
bhoot has joined #ocaml
bhoot has quit [Remote host closed the connection]
bhoot has joined #ocaml
bhoot has quit [Remote host closed the connection]
bhoot has joined #ocaml
bhoot has quit [Remote host closed the connection]
landonf has quit [Ping timeout: 248 seconds]
bhoot has joined #ocaml
landonf has joined #ocaml
euphores has quit [Quit: Leaving.]
lane has quit [Ping timeout: 248 seconds]
077AAIWHV has quit [Ping timeout: 252 seconds]
pmk has quit [Read error: Connection reset by peer]
lain` has quit [Read error: Connection reset by peer]
euphores has joined #ocaml
wagle has quit [Quit: No Ping reply in 180 seconds.]
dh` has joined #ocaml
dh` has quit [Changing host]
dh` has joined #ocaml
bhoot has quit [Remote host closed the connection]
pmk has joined #ocaml
lane has joined #ocaml
patrick_ has joined #ocaml
bhoot has joined #ocaml
wagle has joined #ocaml
bhoot has quit [Remote host closed the connection]
lain` has joined #ocaml
YuGiOhJCJ has joined #ocaml
gdiazlo_caml has quit [Ping timeout: 245 seconds]
bhoot has joined #ocaml
bhoot has quit [Remote host closed the connection]
bhoot has joined #ocaml
bhoot has quit [Remote host closed the connection]
bhoot has joined #ocaml
gdiazlo_caml has joined #ocaml
gdiazlo_caml has quit [Ping timeout: 272 seconds]
bhoot has quit [Remote host closed the connection]
bhoot has joined #ocaml
bhoot has quit [Remote host closed the connection]
gdiazlo_caml has joined #ocaml
bhoot has joined #ocaml
<discocaml>
<heyting> My goal is first to get a historic understanding of Coq -- many times I wondered when working with Coq, "why is this function named like it is", "how come this module has a bit more verbose structure than it should have", "why are some modules named in ALL CAPS". Now that I got into OCaml a bit, I see that some of the conventions in Coq are actually inherited from OCaml. Another smaller reason is that OCaml modules and functors seem really fun
<discocaml>
<heyting>
<discocaml>
<heyting> The second reason for learning OCaml is simply to browse the Coq source more efficiently (i.e. understanding the project faster, perhaps even one day making changes to it).
<discocaml>
<heyting>
<discocaml>
<heyting> Last but not least, at some point in my life (I am a recent CS grad), I would love to get a job in OCaml/Coq because of all the languages I've worked with up until now, OCaml seems like the golden middle of them all.
gdiazlo_caml has quit [Ping timeout: 248 seconds]
bhoot has quit [Remote host closed the connection]
bhoot has joined #ocaml
bhoot has quit [Remote host closed the connection]
torretto has quit [Remote host closed the connection]
gdiazlo_caml has joined #ocaml
torretto has joined #ocaml
greaser|q has quit [Quit: No Ping reply in 180 seconds.]
greaser|q has joined #ocaml
bibi_ has quit [Quit: Konversation terminated!]
YuGiOhJCJ has quit [Remote host closed the connection]
YuGiOhJCJ has joined #ocaml
gdiazlo_caml has quit [Ping timeout: 252 seconds]
gdiazlo_caml has joined #ocaml
gdiazlo_caml has quit [Ping timeout: 272 seconds]
bhoot has joined #ocaml
gdiazlo_caml has joined #ocaml
Tuplanolla has joined #ocaml
bhoot has quit [Remote host closed the connection]
gdiazlo_caml has quit [Ping timeout: 252 seconds]
alexherbo2 has joined #ocaml
bartholin has joined #ocaml
gdiazlo_caml has joined #ocaml
gdiazlo_caml has quit [Ping timeout: 248 seconds]
vukung has joined #ocaml
dh` has quit [Ping timeout: 248 seconds]
gdiazlo_caml has joined #ocaml
gdiazlo_caml has quit [Ping timeout: 272 seconds]
alexherbo2 has quit [Remote host closed the connection]
alexherbo2 has joined #ocaml
gdiazlo_caml has joined #ocaml
cedric has joined #ocaml
cedric has quit [Client Quit]
gdiazlo_caml has quit [Ping timeout: 252 seconds]
vukung has quit [Quit: Leaving]
gdiazlo_caml has joined #ocaml
bhoot has joined #ocaml
dawids has joined #ocaml
dawids has quit [Remote host closed the connection]
torretto has quit [Remote host closed the connection]
bhoot has quit [Remote host closed the connection]
gdiazlo_caml has quit [Ping timeout: 252 seconds]
bhoot has joined #ocaml
gdiazlo_caml has joined #ocaml
Anarchos has joined #ocaml
gdiazlo_caml has quit [Ping timeout: 272 seconds]
gdiazlo_caml has joined #ocaml
gdiazlo_caml has quit [Ping timeout: 248 seconds]
gdiazlo_caml has joined #ocaml
euphores has quit [Quit: Leaving.]
gdiazlo_caml has quit [Ping timeout: 252 seconds]
gdiazlo_caml has joined #ocaml
gdiazlo_caml has quit [Ping timeout: 246 seconds]
Anarchos has quit [Quit: Vision[]: i've been blurred!]
bhoot has quit [Remote host closed the connection]
<discocaml>
<jmiven> there are two windows ports of the compiler. One is based on MSVC, but the other is based on mingw-w64 / GCC and is better supported at the moment
gdiazlo_caml has joined #ocaml
alexherbo2 has quit [Remote host closed the connection]
alexherbo2 has joined #ocaml
gdiazlo_caml has quit [Ping timeout: 272 seconds]
alexherbo2 has quit [Remote host closed the connection]
pi3ce has joined #ocaml
bhoot has joined #ocaml
waleee has joined #ocaml
gdiazlo_caml has joined #ocaml
gdiazlo_caml has quit [Ping timeout: 246 seconds]
<discocaml>
<djaruun> i wanted to try to make a simple test website with ocaml and found the dream frameowkr that looked pretty cool and simple. but when i run opam install dream to install it i get this error after a while of it ocmpiling and fixing deps. It is bigarray-overlap that cannot be built for some reason. Can someone help me with this please? (im on debain 12 wsl using ocaml 5.2.0)
<discocaml>
<djaruun> ```
<discocaml>
<djaruun> #=== ERROR while compiling bigarray-overlap.0.2.1 =============================#
bhoot has quit [Remote host closed the connection]
gdiazlo_caml has joined #ocaml
alexherbo2 has quit [Remote host closed the connection]
chrisz has quit [Ping timeout: 245 seconds]
chrisz has joined #ocaml
gdiazlo_caml has quit [Ping timeout: 246 seconds]
gdiazlo_caml has joined #ocaml
gdiazlo_caml has quit [Ping timeout: 252 seconds]
<discocaml>
<barconstruction> The Coq documentation comments that ML is regarded as a "sweet spot" in language design - a type system that helps you without hindering you too much from being productive. I didn't know what they meant by this until I started using OCaml. Now I think I would use OCaml for lots of purposes other than writing coq plugins.
<discocaml>
<barconstruction> "golden middle" is another good term. Not as comprehensive as agda's type system but more restrictive than C# or a dynamic language
gdiazlo_caml has joined #ocaml
gdiazlo_caml has quit [Ping timeout: 252 seconds]
Serpent7776 has joined #ocaml
<discocaml>
<barconstruction> I think the ALL CAPS thing is actually older than OCaml, it's an ML thing. I don't see much ALL CAPS in OCaml these days.
Guest75 has joined #ocaml
Guest75 has quit [Quit: Client closed]
Guest75 has joined #ocaml
Anarchos has joined #ocaml
Guest75 has quit [Quit: Client closed]
Guest75 has joined #ocaml
Guest75 has quit [Client Quit]
Guest83 has joined #ocaml
dh` has joined #ocaml
Guest83 has quit [Client Quit]
Guest75 has joined #ocaml
Guest75 has quit [Client Quit]
Guest75 has joined #ocaml
Guest3 has joined #ocaml
Guest75 has quit [Client Quit]
Guest3 has quit [Client Quit]
gdiazlo_caml has joined #ocaml
YuGiOhJCJ has quit [Quit: YuGiOhJCJ]
<discocaml>
<Kali> i only see all caps for module types
bhoot has joined #ocaml
gdiazlo_caml has quit [Remote host closed the connection]
gdiazlo_caml has joined #ocaml
micro has quit [Quit: Lost terminal]
thizanne has joined #ocaml
tomku has quit [Ping timeout: 265 seconds]
gdiazlo_caml has quit [Ping timeout: 272 seconds]
gdiazlo_caml has joined #ocaml
euphores has joined #ocaml
bhoot has quit []
Techcable has quit [Ping timeout: 260 seconds]
abbe__ has quit [Ping timeout: 260 seconds]
Techcable has joined #ocaml
abbe__ has joined #ocaml
gdiazlo_caml has quit [Ping timeout: 255 seconds]
gdiazlo_caml has joined #ocaml
gdiazlo_caml has quit [Ping timeout: 246 seconds]
greaser|q has quit [Changing host]
greaser|q has joined #ocaml
greaser|q is now known as GreaseMonkey
bartholin has quit [Quit: Leaving]
f[x] has joined #ocaml
dh` has quit [Quit: bbl]
gdiazlo_caml has joined #ocaml
Serpent7776 has quit [Ping timeout: 252 seconds]
<twobitsprite>
I have a dune file rule to build a dependency (a Cap'n Proto module) and I'm getting this error: kj/filesystem-disk-unix.c++:1734: warning: PWD environment variable doesn't match current directory; pwd = /home/isaac/dev/olarn
<twobitsprite>
the dune file is in ./lib/olarnp/dune and I'm invoking dune from .
f[x] has quit [Remote host closed the connection]
<twobitsprite>
(as in, from above the lib directory)
<twobitsprite>
The rule I have in my dune file is: