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)
<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
<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]