<eikke__>
pippijn: I expect custom rules to be required, but even then, I seem to be unable to get things to work
<eikke__>
case at hand: we have a custom preprocessor in our source tree, which uses camlp4of, which works just fine
<eikke__>
we used to have coverage checking with 'bisect', using -syntax and other arguments, but these seem to conflict with the '-pp' arguments added for our custom preprocessor
<eikke__>
basically: compilation with bisect succeeds, but running the thing results in an empty report, so I guess the '-pp' overrules '-syntax'
<Drup>
eikke__: do you have a nice working example with ocamlbuild (even better, oasis) with bisect ?
<Drup>
I was looking for one
siddharthv is now known as siddharthv_away
<eikke__>
Drup: there's some stuff in the manual
ontologiae has quit [Ping timeout: 240 seconds]
darkf has quit [Quit: Leaving]
michael_lee has quit [Read error: Connection reset by peer]
thomasga has joined #ocaml
avsm has joined #ocaml
divyanshu has quit [Quit: Computer has gone to sleep.]
ollehar has quit [Ping timeout: 252 seconds]
tulloch has quit [Ping timeout: 252 seconds]
tulloch has joined #ocaml
tnguyen has joined #ocaml
<eikke__>
is there a way to have multiple source 'paths' in an oasis file?
shinnya has joined #ocaml
ontologiae has joined #ocaml
<Drup>
eikke__: not really, but you can give a path for modules names
dotfelix has joined #ocaml
dotfelix has quit [Client Quit]
ustunozgur has quit [Remote host closed the connection]
lostcuaz has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
zarul has quit [Read error: Connection reset by peer]
studybot has joined #ocaml
studybot_ has joined #ocaml
manizzle has joined #ocaml
studybot has quit [Ping timeout: 240 seconds]
divyanshu has joined #ocaml
tnguyen has quit [Quit: tnguyen]
WraithM has quit [Ping timeout: 255 seconds]
pminten has joined #ocaml
pminten has quit [Client Quit]
arj has quit [Quit: Leaving.]
tidren has joined #ocaml
struktured has quit [Ping timeout: 255 seconds]
rgrinberg has joined #ocaml
zpe has quit [Remote host closed the connection]
tobiasBora has joined #ocaml
ustunozgur has joined #ocaml
ollehar has joined #ocaml
_andre has quit [Quit: leaving]
ollehar1 has joined #ocaml
Enjolras has quit [Read error: Connection reset by peer]
tane has joined #ocaml
divyanshu has quit [Ping timeout: 258 seconds]
zpe has joined #ocaml
divyanshu has joined #ocaml
Submarine has joined #ocaml
Submarine has joined #ocaml
ontologiae has quit [Ping timeout: 255 seconds]
struktured has joined #ocaml
ygrek has quit [Ping timeout: 252 seconds]
divyanshu has quit [Ping timeout: 250 seconds]
divyanshu has joined #ocaml
ustunozgur has quit [Remote host closed the connection]
Kakadu has quit [Quit: Page closed]
michael_lee has joined #ocaml
oriba has joined #ocaml
Kakadu has joined #ocaml
avsm1 has joined #ocaml
shinnya has quit [Ping timeout: 240 seconds]
olauzon has joined #ocaml
<Drup>
AltGr: do you want bug report for basic stuff broken on opam trunk ?
<Drup>
(just now, it was not updating a package archive while it was modified in opam repository)
<AltGr>
depends on what area ?
<AltGr>
hrm, yes, that sounds interesting
<Drup>
(I had to delete the tar.gz in .opam/archive to trigger the redownload)
<Drup>
ok, opening a bug report
avsm has quit [Ping timeout: 240 seconds]
<AltGr>
is there any support for wiki branches on github ?
<AltGr>
just rewrote a big part of opam's tutorial but some of it won't apply before 1.2 and at the moment it's invisible
lostcuaz has joined #ocaml
<avsm1>
AltGr: sadly not, i wanted the same thing for mirage
<avsm1>
put it up on your personal opam fork and send it to opam-devel for review?
<whitequark>
AltGr: I think you can access the wiki as a git archive
<whitequark>
git repo*
<whitequark>
while it may not be exposed in UI, that may make things simpler
roppongininja has quit [Ping timeout: 252 seconds]
<Anarchos>
I did the mistake to upgrade my ocaml version to daily one --> camlp5 does not compile anymore ---> unable to compile coq. Epic fail \o/
<whitequark>
camlp5 ಠ_ಠ
<whitequark>
coq still uses that, huh
<Anarchos>
it seems.
<whitequark>
by the way--any good Coq tutorial?
<whitequark>
I always wanted to play with it, but it's... quite esoteric
<Anarchos>
whitequark software foundations, Benjamin C. Pierce ?
Hannibal_Smith has joined #ocaml
<whitequark>
"I want to make a wobbly window with JavaScript" "here you are, five volumes of The Art of Programming"
Eyyub has joined #ocaml
adrien_oww has quit [Ping timeout: 250 seconds]
<Anarchos>
whitequark the art of *computer* programming ?
Mandus has quit [Read error: Operation timed out]
Mandus has joined #ocaml
<whitequark>
yes, yes
<Anarchos>
whitequark by our beloved Donald Knuth ?
<whitequark>
yes :)
<whitequark>
(it's called "TAOP" in Russian translation, I believe, hence the error.)
<Anarchos>
whitequark oh gavaritie li vouyi pa russkiy ?
<whitequark>
da
<Anarchos>
whitequark i bought a math book from russian teachers. Very impressive
tlockney_away is now known as tlockney
<whitequark>
what is?
mort___ has joined #ocaml
<ggole>
I think whitequark is asking for a less, uh, comprehensive approach to theorem proving.
<whitequark>
I am :)
<def-lkb>
SF is quite good to discover Coq. Otherwise, the CoqArt is a bit more direct, but harder. The french version is free online.
<def-lkb>
Not sure about the english one…
<whitequark>
SF?
<Anarchos>
whitequark software foundations, the book i referred to you
<def-lkb>
Software Foundations
<def-lkb>
yep
<whitequark>
oh
<def-lkb>
The last one I know is CPDT by Adam Chlipala. Good too, more practical
* whitequark
sighs
<whitequark>
let me elaborate
<whitequark>
I don't really want a comprehensive manual (which I will likely have to buy off Amazon, in paper, and wait a month for delivery)
<whitequark>
I want a blog post with a 40-minute introduction. Something like that. Just to get a grasp of how it works
<Anarchos>
whitequark there is none. You have to read first chapter of softaware foundastions, which took me only 3 weeks
<Anarchos>
whitequark you do'nt need to read all the book to get fluent in coq !
<whitequark>
only 3 weeks ಠ_ಠ
<whitequark>
ok, I guess I don't really want to play with it anymore
<def-lkb>
whitequark: in practice, SF & CPDT are quick, you don't need to get everything on first read.
<def-lkb>
CoqArt is much more involved.
<def-lkb>
And they can be read online. But yes, I don't think there is a "one blog post long" introduction to Coq :)
<whitequark>
ok, I see a pdf of CPDT. let's give it a try.
<whitequark>
I think there really should be, at least if there's some goal to get more people to use Coq :p
<whitequark>
perhaps if Coq is a part of your curriculum, then saying "just read this 400-page book" is ok. but not if you want to attract people who are just curious about it and/or more formal programming techniques...
<Anarchos>
whitequark i just said 'have a look on it',not 'you must read all the 400 pages'. If you fear difficulties you won't never success in everything, cause life is difficult to achieve :)
tobiasBora has quit [Ping timeout: 265 seconds]
maattdd has quit [Ping timeout: 258 seconds]
* whitequark
shrugs
<whitequark>
I don't fear difficulties, I see a time/benefit ratio
ustunozgur has quit [Remote host closed the connection]
<whitequark>
anyway, reading it already.
ustunozgur has joined #ocaml
<smondet>
whitequark: SF starts slowly very good introduction
eizo has joined #ocaml
<kakadu_>
CoqArt is not available online, isn't it?
<Anarchos>
whitequark SF is very interesting in its time/benefit ratio !!
<Anarchos>
kakadu_ only in french
kakadu_ is now known as Kakadu
<whitequark>
oh, I even bookmarked SF a long time ago
avsm has joined #ocaml
<whitequark>
hmm
roppongininja has joined #ocaml
<smondet>
whitequark: SF is the best book ever written on the whole of Computer Science, really worth the time !
<whitequark>
fine, fine, you've convinced me :D
nikki93 has quit [Remote host closed the connection]
<smondet>
:)
rgrinberg has quit [Read error: Connection reset by peer]
<whitequark>
tautologico: what do you think I'm doing right now?
<tautologico>
whitequark: very good, tell me when it's done and I'll test it
maattdd has joined #ocaml
<whitequark>
well, I'm fixing this one, rather
nikki93 has quit [Remote host closed the connection]
olauzon has quit [Ping timeout: 265 seconds]
eizo has quit [Ping timeout: 240 seconds]
<tautologico>
the repo even includes a Basics.v file that probably shouldn't be there
maattdd has quit [Ping timeout: 240 seconds]
araujo has joined #ocaml
araujo has quit [Max SendQ exceeded]
tulloch has quit [Ping timeout: 252 seconds]
araujo has joined #ocaml
<whitequark>
so horrible. it iterates the Coq output character by character, and to make ST responsive it makes a gettimeofday() call *before every single character* and returns if more than 1s has passed
* whitequark
tries not to cry.
<whitequark>
although, what should I expect if Coq-extracted code represents bytes by 8-tuples of booleans?
tobiasBora has joined #ocaml
nikki93 has joined #ocaml
tidren has joined #ocaml
Hannibal_Smith has quit [Quit: Sto andando via]
NoNNaN has quit [Ping timeout: 272 seconds]
tidren has quit [Ping timeout: 250 seconds]
ontologiae has quit [Ping timeout: 255 seconds]
NoNNaN has joined #ocaml
struktured has quit [Ping timeout: 240 seconds]
avsm has joined #ocaml
thomasga has quit [Quit: Leaving.]
ustunozg_ has joined #ocaml
claudiuc has joined #ocaml
<whitequark>
the " < " combination can't normally appear in Coq output, right?
ustunozgur has quit [Ping timeout: 240 seconds]
Eyyub has quit [Ping timeout: 240 seconds]
shinnya has quit [Ping timeout: 265 seconds]
claudiuc_ has joined #ocaml
claudiuc has quit [Ping timeout: 255 seconds]
shinnya has joined #ocaml
thomasga has joined #ocaml
mika1 has joined #ocaml
mika1 has quit [Client Quit]
ikaros has quit [Ping timeout: 264 seconds]
thomasga has quit [Client Quit]
Eyyub has joined #ocaml
thomasga has joined #ocaml
iorivur has quit [Read error: Connection reset by peer]
ikaros has joined #ocaml
ikaros has quit [Client Quit]
tulloch has joined #ocaml
racycle_ has joined #ocaml
tidren has joined #ocaml
ontologiae has joined #ocaml
tidren has quit [Ping timeout: 252 seconds]
tianon has quit [Ping timeout: 246 seconds]
lostcuaz has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
tulloch has quit [Read error: Connection reset by peer]
tulloch has joined #ocaml
ollehar has quit [Ping timeout: 252 seconds]
maattdd has joined #ocaml
ustunozg_ has quit [Remote host closed the connection]
maattdd has quit [Ping timeout: 258 seconds]
zpe has quit [Remote host closed the connection]
tianon has joined #ocaml
roppongininja has quit [Remote host closed the connection]
roppongininja has joined #ocaml
darkf has joined #ocaml
* whitequark
sighs
<whitequark>
tautologico: I entirely rewrote its IO handling, now it works well
<whitequark>
the keybindings on linux are still kinda broken, though
roppongininja has quit [Remote host closed the connection]
roppongininja has joined #ocaml
avsm has quit [Quit: Leaving.]
roppongininja has quit [Ping timeout: 240 seconds]
madroach has quit [Ping timeout: 252 seconds]
madroach has joined #ocaml
PryMar56 has joined #ocaml
tobiasBora has quit [Quit: Konversation terminated!]
NoNNaN has quit [Remote host closed the connection]
tidren has joined #ocaml
NoNNaN has joined #ocaml
<tautologico>
whitequark: cool, will test it later