Nahra``` has quit [Read error: Connection reset by peer]
Nahra``` has joined #ocaml
yomimono has joined #ocaml
madroach has quit [Ping timeout: 246 seconds]
l1x has quit [Read error: Connection reset by peer]
madroach has joined #ocaml
l1x has joined #ocaml
Major_Biscuit has quit [Quit: WeeChat 1.3]
mcint has joined #ocaml
mankyKitty has quit [Ping timeout: 240 seconds]
chambart has quit [Ping timeout: 265 seconds]
oskarth has quit [Ping timeout: 250 seconds]
lopex has quit [Ping timeout: 240 seconds]
mankyKitty has joined #ocaml
oskarth has joined #ocaml
sspi has quit [Ping timeout: 256 seconds]
lopex has joined #ocaml
msch has quit [Ping timeout: 256 seconds]
msch has joined #ocaml
sspi has joined #ocaml
FreeBirdLjj has joined #ocaml
JacobEdelman has quit [Quit: Connection closed for inactivity]
mcint has quit [Quit: hibernating...]
mcmillhj_ has quit [Quit: Lost terminal]
mcmillhj_ has joined #ocaml
igoroliveira has quit [Quit: Connection closed for inactivity]
ldopa has quit [Ping timeout: 256 seconds]
FreeBirdLjj has quit [Remote host closed the connection]
FreeBirdLjj has joined #ocaml
psy_ has quit [Ping timeout: 240 seconds]
hay207 has joined #ocaml
yomimono has quit [Ping timeout: 246 seconds]
nullcatxxx_ has joined #ocaml
FreeBirdLjj has quit [Remote host closed the connection]
FreeBird_ has joined #ocaml
_whitelogger has joined #ocaml
JacobEdelman has joined #ocaml
badon has joined #ocaml
ygrek has quit [Ping timeout: 260 seconds]
hay207 has quit [Ping timeout: 256 seconds]
hay207 has joined #ocaml
mac10688 has quit [Ping timeout: 272 seconds]
hay207 has quit [Ping timeout: 246 seconds]
hay207_ has joined #ocaml
BitPuffin|osx has quit [Ping timeout: 240 seconds]
contempt has quit [Ping timeout: 255 seconds]
infinity0 has quit [Ping timeout: 272 seconds]
cody` has quit [Quit: Connection closed for inactivity]
infinity0 has joined #ocaml
Mercuria1Alchemi has joined #ocaml
ncthom91 has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
contempt has joined #ocaml
Mercuria1Alchemi has quit [Ping timeout: 255 seconds]
JacobEdelman has quit [Quit: Connection closed for inactivity]
pierpa has quit [Ping timeout: 240 seconds]
strmpnk has quit [Ping timeout: 240 seconds]
strmpnk has joined #ocaml
darkf has joined #ocaml
palomer has quit [Quit: palomer]
palomer has joined #ocaml
ygrek has joined #ocaml
govg has quit [Ping timeout: 255 seconds]
govg has joined #ocaml
Sorella has quit [Quit: Connection closed for inactivity]
contempt has quit [Remote host closed the connection]
cc_evo has joined #ocaml
damason has quit [Ping timeout: 240 seconds]
cross has quit [Quit: Lost terminal]
sbrouf has joined #ocaml
ia0 has quit [Quit: leaving]
ia0 has joined #ocaml
Haudegen has quit [Ping timeout: 255 seconds]
cc_evo has quit [Quit: Leaving.]
sbrouf has quit [Ping timeout: 256 seconds]
johnf_ has joined #ocaml
johnf has quit [Ping timeout: 256 seconds]
sz0 has joined #ocaml
Simn has joined #ocaml
nullcatxxx_ has quit [Quit: My Mac has gone to sleep. ZZZzzz…]
ygrek has quit [Ping timeout: 240 seconds]
Haudegen has joined #ocaml
contempt has joined #ocaml
ely-se has joined #ocaml
contempt has quit [Remote host closed the connection]
wolfcore is now known as u
u is now known as wolfcore
sbrouf has joined #ocaml
wolfcore is now known as kx
kx is now known as wolfcore
jimt has quit [Ping timeout: 240 seconds]
AlexRussia has quit [Ping timeout: 256 seconds]
dch has quit [Ping timeout: 240 seconds]
l1x has quit [Ping timeout: 260 seconds]
strmpnk has quit [Ping timeout: 240 seconds]
sbrouf has quit [Ping timeout: 240 seconds]
dch has joined #ocaml
lambdahands has quit [Ping timeout: 260 seconds]
strmpnk has joined #ocaml
lambdahands has joined #ocaml
strmpnk has quit [Ping timeout: 255 seconds]
dch has quit [Ping timeout: 272 seconds]
cyraxjoe has quit [Ping timeout: 240 seconds]
lambdahands has quit [Ping timeout: 255 seconds]
dch has joined #ocaml
dch has quit [Ping timeout: 246 seconds]
Major_Biscuit has joined #ocaml
<reynir>
Is it possible to open a module but renaming a value? For example, if there's a module Foo with a type t I'd like to rename the type to as type foo
badon has quit [Ping timeout: 265 seconds]
Anarchos has joined #ocaml
dch has joined #ocaml
<flux>
I was hoping to say there's a way to rename types in signatures, but I guess it doesn't work for structs?
eikke has joined #ocaml
strmpnk has joined #ocaml
lambdahands has joined #ocaml
jonludlam has joined #ocaml
l1x has joined #ocaml
chambart has joined #ocaml
Anarchos has quit [Ping timeout: 252 seconds]
Anarchos has joined #ocaml
larhat1 has quit [Quit: Leaving.]
FreeBird_ has quit [Remote host closed the connection]
Major_Biscuit has quit [Ping timeout: 260 seconds]
_andre has joined #ocaml
jonludlam has quit [Ping timeout: 255 seconds]
sbrouf has joined #ocaml
jonludlam has joined #ocaml
dsheets_ has joined #ocaml
Sorella has joined #ocaml
contempt has joined #ocaml
octachron has joined #ocaml
contempt has quit [Disconnected by services]
contempt has joined #ocaml
contempt has quit [Ping timeout: 272 seconds]
contempt has joined #ocaml
ely-se has quit [Quit: leaving]
AlexRussia has joined #ocaml
sbrouf has quit [Ping timeout: 260 seconds]
mort___ has joined #ocaml
contempt has quit [Disconnected by services]
contempt has joined #ocaml
strmpnk has quit [Ping timeout: 265 seconds]
strmpnk has joined #ocaml
lambdahands has quit [Ping timeout: 240 seconds]
badon has joined #ocaml
jonludlam has quit [Remote host closed the connection]
strmpnk has quit [Ping timeout: 240 seconds]
l1x has quit [Ping timeout: 272 seconds]
mort___ has quit [Quit: Leaving.]
dch has quit [Ping timeout: 265 seconds]
mort___ has joined #ocaml
l1x has joined #ocaml
l1x has quit [Ping timeout: 240 seconds]
ggole has joined #ocaml
lambdahands has joined #ocaml
sz0 has quit [Quit: Connection closed for inactivity]
lambdahands has quit [Ping timeout: 260 seconds]
ely-se has joined #ocaml
zpe has joined #ocaml
fluter has quit [Ping timeout: 250 seconds]
dch has joined #ocaml
lambdahands has joined #ocaml
fluter has joined #ocaml
Algebr` has joined #ocaml
dsheets_ has quit [Ping timeout: 246 seconds]
dsheets_ has joined #ocaml
l1x has joined #ocaml
strmpnk has joined #ocaml
govg has quit [Ping timeout: 265 seconds]
Algebr has quit [Ping timeout: 246 seconds]
maikii has joined #ocaml
Simn has quit [Read error: Connection reset by peer]
dch has quit []
dch has joined #ocaml
l1x has quit []
l1x has joined #ocaml
strmpnk has quit []
strmpnk has joined #ocaml
<Anarchos>
marrant, je suis en train de réimplémenter mizar en ocaml :)
<octachron>
reimplementing a full star in ocaml sounds like a lot of work
maikii has quit [Ping timeout: 252 seconds]
<Anarchos>
octachron: the mizar system, a formal system to verify demonstrations
jimt has joined #ocaml
lambdahands has quit []
lambdahands has joined #ocaml
<zozozo>
Anarchos: what's the mathematical foundation of the mizar system ?
<Anarchos>
zozozo: first order logic, with axiom schemata.
<zozozo>
Anarchos: sequent calculus style ?
<Anarchos>
yes
<zozozo>
interesting
<zozozo>
is your reimplementation open-source ?
lambdahands_ has joined #ocaml
d0nn1e has quit [Ping timeout: 240 seconds]
<Anarchos>
zozozo: it is not finished, but it will be
<Anarchos>
the trickiest part being to code an unification algorithm to verify that a formula is an instance of an axiom schema.
<companion_cube>
will it be able to parse the mizar scripts?
<Anarchos>
companion_cube: not at all.
<Anarchos>
companion_cube: i hope to have a frontend able to deal with latex formulas.
<zozozo>
Anarchos: tricky ? is it harder than for isntance, plain robinson unification ?
<Anarchos>
i don't know robinson unification
d0nn1e has joined #ocaml
hay207_ has quit [Remote host closed the connection]
<Anarchos>
zozozo: for my code, i implement the martelli-montanari algorithm.
<companion_cube>
sounds really overkill
<zozozo>
I agree
<Anarchos>
companion_cube: it is also a good distraction to write it in ocaml since i could not find an ocaml implementation ;)
<zozozo>
Anarchos: well, unification algorithms are quite tied to the implementation of terms
<Anarchos>
zozozo: that is why i stick to simplest term : constant, variables, functions, and that's it.
<zozozo>
so, a library who exports a sufficiently adaptable one would have to use a mechanism like views, which would likely degrade performances
<zozozo>
Anarchos: yeah, but even so there are a lot of choices in how to represent variables, applications, etc..
<companion_cube>
robinson unification is like 20 lines
<companion_cube>
so it's usually simpler to rewrite it
<Anarchos>
zozozo: so what do you advise me to do ?
<zozozo>
companion_cube: meh... make that 30
<Anarchos>
companion_cube: really ?
<zozozo>
Anarchos: robinson unification
<companion_cube>
30 with occur-check, ok
<Anarchos>
so you advise me to delay the performance analysis to see if unification is one ?
<zozozo>
that seems reasonable
<companion_cube>
I think so
<zozozo>
robinson unification is already quite fast in most cases I'd say
<companion_cube>
then there is the almost-linear algo, which is still relatively simple, using a graph to delay occur-checks
<companion_cube>
I believe ocamlc uses something like this
<companion_cube>
(Robinson unification but delayed occur-check)
<Anarchos>
companion_cube: any url to copy/paste code from ?
hay207 has quit [Remote host closed the connection]
<zozozo>
Anarchos: in my example, Meta are what you call variables
<zozozo>
plus there is some code to do unification of types too, but you can ignore that
<Anarchos>
zozozo: your code is hard to read...
<zozozo>
sorry, :p
<zozozo>
basically, the idea is to keep a triple (current_subst, left_term, right_term)
<zozozo>
whenever you encounter an application, you fold over the arguments
<zozozo>
and when you encounter a variable there are two cases
<zozozo>
either the variable is bound in the current subst, in which case, you continue to try and unify with the term to which it is bound
<Anarchos>
zozozo: i will read the ocaml compiler unification module ;)
<zozozo>
or it is not bound, in which case you return the current substitution, with an additional binding
BitPuffin has joined #ocaml
<zozozo>
and there is a occurs check that ensures you do not add a binding from a variable to a term that contains this variable
badon_ has joined #ocaml
badon has quit [Disconnected by services]
badon_ is now known as badon
jonludlam has joined #ocaml
zpe has quit [Remote host closed the connection]
zpe has joined #ocaml
AlexRussia has quit [Quit: WeeChat 1.4-dev]
zpe has quit [Ping timeout: 260 seconds]
AlexRussia has joined #ocaml
igoroliveira has joined #ocaml
johnf_ has quit [Read error: Connection reset by peer]
ely-se has quit [Quit: leaving]
johnf_ has joined #ocaml
Major_Biscuit has joined #ocaml
kaustuv has joined #ocaml
<kaustuv>
Will flambda break (code that uses) Obj? I'm thinking of the hacks that make List.map tail-recursive or Deque.t covariant...
<companion_cube>
it might, yes, I think
<companion_cube>
especially code that pretends something is immutable but changes it nevertheless
<def`>
yes, you might get out have that by defining a mutable list, and coercing it to non-mutable once
<def`>
but mutating immutable breaks invariants assumed by flambda
<Drup>
kaustuv: "I you use Obj.magic, I *will* break your code" -- Pierre Chambart, 2014
<Drup>
(from a talk)
<Drup>
:3
* ggole
wonders if that is anything more interesting that forwarding
<edwin>
maybe there should be a compiler warning when you use Obj.magic
<def`>
:D
<def`>
"deprecated: Obj.magic never existed"
<companion_cube>
heh
<Drup>
I think someone wanted [@unsafe] similar to [@deprecated]
<ggole>
Rust envy!
<flux>
next up.. [@throws ] specifiers ;-)
<edwin>
can menhir generate code without Obj.magic though?
<kaustuv>
So... is there a [@noinline]?
<Drup>
one of the two backend, I think ?
<Drup>
kaustuv: it's not called like that, but yes
<companion_cube>
[@yolo]
<def`>
edwin: it doesn't use Obj.magic for mutation, just storing existentials type
<def`>
edwin: from the point of view of the backend, it looks like GADTs
<Drup>
:magic GADT:
<def`>
(actually, the state is used to encode type information, with a GADT not following the OCaml representation :))
<ggole>
So it's type any = Any : 'a t -> any, but without the indirection?
* ggole
has wanted that before
<def`>
ggole: in practice it is more
<def`>
type 'a state = S0 : int state | S1 : string state | ...
<def`>
type frame = Frame : 'a state * 'a -> frame
<edwin>
same for Coq I guess, its using Obj.magic because ocaml's type system can't express Coq's?
<def`>
yes
<kaustuv>
How much "inlining" is planned? Would it, for instance, try to turn a [let f (x, y) = foo] to a [let f x y = foo] as long as all uses of f are suitably scoped?
<ggole>
There's already a similar optimisation
Anarchos has quit [Ping timeout: 252 seconds]
<ggole>
Not restricted to scope, either - but it only applies to known call sites
ely-se has joined #ocaml
dsheets_ has quit [Ping timeout: 240 seconds]
<chambart>
*DON'T* use Obj.magic if you don't know OCaml backend in details and you know exactly which version of the compiler you are using.
<companion_cube>
:D
<def`>
chambart: all the fun in OCaml come with magic :)
<chambart>
especially the segfault, or even more fun, the corruptions without segfaults !
rossberg_ has quit [Remote host closed the connection]
<companion_cube>
why would we have to choose between the fun of OCaml and the joys of C?
<kaustuv>
There is a comment (by gasche) explaining why
<def`>
kaustuv: I think they should you use a hack like in Async/Lwt to make the typechecker believe it is covariant
<def`>
but not touch the internal representation
<kaustuv>
Ah, I am not that familiar with these libraries. What specific hack should I look for?
lambdahands_ has quit []
<def`>
kaustuv: the current implementation coerce between mutable and non mutable in the structure
struktured has joined #ocaml
<kaustuv>
def`: If I understand you correctly, then that is also what BatSplay does
struktured has quit [Client Quit]
<def`>
as such the type is already considered covariant in the structure, but this violates the expectation that non mutable types should not be mutated
<def`>
kaustuv: yes, I describe the splay tree
ely-se has quit [Quit: leaving]
<def`>
the trick in Async is to not touch the implementation
<kaustuv>
(PS, I think making 'a Map.t covariant was a mistake. Or perhaps making BatSplay ascribe to Map.S was a mistake.)
dsheets has joined #ocaml
<def`>
so the type is invariant in the structure, but coerce the signature so that the type is exported as covariant
<def`>
hence you lie only about the variance of parameters (which is not a lie, just a conservative approximation of the type checker)
<def`>
just relaxing a*
<Drup>
kaustuv: making map covariant is very useful, so no
<def`>
whereas here, the code really lies about mutability
<kaustuv>
Yes, I think BatSplay's days are numbered. Not just because of flambda, but because it's not thread-safe (with a multicore runtime) either, and purely functional data ought to be thread-safe.
<kaustuv>
More accurately, the performance benefits of splaying is not necessarily preserved in a multicore runtime.
<companion_cube>
monothread persistent structures are still useful, imho
<def`>
is there any convincing usecase for the splay tree ?
<companion_cube>
HAMT are nice too
<companion_cube>
or persistent arrays
<Drup>
def`: it's very circumstantial, but I don't understand why it needs mutability.
<kaustuv>
def`: indexing data structures in theorem provers.
<kaustuv>
def`: but these days I am rethinking some of my assumptions about those anyway and maybe I should try not using splay trees by default
<def`>
kaustuv: that's a convincing usecases for any map
<def`>
why a splaytree ?!
<kaustuv>
because splay trees stop being O(log n) lookup if you keep indexing the same element a lot.
<Drup>
def`: it depends on your access pattern basically, if you tend to access the same elements multiple time successively, it's very fast.
<kaustuv>
I benchmarked many different map implementations during my phd (in SML/MLton) and I remember splay trees being a huge improvement. But that is over a decade ago and I couldn't recall any details today. Anyhow, regardless of this particular niche, I wonder if we should just stop pretending (as a community) that some kinds of data are functional when they actually aren't.
<edwin>
what if you use a smaller map or hashtbl as a cache (that fits into some level of L* cache) and access the large and slower map only on a miss? (probably still slower than a splay tree, but is it much better than a regular map?)
<Drup>
kaustuv: I have seen this kind of hack *nowhere* except in batteries
<mrvn>
kaustuv: you need both
<Drup>
I think it's a bit of a sketch to say that "the community" is doing this
<kaustuv>
Drup: a tail-recursive List.map is basically the same hack, only more nefarious
<Drup>
and only batteries is doing this.
<kaustuv>
ExtLib as well. Maybe also Core?
<companion_cube>
kaustuv: which kind of theorem prover?
<def`>
kaustuv: the tail-rec hack is multicode friendly though
<Drup>
kaustuv: extlib is included in batteries, it's the same
<def`>
thread friendly* sorry
<Drup>
(Core uses a different technique)
<kaustuv>
Does Core use List.rev twice?
<companion_cube>
containers uses the same technique as Core, I believe (only a bit more naive)
<Drup>
kaustuv: no, it's not tail rec, just stays "under the stack limit"
<kaustuv>
That's invoking magic of a different kind then.
cross has joined #ocaml
<Drup>
look at the implementation, it's not that magical
contempt has quit [Ping timeout: 256 seconds]
<kaustuv>
Knowing the stack limit is magical.
contempt has joined #ocaml
<def`>
kaustuv: actually they use a constant stack space, big but not too much
<def`>
this is just to efficiently handle the common cases of small lists
<ggole>
It's just unrolling, really
ncthom91 has joined #ocaml
<def`>
ggole: I was thinking of the limit before switching to an array
freehck has joined #ocaml
<freehck>
hello
<def`>
unrolling is an optimisation, whereas the other trick enforce a strict upperbound on stack space consumption
<freehck>
Whats the best solution for asynchronous command execution?
<kaustuv>
I vaguely remember writing code like [type 'a list1 = Cons of 'a * 'a list] and relying on Obj.magic to corece 'a list1 to 'a list. I suppose these kinds of things are out as well?
<freehck>
I'd like to run some command in parallel with current process (f.e. with fork), and to get an answer which contain status, standard output and standard errors of a subprocess.
<freehck>
And I need this answer to be something like a message, that I could read when I want.
<freehck>
I'm looking now on Ocamlnet Shell, but dunno whether it's a good one variant for this purpose.
<companion_cube>
freehck: create_process is not enough then?
ely-se has joined #ocaml
kaustuv has left #ocaml ["ERC Version 5.3 (IRC client for Emacs)"]
<edwin>
would Lwt_process have something you need?
<freehck>
companion_cube: do I need to care about reading file descriptors myself in case of using Unix.create_process?
<companion_cube>
oh, yeah, probably, but it's not very hard
<freehck>
companion_cube: I mean, if I don't read a descriptor in time, the subprocess will be freezed until I read it?
<companion_cube>
I'm not sure how the OS buffers pipe
<freehck>
companion_cube: pipes have the same problem, but they also have a small system buffer.
<freehck>
companion_cube: Have you testet CCUnix youself?
<freehck>
Or maybe do you know somebody who used it?
<companion_cube>
well I wrote it and I use it in small scripts ;)
<companion_cube>
but it's quite limited indeed
<companion_cube>
if your subprocess expects interactions, then you probably need Lwt
<companion_cube>
(for you will need concurrency anyway)
<freehck>
companion_cube: doesn't it have a deadlock when you have a big error output?
<companion_cube>
oh, did you observe this?
<freehck>
I see that you are reading output first and errors then.
caml has joined #ocaml
<freehck>
Usually, if the pipe for errors is full and it's not read so the deadlock happen.
<freehck>
Because you're still trying to read output.
<companion_cube>
I suppose it could happen
<freehck>
Well, your functions seem to be quite similar to my own ones. The first variant of them I mean.
<caml>
Guys, I am using "ocamlfind ocamlopt ..." to build a project. Although I have "-o myexec" switch, but it doesn't create executable file. It doesn't throw any error when bulding. Any idea?
<freehck>
edwin: will a process that has bin executed with Lwt_process.exec continue to run if I don't use pread in time?
<freehck>
s/bin/been/
zpe has joined #ocaml
<edwin>
freehck: it'll run until the OS's pipe becomes full, pipe buffer size is OS dependent
<freehck>
edwin: so what's the difference between Lwt_process.exec and Unix.create_process?
<freehck>
edwin: Lwt is for concurrent threading, ysd?
<chambart>
Kakadu, I didn't look, but I know it is wrong ;)
<edwin>
pipe(7): 'Since Linux 2.6.35, the default pipe capacity is 65536 bytes, but the capacity can be queried and set using the fcntl(2) F_GETPIPE_SZ and F_SETPIPE_SZ operations'
tane has joined #ocaml
<edwin>
Lwt_process is useful if you already use Lwt
<edwin>
and there are some convenience functions as well, like Lwt_process.with_process_full
psy_ has joined #ocaml
ggole has quit []
<freehck>
People, what is Async for?
<Kakadu>
chambart: mmm?
<companion_cube>
it's an alternative to Lwt, freehck
<freehck>
Hm... Maybe I need to write my own module to call commands asyncronously?
ril has joined #ocaml
ely-se has quit [Quit: leaving]
slash^ has joined #ocaml
zpe has quit [Remote host closed the connection]
zpe has joined #ocaml
johnf has joined #ocaml
johnf_ has quit [Ping timeout: 260 seconds]
zpe has quit [Remote host closed the connection]
zpe has joined #ocaml
govg has joined #ocaml
zpe has quit [Ping timeout: 272 seconds]
ncthom91 has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
ril has quit [Quit: My Mac has gone to sleep. ZZZzzz…]