zebrag has quit [Remote host closed the connection]
zebrag has joined #ocaml
waleee has quit [Ping timeout: 240 seconds]
waleee has joined #ocaml
zebrag has quit [Remote host closed the connection]
zebrag has joined #ocaml
minimario has quit [Quit: Client closed]
noddy has joined #ocaml
Geekingfrog has quit [Ping timeout: 250 seconds]
Geekingfrog has joined #ocaml
vb has quit [Ping timeout: 252 seconds]
vb has joined #ocaml
hendursaga has quit [Remote host closed the connection]
hendursaga has joined #ocaml
waleee has quit [Ping timeout: 252 seconds]
sagax has quit [Excess Flood]
zebrag has quit [Quit: Konversation terminated!]
mbuf has joined #ocaml
gravicappa has joined #ocaml
Drup has quit [*.net *.split]
Drup has joined #ocaml
favonia has quit [Ping timeout: 250 seconds]
favonia has joined #ocaml
mbuf has quit [Quit: Leaving]
xd1le has joined #ocaml
elf_fortrez has joined #ocaml
Haudegen has joined #ocaml
rwmjones_ is now known as rwmjones
elf_fortrez has quit [Quit: Client closed]
chrisz has joined #ocaml
favonia has quit [Ping timeout: 240 seconds]
mro has joined #ocaml
hendursa1 has joined #ocaml
mbuf has joined #ocaml
hendursaga has quit [Ping timeout: 276 seconds]
bartholin has joined #ocaml
olle has joined #ocaml
mro has quit [Remote host closed the connection]
mro has joined #ocaml
Guest59 has joined #ocaml
Guest59 has quit [Client Quit]
Guest24 has joined #ocaml
adrien_ is now known as adrien
<d_bot>
<Ulugbek> Hi. I have a compiler-related question: what is `Parsetree.location_stack` used for? what does it represent?
Guest24 has quit [Quit: Client closed]
hackinghorn has joined #ocaml
hornhack has joined #ocaml
hackinghorn has quit [Ping timeout: 252 seconds]
mro has quit [Remote host closed the connection]
Guest47 has joined #ocaml
Guest47 has quit [Client Quit]
mro has joined #ocaml
<d_bot>
<octachron> It is used to keep track of a history of locations for fragments of the ast that have been moved around: https://github.com/ocaml/ocaml/pull/1960
Haudegen has quit [Quit: Bin weg.]
mro has quit [Remote host closed the connection]
mro has joined #ocaml
mro has quit [Quit: Leaving...]
favonia has joined #ocaml
krnkktz has quit [Quit: Bridge terminating on SIGTERM]
mewfree[m] has quit [Quit: Bridge terminating on SIGTERM]
smondet[m] has quit [Quit: Bridge terminating on SIGTERM]
Tardigreat[m] has quit [Quit: Bridge terminating on SIGTERM]
marinelli[m] has quit [Quit: Bridge terminating on SIGTERM]
fluxm has quit [Quit: Bridge terminating on SIGTERM]
mclovin has quit [Quit: Bridge terminating on SIGTERM]
schube[m] has quit [Quit: Bridge terminating on SIGTERM]
<mclovin>
you should switch to @v2 and it'll fix it
<mclovin>
if you're talking about the `depext not found` error
neiluj has quit [Quit: Leaving]
<d_bot>
<RegularSpatula> I'm using v2...it's not really any specific errors. It's just libraries randomly won't compile, but it will be different ones each time it fails (..it doesn't always fail either). This happens across multiple projects as well.
<d_bot>
<RegularSpatula> I can generally rerun a failing job and it will be fine, but it is weird
elf_fortrez has quit [Ping timeout: 256 seconds]
favonia has quit [Remote host closed the connection]
elf_fortrez has joined #ocaml
<companion_cube>
olle: that's a hilariously bad take
<companion_cube>
rust, bad ergonomics? try C++
<companion_cube>
(or C)
<Fardale>
@RegularSpatula did you try to do sequential compilation ie setting the limit of parallel job at 1 for opam and dune?
<d_bot>
<RegularSpatula> I haven't, no, but I will try it...thanks for the suggestion
<olle>
companion_cube: compared to any GC lang
<olle>
Hm, C vs Rust in lang ergonomics.
<companion_cube>
adding linear types to a GC language will bring you the same kind of (non-)ergonomics
<companion_cube>
just look at Mezzo :p
<Tardigreat[m]>
not necessarily, with QTT it can be quite nice (which is a superset of linear types in a way)
<Corbin>
olle: C++ has *syntactic* ergonomic issues. `> >` vs `>>` took decades to get fixed, and I'm not sure if it's really fixed or not.
<companion_cube>
QTT?
<Tardigreat[m]>
qunatitative type theory
<companion_cube>
C++ has all sorts of ergonomic issues, the worst of which are the mountains of footguns
<companion_cube>
Tardigreat[m]: never heard of that
<companion_cube>
is it really easier to use than rust, though?
<Tardigreat[m]>
yes
<olle>
companion_cube: Yes, guess I should have been more specific. :)
<Corbin>
companion_cube: QTT annotates terms with how they will be used; they can be affine, linear, or never used. The "quantity" is the number of uses.
<companion_cube>
Tardigreat[m]: what does a mutable borrow look like?
<olle>
companion_cube: Is Mezzo opt-in linear types?
<Corbin>
Idris' implementation is interesting because they try to ensure that proofs are never used, and their implementation removes everything which is never used.
<companion_cube>
it's also a research language tht is not maintained.
<Tardigreat[m]>
companion_cube: it doesn't really need a notion of a "mutable borrow". that's a rust concept that comes from how it represents things. you can use QTT to build a type theory that has that notion, but the most notable implementation is as Corbin said in idris
<Corbin>
Or I guess that proofs are linear? And then the consumed proof is like a unit type whose values are never used. I freely admit that I don't grok Idris 2 very well.
<Tardigreat[m]>
which is just your regular dependent types
<Tardigreat[m]>
+ QTT i guess
<Tardigreat[m]>
plus QTT, rather. damn matrix
<companion_cube>
I mean, how do you write the *equivalent* of a mutable borrow
<companion_cube>
afaik, with true linear types, you have to give the value, and get it back in a tuple when the borrow ends
<Tardigreat[m]>
Corbin: the goal of it in idris 2 is to reason about what exists at runtime vs what doesn't AFAIK
<companion_cube>
no offense but I also doubt Idris2 is more ergonomic than rust :D
<olle>
companion_cube: linear --> must use once, right? but there's the entire affine cube thingy
<Tardigreat[m]>
companion_cube: it really depends on the type theory. in dependent types you could just require a proof of equality of terms at a type level
<companion_cube>
> just
<Tardigreat[m]>
in other type theories, you could have something like a rust borrow checker
<companion_cube>
I'm not very convinced :)
<Corbin>
Tardigreat[m]: Yeah. In general, we want "proofs" in the Coq/Agda sense to be erased at runtime, because they don't do anything after extraction. And QTT for Idris 2 lets the implementation make a guarantee along those lines.
<Tardigreat[m]>
i don't know why you're so insistent on comparing languages instead of the underlying ideas in the type theory (in this case, a type theory based on linear logic vs QTT)
<Tardigreat[m]>
the implementation of a language in this case is irrelevant. different languages can use the same idea differently
<companion_cube>
rust is based on affine types
<companion_cube>
I thought we were discussing ergonomics, Tardigreat[m].
<companion_cube>
which pretty much requires talking about concrete instances of the theory
<companion_cube>
it's like dependent types, they're super cool, but notoriously hard to use
<Tardigreat[m]>
and i took issue with "adding linear types to a GC language will bring you the same kind of (non-)ergonomics", which is just not true
<Tardigreat[m]>
you can make it ergonomic
<Corbin>
Yeah. So the apples-to-apples comparison might be Rust's mutable borrows vs. Idris' state monad and linear types.
<companion_cube>
I'd like a constructive proof of that Tardigreat[m].
<companion_cube>
"you can make it ergonomic" is the part I doubt
<olle>
F* is a good example of an ergonmic language, I'd say.
<Tardigreat[m]>
companion_cube: it will depend on the language, but idris2's QTT is pretty easy to use. you might not like it, but you can write meaningful programs and proofs in it
<companion_cube>
:D compared to rust? really?
<olle>
Maybe because it's opt-in?
<Tardigreat[m]>
i'd argue that ocaml is largely unergonomic in many ways, but people might disagree with me
<Tardigreat[m]>
if you're arguing taste, that will always be personal preference
<companion_cube>
I'd agree on some aspects, yes
<Corbin>
companion_cube: I personally don't like it, but https://concatenative.org/wiki/view/Popr is relatively ergonomic for a concatenative language, and its type system corresponds to a linear logic.
<companion_cube>
OCaml lacks a good deriving infrastructure for example
Haudegen has quit [Quit: Bin weg.]
<companion_cube>
> FPGA
<companion_cube>
let me guess, no dynamic allocation
<Tardigreat[m]>
it also has an incredibly hostile pattern matching syntax for functions :P
<companion_cube>
?
<companion_cube>
you mean using `match`?
<Tardigreat[m]>
let x y = function ... instead of just being able to match on every argument
<companion_cube>
let f x y z = match on all arguments
<companion_cube>
you're welcome ;)
<Corbin>
Ha, now I'm wondering whether there's FPGA designs which can dynamically reallocate gates as RAM.
<companion_cube>
I personally like this better
<companion_cube>
I know the function is defined in one place
<Tardigreat[m]>
yeah, you can do it with match, but i'd argue it's awful that a functional language doesn't let me match like haskell, isabelle, or even SML do. it's personal preference
<Tardigreat[m]>
which is kind of my point, the whole notion of "ergonomics" will be preference, so i find blanket statements that you can't add "ergonomic" linear types to a GC'd language to be a bit too tied to personal preference to say as a fact
<olle>
Ergonomics might be possible to measure.
<Tardigreat[m]>
you can personally dislike the way idris2 does it (and hell, i dislike some things too), but it doesn't mean that it can't be done in a nice way
<olle>
GC is probably more ergonomic than manual mem, for example. Because you abstract away a huge concern.
<companion_cube>
Tardigreat[m]: I think the toplevel matching is a matter of taste
<companion_cube>
I agree with olle
<companion_cube>
I'm quite familiar with rust; maybe Idris2 is more convenient, but I don't think you can just draft it as personal preference.
mbuf has quit [Quit: Leaving]
mro has joined #ocaml
<companion_cube>
and I'd still like to see how you do stuff where rust does borrowing
<companion_cube>
(with code samples)
<olle>
companion_cube: Clean? Uniqueness?
<olle>
Problem is that Rust kind of forces you to be optimal.
<companion_cube>
you can use .clone() if you want, so, not really
<companion_cube>
it does nudge you towards speed, though, yes
<Tardigreat[m]>
it highly depends on the context. it's also a bit of an ambiguous question because rust doesn't actually do borrowing, it does glorified scope-checking. if i try to write a rust program which has an interface where it creates something and i want to be able to immutably give it out to things that ask for it, rust's borrow checker will yell at me because it's really just checking for the context of the stack rather than doing any real
<Tardigreat[m]>
"borrow checking"
<companion_cube>
the borrows are lexically scoped, yes
<olle>
companion_cube: clone or Rc or Arc.
mro has quit [Remote host closed the connection]
<companion_cube>
Tardigreat[m]: I think the real ergonomic solution would be a sort of gradual linear typing :p
<companion_cube>
sth like Perceus on the runtime (which does linear checks dynamically)
<companion_cube>
and a type system on top that can be used to remove parts of these runtime linear checks
<Tardigreat[m]>
i agree that gradually adding things on demand is pretty useful, but is there any reason you think it should be linear instead of just quantified with any number of uses?
<companion_cube>
number of uses seems harder, no?
<Tardigreat[m]>
well, it's probably harder to tie into an optimization pipeline, but i'm not sure it's much harder to implement if you just follow the typing rules of QTT
<companion_cube>
Corbin: a language using only home row is therefore better :p
<Tardigreat[m]>
companion_cube: the paper that it links to explains the rationale, but it's just any natural number. the reason it's distinguishing between 0 and 1 is because 0 is just your typical intuitionistic variables and 1 is linear
<Corbin>
companion_cube: I'm being serious, FWIW; I nearly had to quit this line of work because of tendonitis in the forearms. And this was *after* a childhood of tennis, piano, and bodybuilding; I had all the advantages and still was extremely injured.
<olle>
Corbin: RSI?
<Tardigreat[m]>
Corbin: emacs pinky is very much a real thing i'd say. that's why i always press ctrl with my palm :P
<companion_cube>
Tardigreat[m]: but can you write `(2 int)` in idris?
<companion_cube>
Corbin: yeah emacs is known for that I heard
<olle>
Oh
<olle>
I think one important part of ergonomics is, how many things do I have to keep in my head at once when coding?
<olle>
GC removes one of those things.
<Corbin>
companion_cube: I've always used vim. In my case, I literally wrote too much code at Google. They gave me a couple weeks off, and I got to sit on my couch and do nothing, because doing anything with my arms hurt. I'm very lucky to not have carpal-tunnel damage.
<Tardigreat[m]>
companion_cube: i don't think i've seen it used before, but you should be able to (i think?)
<Tardigreat[m]>
i'd have to try it
<companion_cube>
the page linked seems to say no
<companion_cube>
but maybe it's not up to date
<Corbin>
olle: In general, when you hear me say "ergonomics" without talking about specific injuries, I mean Kolmogorov complexity: Programming languages shouldn't make me repeat myself, shouldn't have so much ceremony and decoration, etc.
<companion_cube>
and like always it's a tradeoff
elf_fortrez has quit [Ping timeout: 256 seconds]
<Tardigreat[m]>
companion_cube: i don't remember with certainty, but when i read the original QTT paper i didn't see any typing rules that would stop you from doing that. maybe it's an idris thing
<olle>
Corbin: Interesting.
<d_bot>
<darrenldl> Corbin: i'm curious actually - i had a very painful pinky when using vanilla emacs a long while ago, do you do anything to help hand recover/prevent damage in general?
<olle>
companion_cube: Yes, I was about to say.
<olle>
You're ergonomic in a certain domain.
<Corbin>
companion_cube: Dunno if you've seen it, but https://typeclasses.com/ghc/lambda-case is an interesting Haskell extension for making pattern-matching syntax smaller. Scheme has match-lambda using the common pattern-matching extension.
<companion_cube>
and caml-light had `fun` with multiple patterns
<companion_cube>
I think there's a lot of small syntactic papercuts in OCaml, like that
<companion_cube>
but it's really not the worst problem ever
<Tardigreat[m]>
Corbin: re writing too much code and arms hurting: that must have been awful, good god
<companion_cube>
not having deriving makes me around 10,000x more mad
glassofethanol has joined #ocaml
<olle>
Another example: Typed effects vs monads everywhere.
<olle>
One is more ergonomic ;)
<companion_cube>
probably :p
<Corbin>
darrenldl: I do so many stretches. The two best ones start by extending the arms out, and untwisting the forearm bones. Then the active stretch is to have one hand gently pull back the fingers of the other hand, hyperextending the wrist **gently**.
<Corbin>
The other one is isometric, the "pianist's stretch": gently open both hands. Like, open them. And then spread the fingers as much as possible. Imagine a pianist trying to increase the distance from their pinky to their thumb.
<Corbin>
Tardigreat[m]: I used to be all hustle. Like, "ooh look, I can write 500loc of Python every day" swagger. And y'know what, it's all bogus. Take care of yourself first.
<olle>
companion_cube: F* vs Coq, in terms of being ergonomic, for sure.
<olle>
If that's fair to compare
<companion_cube>
vs Coq? ah
<companion_cube>
I thought you meant vs rust :p
<olle>
I did, at first. Not so sure now xD
<Tardigreat[m]>
Corbin: that's a very good point
<olle>
Buuut, that's why it would be so interesting to see more alternatives like Rust, because it's only the first experiment.
<olle>
C# with the span stuff
<olle>
Clean with uniqueness
<companion_cube>
there's a new language from microsoft
<companion_cube>
Verona I think
<olle>
They make lots of langs, no?
<companion_cube>
sure, some are even used in practice
<olle>
:O
<companion_cube>
have you heard of typescript? :p
<olle>
Hehe
<olle>
Fraid so
<d_bot>
<darrenldl> Corbin: cheers~
kakadu has quit [Quit: Konversation terminated!]
<olle>
And that's why I think Rust is in no way the end-goal of ergonomic manual mem
cedric has joined #ocaml
<companion_cube>
no, but it's the best we have in 2021
<olle>
Personally I preferred version 0.4, but sure ;)
<olle>
Or just pre-1.0
<Corbin>
Tooling helps a lot. Rust's compiler error messages often suggest what I did wrong along with a reasonable suggestion for how to fix it. It's just like when I learned C++, but with fewer search-engine queries for inscrutable error codes.
<olle>
True, true
<olle>
Facebook did great job with that, for Hack
<companion_cube>
also with a less bizarre semantics than C++
<olle>
I'm using ~ and @ in my hobby project. That's the level of my disappointment.
<olle>
For stack and regional allocation.
<companion_cube>
-_-
<companion_cube>
I mean
<companion_cube>
yeah, old rust was nothing like current rust
<companion_cube>
it was more like what Go should have been :°
<olle>
hehe
<olle>
companion_cube: Do you contribute to Rust?
<companion_cube>
to the compiler? ahah no
<companion_cube>
although that'd be cool
<olle>
Well, it was written in OCaml first :)
<companion_cube>
a long time ago
<olle>
Yep
Haudegen has joined #ocaml
<d_bot>
<froyo> olle: What's DHT?
<d_bot>
<froyo> the hormone that makes guys bald
<olle>
Right
olle has quit [Ping timeout: 244 seconds]
elf_fortrez has joined #ocaml
<d_bot>
<darrenldl> hm, the tcp udp mentioning makes me want to finally draft up a error corrected udp lib
glassofethanol has quit [Ping timeout: 244 seconds]
Guest49 has joined #ocaml
<Guest49>
hi
<Guest49>
I'm trying to install coq, but opam is giving me some linking errors when building ocamlfind
Corbin has quit [Ping timeout: 244 seconds]
<Guest49>
"relocation R_X86_64_32S against `.rodata' can not be used when making a PIE object; recompile with -fPIE"
<Guest49>
anyone know of a solution
<Guest49>
?
glassofethanol has joined #ocaml
<companion_cube>
if you use the system switch, don't
<Guest49>
I didnt
<Guest49>
I'm on 4.07.0
<companion_cube>
make sure you eval `opam env`
<companion_cube>
and maybe reinstall ocamlfind?
<Guest49>
How would I reinstall it?
<companion_cube>
opam reinstall ocamlfind
<companion_cube>
probably :p
<Guest49>
same error
<companion_cube>
can you start ocaml on the command line?
<companion_cube>
is it 4.07?
<companion_cube>
can you use it to compile a trivial program with ocamlopt?
<Guest49>
linker error when compiling the hello world example
<Guest49>
same as before
<Guest49>
should I try 4.08.1 instead?
<octachron>
You may also want to try a more recent version of OCaml (4.12.0) to avoid possible gcc/clang issues
<companion_cube>
oh shit, gcc 10
<Guest49>
octachron: ok
glassofethanol has quit [Quit: leaving]
<Guest49>
Well it got past ocamlfind now, thanks companion_cube and octachron, really appreciate it.
motherfsck has quit [Quit: quit]
elf_fortrez has quit [Ping timeout: 256 seconds]
hackinghorn has joined #ocaml
hornhack has quit [Ping timeout: 252 seconds]
mmalter has joined #ocaml
mro has joined #ocaml
jess has joined #ocaml
motherfsck has joined #ocaml
cedric has quit [Quit: Konversation terminated!]
Guest49 has quit [Quit: Client closed]
hackinghorn has quit [Quit: Leaving]
olle has joined #ocaml
mro has quit [Ping timeout: 252 seconds]
gravicappa has quit [Ping timeout: 244 seconds]
<d_bot>
<Pokegali> Hi, hum, I'm having trouble installing disml.. It's telling me that it has to downgrade ocaml from 4.12.0 to 4.07.1, however the install fails while compiling ocaml-base-compiler.4.07.1 (make world returns an error). Is there anything I can do ?
<Anarchos>
Pokegali what is the error message of «make world» ?
<d_bot>
<Pokegali> I think it's here : /data/data/com.termux/files/usr/bin/ld: backtrace.pic.o:/data/data/com.termux/files/home/.opam/default/.opam-switch/build/ocaml-base-compiler.4.07.1/byterun/backtrace.c:31: multiple definition of `caml_debug_info'; backtrace_prim.pic.o:/data/data/com.termux/files/home/.opam/default/.opam-switch/build/ocaml-base-compiler.4.07.1/byterun/backtrace_prim.c:47: first defined here
<d_bot>
<Pokegali> And then the next lines are linker failed with error code 1, (make) error 1, (make) error 2
<Anarchos>
Pokegali no idea, sorry
<d_bot>
<Et7f3> Ah their was a patch for 4.08.1 it don't seem to be packported to earlier version
<d_bot>
<Pokegali> So there's no way to install it ?
<d_bot>
<Pokegali> Oh, I have a better one, when I run opam install disml with a fresh install of opam, on my raspberry : "Sorry, no solution found: there seems to be a problem with your request. No solution found, exiting"
olle has quit [Ping timeout: 252 seconds]
infinity0 has quit [Remote host closed the connection]
infinity0 has joined #ocaml
Anarchos has quit [Quit: Vision[0.10.3]: i've been blurred!]
Haudegen has quit [Ping timeout: 252 seconds]
Tuplanolla has quit [Quit: Leaving.]
<d_bot>
<EduardoRFS> I put my gcc hack at /usr/local/bin/gcc