toastal has left #ocaml [Error from remote client]
toastal has joined #ocaml
toastal has quit [Ping timeout: 240 seconds]
waleee has quit [Quit: WeeChat 4.1.2]
Serpent7776 has joined #ocaml
Inline has joined #ocaml
dh` has quit [Quit: Leaving]
waleee has joined #ocaml
gzar has joined #ocaml
Inline has quit [Ping timeout: 255 seconds]
Inline has joined #ocaml
Inline has quit [Remote host closed the connection]
Inline has joined #ocaml
sleepydog has quit [Remote host closed the connection]
brettgilio has quit [Remote host closed the connection]
soni_ has quit [Remote host closed the connection]
philipwhite has quit [Remote host closed the connection]
b0o has quit [Remote host closed the connection]
lane has quit [Remote host closed the connection]
kuruczgy has quit [Remote host closed the connection]
seeg has quit [Remote host closed the connection]
richardhuxton has quit [Remote host closed the connection]
ursa-major has quit [Remote host closed the connection]
immutable has quit [Remote host closed the connection]
henrytill has quit [Remote host closed the connection]
pluviaq has quit [Remote host closed the connection]
whereiseveryone has quit [Remote host closed the connection]
jmcantrell has quit [Remote host closed the connection]
rustyne has quit [Remote host closed the connection]
patrick_ has quit [Remote host closed the connection]
ggb has quit [Remote host closed the connection]
arya_elfren has quit [Remote host closed the connection]
ymherklotz has quit [Remote host closed the connection]
pmk has quit [Write error: Broken pipe]
_alix has quit [Write error: Broken pipe]
Ankhers has quit [Remote host closed the connection]
xvilka has quit [Remote host closed the connection]
ggb has joined #ocaml
lane has joined #ocaml
whereiseveryone has joined #ocaml
pmk has joined #ocaml
patrick_ has joined #ocaml
philipwhite has joined #ocaml
jmcantrell has joined #ocaml
_alix has joined #ocaml
ymherklotz has joined #ocaml
immutable has joined #ocaml
xvilka has joined #ocaml
henrytill has joined #ocaml
rustyne has joined #ocaml
sleepydog has joined #ocaml
Ankhers has joined #ocaml
b0o has joined #ocaml
seeg has joined #ocaml
kuruczgy has joined #ocaml
richardhuxton has joined #ocaml
ursa-major has joined #ocaml
brettgilio has joined #ocaml
pluviaq has joined #ocaml
arya_elfren has joined #ocaml
soni_ has joined #ocaml
waleee has quit [Ping timeout: 264 seconds]
Inline has quit [Remote host closed the connection]
Inline has joined #ocaml
Inline has quit [Client Quit]
toastal has joined #ocaml
jabuxas has joined #ocaml
toastal has quit [Quit: Gateway shutdown]
Inline has joined #ocaml
toastal has joined #ocaml
toastal has quit [Client Quit]
<discocaml>
<otini_> What about Digest?
<discocaml>
<otini_> ah, never mind, it is specifically designed to hash byte sequences
<companion_cube>
Digest doesn't even specify the algorithm
<companion_cube>
it was md5 for a long time
<discocaml>
<otini_> this has been improved in 5.2
<companion_cube>
and also it was slow, ugly, and non compositional :p (one of my most disliked moduels tbh)
<companion_cube>
yeah but you only get a crypto hash with a poor interface
cr1901_ has joined #ocaml
<discocaml>
<otini_> that doesn’t particularly shock me, I expect cryptographic hashes to be computed on stable (or at least versioned) binary representations, which is not doable with polymorphic functions neither default hashing functions
<discocaml>
<otini_> I agree that we lack default functions for non-cryptographic hashing
cr1901 has quit [Ping timeout: 264 seconds]
<companion_cube>
we most defiitely do
<companion_cube>
if you want a nice crypto hashing library, just look at cryptokit
<companion_cube>
it's 100x better than Digest
<companion_cube>
(and serves different purposes)
<hannes>
..or take a look at digestif..
<companion_cube>
no offense but isn't it sth that allocates lots of cstructs?
<companion_cube>
(I last looked years ago, I could be way off tracks)
<companion_cube>
but it returns a new ctx every time
<hannes>
if you use digest_*, no. it really depends on which function you use. but well, I won't discuss the API differences in detail.
<companion_cube>
I guess my needs are that I hash complex stuff, so one shot functions are not enough and I focus on feed_*
<companion_cube>
for which cryptokit is better since it mutates in place
Inline has quit [Remote host closed the connection]
Inline has joined #ocaml
<discocaml>
<dinosaure> For experience, the mutation can be really dangerous and even more with parallelism
<discocaml>
<dinosaure> When it's aboit cryptographic stuff, and again we talk about a ctx which is probably allocated into the minor heap
Anarchos has joined #ocaml
<Anarchos>
ARe patches welcome to enable native compilation for a specific platform on the 4.14 branch ?
<companion_cube>
4.14, I kind of doubt it :D
<Anarchos>
i miss my native compiler on HaikuOS, i have to pin a local repo with native compilation/dynlink enable. The testsuite runs fine, excpet for 2 tests.
<discocaml>
<froyo> I remember back in the days of 4.11/4.12 someone posted a bounty to bring Plan9's OCaml compiler up to date
<Anarchos>
companion_cube without native compilation, i can't compile coq
<discocaml>
<otini_> we really need for Coq to compile with ocaml 5
<companion_cube>
Coq doesn't work on OCaml 5 ? :/
<discocaml>
<otini_> i’ve heard it doesn’t
<Anarchos>
i have some other opam packages that are not ported to ocaml5 so i have to stick to LTS version
<discocaml>
<otini_> I’d be very interested to know which packages that is, anything that compiles on 4.14 and not 5.x is a bug
<discocaml>
<otini_> except for some minor breaking changes that should be easy to fix
<Anarchos>
otini_ i must try on trunk or another branch ?
<discocaml>
<otini_> no, you should try with a released version
<discocaml>
<otini_> the latest one being 5.2.0
<discocaml>
<otini_> many packages are broken on trunk
<Anarchos>
ok. Will try tonight
<Anarchos>
companion_cube i am still working on my math verifier
<discocaml>
<otini_> Anarchos thanks
<companion_cube>
Anarchos: you could use a less esoteric OS
<Anarchos>
companion_cube that's my choice :)
<companion_cube>
yeah but you inflict a lot of pain on yourself
jabuxas has quit [Ping timeout: 268 seconds]
<Anarchos>
companion_cube my goal is also to attract people to Haiku.
Anarchos has quit [Quit: time to go home from work]
<companion_cube>
😂
<companion_cube>
oh no
hannes has quit [Quit: leaving]
<discocaml>
<octachron> @otini_ , Coq works with OCaml 5.2; but with one feature (native-compute) disabled. In the case of Coq, the issue is that part of Coq were written by people *very* familiar with the OCaml runtime and some of the tricks used were no longer valid in OCaml 5.
<discocaml>
<drupyog> You say "very familiar", I hear "blazingly imprudent"
<discocaml>
<otini_> How important is native-compute?
<discocaml>
<drupyog> You say "very familiar", I hear "blazingly imprudent" 😄
<discocaml>
<otini_> (thanks for the correction)
<discocaml>
<._null._> It's used by a handful of people to do computations very fast (there is already a VM to do computations fast, but that was not fast enough for some)
<discocaml>
<otini_> put this way, it doesn’t seem very important
<discocaml>
<._null._> It's very important to few people
<companion_cube>
are people not worried that lean is going to completely shadow Coq?
<discocaml>
<._null._> Coq still has quite a few things going for it
<discocaml>
<._null._> From my point of view, Lean only has mathlib and hype
<companion_cube>
single unified langauge and meta language? easy to install? direct native evaluation?
<companion_cube>
I think Coq's existing user base will stick with it
<companion_cube>
but most new users will go to lean
<discocaml>
<._null._> I'm obviously biased because I use opam regularly, but with Coq Platform I thought Coq became fine to install.
<discocaml>
<._null._> Not sure what you mean with direct native evaluation; Coq has fast evaluation (in a VM or natively) and can extract code to other languages
<discocaml>
<._null._> Lean is generally slower than Coq, or so I hear
<companion_cube>
not what I heard tbh
<companion_cube>
Lean compiles most code (including tactics you write) to C++
<discocaml>
<otini_> @._null._ I’d be interested to contact (some of) these people, in the compiler team at Tarides we do want to help transition to ocaml 5 (although I can’t guarantee that the ocaml maintainers will bend over backwards to support runtime hacks)
Inline has quit [Remote host closed the connection]
Inline has joined #ocaml
<companion_cube>
yeah, lean3
<companion_cube>
now it's lean4
<companion_cube>
explicitly designed for speed :s
<discocaml>
<._null._> Hence why I said I didn't find anything
<discocaml>
<otini_> Thanks!
<discocaml>
<._null._> Ok, I was unclear but I meant I found no conclusive results
<companion_cube>
I don't know if native compute is faster or slower than lean4
<companion_cube>
but what I do know is that a ltac tactic will be slower than a lean4 tactic, all things being equal
<companion_cube>
(and writing tactics in OCaml is not going to be commonplace)
<discocaml>
<._null._> Writing tactics in Ltac is already not commonplace
<companion_cube>
isn't the basic tactic language, ltac?
<companion_cube>
or do you mean that mtac or whatever is now the new default?
<discocaml>
<._null._> Yes, but one rarely defines tactics. You usually only use the default tactics. Did you mean that proofs were also compiled to C++ ?
<companion_cube>
well in lean4 you can write tactics as easily as you write functions
<companion_cube>
that's going to make a big difference imho
<discocaml>
<._null._> It's still functions on an AST, not that easy
<companion_cube>
even tacticals that compose 12 other tactics will be natively compiled
mbuf has quit [Quit: Leaving]
<discocaml>
<._null._> I can't think of any complex tactic that is implemented in ltac, solvers like lia use OCaml iirc
<companion_cube>
… yeah
<companion_cube>
so you're more or less stuck with the builtin ones
<companion_cube>
but in lean you can make your own tactic, and it's installable like any other package
<companion_cube>
and it'll be competitive with OCaml
<discocaml>
<._null._> I don't see how writing a non-trivial tactic becomes easy enough that going to OCaml is a formality
<discocaml>
<._null._> is not*
<discocaml>
<._null._> I may just be bad at conceiving useful tactics
<companion_cube>
going to OCaml means you have to learn OCaml and the Coq internal API
<companion_cube>
(and how to compile the tactic, I guess, oof)
<discocaml>
<._null._> That's how hard I take tactic writing to be
<companion_cube>
that's on top of writing the actual tactic
<discocaml>
<._null._> indeed
<companion_cube>
oh good, they ended up using an actual hash function
<companion_cube>
but a tactic to normalize sth in a monoid by leverage associativity, say, shouldn't be that hard to write
<companion_cube>
leveraging*
<discocaml>
<._null._> It also already exists
<companion_cube>
I'm taking that as an easy example
<companion_cube>
imagine it didn't
<companion_cube>
and you had to write it in OCaml
<discocaml>
<._null._> It's also simple enough that ltac shouldn't slow it down
<companion_cube>
hmm idk :)
<companion_cube>
but wait a few years and you'll see what the lean people are working on, directly in lean4, and see how it fares compared to decades of Coq
jabuxas has joined #ocaml
Serpent7776 has quit [Ping timeout: 240 seconds]
<bartholin>
what about Ltac2 (by Pierre-Marie Pédrot)?
<discocaml>
<._null._> I'm pretty sure its purpose is to be a better language (typed), not to be faster
<discocaml>
<Kali> and ltac2 is only dynamically typed, not statically, in order to preserve backwards compatibility with ltac
<discocaml>
<Kali> wait, no, i mixed that up
<discocaml>
<Kali> > Ltac2 provides the standard type constructions from ML, namely prenex polymorphism and the ability to define algebraic datatypes. This is already a great step forward compared to Ltac1, that merely has a second-class support for a handful of data structures like lists, and, to add insult to injury, is dynamically typed.
<discocaml>
<Kali> >
<discocaml>
<Kali> > Contrarily to languages like Mtac2, the type system of Ltac2 does not enforce much, and many sanity checks are performed at runtime. This is imposed by the backward compatibility constraint
waleee has joined #ocaml
Anarchos has joined #ocaml
<Anarchos>
which switch should i use '5.2.0' or '5.2.0+options' ?
<discocaml>
<shiny_dev> hello
<discocaml>
<shiny_dev> @bluddy5
<discocaml>
<shiny_dev> nice to meet you
<discocaml>
<shiny_dev> is there any opportunity to work with you?
<companion_cube>
🤔
<companion_cube>
Anarchos: it pains me to see you spend so much time on things that are trivially solved on any mainstream OS
<companion_cube>
pushing more people to Haiku will never ever work, realistically
<discocaml>
<froyo> companion_cube: here's your "no fun allowed" picket, you dropped it
<discocaml>
<froyo> :P
<companion_cube>
I mean if it's fun to struggle installing OCaml, then installing Coq, for months and years on end, then sure :p
Tuplanolla has joined #ocaml
<discocaml>
<froyo> there's a sizeable chunk of people who enjoy a little pain every now and then
Serpent7776 has joined #ocaml
<Armael>
I mean, we're all ocaml users here, so...
<companion_cube>
idk, I can't take this level of pain personally :D
<discocaml>
<froyo> Armael: heresy!
<Anarchos>
companion_cube i do'nt know if you saw it, but is
<Anarchos>
but i successfully installed compcert
<companion_cube>
thought you couldn't install coq? :o
hannes has joined #ocaml
<Anarchos>
companion_cube i could but i had to reenable 'native/natdynlink'
<Anarchos>
is there a mean to reinstall the same list of packages on another switch with opam ?
<discocaml>
<._null._> `opam switch export` then `opam switch import`
<Anarchos>
._null_. thanks
<octachron>
Anarchos, I generally don't have the time to mention it; but you are aware that you propose your patches for supporting Haiku to the compiler, aren't you?
<Anarchos>
octachron yes, i already got some patches included in the past
<octachron>
If they are not intrusive for other OSs they will be accepted with little difficulties; but they are no plans by maintainers to increase the list of officially supported OS
<Anarchos>
octachron that seems fine.
Serpent7776 has quit [Ping timeout: 268 seconds]
Anarchos has quit [Quit: Vision[]: i've been blurred!]
jabuxas has quit [Ping timeout: 268 seconds]
<discocaml>
<otini_> > <Anarchos> which switch should i use '5.2.0' or '5.2.0+options' ?
<discocaml>
<otini_> 5.2.0 unless you want a special non-default config (frame pointer support, flambda, …)
Anarchos has joined #ocaml
<Anarchos>
how to create an opam switch with the ocaml compiler coming from a local directory with its sources ?
bartholin has quit [Quit: Leaving]
Anarchos has quit [Quit: Vision[]: i've been blurred!]
<discocaml>
<._null._> If you `opam pin` that repository, it should see all packages and when you ask install it from there