00:00
ankit9 has joined #ocaml
00:07
lggr has quit [Ping timeout: 248 seconds]
00:09
lggr has joined #ocaml
00:18
lggr has quit [Ping timeout: 252 seconds]
00:20
lggr has joined #ocaml
00:27
lggr has quit [Ping timeout: 268 seconds]
00:35
lggr has joined #ocaml
00:40
Anarchos has quit [Quit: Vision[0.9.7-H-090423]: i've been blurred!]
00:44
lggr has quit [Ping timeout: 252 seconds]
00:47
lggr has joined #ocaml
00:48
lopex has joined #ocaml
00:54
lggr has quit [Ping timeout: 252 seconds]
00:58
lggr has joined #ocaml
01:05
lggr has quit [Ping timeout: 260 seconds]
01:10
abeaulieu has quit [Ping timeout: 246 seconds]
01:12
abeaulieu has joined #ocaml
01:13
lggr has joined #ocaml
01:20
madroach has quit [Ping timeout: 265 seconds]
01:21
lggr has quit [Ping timeout: 244 seconds]
01:21
madroach has joined #ocaml
01:31
lggr has joined #ocaml
01:39
lggr has quit [Ping timeout: 272 seconds]
01:41
lggr has joined #ocaml
01:45
wtetzner has joined #ocaml
01:49
lggr has quit [Ping timeout: 260 seconds]
01:55
lggr has joined #ocaml
02:02
lggr has quit [Ping timeout: 260 seconds]
02:11
lggr has joined #ocaml
02:14
Playground has joined #ocaml
02:18
lggr has quit [Ping timeout: 248 seconds]
02:22
lggr has joined #ocaml
02:27
Playground has quit [Ping timeout: 248 seconds]
02:28
lggr has quit [Ping timeout: 245 seconds]
02:33
lggr has joined #ocaml
02:38
Playground has joined #ocaml
02:43
lggr has quit [Ping timeout: 260 seconds]
02:44
lggr has joined #ocaml
02:44
mattrepl has quit [Quit: mattrepl]
02:54
lggr has quit [Ping timeout: 272 seconds]
02:55
lggr has joined #ocaml
03:03
lggr has quit [Ping timeout: 246 seconds]
03:13
lggr has joined #ocaml
03:22
lggr has quit [Ping timeout: 240 seconds]
03:23
Playground has quit [Quit: lag]
03:24
lggr has joined #ocaml
03:31
lggr has quit [Ping timeout: 246 seconds]
03:33
lggr has joined #ocaml
03:42
lggr has quit [Ping timeout: 244 seconds]
03:43
Playground has joined #ocaml
03:44
lggr has joined #ocaml
03:49
cdidd has joined #ocaml
03:53
Ptival has joined #ocaml
03:53
lggr has quit [Ping timeout: 252 seconds]
03:55
lggr has joined #ocaml
04:02
lggr has quit [Ping timeout: 246 seconds]
04:03
lggr has joined #ocaml
04:12
lggr has quit [Ping timeout: 246 seconds]
04:14
lggr has joined #ocaml
04:24
lggr has quit [Ping timeout: 268 seconds]
04:26
lggr has joined #ocaml
04:30
Ptival has quit [Quit: Quat]
04:33
lggr has quit [Ping timeout: 246 seconds]
04:35
lggr has joined #ocaml
04:44
lggr has quit [Ping timeout: 255 seconds]
04:46
lggr has joined #ocaml
04:47
tufisi has joined #ocaml
04:55
lggr has quit [Ping timeout: 252 seconds]
04:57
lggr has joined #ocaml
05:03
osa1 has quit [Quit: Konversation terminated!]
05:06
lggr has quit [Ping timeout: 255 seconds]
05:08
lggr has joined #ocaml
05:08
thelema_ has quit [Read error: Connection reset by peer]
05:10
jonafan has quit [Ping timeout: 264 seconds]
05:10
jonafan has joined #ocaml
05:13
thelema has joined #ocaml
05:17
lggr has quit [Ping timeout: 268 seconds]
05:19
othiym23 has quit [Ping timeout: 276 seconds]
05:19
lggr has joined #ocaml
05:25
lggr has quit [Ping timeout: 244 seconds]
05:33
lggr has joined #ocaml
05:43
lggr has quit [Ping timeout: 264 seconds]
05:44
lggr has joined #ocaml
05:52
lggr has quit [Ping timeout: 240 seconds]
05:53
Playground has quit [Ping timeout: 244 seconds]
05:55
Playground has joined #ocaml
05:59
lggr has joined #ocaml
06:01
pqmodn_ has quit [Changing host]
06:01
pqmodn_ has joined #ocaml
06:01
pqmodn_ is now known as pqmodn
06:04
avsm1 has joined #ocaml
06:07
lggr has quit [Ping timeout: 268 seconds]
06:10
Playground has quit [Ping timeout: 272 seconds]
06:14
lggr has joined #ocaml
06:16
Playground has joined #ocaml
06:20
avsm1 has quit [Quit: Leaving.]
06:20
avsm has joined #ocaml
06:23
lggr has quit [Ping timeout: 260 seconds]
06:24
avsm has quit [Ping timeout: 244 seconds]
06:25
lggr has joined #ocaml
06:30
Playground has quit [Read error: Connection reset by peer]
06:34
lggr has quit [Ping timeout: 244 seconds]
06:36
lggr has joined #ocaml
06:42
eni has joined #ocaml
06:44
othiym23 has joined #ocaml
06:45
lggr has quit [Ping timeout: 260 seconds]
06:47
lggr has joined #ocaml
06:47
pango is now known as pangoafk
06:55
lggr has quit [Ping timeout: 252 seconds]
06:57
eni has quit [Ping timeout: 240 seconds]
07:01
lggr has joined #ocaml
07:06
Catnaroek has joined #ocaml
07:10
djcoin has joined #ocaml
07:10
lggr has quit [Ping timeout: 264 seconds]
07:12
lggr has joined #ocaml
07:14
BiDOrD has joined #ocaml
07:17
BiDOrD_ has quit [Ping timeout: 252 seconds]
07:19
lggr has quit [Ping timeout: 244 seconds]
07:20
lggr has joined #ocaml
07:21
ftrvxmtrx has joined #ocaml
07:30
lggr has quit [Ping timeout: 255 seconds]
07:31
lggr has joined #ocaml
07:38
lggr has quit [Ping timeout: 272 seconds]
07:41
eni has joined #ocaml
07:43
ankit9 has quit [Read error: Connection reset by peer]
07:44
lggr has joined #ocaml
07:49
osa1 has joined #ocaml
07:51
lggr has quit [Ping timeout: 246 seconds]
07:53
lggr has joined #ocaml
07:59
ankit9 has joined #ocaml
07:59
ankit9 has quit [Client Quit]
08:02
lggr has quit [Ping timeout: 252 seconds]
08:04
lggr has joined #ocaml
08:04
ankit9 has joined #ocaml
08:13
lggr has quit [Ping timeout: 248 seconds]
08:13
Yoric has joined #ocaml
08:17
lggr has joined #ocaml
08:18
ontologiae has joined #ocaml
08:21
lggr has quit [Ping timeout: 240 seconds]
08:27
Yoric has quit [Remote host closed the connection]
08:28
Yoric has joined #ocaml
08:35
lggr has joined #ocaml
08:42
ontologiae has quit [Ping timeout: 246 seconds]
08:45
lggr has quit [Ping timeout: 272 seconds]
08:46
lggr has joined #ocaml
08:56
lggr has quit [Ping timeout: 272 seconds]
08:57
lggr has joined #ocaml
09:04
lggr has quit [Ping timeout: 260 seconds]
09:07
fasta has quit [Remote host closed the connection]
09:07
fasta has joined #ocaml
09:07
iZsh has quit [Ping timeout: 240 seconds]
09:08
lggr has joined #ocaml
09:08
err404 has joined #ocaml
09:11
ski has quit [Ping timeout: 260 seconds]
09:11
iZsh has joined #ocaml
09:17
lggr has quit [Ping timeout: 248 seconds]
09:19
lggr has joined #ocaml
09:23
osa1 has quit [Quit: Konversation terminated!]
09:26
lggr has quit [Ping timeout: 246 seconds]
09:29
ankit9 has quit [Ping timeout: 260 seconds]
09:32
ontologiae has joined #ocaml
09:35
lggr has joined #ocaml
09:41
ankit9 has joined #ocaml
09:42
lggr has quit [Ping timeout: 244 seconds]
09:43
lggr has joined #ocaml
09:48
joewilliams has quit [Remote host closed the connection]
09:48
lopex has quit [Remote host closed the connection]
09:48
bobry has quit [Write error: Broken pipe]
09:51
lggr has quit [Ping timeout: 244 seconds]
09:52
adrien has quit [Ping timeout: 268 seconds]
09:52
joewilliams has joined #ocaml
09:52
lggr has joined #ocaml
09:55
adrien has joined #ocaml
09:59
lggr has quit [Ping timeout: 246 seconds]
10:02
eni has quit [Ping timeout: 245 seconds]
10:04
ankit9 has quit [Ping timeout: 240 seconds]
10:07
lggr has joined #ocaml
10:07
bobry has joined #ocaml
10:10
ontologi1e has joined #ocaml
10:13
ontologiae has quit [Ping timeout: 255 seconds]
10:13
lggr has quit [Ping timeout: 240 seconds]
10:14
ollehar has joined #ocaml
10:17
ontologi1e has quit [Read error: Connection reset by peer]
10:17
ankit9 has joined #ocaml
10:17
ontologiae has joined #ocaml
10:19
lopex has joined #ocaml
10:22
lggr has joined #ocaml
10:28
jathd has joined #ocaml
10:31
lggr has quit [Ping timeout: 248 seconds]
10:32
lggr has joined #ocaml
10:39
ankit9 has quit [Read error: Connection reset by peer]
10:41
lggr has quit [Ping timeout: 240 seconds]
10:44
lggr has joined #ocaml
10:53
lggr has quit [Ping timeout: 255 seconds]
10:55
lggr has joined #ocaml
10:56
err404 has quit [Remote host closed the connection]
10:59
_andre has joined #ocaml
11:02
lggr has quit [Ping timeout: 246 seconds]
11:04
larhat has quit [Quit: Leaving.]
11:06
lggr has joined #ocaml
11:11
sgnb`` is now known as sgnb
11:13
lggr has quit [Ping timeout: 240 seconds]
11:20
lggr has joined #ocaml
11:29
lggr has quit [Ping timeout: 240 seconds]
11:31
lggr has joined #ocaml
11:40
lggr has quit [Ping timeout: 244 seconds]
11:41
lggr has joined #ocaml
11:42
<
hcarty >
thelema: I have an untested patch to fix compilation of the Cairo bindings under OCaml 4.00.0
11:44
<
hcarty >
thelema: "untested" in that I it builds and installs, but I haven't tested the bindings yet
11:47
dwmw2_gone has quit [Ping timeout: 260 seconds]
11:49
lggr has quit [Ping timeout: 272 seconds]
11:53
lggr has joined #ocaml
12:00
lggr has quit [Ping timeout: 246 seconds]
12:00
larhat has joined #ocaml
12:03
gnuvince has quit [Ping timeout: 252 seconds]
12:04
<
adrien >
cairo "1"?
12:04
<
hcarty >
adrien: cairo2
12:05
<
adrien >
oh, only a bit surprised
12:06
<
hcarty >
adrien: It has a pretty heavily customized setup.ml so a 'oasis setup' with oasis 0.3.0 didn't do the trick as it might have otherwise.
12:08
<
adrien >
ah, yeah, not suprised for that :P
12:10
lggr has joined #ocaml
12:13
eni has joined #ocaml
12:15
avsm has joined #ocaml
12:15
avsm has quit [Client Quit]
12:20
lggr has quit [Ping timeout: 260 seconds]
12:22
lggr has joined #ocaml
12:29
lggr has quit [Ping timeout: 260 seconds]
12:31
sepp2k has joined #ocaml
12:37
tufisi has quit [Quit: ...]
12:37
lggr has joined #ocaml
12:39
tufisi has joined #ocaml
12:39
mnabil has joined #ocaml
12:39
dwmw2_gone has joined #ocaml
12:40
gnuvince has joined #ocaml
12:43
Snark_ has joined #ocaml
12:47
lggr has quit [Ping timeout: 260 seconds]
12:49
lggr has joined #ocaml
12:52
tufisi has quit [Quit: ...]
12:55
tufisi has joined #ocaml
12:59
lggr has quit [Ping timeout: 268 seconds]
13:00
lggr has joined #ocaml
13:01
tufisi has quit [Quit: ...]
13:02
tufisi has joined #ocaml
13:05
fraggle_laptop has joined #ocaml
13:07
lggr has quit [Ping timeout: 240 seconds]
13:16
lggr has joined #ocaml
13:19
Catnaroek has quit [Ping timeout: 268 seconds]
13:20
fraggle_ has quit [Ping timeout: 240 seconds]
13:21
ontologiae has quit [Ping timeout: 240 seconds]
13:22
jave has quit [Ping timeout: 244 seconds]
13:23
ontologiae has joined #ocaml
13:23
lggr has quit [Ping timeout: 260 seconds]
13:27
osa1 has joined #ocaml
13:27
lggr has joined #ocaml
13:28
Playground has joined #ocaml
13:28
gnuvince has quit [Ping timeout: 245 seconds]
13:30
gnuvince has joined #ocaml
13:31
jave has joined #ocaml
13:32
lggr has quit [Ping timeout: 245 seconds]
13:33
fraggle_ has joined #ocaml
13:38
lggr has joined #ocaml
13:48
lggr has quit [Ping timeout: 252 seconds]
13:49
lggr has joined #ocaml
13:52
Playground has quit [Quit: brb]
13:59
lggr has quit [Ping timeout: 245 seconds]
14:01
lggr has joined #ocaml
14:08
lggr has quit [Ping timeout: 255 seconds]
14:08
ontologiae has quit [Read error: Connection reset by peer]
14:08
ontologiae has joined #ocaml
14:12
lggr has joined #ocaml
14:19
lggr has quit [Ping timeout: 260 seconds]
14:20
fraggle_laptop has quit [Ping timeout: 240 seconds]
14:26
lggr has joined #ocaml
14:32
larhat has quit [Read error: Connection reset by peer]
14:32
larhat1 has joined #ocaml
14:33
mattrepl has joined #ocaml
14:33
lggr has quit [Ping timeout: 264 seconds]
14:38
ftrvxmtrx has quit [Quit: Leaving]
14:41
Yoric has quit [Ping timeout: 246 seconds]
14:42
lggr has joined #ocaml
14:46
Snark_ is now known as Snark
14:48
fraggle_laptop has joined #ocaml
14:51
lggr has quit [Ping timeout: 240 seconds]
14:53
lggr has joined #ocaml
15:00
lggr has quit [Ping timeout: 244 seconds]
15:02
err404 has joined #ocaml
15:04
lggr has joined #ocaml
15:11
lggr has quit [Ping timeout: 244 seconds]
15:12
Ptival has joined #ocaml
15:12
Yoric has joined #ocaml
15:14
ollehar has quit [Ping timeout: 252 seconds]
15:18
lggr has joined #ocaml
15:20
gnuvince has quit [Ping timeout: 255 seconds]
15:23
lggr has quit [Ping timeout: 260 seconds]
15:24
gnuvince has joined #ocaml
15:35
lggr has joined #ocaml
15:42
lggr has quit [Ping timeout: 260 seconds]
15:49
Ptival has quit [Read error: Connection reset by peer]
15:51
lggr has joined #ocaml
16:01
lggr has quit [Ping timeout: 264 seconds]
16:09
lggr has joined #ocaml
16:16
lggr has quit [Ping timeout: 240 seconds]
16:16
ontologiae has quit [Ping timeout: 252 seconds]
16:19
ulfdoz has joined #ocaml
16:20
lggr has joined #ocaml
16:27
lggr has quit [Ping timeout: 240 seconds]
16:31
eni has quit [Ping timeout: 256 seconds]
16:32
Cyanure has joined #ocaml
16:33
osa1 has quit [Quit: Konversation terminated!]
16:37
sepp2k1 has joined #ocaml
16:37
lggr has joined #ocaml
16:38
sepp2k has quit [Ping timeout: 264 seconds]
16:45
lggr has quit [Ping timeout: 272 seconds]
16:48
lggr has joined #ocaml
16:52
eni has joined #ocaml
16:52
osa1 has joined #ocaml
16:52
Ptival has joined #ocaml
16:55
lggr has quit [Ping timeout: 252 seconds]
17:00
pangoafk is now known as pango
17:04
fraggle_laptop has quit [Read error: Connection reset by peer]
17:05
lggr has joined #ocaml
17:07
ski has joined #ocaml
17:12
lggr has quit [Ping timeout: 245 seconds]
17:12
Ptival has quit [Ping timeout: 252 seconds]
17:16
lggr has joined #ocaml
17:22
eni has quit [Ping timeout: 272 seconds]
17:25
lggr has quit [Ping timeout: 248 seconds]
17:26
gnuvince has quit [Ping timeout: 244 seconds]
17:27
lggr has joined #ocaml
17:28
Yoric has quit [Ping timeout: 246 seconds]
17:31
Ptival has joined #ocaml
17:32
Yoric has joined #ocaml
17:35
lggr has quit [Ping timeout: 272 seconds]
17:36
emmanuelux has quit [Quit: emmanuelux]
17:38
lggr has joined #ocaml
17:44
Snark has quit [Quit: Quitte]
17:46
lggr has quit [Ping timeout: 264 seconds]
17:49
gnuvince has joined #ocaml
17:58
lggr has joined #ocaml
18:05
lggr has quit [Ping timeout: 240 seconds]
18:09
lggr has joined #ocaml
18:10
emmanuelux has joined #ocaml
18:12
sivoais has quit [Read error: Connection reset by peer]
18:13
sivoais has joined #ocaml
18:17
lggr has quit [Ping timeout: 264 seconds]
18:24
fraggle_ has quit [Ping timeout: 250 seconds]
18:26
lggr has joined #ocaml
18:29
fraggle_ has joined #ocaml
18:34
lggr has quit [Ping timeout: 255 seconds]
18:41
lggr has joined #ocaml
18:47
djcoin has quit [Quit: WeeChat 0.3.7]
18:48
Yoric has quit [Ping timeout: 246 seconds]
18:49
lggr has quit [Ping timeout: 264 seconds]
18:58
lggr has joined #ocaml
19:08
larhat1 has quit [Quit: Leaving.]
19:08
lggr has quit [Ping timeout: 272 seconds]
19:09
lggr has joined #ocaml
19:11
Ptival has quit [Ping timeout: 248 seconds]
19:18
lggr has quit [Ping timeout: 240 seconds]
19:19
Yoric has joined #ocaml
19:20
lggr has joined #ocaml
19:24
Anarchos has joined #ocaml
19:25
gnuvince has quit [Ping timeout: 246 seconds]
19:26
ftrvxmtrx has joined #ocaml
19:28
lggr has quit [Ping timeout: 244 seconds]
19:35
lggr has joined #ocaml
19:40
osa1 has quit [Quit: Konversation terminated!]
19:42
lggr has quit [Ping timeout: 246 seconds]
19:47
lggr has joined #ocaml
19:47
Yoric has quit [Ping timeout: 246 seconds]
19:56
lggr has quit [Ping timeout: 264 seconds]
19:58
lggr has joined #ocaml
20:07
eni has joined #ocaml
20:07
lggr has quit [Ping timeout: 248 seconds]
20:08
gnuvince has joined #ocaml
20:10
lggr has joined #ocaml
20:11
_andre has quit [Quit: leaving]
20:17
lggr has quit [Ping timeout: 240 seconds]
20:26
larhat has joined #ocaml
20:26
lggr has joined #ocaml
20:34
lggr has quit [Ping timeout: 244 seconds]
20:37
chispita has joined #ocaml
20:37
<
chispita >
How do I translate an ocaml routine to Coq .v file?
20:40
lggr has joined #ocaml
20:41
<
chispita >
How do I translate an ocaml routine to Coq?
20:42
<
chispita >
(not .v file)
20:48
lggr has quit [Ping timeout: 272 seconds]
20:50
Xizor has joined #ocaml
20:52
lggr has joined #ocaml
20:52
Cyanure has quit [Remote host closed the connection]
20:55
<
Anarchos >
chispita can you explain ?
20:55
<
Anarchos >
with the Definition keyword maybe ?
20:57
<
chispita >
Anarchos: I have a simple function in OCaml, just a few lines. I'd like to send it to Coq for a formal proof.
20:58
<
chispita >
Anarchos: is there a translator from OCaml to Coq proofs?
20:58
<
Anarchos >
chispita it is a nonsense
20:58
<
Anarchos >
you have to make your need more precise
20:59
lggr has quit [Ping timeout: 244 seconds]
21:00
Ptival has joined #ocaml
21:02
<
chispita >
Since I cannot write it in Coq(because I have been trying the past 4 weeks) I would like to translate the OCaml to Coq
21:03
<
Anarchos >
chispita i am not skilled enough to help you sorry
21:03
lggr has joined #ocaml
21:05
<
chispita >
In 4 weeks requesting help on these chat rooms, only one guy in the #coq room offered me help.
21:05
<
Anarchos >
chispita did you try the#coq channel ?
21:05
<
chispita >
Anarchos: yes, I remember you from there
21:05
<
Anarchos >
wops interlacing
21:06
<
chispita >
The single Coq book costs U$ 110. There is no help on these chat rooms. The language is very difficult and complicated. I should just give up and use something else.
21:06
<
chispita >
OCaml and Coq will never be mainstream this way
21:07
<
Anarchos >
chispita do you read french ?
21:07
<
Anarchos >
chispita coq is a vey different paradigm in which you can make logical construcive demonstration
21:07
<
chispita >
Anarchos: no French....
21:07
<
Anarchos >
chispita coq is not intended to be an IDE !
21:07
<
chispita >
Unfortunately.
21:07
<
Anarchos >
chispita the generation of the code from a proof is a side effect of curry-howard isomorphism
21:08
<
chispita >
But if I need to prove an external program with it, is it possible?
21:08
<
Anarchos >
chispita but going backwards is pretty undefined unless you tell what you want to do with the corresponding proof !
21:08
larhat has quit [Ping timeout: 240 seconds]
21:08
<
Anarchos >
chispita the very question is : what do you want to proove ?
21:09
<
chispita >
I would like to prove that a list nat -> listnat ->listnat is sorted after it is returned by that function.
21:10
<
chispita >
i have built sorted lists by hand, and proved it
21:10
<
chispita >
1 :: 2 :: 3 :: 4 :: [] is sorted
21:10
<
chispita >
but i need a function that now takes 2 :: 5 :: 1 :: [] and returns 1 :: 2 :: 5 :: []
21:10
<
chispita >
i can't do that...
21:10
lggr has quit [Ping timeout: 240 seconds]
21:11
<
Anarchos >
chispita you will have to specify the logical formula meaning : list is sorted...
21:11
<
chispita >
i have that one!
21:12
eni has quit [Ping timeout: 245 seconds]
21:12
<
Anarchos >
the proof you want is a really difficult in coq for a beginner
21:12
<
Ptival >
chispita: what kind of sort did you write?
21:12
<
Anarchos >
Ptival help him cause i am unable ....
21:12
<
Ptival >
there are some sorts that will be hard to make Coq accept, for termination-checking reasons
21:13
<
Ptival >
I can probably help, and have nothing better to do at the moment :)
21:15
<
chispita >
Ptival: hopefully you can help me....i am unable to learn this unless i have a practical example...
21:16
<
chispita >
i have lists. i can prove those lists are sorted, equivalent, transitive
21:16
<
chispita >
so if i build a list by hand and Eval compute in LIST it works ok
21:16
<
chispita >
apply is_sorted.
21:17
<
chispita >
now. given a list like 2 :: 5 :: 1 :: [] i need to specify a function that returns 1 :: 2 :: 5 :: []
21:17
<
chispita >
i thought i could import from OCaml, since my Coq language skills are limited
21:19
<
Anarchos >
chispita Definition f : fun nat list -> nat list := fun l => <sorted l to implement like in caml>
21:20
lggr has joined #ocaml
21:20
<
chispita >
Does Coq recognize the OCaml syntax?
21:21
<
chispita >
(Thanks, Anarchos, you Ptival and I think ziman from #coq were the only ones who helped me)
21:22
<
Anarchos >
chispita no for the syntax, but is really close
21:22
<
Anarchos >
chispita #coq is a low traffic channel :)
21:22
<
chispita >
Anarchos: my problem is not the logic, or the idea in Coq, it is the language
21:22
<
Anarchos >
chispita for the syntax you can find samples in english on google i guess
21:22
<
chispita >
Anarchos: yes, understood about #coq....unfortunately...i think this is a great technology that deserved more publicity
21:23
<
Anarchos >
chispita sure but not easy as it is so new for mainstream programmers
21:23
<
Anarchos >
chispita and language is very demanding to understand
21:24
<
chispita >
Anarchos: understood
21:24
<
chispita >
Anarchos: it is a bit frustrating in the beginning i guess?
21:25
<
Anarchos >
chispita yes it is, but when you begin to follow tutorials it is very addicting :)
21:25
<
chispita >
Anarchos: is there a bubblesort in coq somewhere?
21:25
<
Anarchos >
chispita no idea
21:25
<
chispita >
Anarchos: tutorial, i mean, so i can follow?
21:27
lggr has quit [Ping timeout: 245 seconds]
21:31
lggr has joined #ocaml
21:33
eni has joined #ocaml
21:41
lggr has quit [Ping timeout: 255 seconds]
21:43
lggr has joined #ocaml
21:43
Tobu has quit [Remote host closed the connection]
21:44
Tobu has joined #ocaml
21:48
ontologiae has joined #ocaml
21:50
cabbagebot has joined #ocaml
21:52
lggr has quit [Ping timeout: 255 seconds]
21:55
lggr has joined #ocaml
21:59
<
Ptival >
chispita: sorry, was afk, reading up :)
22:00
<
chispita >
Ptival: no problem. studying coq here in the meantime
22:00
<
Ptival >
chispita: do you have your OCaml code somewhere?
22:01
<
chispita >
i want to test this: give a function 2 :: 5 :: 1 :: [] then when i do Eval compute in myfunction 2 :: 5 :: 1 :: [] it gives me 1 :: 2 :: 5 :: []
22:01
<
Ptival >
there is a merge sort in the stdlib
22:02
<
chispita >
Ptival: i found that too. i'd like to write my own....so i can modify it and learn
22:05
lggr has quit [Ping timeout: 264 seconds]
22:07
lggr has joined #ocaml
22:08
<
chispita >
Ptival: basically i would like to understand how to translate my non-functional ideas to Coq
22:09
<
chispita >
Ptival: so for that, i need to get my head to understand Coq. if i use a library function(i have read it on coq.inria.fr) I would just be a user...i would like to understand it...
22:10
wtetzner has quit [Read error: Connection reset by peer]
22:12
wtetzner has joined #ocaml
22:12
<
chispita >
Ptival: nice! What is happening there?!
22:15
<
chispita >
understand this: let fix _bsort s :=
22:15
lggr has quit [Ping timeout: 248 seconds]
22:15
<
chispita >
in fact from match s with down i understand everything !
22:15
<
chispita >
i just don't understand this: Fixpoint bsort {t} eq (gt: t -> t -> bool) s :=
22:16
<
chispita >
Fixpoint declares a recursive function. bsord is the name. from {t} eq (gt: t -> t -> bool) s I don't get it :(
22:16
<
Anarchos >
fixpoint is like let rec
22:19
lggr has joined #ocaml
22:20
ftrvxmtrx has quit [Ping timeout: 250 seconds]
22:24
cabbagebot has quit [Ping timeout: 272 seconds]
22:25
<
chispita >
let rec = let recursive?
22:26
lggr has quit [Ping timeout: 252 seconds]
22:27
<
Anarchos >
chispita let rec as in ocaml
22:27
<
chispita >
Anarchos: got it ;)
22:28
<
chispita >
If one knows OCaml then Coq becomes a lot easier, right?
22:28
<
Anarchos >
chispita right
22:28
<
Anarchos >
chispita but objects or imperative features are not needed, only the functional paradigm
22:30
<
chispita >
understood.
22:32
cabbageb1t has joined #ocaml
22:34
lggr has joined #ocaml
22:41
lggr has quit [Ping timeout: 244 seconds]
22:43
lggr has joined #ocaml
22:47
cabbageb1t has quit [Ping timeout: 248 seconds]
22:53
eni has quit [Quit: Leaving]
22:53
lggr has quit [Ping timeout: 245 seconds]
22:55
lggr has joined #ocaml
22:59
<
Ptival >
I just passed eq (the equality comparison) and gt (the comparison) as arguments to bsort
22:59
<
Ptival >
because there is no polymorphic comparison available in Coq
23:00
<
Ptival >
chispita: the problem is, Coq does not accept this definition because of how the recursive calls are done
23:01
<
Ptival >
so you would probably have to specify a termination argument
23:02
lggr has quit [Ping timeout: 252 seconds]
23:06
hongboz has joined #ocaml
23:06
lggr has joined #ocaml
23:09
<
chispita >
Ptival: I can't seem to compile the function you sent over :(
23:09
hongboz has quit [Remote host closed the connection]
23:09
<
chispita >
Recursive definition of _bsort is ill-formed.
23:09
<
chispita >
Recursive call to _bsort has principal argument equal to "x :: xs" instead of one of the following variables: "l" "xs".
23:13
ontologiae has quit [Ping timeout: 260 seconds]
23:13
<
Ptival >
that's what I mentioned
23:14
<
Ptival >
the problem is, in Coq, you can only define recursive functions who recur in a structurally-decreasing fashion
23:14
<
chispita >
Ptival: hmm.
23:15
<
chispita >
I read about that, so they're not infinite
23:15
lggr has quit [Ping timeout: 255 seconds]
23:16
<
chispita >
what does the " in " after the let fix do?
23:16
<
Ptival >
but in this case, unfortunately, you want recursion that is founded on some other argument
23:16
<
chispita >
Ptival: understood
23:16
<
Ptival >
oh, it's just the "in" that goes with the "let"
23:16
<
chispita >
yes but what is it? i don't understand that part of the let
23:17
<
Ptival >
to define _bsort as a local function
23:17
<
Ptival >
I don't understand what you don't understand
23:17
<
chispita >
i am so lost, i am unable to explain myself lol
23:17
<
Ptival >
it's just like in OCaml
23:17
<
chispita >
let ..... in THIS HERE. what does the THIS HERE clause do?
23:19
larhat has joined #ocaml
23:19
<
Ptival >
THIS HERE is the actual term
23:19
<
Ptival >
(let foo = bar in 42) is 42
23:20
<
Ptival >
(let foo = bar in 42 + foo) is (42 + bar)
23:20
<
Ptival >
do you understand the OCaml bubble sort code you linked earlier?
23:20
<
chispita >
no ! is it too much trouble to ask for a brief explanation?
23:20
<
Ptival >
no it's not
23:21
<
Ptival >
you're learning OCaml too then?
23:21
<
chispita >
in reality, i am trying to learn Coq, but i understand zero of the language....
23:21
<
chispita >
the logic is ok.
23:21
<
chispita >
tactics = ok
23:21
<
chispita >
i have proved over 200 little exercizes
23:21
<
chispita >
but then the language....i am weak in functional programming...
23:22
<
chispita >
i assume OCaml is good to learn Coq?
23:22
<
Ptival >
it's very similar (for the definition of functions part)
23:22
<
Ptival >
so basically let is used to name things
23:22
<
Ptival >
let some_name = some_computation in something
23:23
<
Ptival >
something can refer to some_name whenever it wants to refer to the result of some_computation
23:24
lggr has joined #ocaml
23:25
<
chispita >
ok. farther down in the program, how do you employ some_name?
23:25
<
chispita >
or don't you?
23:25
<
Ptival >
you just write some_name
23:26
<
chispita >
when you write some_name. the return from that is something. right?
23:26
<
Ptival >
so for instance in that bsort code
23:26
<
Ptival >
first it defines a local _bsort function
23:26
<
Ptival >
that's all the lines from the first "let" to the first "in"
23:27
<
Ptival >
then the rest is
23:27
<
Ptival >
let t = _bsort s in (if t = s then t else bsort t)
23:28
<
Ptival >
so the three occurences of t inside the parentheses could be replaced by (_bsort s)
23:28
<
Ptival >
but the advantage of having the let is, first, that you type (_bsort s) only once, and only have to type t whenever you want to refer to it
23:28
<
Ptival >
and second, t is only computed once
23:29
<
Ptival >
while, if you had (if _bsort s = s then _bsort s else bsort (_bsort s))
23:29
Tobu has quit [Read error: Connection reset by peer]
23:29
<
Ptival >
then _bsort s would be computed twice
23:29
Tobu has joined #ocaml
23:29
<
Ptival >
once for the condition, and once again in the taken branch
23:30
<
Ptival >
for a simpler example
23:30
<
chispita >
following you
23:30
<
Ptival >
let fib10 = fib 10 in fib10 + fib10 (* computes fib 10 once *)
23:30
<
Ptival >
fib 10 + fib 10 (* computes fib 10 once *)
23:31
<
Ptival >
so you can name intermediate results using this let ... in ... syntax
23:31
<
Ptival >
and they will be computed once and for all
23:31
lggr has quit [Ping timeout: 252 seconds]
23:31
<
Ptival >
and you can give them nifty names that help simplifying the following code
23:33
<
chispita >
you've made it so much clearer. re-reading the bsort function now starts to make sense
23:33
<
Ptival >
so the first "let" actually does not define a constant, but a local function
23:34
<
Ptival >
the syntax is let <name> <arg1> ... <argn> = <body> in <body of the whole thing which may call "name">
23:38
<
chispita >
the "immediate" thing that is executed is after IN right? the stuff between let ....HERE... in is the definition that the stuff after ... in ...HERE ... will use?
23:41
lggr has joined #ocaml
23:42
Anarchos has quit [Quit: Vision[0.9.7-H-090423]: i've been blurred!]
23:43
<
chispita >
Ptival: time to go back to study this more! thanks for your help, this really cleared lots of things up!
23:43
<
chispita >
Anarchos: thanks as well for your help.
23:47
mattrepl has quit [Quit: mattrepl]
23:48
<
Ptival >
chispita: it depends on whether it's a let constant = ... or a let function x y = ...
23:49
<
Ptival >
if you write 'let blarg = computation1 in computation2' in OCaml
23:49
<
Ptival >
then computation1 is first executed
23:49
<
Ptival >
even if computation2 does not refer to blarg
23:49
<
Ptival >
(unless it's optimized away by the compiler, but I guess it's not since OCaml is not pure)
23:50
emmanuelux has quit [Ping timeout: 246 seconds]
23:50
<
Ptival >
but what the whole thing returns is the result of computation2
23:50
lggr has quit [Ping timeout: 252 seconds]
23:50
<
Ptival >
it's a bit different in another language called Haskell that is lazy
23:55
lggr has joined #ocaml