<octachron>
gasche, are you also currently posting the link to discuss?
def has joined #ocaml
<octachron>
nevermind, def already posted the link to discuss. Thanks!
<d_bot>
<Def> Thanks Leonidas
<def>
ahah, it is the bot
<def>
Too much magic. thanks octachron :)
<d_bot>
<undu> I'm sad I'll miss the conference 😦
Skyfire has quit [Ping timeout: 250 seconds]
<gasche>
The replays should be available later
Skyfire has joined #ocaml
<gasche>
I wonder what keyboard-press-overlay is used in the GopCaml video, it's rather nice.
<def>
(the replays will be available, with closed captions added as a bonus!)
bartholin has joined #ocaml
<xd1le>
nice it reminds me of glr
mro has joined #ocaml
mro has quit [Remote host closed the connection]
Ilias has joined #ocaml
mro has joined #ocaml
<xd1le>
does the mode also handle indentation when deleting regions, or is emacs handling that?
<d_bot>
<dinosaure> I don't really understand why OCaml can not infer that the `B` case is impossible when you are only able to generate a `b g` which can only be an `int g`: https://paste.isomorphis.me/RCd
tsmc has joined #ocaml
<Armael>
dinosaure: the B case is not impossible, you *can* get B as input of the function
<Armael>
it's just that then you can't produce an output, but that's on you (the implementor of the function) to handle :p
<Armael>
(you could still raise an exception for instance)
<gasche>
If your input type was `(b, b) t` then presumably it would be impossible.
Haudegen has joined #ocaml
<d_bot>
<dinosaure> hmmhmm
<gasche>
huh, nevermind
<gasche>
(I read `B : (string, int) t`)
<d_bot>
<dinosaure> ok, let's put some fancy `assert false` so 🙂
Guest7095 has joined #ocaml
gopiandcode has joined #ocaml
Guest7095 has quit [Quit: Client closed]
Anarchos has joined #ocaml
nojb has joined #ocaml
Geekingfrog_ is now known as Geekingfrog
hendursa1 has joined #ocaml
hendursaga has quit [Ping timeout: 276 seconds]
TomR has joined #ocaml
tsmc has quit [Quit: Client closed]
gasche has quit [Quit: Client closed]
mseri has joined #ocaml
Anarchos has quit [Quit: Vision[0.10.3]: i've been blurred!]
gasche has joined #ocaml
<mseri>
Is the live session restarting at the same youtube url?
Guest7096 has joined #ocaml
<TomR>
I hope so.
<TomR>
Yes!
Guest7096 has quit [Client Quit]
<mseri>
indeed, is live just now, thanks!
haesbaer1 has quit [Ping timeout: 252 seconds]
haesbaert has joined #ocaml
Ilias has quit [Quit: Client closed]
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
nojb has quit [Remote host closed the connection]
nojb has joined #ocaml
nojb has quit [Remote host closed the connection]
nojb has joined #ocaml
nojb has quit [Remote host closed the connection]
nojb has joined #ocaml
nojb has quit [Remote host closed the connection]
nojb has joined #ocaml
nojb has quit [Remote host closed the connection]
nojb has joined #ocaml
emile87 has joined #ocaml
emile87 is now known as emiler
nojb has quit [Remote host closed the connection]
nojb has joined #ocaml
TomR has quit [Quit: Client closed]
nojb has quit [Remote host closed the connection]
nojb has joined #ocaml
Anarchos has joined #ocaml
Guest552 has joined #ocaml
Guest552 has quit [Client Quit]
Julow has joined #ocaml
mseri has quit [Quit: Client closed]
gadmm has joined #ocaml
<Anarchos>
why is 4.13.0 not tagged on github ?
<octachron>
Because it is not released?
<octachron>
The alpha and beta releases for 4.13.0 are tagged on github.
hendursa1 has quit [Remote host closed the connection]
<octachron>
Anarchos, I am not sure what you mean, sorry. 4.12.0 is indeed released and tagged on github.
gadmm80 has joined #ocaml
gadmm80 has quit [Client Quit]
gadmm73 has joined #ocaml
<gasche>
@gadmm I suspect that the attendance is rather high even outside the OCaml Workshop days. I joined slightly before the workshop started, and there were 140 people already.
<gadmm73>
nice!
<gadmm73>
good to know
<gasche>
(But the standard way to use IRC nowadays is through an always-present remote, so it's not clear how many people are actually reading the chat on any given day.)
gadmm has quit [Ping timeout: 246 seconds]
<gadmm73>
Unfortunately my University's network seems to block IRC / this web client. I am currently on my mobile data (what I already have to do to connect to my institution's SMTP server), but I'll have to disconnect now to connect to ICFP
<gadmm73>
bye!
gadmm73 has quit [Client Quit]
<Anarchos>
octachron i expected to see 4.13 in the list
<gasche>
@Anarchos 4.13 is not released yet.
<Anarchos>
gasche oh ok
nojb has quit [Remote host closed the connection]
<gasche>
(At the workshop, on the Airmeet interface) it's frustrating how we get kicked out of the room when the sessino end.
<gasche>
I was typing a silly joke and boom, no time to post it.
<reynir>
will it be possible to find ocaml workshop recordings later?
<gasche>
yes!
<gasche>
I think that @def is planning to make more precise announces about that at some point. But "yes".
<gasche>
(Wow does IRC send "Julow is typing" informantion these days? So 21st century!)
<d_bot>
<andreypopp> @Drup trying out dowsing now and it's veeery fast! One question — is there some ranking algo planned? Right now for `_ list -> int` it returns `'a -> int` functions first.
mro has joined #ocaml
<d_bot>
<Drup> yes, there si
<d_bot>
<Drup> but none is implemented yet
nojb has quit [Remote host closed the connection]
<d_bot>
<Drup> In general, there are lot's of things to finetune
nojb has joined #ocaml
mro has quit [Ping timeout: 240 seconds]
nojb has quit [Remote host closed the connection]
nojb has joined #ocaml
nojb has quit [Remote host closed the connection]
nojb has joined #ocaml
nojb has quit [Remote host closed the connection]
nojb has joined #ocaml
mro has joined #ocaml
nojb has quit [Remote host closed the connection]
nojb has joined #ocaml
nojb has quit [Remote host closed the connection]
Guest73 has quit [Quit: Client closed]
nojb has joined #ocaml
nojb has quit [Remote host closed the connection]
Haudegen has quit [Quit: Bin weg.]
mro has quit [Remote host closed the connection]
nojb has joined #ocaml
n-osborne has joined #ocaml
mro has joined #ocaml
xd1le has quit [Quit: xd1le]
mro has quit [Read error: Connection reset by peer]
mro has joined #ocaml
nojb has quit [Remote host closed the connection]
<d_bot>
<andreypopp> I understand. But it's already impressive how fast it is, it can probably be used with interactive like workflow (a-la fzf)
<d_bot>
<Drup> yes, that's the goal. It still has some catastrophic corner cases, performance wise (some of the uber-polymorphic combinators in core-extra ಠ_ಠ)
<d_bot>
<Drup> Actually, for matching, it's not a problem, only for unification
<companion_cube>
Yo gasche
<gasche>
Yo back
<companion_cube>
Hope you're doing well :)
<Drup>
Hey, it's been a while since you hanged around here !
<gasche>
I am still of the general opinion that IRC chats are bad places to hang out, but I joined on the occasion of the OCaml Workshop.
nojb has joined #ocaml
<companion_cube>
Yeah they're full of shady people
<companion_cube>
Like ocabot
Guest68 has joined #ocaml
<gasche>
(How did people in EU timezones manage to watch the last two talks, did you not take a lunch break? Wild!)
<d_bot>
<Kakadu> gasche: I put my plate before monitor and watched 🙂
<gasche>
My problem with IRC (or any other similar instant-chat platform) is that I've observed many times that over time it creates sub-communities of people with a specific sub-culture that differs from the main project, and creates an observability problem from the outside: if you are not "in", you will miss some shared information, not understand how
<gasche>
some decisions/discussions happen or be unable to participate. I don't like that evolution, so I prefer not to participate.
<gasche>
(Also: when I do, it's very nice, and then I spend all my time talking instead of getting other stuff done.)
<octachron>
I am not sure that avoiding the subgroup that you can recognize really reduces fragmentation rather than creating subtler fragmentation that you no longer recognize.
<gasche>
Another problem with IRC is that the content poured in it ends up being fairly unstructured and hard to search; in a sense it is "lost" for the future, unlike posts on Discuss for example.
<sadiq_>
it's useful for having short back and forths.
sadiq_ is now known as sadiq
<companion_cube>
It's friendlier than discuss :)
<gasche>
I don't disagree, but this immediacy has a cost in terms of reusability of the question/answer and content in general.
<companion_cube>
Sure
<gasche>
It may be more accessible (lower barrier to entry) to some newcomers than Discuss or some other platforms. And also it's hard to work against cultural habits like "all projects have a Discord, I just join the Discord"..
<companion_cube>
Not sure how much beginners reyse existing discuss posts
<companion_cube>
Yeah discord is, sadly, easier
<gasche>
(My "content gets lost" criticism also applies to Twitter/Mastodon/etc.)
nojb has quit [Remote host closed the connection]
nojb has joined #ocaml
<sadiq>
yea.
<sadiq>
it is possible to make the IRC logs searchable
<sadiq>
maybe that's something that could be done on the new ocaml.org?
<gasche>
And whitequark has nice logs
<gasche>
but the way we write on IRC is not conductive to content that it nice to serach, and to come back to after the fact
<gasche>
(plus: no threading at all, etc.)
<gasche>
Btw.: hi @sadiq :-)
<sadiq>
hi gabriel =)
nojb has quit [Remote host closed the connection]
nojb has joined #ocaml
<def>
(retrieving Q/A from an IRC log, that's a job for some IA/NLP :P)
<zozozo>
hi gasche
nojb has quit [Remote host closed the connection]
<gasche>
hi @zozozo; I had a question on Alt-Ergo this morning, where were you ? :-) (The question was "why does Why3 need to split_vc so often, why can't SMT solvers do it themselves?")
<zozozo>
gasche: sorry, I woke up quite late (and also forgot to register for icfp, so I'm following the talks on youtube, :p )
<zozozo>
ah, the split thing is... an interesting question
<zozozo>
the thing is that it's not easy to do well and correctly once the formulas are turned into cnf and fed to the solver, so it could have to be done before as some kind of pre-processing, which seems doable, just adds some work
<d_bot>
<EduardoRFS> oh gasche here
<zozozo>
(and then, it becomes a bit hard to adequately share the progress/reasoning done between the various split goals)
<gasche>
Does Alt-Ergo support first-class syntax for ADTs and pattern-matching like CVC?
<companion_cube>
Does AE turn non ground formulas into cnf?
<companion_cube>
Deno
<companion_cube>
Lolol bad autocorrect
salkin has joined #ocaml
Guest27 has joined #ocaml
Guest27 has quit [Client Quit]
<d_bot>
<EduardoRFS> "25 years of OCaml", are we getting an OCaml 2?
<gasche>
I don't follow, we are at OCaml 4 already right?
<sadiq>
is the youtube live feed broken for anyone else?
favonia has joined #ocaml
<d_bot>
<EduardoRFS> broken here too after the session ends
<d_bot>
<EduardoRFS> we can call it OCaml 1.4.13 and do a big breaking change, think Perl 6
<gasche>
ah
<d_bot>
<EduardoRFS> imagine cleaning up the typer
<d_bot>
<EduardoRFS> reverting the typing order of `let`
<d_bot>
<EduardoRFS> removing `Field()`
<sadiq>
it's always a little sad when you do git blame on some code you are editing and the commit messages are in French and from ~20 years ago. You kind of want to leave them alone.
<d_bot>
<EduardoRFS> Had this same feeling a lot this week, ~26 years ago, and I changed the line, it feels wrong
<gasche>
Relatedly, I think that "git blame" is a really poor interface to explore the history of code. We should have something much better, less robust to silly changes etc.
<gasche>
(Probably as a TUI rather than just a CLI tool. But even say magit doesn't have something as nice as we could have.)
<gasche>
even following a file after renames is painful, even though git tracks renaming information in the first place
<d_bot>
<EduardoRFS> if we had a diff over AST instead of actual text it would already solve half my problems
<zozozo>
gasche: I think so for ADTs (the native language has a syntax for that I think)
<zozozo>
companion_cube: I don't know, I'd have to look at it, but I think that ae does the same as most SMT and turns non-ground formuals into cnf, and then determine some triggers for these formulas
Haudegen has joined #ocaml
<zozozo>
(sorry for the dealy, watching the talks took a bit more attention than planned, :p )
<sadiq>
is there another live stream?
<gasche>
I'm expecting the stream to start again when the session resumes, in about 10mn
<companion_cube>
Handling match isn't hard once you have datatypes anyway
<sadiq>
oh, that would make sense.
<companion_cube>
Well, shallow match
<zozozo>
yeah, AE has some support for that
<companion_cube>
Does AE still do pure trigger matching these days?
<zozozo>
I think so, but I'm not completely sure about that (I think there's also probably some kind of arithmetic instantiation somewhere)
<d_bot>
<Christophe> Aah OK, reaction to the live, I'll watch that later it sounds super interesting!
<d_bot>
<froyo> yeah it was actually really nice
<d_bot>
<froyo> and Xavier has a nice smile
Guest5056 has joined #ocaml
<companion_cube>
Xavier is a cool person
<companion_cube>
I just wish he had more place in his heart for imperative primitives :-°
<d_bot>
<froyo> :P
<d_bot>
<EduardoRFS> what you're talking about? We have Obj.magic, that's enough primitives
Guest15 has joined #ocaml
<companion_cube>
:)
Guest5 has quit [Ping timeout: 246 seconds]
<def>
clippy says: Obj.set_field
<companion_cube>
I would seriously love having `let mut`, `break`, `return`, `continue`
<d_bot>
<froyo> vectorization prims in ocaml when
<zozozo>
def: flambda says: if you use Obj, I will break your code, :D
<d_bot>
<EduardoRFS> Obj.magic + int_as_pointer and you can even do goto using OCaml
mro_ has joined #ocaml
<companion_cube>
can I use Obj.set_field on the stack? 🤔
mro__ has joined #ocaml
<zozozo>
companion_cube: not sure, given that Obj.set_field dereferences the value/pointer that you give it, so you'd need a value that points to the stack, which is not possible currently, I think ?
<companion_cube>
surely you can cast any int into a pointer using the goodness in Obj? :DDD
<zozozo>
sure
<companion_cube>
(jk, I don't want to give you heart attacks)
<zozozo>
but it's not clear how to get an idea of where your stack is
<zozozo>
and else, with aslr, you'll probably cause a segfault if you try to set an arbitrary memory location
mro has quit [Ping timeout: 240 seconds]
<d_bot>
<EduardoRFS> better than set_field, is Obj.magic + := because then you ignore the existance of float arrays
<d_bot>
<EduardoRFS> reduce a couple instructions
Guest15 has quit [Quit: Client closed]
mro_ has quit [Ping timeout: 250 seconds]
<d_bot>
<EduardoRFS> zozozo: I think you may be able to access Caml_state which has a pointer to the stack
hackinghorn has joined #ocaml
<companion_cube>
curse you, float arrays
hornhack has quit [Ping timeout: 250 seconds]
<zozozo>
@EduardoRFS : that could be a solution, but I'm not sure you can get it purely from the ocaml side... it's either in a dedicated register (pre-multicore-required-changes iirc), or in a thread-global in C code, so not easy to get to
<zozozo>
I agree with companion_cube , float arrays are really annoying
<olle>
Soon you can all use my own programming language with memory-safe opt-out of GC ^^
<olle>
Maybe...
<d_bot>
<froyo> one day
<d_bot>
<froyo> every time i talk about sixten with friends i get hype back
<companion_cube>
I'm kind of looking at carp personally
<companion_cube>
And... Zig
<olle>
Is carp with or without lifetime annotations?
<companion_cube>
Without I think
<d_bot>
<EduardoRFS> ```ocaml
<d_bot>
<EduardoRFS> external caml_state: 'a -> unit = "Caml_state"
<d_bot>
<EduardoRFS> let x = caml_state
<d_bot>
<EduardoRFS> ```
<d_bot>
<EduardoRFS> now I have a pointer to Caml_state, and I have no problem on using it
<zozozo>
ah, nice indeed...
<zozozo>
"how to break ocaml" version n°36
<zozozo>
(maybe the external caml_state should have type unit -> Obj.t rather than 'a -> unit ?)
<gasche>
Zig has amazing tooling work done on the low-level internals (cross-compilation, etc.); it feels like a much nicer C for close-to-system programming nowadays.
<olle>
Is Zig even memory safe?
<d_bot>
<EduardoRFS> zozozo: it doesn't matter, I will need to use instruction decoding to extract the pointer anyway, as just refering to the external already calls the function
<olle>
The more you know, the less you search for it? :) So doesn't count senior devs?
<companion_cube>
also good luck handling weird language names like "go"
<companion_cube>
it's like using stackoverflow statistics
<d_bot>
<davesnx> That's really not accurate
<Tardigreat[m]>
i don't understand why language popularity stuff like TIOBE matters at all. use the right tool for the job
<olle>
Uh, because we're talking about how to target your new shiny programming language? :)
<Tardigreat[m]>
TIOBE won't help you at targeting anything if the language is a piece of crap. find a niche for it and be better than everyone else at it
<companion_cube>
yep
<companion_cube>
and sometimes a killer app can do great things for a language's popularity
<companion_cube>
like Rails did for ruby
<olle>
Tardigreat[m]: A *new* niche?
<olle>
The most common niche I see is "systems programming language".
<Tardigreat[m]>
not necessarily, there are plenty of niches that are "filled" but have a bunch of clunky things holding people back from doing what they want to do
<olle>
Really?
<Tardigreat[m]>
yes, because no language other than C and C++ seem to understand that what matters in systems programming is out of bound dependency management, dynamic linking and sensible deployment stories
<companion_cube>
well, C isn't exactly the most convenient tool 😂
<companion_cube>
Tardigreat[m]: dynamic linking and sensible deployment, in the same sentence? :)
<companion_cube>
half of what makes Go popular is static linking, for example
<Tardigreat[m]>
companion_cube: users don't want to download 100GB of data because librust had a bug
<olle>
Probably 80% what makes Go popular is Google marketing brand recognition.
<Tardigreat[m]>
the biggest consumers of systems programming are operating system vendors, not google who can just afford to create massive binaries and recompile everything on demand
<companion_cube>
Tardigreat[m]: ah, you mean for end user stuff.
<companion_cube>
well, people mostly use windows, where it's not static linking, but each program has its own world
<companion_cube>
so in practice not sure it changes that much
<companion_cube>
so that's Talex talking?
<Tardigreat[m]>
companion_cube: it changes a lot, i wanted to use a better language than C in some of my projects that need to be deployed to consumers (i looked at rust for this particular thing). the problem was that (a) cargo had no way to say anything about system library versions; (b) everything would be statically linked and with just initial functionality, the binary was huge and in a massive dependency hell already
<Tardigreat[m]>
like it or not, people have done a lot of work on getting packaging right (even microsoft), and having every language reinvent its own tool that statically links a bunch of unmaintained bitrotted crap that needs to be manually updated by the person that forgot about the project is not good
<companion_cube>
🤷
<companion_cube>
it's good to have both options I guess
<companion_cube>
with `unsafe` you can use dlopen/dlsym
<companion_cube>
it's just crappy because it has to go through C signatures…
<Tardigreat[m]>
yeah, but you have no way to say: "i want libfoo >= x.y" in the build system itself
<Tardigreat[m]>
cargo doesn't know anything about this, for example
<companion_cube>
right, no notion of depext
<companion_cube>
just sys-…
<Armael>
companion_cube: tracing support!
<companion_cube>
yessssss
<companion_cube>
can't wait for effects to land
<companion_cube>
so that tiny_httpd can take the lead of the benchmark game 🤔
<companion_cube>
🤔🤔👱🏾
<companion_cube>
🤔
<olle>
Tardigreat[m]: Tooling, eh. Hm.
<olle>
One of the reasons why picking a lang is such a big commitment.
<Tardigreat[m]>
having done some packaging for a few things like that... i can safely say that ocaml didn't make me want to jump off a building, but rust certainly did :P
<companion_cube>
e f f e c t s y s t e m
<Armael>
looks very solid
<companion_cube>
Tardigreat[m]: funny, that's the opposite of my experience, but I'm not a packager
<olle>
Typed effects, still, right?
<companion_cube>
nope
<olle>
Nope?
<companion_cube>
even for OCaml I'd just make a local switch, compile the thing, and package he binary
<companion_cube>
the*
<companion_cube>
olle: typed effects will come later
<d_bot>
<leviroth> There was some talk about dowsing above, but I couldn't find the talk that prompted it (assuming there was one). Does anyone know what it was?
<olle>
companion_cube: They'll add effects first and typed effects later...?
<companion_cube>
yes
<olle>
companion_cube: Wouldn't that create a pretty big technical debt in all code using effects?
<companion_cube>
I have no idea
<Armael>
@leviroth : it was in the ML workshop; I assume they have recordings on youtube
<octachron>
companion_cube, it is not that clear that effect will come before typed effects
<companion_cube>
Tardigreat[m]: that said I've heard other people complain about the packaging
<Tardigreat[m]>
olle: yeah, "simple" tooling that can check external dependencies is one of the main reasons why i still use C, C++, various schemes (not all) and lua in things
<companion_cube>
octachron: oh? so we're going to have to wait years for effects then?
<olle>
Tardigreat[m]: Huh.
<olle>
The longer you wait, the better it feels :D
<Tardigreat[m]>
companion_cube: yeah, there are definitely things that can be improved, but cargo is just one of those things that even if program X builds with libfoo 2.0 just fine and you have your own crate "upstream" instead of crates.io, you can't force it to actually build without changing the cargo description which is just nuts
<companion_cube>
you mean without updating the lockfile?
<Tardigreat[m]>
so in cargo.toml you'd have your dependencies with versions. that's the authority on what library versions are accepted and there's no vetoing it
<companion_cube>
yes
<Tardigreat[m]>
which means for unmaintained upstreams, you either fork it or accept some ancient and vulnerable library version
<companion_cube>
(and I like it)
<Tardigreat[m]>
because littlebean69 (made up name in case someone finds this person on github...) on github last touched their project in 2017 and has since moved on to new adventures and lost their password, so your options are to either fork it or accept a life of using software that hasn't updated its dependency versions since 2017
<companion_cube>
well, unmaintained software is unmaintained, what other options do you have
<Tardigreat[m]>
which then means you need to carry around ~10 versions of the same library that is fully backwards compatible in your package repo
<Tardigreat[m]>
yeah, but with rust it propagates to library versions
<companion_cube>
fork and use a git path, worst case
<Tardigreat[m]>
so instead of having libfoo which is backwards-compatible once, you have libfoo 10-20 timies
<Tardigreat[m]>
times, rather
<octachron>
companion_cube, maybe. It is at least beyond my ability to make time estimate.
<companion_cube>
ugh
<d_bot>
<froyo> Tardigreat[m]:
<d_bot>
<froyo> > Static binaries are huge
<d_bot>
<froyo> funny how this is implied when in reality it doesn't need to be. musl-gcc static binaries are competitively close to dynamic ones, and zig binaries are smaller than dynamic c binaries
<gasche>
dear IRC crowd, what are cool new OCaml projects people should know about?
<d_bot>
<froyo> what's the preferred system for docker images? alpine
<Tardigreat[m]>
yeah, it doesn't need to be, but even if it's not, if you deploy your entire base for an OS statically linked and then a core library that everything depends on has a bug, you essentially need to redownload every single binary. this also isn't a necessity as there could be mechanisms to help this, but then you're essentially reinventing dynamic linking in a way
<gasche>
(nothing against debates on binary size and static vs. dynamic linking, but ahem)
<Tardigreat[m]>
a small docker container is a different use-case from someone installing an operating system on their laptop or desktop that uses all kinds of weird software
<d_bot>
<froyo> that's a trade-off still
<d_bot>
<froyo> you know
<Tardigreat[m]>
(besides, guix and nix produce smaller docker containers than alpine)
<Tardigreat[m]>
which are not statically linked
<d_bot>
<froyo> how dynlib version mismatching is a thing
<gasche>
One talk at the OCaml workshop today made me want to look into Monolith more closely ( https://gitlab.inria.fr/fpottier/monolith ). In particular I hadn't realized that it was AFL-based (otherwise I would have looked earlier).
<companion_cube>
gasche: depends, are you interested in theorem proving? 🙃
<gasche>
yes!
<d_bot>
<froyo> and unpatched bugs lead to whole system vulnerability
<d_bot>
<froyo> version mismatching leads to stuff like stow and nix and windows in which.. you end up with more bloat because you just bypass this dependency hell by making copies of the dynlibs
<Tardigreat[m]>
yeah, dynamic linking has problems. i'm not claiming it doesn't. i'm claiming that forced static linking without external dependency management is a pipe dream put into tools that just causes pain. having the option to statically link or dynamically link things is great. forcing one is just plain dumb
<d_bot>
<froyo> so really you end up running in circles
<gasche>
the talks on Multicore OCaml also had me itching to play a bit more with it
<gasche>
(I've done some light hacking already on the DomainsLib API for example)
<gasche>
I'm curious to know if we could improve the "standard library for Multicore OCaml" experience
<companion_cube>
gasche: well, zipperposition won CASC this year again ;)
<gasche>
congrats!
<gasche>
I think when I watched the IJCAR talks, the results were not available
<gasche>
so are some people actively working on it these days? (are you?)
<companion_cube>
some people in Amsterdam, not me
<gasche>
(Multicore OCaml personal wishes: (1) open an RFC to move Random to a splittable generator, (2) implement a "dynamic checking ownership-passing" container for unsafe mutable data-structtures)
<gasche>
(well just ideas from today)
<companion_cube>
ohh yes
<companion_cube>
Random being splittable would be awesome
<gasche>
I think we need to write an RFC, and write a small benchmark to check Xavier's splittable generators against the current implementation. (And possibly think of a macro-benchmark that uses Random a lot, but does useful stuff as well.)
<d_bot>
<froyo> from what i heard by 5.0 we'll be able to pick the runtime variant per-compilation, is that true?
<companion_cube>
there's a bunch of QCheck tests in the wild, that shoudl exercize Random :)
<gasche>
wow, you're better than Vampire now
<gasche>
it's really impressive
<companion_cube>
only on HO
<companion_cube>
but yes
<companion_cube>
it's all thanks to the Amsterdam team under Jasmin :)
<companion_cube>
they're good
<gasche>
what about "Large Theory Batch", any ideas what's needed there?
<d_bot>
<froyo> i mean we already sort of have that ability but i mean multicore vs classic
* Tardigreat[m]
eagerly awaits full upstreaming of multicore ocaml
<companion_cube>
it's different, and no one cared enough
<d_bot>
<leviroth> Thanks Armael, looks like it was the "Isomorphisms are back" talk
<gasche>
@companion_cube a little mouse tells me you are also hacking on SMTs
<companion_cube>
:p
<gasche>
can I ask what happened to the efforts to use model-constructing stuff (mcsat / archsat?)
<companion_cube>
there's still zozozo's msat, of course :)
<companion_cube>
and my experiments using mc2, but it's kind of at a standstill right now
<gasche>
I thought McFoo was the bee's knees and everyone should use that
<companion_cube>
:D mcSAT is cool
<gasche>
(at least on the subset where we know how to combine their theories)
<companion_cube>
it's just quite experimental compared to mainstream
<gasche>
which of these approaches should we try to start from if one wanted to do dependent-types ATP for Coq?
<gasche>
(I would guess superposition in general, but SMT if we want to be good at numerical mathematics?)
<companion_cube>
ah, that's a really good question
<companion_cube>
both, probably, but for different things
<companion_cube>
in practice SMT works better and there's SMTCoq
<companion_cube>
but dependent types are quantifier heavy so that's hard to extend
<companion_cube>
so far Jasmin's efforts to get good HO (like HOL) provers have borne more fruits on the superposition side
<gasche>
what's the state of the art to have both higher-order and modulo-theories working well?
<gasche>
(iirc. there was "avatar modulo theories" supposed to get the best of both worlds, does this work in practice?)
* Anarchos
wishes to be brave enough to tackle ATS…
hendursa1 has quit [Quit: hendursa1]
hendursaga has joined #ocaml
<companion_cube>
well :D
<companion_cube>
there's no such state of the art sadly, I think
<companion_cube>
cvc5 perhaps
<companion_cube>
it does both, but the HO support is still not too good afaik
gasche has quit [Quit: Client closed]
gasche has joined #ocaml
<gasche>
(I'll be away from keyboard for a few hours)
olle has quit [Ping timeout: 240 seconds]
waleee has joined #ocaml
Skyfire has quit [Quit: WeeChat 3.2]
hendursaga has quit [Remote host closed the connection]
hendursaga has joined #ocaml
gravicappa has joined #ocaml
n-osborne has quit [Quit: Client closed]
mbuf has quit [Quit: Leaving]
<sadiq>
froyo: I didn't see this answered on IRC but the intention is no, there will be no runtime variants. 5.0 will just be multicore.
<companion_cube>
what about 5.1? :)
<reynir>
o/
<sadiq>
even then, the intention is to only have the multicore GC. There just isn't the resources to maintain and test two separate GCs and runtimes.
<companion_cube>
(hopefully same goes for flambda2)
<sadiq>
this is also partly why multicore has taken some time, we want to make sure that we maintain backwards compatibility with both existing code and the performance users expect.
emiler has quit [Quit: Client closed]
Haudegen has quit [Quit: Bin weg.]
<zozozo>
companion_cube: that's indeed the long term plan for flambda2 (but it's not going to be easy I suspect)
rgrinberg has joined #ocaml
<companion_cube>
even if -Oclassic is the implicit default? :)
<reynir>
"can I disappear?" :D
<companion_cube>
yasss QCheck
<companion_cube>
otoh, going throught Coq ?!?!??!
<Guest5056>
ppx or coq, pick your poison
<companion_cube>
I mean ppx would be much simpler in this case :D
<companion_cube>
does this… only work for pure code?
elf_fortrez has joined #ocaml
Anarchos has quit [Quit: Vision[0.10.3]: i've been blurred!]
<d_bot>
<froyo> sadiq: I see, thanks
Skyfire has joined #ocaml
Haudegen has joined #ocaml
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
average has quit [Quit: Connection closed for inactivity]
gasche has quit [Quit: Client closed]
rgrinberg has joined #ocaml
rgrinberg has quit [Client Quit]
gravicappa has quit [Ping timeout: 252 seconds]
daachi has joined #ocaml
zebrag has joined #ocaml
Guest2 has joined #ocaml
Guest2 has quit [Client Quit]
gravicappa has joined #ocaml
<d_bot>
<RegularSpatula> Is there a reason that Cmdliner has `Arg.(&)` other than the fact that the cmdliner library predates the `Pervasives.(@@)` operator? I.e., was there just no such operator at the time cmdliner was written? (From git it looks like cmdliner was sometime in 2011, whereas the `@@` operator came in 2013, as far as I can tell from google...)
<d_bot>
<hcarty> @RegularSpatula I think that is most or possibly all of the reason - there was no similar operator in stdlib
<d_bot>
<carmysilna> Does OCaml have support for something like Haskell's pattern synonyms where you can define alternative syntaxes or constructors to make certain repeated pattern matches less verbose?