tulloch has quit [Read error: Connection reset by peer]
tulloch has joined #ocaml
eikke__ has quit [Ping timeout: 240 seconds]
maattdd has quit [Ping timeout: 252 seconds]
ontologiae has quit [Ping timeout: 265 seconds]
tidren has joined #ocaml
tidren has quit [Ping timeout: 245 seconds]
csakatoku has joined #ocaml
racycle_ has quit [Quit: ZZZzzz…]
Eyyub has quit [Quit: WeeChat 0.4.1]
Eyyub has joined #ocaml
tulloch_ has joined #ocaml
shinnya has quit [Ping timeout: 252 seconds]
tulloch has quit [Ping timeout: 245 seconds]
q66 has quit [Quit: Leaving]
rgrinberg has quit [Quit: Leaving.]
zpe has joined #ocaml
paolooo has joined #ocaml
zpe has quit [Ping timeout: 240 seconds]
michael_lee has joined #ocaml
paolooo has quit [Quit: Page closed]
tulloch_ has quit [Ping timeout: 240 seconds]
jwatzman|work has quit [Quit: jwatzman|work]
WraithM has joined #ocaml
tidren has joined #ocaml
WraithM has quit [Remote host closed the connection]
tidren has quit [Ping timeout: 240 seconds]
malo has quit [Quit: Leaving]
WraithM has joined #ocaml
studybot_ has quit [Read error: Connection reset by peer]
manizzle has quit [Ping timeout: 265 seconds]
rgrinberg has joined #ocaml
Eyyub has quit [Ping timeout: 258 seconds]
lostcuaz has joined #ocaml
WraithM has quit [Remote host closed the connection]
studybot has joined #ocaml
tidren has joined #ocaml
tidren has quit [Ping timeout: 264 seconds]
araujo has quit [Quit: Leaving]
zpe has joined #ocaml
manizzle has joined #ocaml
zpe has quit [Ping timeout: 276 seconds]
manizzle has quit [Remote host closed the connection]
manizzle has joined #ocaml
keen_______ has joined #ocaml
manizzle has quit [Ping timeout: 240 seconds]
tnguyen has quit [Ping timeout: 240 seconds]
NoNNaN has quit [Remote host closed the connection]
roppongininja has joined #ocaml
roppongininja has quit [Ping timeout: 255 seconds]
alex`` has quit [Remote host closed the connection]
NoNNaN has joined #ocaml
tlockney_away is now known as tlockney
tidren has joined #ocaml
racycle__ has joined #ocaml
tidren has quit [Ping timeout: 240 seconds]
tidren has joined #ocaml
zpe has joined #ocaml
tlockney is now known as tlockney_away
zpe has quit [Ping timeout: 240 seconds]
tlockney_away is now known as tlockney
siddharthv_away is now known as siddharthv
divyanshu has joined #ocaml
keen_______ has quit [Ping timeout: 240 seconds]
csakatoku has quit [Remote host closed the connection]
racycle__ has quit [Quit: ZZZzzz…]
NoNNaN has quit [Ping timeout: 272 seconds]
NoNNaN has joined #ocaml
bjorkintosh has quit [Ping timeout: 276 seconds]
lostcuaz has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
ggole has joined #ocaml
csakatoku has joined #ocaml
PryMar56 has quit [Quit: Leaving]
bjorkintosh has joined #ocaml
tlockney is now known as tlockney_away
tidren has quit [Remote host closed the connection]
tidren has joined #ocaml
tidren has quit [Ping timeout: 264 seconds]
tidren has joined #ocaml
bjorkintosh has quit [Ping timeout: 252 seconds]
tidren has quit [Remote host closed the connection]
bjorkintosh has joined #ocaml
arj has joined #ocaml
tidren has joined #ocaml
ruzu2 has joined #ocaml
ruzu has quit [Read error: Connection reset by peer]
tidren has quit [Remote host closed the connection]
tidren has joined #ocaml
dnm has quit []
tidren has quit [Remote host closed the connection]
zpe has joined #ocaml
tidren has joined #ocaml
_obad_ has quit [Ping timeout: 252 seconds]
zpe has quit [Ping timeout: 240 seconds]
tidren has quit [Remote host closed the connection]
tidren has joined #ocaml
tidren has quit [Remote host closed the connection]
rgrinberg has quit [Quit: Leaving.]
* whitequark
has spent 6.5 hours trying to prove a theorem
<whitequark>
turns out it was wrong
<whitequark>
-_-'
zpe has joined #ocaml
<ggole>
Heh.
<ggole>
Pierce has a thing in TAPL about that: Why bother proving theorems about languages when they usually aren't very interesting? A: They are usually wrong.
<whitequark>
ooooooh. it's the fact that my binary numbers have more than one representation
<whitequark>
or specifically, zero has more than one representation
<whitequark>
Coq asked me to prove BO = BD BO
<ggole>
Hmm, I don't have Coq installed at the moment.
<whitequark>
apt-get install coq ? :P
<ggole>
Yeah, it's more the emacs stuff (proof general) that takes a bit of fiddling about
<whitequark>
grmbl. no idea whatsoever on what to do with this.
keen_______ has joined #ocaml
nikki93 has quit [Remote host closed the connection]
nikki93 has joined #ocaml
nikki93 has quit [Remote host closed the connection]
ruzu2 has quit [Read error: Connection reset by peer]
ruzu has joined #ocaml
<ggole>
Hmm, CoqIDE gets into this state where it doesn't let you edit the code or close the buffer. ಠ_ಠ
maattdd has joined #ocaml
ygrek has joined #ocaml
ygrek_ has joined #ocaml
lordkryss has joined #ocaml
Submarine has joined #ocaml
Submarine has quit [Changing host]
Submarine has joined #ocaml
<ggole>
FFS, who puts (setq byte-compile-error-on-warn t) in their makefile and provides no way to turn it off? :|
nikki93 has joined #ocaml
nikki93 has quit [Ping timeout: 258 seconds]
WraithM has joined #ocaml
<adrien>
guile?!
pyon has quit [Quit: reboot]
eikke__ has joined #ocaml
ygrek_ has quit [Quit: ygrek_]
csakatoku has quit [Remote host closed the connection]
nikki93 has joined #ocaml
thomasga has joined #ocaml
csakatoku has joined #ocaml
ustunozgur has joined #ocaml
tautologico has quit [Quit: Connection closed for inactivity]
nikki93 has quit [Remote host closed the connection]
zpe has quit [Remote host closed the connection]
zpe has joined #ocaml
Submarine has quit [Remote host closed the connection]
zpe has quit [Ping timeout: 240 seconds]
roppongininja has joined #ocaml
roppongininja has quit [Remote host closed the connection]
maattdd has quit [Ping timeout: 255 seconds]
ruzu has quit [Read error: Connection reset by peer]
ruzu has joined #ocaml
ustunozgur has quit [Remote host closed the connection]
rz has quit [Ping timeout: 255 seconds]
ustunozgur has joined #ocaml
avsm has joined #ocaml
zpe has joined #ocaml
Kakadu has joined #ocaml
maattdd has joined #ocaml
<gasche>
whitequark: as you probably found out by now
<gasche>
there is no "short way" into Coq
<gasche>
only the long, painful way
<gasche>
the time you spend any given chapter of Software Foundations is neglegible over the time you'll struggle to do the exercises
<gasche>
(technically the answer to "a quick introduction to proof assistants" should not be "there is no such introduction yet, come back next year" but "there is no such proof assistant yet, come back in ten years"
<gasche>
)
<companion_cube>
"a no such introduction to quick proof assistants"
troydm has quit [Ping timeout: 252 seconds]
<NoNNaN>
"thats not entirely true, show me your proof" :)
robink has quit [Ping timeout: 264 seconds]
ruzu has quit [Read error: Connection reset by peer]
thomasga has quit [Quit: Leaving.]
<avsm>
gasche: whitequark: there will hopefully be an icfp/cufp Coq tutorial this year
<NoNNaN>
I just wondering how it is possible to find bugs in a 8GB generated coq proof
thomasga has joined #ocaml
ruzu has joined #ocaml
robink has joined #ocaml
<flux>
or even understand what is being proven :)
<gasche>
avsm: who is giving it?
<flux>
I would give that whatever it proves it does correctly, it is after all verified
<avsm>
gasche: not confirmed it, a few have been asked
<gasche>
flux: Coq reduces the "misunderstanding surface" from (all the code/proofs) to (the specification/statements)
<gasche>
which is often an several-orders-of-magnitude improvement
nikki93 has joined #ocaml
<flux>
gasche, yes, but it of course depends on how the proof is written, not all proofs automatically have this property :)
<flux>
"we show that the system is correct. the correctnes of the system is proven by the following generated 1024 lemmas:"
nikki93 has quit [Ping timeout: 255 seconds]
ruzu has quit [Read error: Connection reset by peer]
ruzu has joined #ocaml
troydm has joined #ocaml
<Kakadu>
Btw
torben_ has joined #ocaml
<torben_>
Hi!
<torben_>
I've got an interview with Jane Street coming up.
<Kakadu>
About OCaml Workshop 2013. Is video already available?
<torben_>
Can anyone point me towards a resource that gets me up to speed with OCaml quickly?
<torben_>
I've got a reasonably strong background in Haskell
<torben_>
so, I can handle a more advanced tutorial
<torben_>
(but I don't think I'd have the time to go through Real World Ocaml)
ruzu has quit [Read error: Connection reset by peer]
ontologiae has joined #ocaml
dsheets has quit [Ping timeout: 264 seconds]
ruzu has joined #ocaml
<torben_>
(oh, of course I can google myself; but it would be good to tap into the community wisdom for finding the most well-regarded sources, that's why I'm asking ;))
<gasche>
torben_: you could read the OCaml manual directly
<gasche>
it starts with an introduction that will let you know the syntax differences from Haskell
<gasche>
and then you've got an exhaustive language reference
ruzu has quit [Read error: Connection reset by peer]
<gasche>
torben_: then you should probably learn to use one of the asynchronous monadic libraries (Async or Lwt)
ruzu has joined #ocaml
<gasche>
(being familiar with the language in general does not suffice to be at ease with those; the other case would be reactive programming (React))
darkf_ has joined #ocaml
<torben_>
Great. I just skimmed the manual, and it seems quite thorough. Thanks for the help!
ruzu2 has joined #ocaml
dsheets has joined #ocaml
darkf has quit [Ping timeout: 265 seconds]
ruzu2 has quit [Read error: Connection reset by peer]
ruzu has quit [Ping timeout: 245 seconds]
tulloch has joined #ocaml
ruzu has joined #ocaml
torben_ has quit [Ping timeout: 240 seconds]
ruzu has quit [Read error: Connection reset by peer]
ruzu has joined #ocaml
ruzu has quit [Read error: Connection reset by peer]
ollehar has joined #ocaml
ruzu has joined #ocaml
maattdd has quit [Ping timeout: 276 seconds]
mort___ has joined #ocaml
mort___ has quit [Ping timeout: 240 seconds]
csakatoku has quit [Remote host closed the connection]
ruzu has quit [Read error: Connection reset by peer]
ruzu has joined #ocaml
csakatoku has joined #ocaml
maattdd has joined #ocaml
Nuki has quit [Remote host closed the connection]
Nuki has joined #ocaml
darkf_ is now known as darkf
eikke__ has quit [Ping timeout: 255 seconds]
thomasga has quit [Quit: Leaving.]
acieroid` has joined #ocaml
vpit3833 has joined #ocaml
thomasga has joined #ocaml
Valda has joined #ocaml
smondet_ has joined #ocaml
_2can_ has joined #ocaml
finnrobi_ has joined #ocaml
yastero_ has joined #ocaml
ollehar has quit [Ping timeout: 252 seconds]
venk has quit [Ping timeout: 252 seconds]
acieroid has quit [Ping timeout: 252 seconds]
_2can has quit [Ping timeout: 252 seconds]
yastero has quit [Ping timeout: 252 seconds]
brendan has quit [Ping timeout: 252 seconds]
smondet has quit [Ping timeout: 252 seconds]
Valdo has quit [Ping timeout: 252 seconds]
cdidd has quit [Ping timeout: 252 seconds]
finnrobi has quit [Ping timeout: 252 seconds]
Valda is now known as Valdo
rand000 has joined #ocaml
cdidd has joined #ocaml
brendan has joined #ocaml
<Drup>
grmbl, I stumble upon a super quick tutorial to ocaml for the haskeller, I don't find it anymore
<Drup>
(well, torben_ is gone anyway)
ikaros has joined #ocaml
ebzzry_ has joined #ocaml
Mandus_ has joined #ocaml
_2can has joined #ocaml
_andre has joined #ocaml
Mandus_ has quit [Remote host closed the connection]
tulloch has quit [Remote host closed the connection]
csakatok_ has joined #ocaml
ollehar has joined #ocaml
thomasga has quit [Quit: Leaving.]
csakatoku has quit [Ping timeout: 252 seconds]
<gasche>
Drup: ezyang's?
ontologiae has quit [Ping timeout: 240 seconds]
Mandus_ has joined #ocaml
eikke__ has joined #ocaml
csakatok_ has quit [Ping timeout: 265 seconds]
<Drup>
gasche: do you have a link ? I don't find it
<ggole>
I don't see how first-class modules affect it though
<ggole>
(And this may be a different problem entirely.)
<Drup>
ggole: by unpacking and repacking modules as list elements, to carry them around
<ggole>
I think that's a different problem.
<ggole>
This is just to get around the fact that GADT typing bitches that the list *element type* can't be returned because it is a GADT type variable, even though we don't want it to be
<whitequark>
then do: utop; #ppx "ppx_protobuf";; #require "protobuf";; type foo = int [@@protobuf];;
<whitequark>
findlib isn't yet able to load ppx extensions...
Nuki has joined #ocaml
<philtor>
ok, utop installed.
<philtor>
hmm... seems to be stuck at: type foo = = int [@@protobuf];;
<philtor>
utop just kind of hung there.
<philtor>
Not getting a prompt.
<whitequark>
did you really use "type foo = = int" ?
<whitequark>
with two equality signs?
<philtor>
(on the positive side, the #ppx ... and #require "protobuf" worked.
<philtor>
no:
<philtor>
utop # type foo = int [@@protobuf];;
<whitequark>
that's odd
<philtor>
just hangs there
<whitequark>
it worked for me
<whitequark>
kill it and try again?
<philtor>
Hmm.. is there anyway to get a stacktrace on utop?
<philtor>
Yeah, I killed it and tried again.
<whitequark>
what's your OS?
<philtor>
Linux. Fedora 20
<whitequark>
hmm, sounds fine
mort___ has joined #ocaml
<philtor>
$ uname -a
<philtor>
Linux quad.ftrdhcpuser.net 3.8.8-203.fc18.x86_64 #1 SMP Wed Apr 24 13:12:26 UTC 2013 x86_64 x86_64 x86_64 GNU/Linux
maattdd has quit [Ping timeout: 276 seconds]
<whitequark>
practically identical to my system, yeah
<whitequark>
try it in regular toplevel
<whitequark>
ocaml -ppx ppx_protobuf -dsource; #use "topfind";; #require "protobuf";; type foo = int [@@protobuf];;
<whitequark>
paste all of the output
<jpdeplaix>
whitequark: if you have the time, can you ping for my email to llvm-commits ?
<whitequark>
jpdeplaix: I need chapuni64, and he's apparently on vacation or something
<philtor>
whitequark: oh, interesting... it seems my ocaml toplevel is broke.
<philtor>
if I just do:
<philtor>
$ocaml
<philtor>
# let foo = "bar" ;;
<philtor>
it hangs as well.
<whitequark>
wow
* whitequark
sighs
<philtor>
oh, wait a sec...
<philtor>
that's the wrong ocaml I'm getting.
<philtor>
$ which ocaml
<philtor>
~/.opam/4.02.0dev+trunk/bin/ocaml
<philtor>
<- ok that seems right
<philtor>
but then...
<philtor>
$ ocaml
<philtor>
OCaml version 4.02.0+dev5-2014-04-29
<jpdeplaix>
whitequark: ok, no problems
<whitequark>
does the same thing for me
<whitequark>
I guess it has the date hardcoded
<philtor>
well, that may be correct then.
nikki93 has joined #ocaml
tlockney is now known as tlockney_away
<philtor>
yeah, toplevel definitely seems to be broken.
<philtor>
hmm... reinstall?
<philtor>
Well, gotta run. I'll have to give this a try again later.
eizo has quit [Ping timeout: 240 seconds]
roppongininja has quit [Remote host closed the connection]
philtor has quit [Ping timeout: 240 seconds]
krono has joined #ocaml
tidren has joined #ocaml
<krono>
hey
<companion_cube>
ho
<krono>
lets go
<krono>
Ok, I have a question on terminology
<krono>
From what I know, the lisp-y languages call thinks like x::xs / (cons x xs) cons _cells_
<Drup>
yep, it's called the same in ocaml
<krono>
Viewed a bit more abstract, :: is nearly the same as “type 'a lst = Nil | Cons of 'a * 'a lst ;;”
<krono>
would Cons (x, xs) still be called a cell?
<Drup>
you can remove the "nearly"
roppongininja has joined #ocaml
tidren has quit [Ping timeout: 264 seconds]
<krono>
and if so, would this “cell” name still hold for n-ary types?
<krono>
(it is only about finding a good name for 'instances' of a composite type)
<krono>
it is straightforward for cons-cells with “cell” but I haven’t heard of a common terminology for the general concept
<companion_cube>
n-ary types?
<krono>
ie, “type … … of 'a * 'b * 'c ……… * 'n;;”
claudiuc has quit [Remote host closed the connection]
<krono>
I’m talking riddles, right?
<ggole>
Perhaps a better name is 'block'
<ggole>
Lisp conses are a bit different to OCaml lists, too
<ggole>
They're more like a pair of lisp values
<ggole>
Something like type lisp_value = Int of int | Symbol of symbol | <other atoms here> | Cons of lisp_value * lisp_value
<Drup>
"cell" is usually used for stuff like "the value + the pointer to the next bit of the data structure"
<krono>
oh, ok
<krono>
I thought of “data structure instances” but this sounds too OO to talk about algebraic types
<Drup>
if you want to talk about the stuff inside the data structure, well, they are just elements
<krono>
no, not inside, the thing itself
<Drup>
well, if it's the thing itself, call it a thing :D
<krono>
That’s a bit tough in academic papers :D
maattdd has joined #ocaml
<ggole>
"object" maybe
<ggole>
That's vague enough
<ggole>
It's basically "thing" but you sound smarter
<krono>
yes, maybe, but it has this OO connotation I want to avoid, currently
<Drup>
krono: I mean, if you use a thing of type list, well, call it a list.
keen_ has quit [Ping timeout: 276 seconds]
<krono>
And for a tree, call it tree, right.
<Drup>
:D
<Drup>
object works
<Drup>
inhabitant of a type, is the very technical term
<krono>
pom pom pom
<Drup>
but it's usually used in proof theory
<ggole>
I think if you are explicitly discussing representation object is reasonable
<krono>
yes, this seems reasonable
<ggole>
Or "value", if it doesn't happen to matter whether it is a block-structured thingy or an immediate thingy
<krono>
well, _that_ does matter a lot for me, so I would have to skip value today
<ggole>
Right.
<krono>
Do you know of hand some paper that deals with the representation of “instances/objects of types” in OCaml/CamlLight? (I mean, beside the ZINC paper)
<ggole>
The manual has a page on interfacing with C that has a lot of details
<ggole>
And real world ocaml spends some time on it