willb has quit [Read error: 110 (Connection timed out)]
willb has joined #ocaml
seafood has quit []
seafood has joined #ocaml
Associat0r has quit []
seafood_ has joined #ocaml
Ched has quit [Read error: 60 (Operation timed out)]
seafood_ has quit [Client Quit]
seafood_ has joined #ocaml
seafood has quit [Read error: 104 (Connection reset by peer)]
Ched has joined #ocaml
seafood_ has quit []
seafood has joined #ocaml
Associat0r has joined #ocaml
mbishop has quit ["Leaving"]
Associat0r has quit []
seafood has quit [Read error: 104 (Connection reset by peer)]
Alpounet has quit ["Quitte"]
seafood has joined #ocaml
seafood has quit [Client Quit]
mbishop has joined #ocaml
seafood has joined #ocaml
seafood has quit [Client Quit]
seafood has joined #ocaml
seafood has quit [Client Quit]
Associat0r has joined #ocaml
seafood has joined #ocaml
seafood_ has joined #ocaml
seafood_ has quit []
seafood has quit [Read error: 110 (Connection timed out)]
mpwd has quit [Read error: 110 (Connection timed out)]
Associat0r has quit []
aldebrn has quit [Read error: 60 (Operation timed out)]
jeddhaberstro has quit []
julm has quit [Read error: 60 (Operation timed out)]
Snark has joined #ocaml
julm has joined #ocaml
mpwd has joined #ocaml
mpwd has quit [Read error: 110 (Connection timed out)]
schme has joined #ocaml
willb1 has joined #ocaml
willb has quit [Read error: 110 (Connection timed out)]
ikaros has joined #ocaml
Camarade_Tux has joined #ocaml
mpwd has joined #ocaml
seafood has joined #ocaml
_zack has joined #ocaml
jeanbon has joined #ocaml
_zack has quit [Read error: 110 (Connection timed out)]
willb1 has quit [Read error: 54 (Connection reset by peer)]
willb1 has joined #ocaml
aym has joined #ocaml
aym has left #ocaml []
komar_ has joined #ocaml
youscef has joined #ocaml
willb2 has joined #ocaml
<Camarade_Tux>
hmmm, for ocaml-gir, I have to bind some constants : how should I show that on the ocaml side ? polymorphic variants which I catch in the bindings layer and which I translate ?
<Camarade_Tux>
(trying to come with a nice api ;) )
<Camarade_Tux>
s/come/come up/
willb1 has quit [Read error: 110 (Connection timed out)]
<mrvn>
Camarade_Tux: like const int foo = 17; ?
<Camarade_Tux>
mrvn, yes
<mrvn>
let foo = 17
<mrvn>
And in the bindings you use Val_int() and Int_val()
<Camarade_Tux>
I have tons of them and that would require referencing to the module or at least opening it
<Camarade_Tux>
(names are pretty long)
<mrvn>
No way around it.
Yoric[DT] has joined #ocaml
<Yoric[DT]>
hi
seafood has quit []
<Camarade_Tux>
hi Yoric[DT]
<Yoric[DT]>
How do you do?
<Yoric[DT]>
Neighbour :)
<Camarade_Tux>
fine, thanks, and you ? :)
<Camarade_Tux>
you weren't living in Paris a few months ago, right ?
<Yoric[DT]>
Well, I'm living a weird life.
<Yoric[DT]>
But yes, I was living in Paris.
<Yoric[DT]>
(not just in Paris, though)
<Camarade_Tux>
I see, moving around a lot
seafood has joined #ocaml
<Yoric[DT]>
Yeah.
<Yoric[DT]>
Should get settled now.
Lomono has quit ["Don't even think about saying Candlejack or else you wi"]
jmou has joined #ocaml
julm has quit [Read error: 110 (Connection timed out)]
itewsh has joined #ocaml
Alpounet has joined #ocaml
jmou is now known as julm
Lomono has joined #ocaml
<Camarade_Tux>
ok, camlp5 not working with 3.11;
<Camarade_Tux>
*3.11.1
<Camarade_Tux>
I'm now missing half of my packages ='(
komar_ has quit [Read error: 60 (Operation timed out)]
<thelema>
the original problem is one of cp, now that seems fixed, and we've got an earlier bug relating to capitalization of files as checked out from git?
<thelema>
under OSX
<hcarty>
I'm not sure how this conflict is occuring
<thelema>
OSX has a case-preserving filesystem. It's not case sensitive, but it does remember what case you used.
<hcarty>
The change was an alias in batteries.ml
<hcarty>
Hmm
<thelema>
yes, that change couldn't have done it.
<thelema>
(from what I understand)
<thelema>
my question is why does "src/libs/camlzip/gzip.cmi
<thelema>
" get produced instead of "src/libs/camlzip/gZip.cmi"?
<hcarty>
Yes, I'm wondering that as well
<thelema>
a build problem?
<hcarty>
Perhaps
<thelema>
or a git checkout problem?
* thelema
wishes for a ls -l src/libs/camlzip/
<hcarty>
I don't have access to OSX to test locally, unfortunately
* thelema
makes a request of ben
<hcarty>
thelema: Thank you
<thelema>
I don't think it could be in the repo wrong, because those of us using linux would have problems
<thelema>
so where is the problem, and why didn't this problem show up earlier?
<hcarty>
It looks like the sort of problem that came from trying to rename gZip.* -> gzip.* in the Batteries source tree
jeff_s_ has joined #ocaml
<thelema>
The only reason to think it was your name change was that we hadn't seen this problem earlier, and it looks like it'd show up earlier in the build process than the doc copying problem
<thelema>
that was Nov 2, 08
<thelema>
git commit 807bc40
<thelema>
and the bug was submitted in april, so...
<thelema>
pinging anyone using OSX!
<hcarty>
thelema: Ah, no. My change was later than that.
<hcarty>
It wasn't a change to gZip.ml, it was a change to batteries.ml
<thelema>
yes, your change didn't rename the file, it just changed the module mapping in batteries.ml
<hcarty>
Oh, sorry - I see what you're saying
<mpwd>
Does anyone have any pointers to monad stuff in Ocaml?
<mpwd>
btw, I'm an OSX guy, thelema
<Alpounet>
mpwd, in batteries's git, "alp" branch, there is a beginning of Monadic stuffs
<mpwd>
cool
<Alpounet>
there's an Enum monad
<Alpounet>
an Option monad
<mpwd>
I think I saw this
<mpwd>
Do you have a list monad yet?
<Alpounet>
no, 'cause for the moment it's been decided Enum was the central container type
<Alpounet>
like List is for Haskell's stdlib
<mpwd>
oh, okay
<Alpounet>
however, we have sequence and foldM equivalents for working on enums of monadic elements
<Alpounet>
that's all for the moment, but Monads aren't hard to implement
<Alpounet>
and for using them, well, using open ... in is a little like using typeclasses... it is a sort of local overloading
<hcarty>
Or use pa-do for even more efficient local overloading! :-)
<mpwd>
how similar is the open ... semantics to typeclassing?
<Alpounet>
mpwd, instead of having typeclass-polymorphism, we have module-polymorphism
<mpwd>
This is nice
<Alpounet>
i.e the compiler won't automatically deduce which module to use, and we have to open it locally by ourselves
<Alpounet>
that's painful compared to typeclass
<mpwd>
Yeah. Bit of a shame
<Alpounet>
but this is, IMO, one of the better way (the best ?) to use monads in OCaml
<mpwd>
Yeah, this looks pretty good
<Alpounet>
Even if there is pa_monad
<mpwd>
I'm not familiar with pa_monad
<Alpounet>
mpwd, as you can see, there isn't that much monadic stuffs in OCaml. Some people (including me) tried to kick-start some basis to build strong monadic modules but there doesn't seem to be that much need in the OCaml community
<Alpounet>
However, if you would like to help on monadic stuffs for Batteries, you're of course welcome
<mpwd>
Well, the researcher I'm working with later this summer has built up a library for doing lazy probabilistic computation, which is essentially a monad that he has adapted from Haskell
<Alpounet>
ok
<mpwd>
More-over, monads are ubiquitous throughout formal methods. After all, proof tactics (if you are familiar with them), are just an instance of the state monad
<mpwd>
Anyway, I'm honestly just a first years master student, but if you think I could help, I could give it a shot
<mpwd>
After reading your blog, I honestly err on the side of wanting to implement most of Control.Monad for each .Monad module...
<Alpounet>
mpwd, I'm not even at the master level of my studies (undergraduate), so of course you can, even more if you're already quite familiar with monads
<Alpounet>
mpwd, you should take a look at the 2 or 3 discussions concerning monads on Batteries ML
<Alpounet>
Batteries' ML*
giulianoxt has joined #ocaml
Lomono has quit [Read error: 113 (No route to host)]
<mpwd>
cool
<mpwd>
I might just give it a shot (no promises, however...)
<Alpounet>
np :)
komar_ is now known as komar__________
komar__________ is now known as komar_
yziquel has joined #ocaml
Amorphous has quit [Read error: 110 (Connection timed out)]
Amorphous has joined #ocaml
yziquel has quit [Read error: 104 (Connection reset by peer)]
willb2 has quit [Read error: 110 (Connection timed out)]
willb2 has joined #ocaml
julm has quit [Read error: 60 (Operation timed out)]
Snark has quit ["Ex-Chat"]
julm has joined #ocaml
willb1 has joined #ocaml
willb2 has quit [Read error: 110 (Connection timed out)]
Lomono has joined #ocaml
* palomer
wishes he could find a twelf guru
* Yoric[DT]
hasn't used Twelf in about 10 years.
<palomer>
it existed 10 years ago?
<Yoric[DT]>
Ok, that may have been 9 years.
<Yoric[DT]>
Spring 2000.
<Yoric[DT]>
During my internship, I used Twelf.
* Yoric[DT]
still has the pdf for an unconvincing paper regarding an algorithm in Twelf.
<Yoric[DT]>
That paper was rejected (fortunately).
<palomer>
do you remember what "well-moded" means?
giulianoxt has left #ocaml []
<Yoric[DT]>
Nope.
<palomer>
hrmph
<palomer>
is it worth learning twelf?
<Yoric[DT]>
Well, I'm no specialist but Andrew Appel, who introduced me to Twelf, eventually gave up on Twelf and went to Coq.
<Yoric[DT]>
That's all I can say.
psnively has joined #ocaml
willb1 has quit [Read error: 104 (Connection reset by peer)]
willb1 has joined #ocaml
<palomer>
well...
<palomer>
I'm finally beginning to understand twelf
<psnively>
Ouch.
<palomer>
ouch?
<psnively>
I prefer Coq. :-)
<maxote>
what's twelf?
<palomer>
can Coq be easily described with a type system?
<psnively>
palomer: I'm not sure I understand the question.
<palomer>
maxote, a (rather poorly documented and sparsely used) theorem proving system
<psnively>
Coq is based on the Calculus of Inductive Constructions, if that helps.
<maxote>
i'm searching a theorem finder but internet looks for theorem provers only.
<palomer>
well... take a simplified ocaml. to verify the correctness of an ocaml program, you have a set of simple typing rules
<palomer>
there's a theorem database somewhere
<palomer>
psnively, can the correctness of a coq proof be described by a small set of theorems?
<psnively>
Ah, the de Bruijn criterion. Absolutely.
<psnively>
Not only that, the current version includes a small, standalone checker.
<palomer>
I always thought you programed in coq with a series of commands
<Alpounet>
like assembly ? :-p
<palomer>
like an interactive system
<psnively>
palomer: it's true that Coq is tactic-based. There's nothing preventing you from writing out terms in the CIC if you're a masochist, though. :-)
<psnively>
Is Twelf not interactive??
rjack has quit ["leaving"]
Smerdyakov has joined #ocaml
<palomer>
twelf isn't particularly interactive
<palomer>
from what I can gather
<psnively>
And right on time, Smerdyakov arrives, who knows how to differentiate between Twelf and Coq much better than I do.
<psnively>
It's true that Twelf is not tactic-based, AFAIK.
<maxote>
was not Twelf used for compiler construction?
<Smerdyakov>
Twelf is special-purpose and Coq is general-purpose, if nothing else.
<maxote>
what about Isabelle? is it special-purpose or general-purpose?
<psnively>
Ah. I just ran godi_console, updated the package list, asked to update, and it's happily rebuilding 24 packages. Nice.
<Smerdyakov>
Isabelle is special-purpose.
<palomer>
forall A. twelf is good at task A -> Coq is equally good at A ?
<Smerdyakov>
I wonder if there's enough critical mass for it to be sensible to have a proof assistant Freenode channel.
<Smerdyakov>
palomer, I didn't claim that, no.
<Smerdyakov>
#coq has pretty good attendance, at least. You can ask Coq questions there (which makes more sense than here).
<palomer>
I want to write a structure editor for a theorem prover
<palomer>
I'm having to pick between coq and twelf
<palomer>
twelf seems to have a simpler type system
<Smerdyakov>
And assembly language has a simpler type system still.
<psnively>
OTOH Coq's is simple enough that there's the standalone checker for it...
<palomer>
what's the standalone checker called?
<palomer>
right, but a structure editor for assembly seems a little pointless
<psnively>
I don't know, never having felt the need to use it.
<psnively>
I dunno. I used a structure editor for Lisp back in the day, and Lisp's structure is ridiculously simple.
<Smerdyakov>
I think it's arguable whether Twelf proof-checking is simpler than Coq proof-checking.
<Smerdyakov>
Twelf has a separate meta-layer for reasoning about logic programs as proofs.
<Smerdyakov>
Whereas everything is really just type-checking in Coq.
<palomer>
what's this meta-layer?
<palomer>
m2?
<Smerdyakov>
That's the one. I don't remember what the number is that comes after "M," but I'll take your word for it. :-)
<palomer>
this conversation's really interesting, but I gotta go eat supper. brb!
jeanbon has quit [Read error: 110 (Connection timed out)]
slash_ has joined #ocaml
Ched has joined #ocaml
psnively has quit []
Smerdyakov has quit ["Leaving"]
Yoric[DT] has quit ["Ex-Chat"]
Associ8or has joined #ocaml
Associ8or has quit [Client Quit]
ellisbben has joined #ocaml
Associat0r has quit []
Associat0r has joined #ocaml
Associat0r has quit [Client Quit]
Associat0r has joined #ocaml
schme has quit [Read error: 113 (No route to host)]