gildor changed the topic of #ocaml to: Discussions about the OCaml programming language | http://caml.inria.fr/ | OCaml 3.12.0 http://bit.ly/aNZBUp
Poet_ has joined #ocaml
Znudzon has quit [Ping timeout: 276 seconds]
Poet_ has quit [Ping timeout: 276 seconds]
Smerdyakov has quit [Quit: Leaving]
ikaros has quit [Quit: Leave the magic to Houdini]
willb1 has quit [Read error: Connection reset by peer]
willb1 has joined #ocaml
sepp2k has quit [Quit: Leaving.]
weihe has quit [Quit: leaving]
somnium has quit [Read error: Connection reset by peer]
|marius| has quit [Remote host closed the connection]
q[mrw] has joined #ocaml
|marius| has joined #ocaml
willb1 has quit [Read error: Connection reset by peer]
willb1 has joined #ocaml
_unK has quit [Remote host closed the connection]
Associat0r has joined #ocaml
willb1 has quit [Read error: Connection reset by peer]
willb1 has joined #ocaml
joewilliams is now known as joewilliams_away
Associat0r has quit [Ping timeout: 265 seconds]
|marius| has quit [Remote host closed the connection]
ulfdoz_ has joined #ocaml
|marius| has joined #ocaml
ulfdoz has quit [Ping timeout: 248 seconds]
willb2 has joined #ocaml
willb1 has quit [Ping timeout: 248 seconds]
rudi_s has quit [Read error: Operation timed out]
Associat0r has joined #ocaml
willb2 has quit [Read error: Connection reset by peer]
willb2 has joined #ocaml
rudi_s has joined #ocaml
q[mrw] has quit [Quit: Leaving]
xmarteo has joined #ocaml
xmarteo has quit [Remote host closed the connection]
ygrek_ has joined #ocaml
willb2 has quit [Read error: Connection reset by peer]
Amorphous has quit [Ping timeout: 245 seconds]
willb2 has joined #ocaml
Amorphous has joined #ocaml
ftrvxmtrx has quit [Ping timeout: 258 seconds]
ftrvxmtrx has joined #ocaml
willb2 has quit [Read error: Connection reset by peer]
willb2 has joined #ocaml
Anarchos has joined #ocaml
Anarchos has quit [Client Quit]
Anarchos has joined #ocaml
|marius| has quit [Remote host closed the connection]
boscop has quit [Ping timeout: 245 seconds]
boscop has joined #ocaml
willb2 has quit [Read error: Connection reset by peer]
willb2 has joined #ocaml
_unK has joined #ocaml
<adrien> btw, last time I had to compile on windows, I simply installed all dependencies in $(ocamlc -where), not very clean but definitely works (was on mingw+msys and ocamlfind probably didn't work very well apparently)
Edward has joined #ocaml
<adrien> bah, I can scroll down the list for go in less than 2 seconds, whatever
willb2 has quit [Read error: Connection reset by peer]
<adrien> ah... and looks like haskell/hackage: packages are split
sepp2k has joined #ocaml
Anarchos has quit [Quit: Vision[0.9.7-H-090423]: i've been blurred!]
Anarchos has joined #ocaml
willb2 has joined #ocaml
Anarchos has quit [Quit: Vision[0.9.7-H-090423]: i've been blurred!]
Edward_ has joined #ocaml
Edward has quit [Ping timeout: 240 seconds]
ikaros has joined #ocaml
pikachuyann has joined #ocaml
Edward_ has quit [Ping timeout: 246 seconds]
ygrek_ has quit [Ping timeout: 245 seconds]
oriba has joined #ocaml
ygrek_ has joined #ocaml
Smerdyakov has joined #ocaml
Poet_ has joined #ocaml
_unK has quit [Remote host closed the connection]
rumpi61 has joined #ocaml
Poet_ has quit [Ping timeout: 255 seconds]
Edward has joined #ocaml
Edward has quit [Client Quit]
Anarchos has joined #ocaml
joewilliams_away is now known as joewilliams
joewilliams is now known as joewilliams_away
<Anarchos> hello
<gildor> Anarchos: hello
<Anarchos> gildor is there a theorem prover for first order logic in ocaml ?
<Smerdyakov> Sort of an odd question, since first-order logic is a subset of higher-order logic, and I assume you know about Coq.
<Anarchos> Smerdyakov sure, but i find Coq so complicated at first try...
<Smerdyakov> You can't get the same things done without a similar level of complication.
<gildor> Anarchos: you might be interested in matita
<Smerdyakov> Why does the OCaml part matter to you?
<Anarchos> because i prefer software written in it !!
willb2 has quit [Quit: Leaving]
<Smerdyakov> I have a feeling Matita makes it easier to feel like you know what's going on, but also _much_ harder to get real work done.
<Smerdyakov> Anarchos, did you read my book, CPDT?
<Anarchos> Smerdyakov i wonder if i should began mine for proving bourbaki ...
Poet_ has joined #ocaml
<Anarchos> Smerdyakov sorry i don't remember which book
<flux> I haven't read it.. but I had it bookmarked! it must count for something! :)
<Anarchos> Smerdyakov i bookmarked it for further reading :)
<Smerdyakov> OK
<flux> smerdyakov, does the book expect the reader to have some level of ability to use Coq?
<Smerdyakov> No, none.
<flux> oh. in that case I must increase the priority :).
<flux> although I'm awfully lazy, I had all the summer time, but didn't really go beyong the second lecture of http://www.seas.upenn.edu/~cis500/current/index.html :-/
<Anarchos> One idea i had is that we could group several demonstrations to a prover and let it extract a skeleton, eg a regular expression based upon names of theorems used, to build skeleton proofs for common cases
Poet_ has quit [Ping timeout: 276 seconds]
<Anarchos> what do you think about that idea ? I think we all learnt to build demonstrations this way .
<Anarchos> strange, the missing link icon don't get update when you recreate the target of the link
* Anarchos apologizes for last sentence : wrong irc channel
Poet_ has joined #ocaml
<Smerdyakov> Anarchos, I'm highly skeptical that it's applicable to the domains I work in.
<Anarchos> Smerdyakov i just thought to that to make the machine to learn how to proof some sample problems by examples
<Smerdyakov> Yes. I'm saying it won't work in most domains.
<Smerdyakov> Or, it would take more effort than just writing an adaptable proof script.
<Smerdyakov> The best case is when you have a decidable theory and can just write a traditional decision procedure. These cases are rare, though.
<Anarchos> so how to decide what step is considered "skippable" in formal proof presentation, to let them look as book ones ??
<Smerdyakov> Read my book.
<Smerdyakov> But you don't want your formal proofs to look like traditional book proofs. Those are too sketchy to be convincing, anyway.
<Anarchos> Smerdyakov i know, i jsut think to do a formal proof, but don't present the really easy or redundants parts of it
<Smerdyakov> Yes. Read me book.
<Anarchos> i will :)
<Smerdyakov> Seriously, this is one of the main focuses in it.
<Anarchos> Smerdyakov what is it about, roughly speaking ?
<Smerdyakov> It's about how to engineer mechanized proofs in Coq.
<Anarchos> ok i will really look to it !
strangy has joined #ocaml
Poet_ has quit [Ping timeout: 240 seconds]
Poet_ has joined #ocaml
Smerdyakov has quit [Quit: Leaving]
Poet_ has quit [Ping timeout: 265 seconds]
Edward has joined #ocaml
_unK has joined #ocaml
Anarchos has quit [Quit: Vision[0.9.7-H-090423]: i've been blurred!]
Poet_ has joined #ocaml
oc13 has joined #ocaml
<oc13> Hi, anyone here?
<oc13> trying to compile a program with ocamlbuild
<oc13> unsing ulex
<oc13> what should i put into my _tags file?
<oc13> i did not get it.
<adrien> oc13: are you using http://brion.inria.fr/gallium/index.php/Using_ocamlfind_with_ocamlbuild or are you using no myocamlbuild.ml (or are you using ocaml 3.12?)
<thelema> assuming you're using a findlib-enabled myocamlbuild, and you have a findlib package ulex, put "<*>: pkg_ulex" in your _tags file
<oc13> i trie the example from ulex (test.ml). With pkg_ulex i get a syntax error.
<thelema> do you have a myocamlbuild.ml file?
<oc13> no
<thelema> you'll need one
<oc13> my first project with ocamlbuild, sorry
<adrien> no problem: copy-paste the code on http://brion.inria.fr/gallium/index.php/Using_ocamlfind_with_ocamlbuild to a file named "myocamlbuild.ml"
<thelema> yes, what adrien said
<adrien> after that you'll be free to use 'pkg_ulex'
<oc13> ok, i will try it, thanks
<adrien> actually, if someone has ocaml 3.12, it'd be good to try *without* the myocamlbuild.ml as 3.12 has support for ocamlfind, I don't know how well it works however
<adrien> (I doubt it can be horribly broken considering the simplicity of the plugin)
drksd has quit [Quit: kwa]
<oc13> thanks, it compiles
<adrien> :-)
Poet_ has quit [Ping timeout: 265 seconds]
|marius| has joined #ocaml
Poet_ has joined #ocaml
Poet_ has quit [Client Quit]
oriba has left #ocaml []
ulfdoz_ has quit [Quit: Reconnecting]
ulfdoz has joined #ocaml
drksd has joined #ocaml
<ulfdoz> Notebook.
<ulfdoz> ewin, sorry.
|marius| has quit [Remote host closed the connection]
Edward has quit [Ping timeout: 276 seconds]
|marius| has joined #ocaml
BiDOrD has joined #ocaml
|marius| has quit [Remote host closed the connection]
BiDOrD has quit [Ping timeout: 252 seconds]
Edward has joined #ocaml
BiDOrD has joined #ocaml
sepp2k1 has joined #ocaml
sepp2k has quit [Ping timeout: 240 seconds]
itewsh has joined #ocaml
ygrek_ has quit [Ping timeout: 245 seconds]
Edward has quit []
oc13 has quit [Ping timeout: 246 seconds]
|marius| has joined #ocaml
rumpi61 has quit [Ping timeout: 258 seconds]
_unK has quit [Remote host closed the connection]
|marius| has quit [Remote host closed the connection]
<MarcWeber> ocamldep.ml contains let load_path = ref ([] : (string * string array) list)
<MarcWeber> Can I dump the value somehow without writing a to string serialization for that type?
<rwmjones> MarcWeber: using something like extlib's Std.dump
itewsh has quit [Ping timeout: 240 seconds]
ikaros has quit [Quit: Leave the magic to Houdini]
pikachuyann has quit [Quit: Quitte]
philtor has joined #ocaml
Associat0r has quit [Quit: Associat0r]
caligula__ has joined #ocaml
caligula_ has quit [Ping timeout: 276 seconds]
philtor has quit [Read error: Operation timed out]