mfurr changed the topic of #ocaml to: OCaml 3.08.2 available! | Archive of Caml Weekly News: http://sardes.inrialpes.fr/~aschmitt/cwn/ | A free book: http://cristal.inria.fr/~remy/cours/appsem/ | Mailing List: http://caml.inria.fr/bin/wilma/caml-list/ | Cookbook: http://pleac.sourceforge.net/
ne1 has quit ["Few people understand understanding."]
humasect has joined #ocaml
Smerdyakov has joined #ocaml
mlh has quit [Read error: 110 (Connection timed out)]
smkl_ has quit [Read error: 110 (Connection timed out)]
humasect has quit ["Leaving.."]
pnou has quit ["leaving"]
smkl_ has joined #ocaml
mattam has quit [Read error: 110 (Connection timed out)]
smkl_ has quit [Read error: 110 (Connection timed out)]
nwsh has joined #ocaml
dross has joined #ocaml
mlh has joined #ocaml
smkl_ has joined #ocaml
KrispyKringle has quit [Read error: 113 (No route to host)]
nwsh has quit []
mlh has quit [Client Quit]
zzorn has quit ["They are coming to take me away, ha ha"]
mlh has joined #ocaml
smkl_ has quit [Read error: 110 (Connection timed out)]
smkl_ has joined #ocaml
det has quit [Read error: 104 (Connection reset by peer)]
det has joined #ocaml
Submarine has joined #ocaml
CLxyz has joined #ocaml
smkl__ has joined #ocaml
smkl_ has quit [Read error: 110 (Connection timed out)]
Nutssh has quit ["Client exiting"]
smkl__ has quit [Read error: 60 (Operation timed out)]
ganjalink has joined #ocaml
vezenchio has joined #ocaml
smimou has joined #ocaml
_JusSx_ has joined #ocaml
smkl__ has joined #ocaml
gim has quit ["reboot"]
gim has joined #ocaml
smkl__ is now known as smkl
ganjalink has quit ["Quit rulez !"]
kuribas has joined #ocaml
smkl has quit [Read error: 110 (Connection timed out)]
mlh has quit ["Chatzilla 0.9.66e [Firefox 1.0/20041107]"]
cjohnson has joined #ocaml
smkl has joined #ocaml
kuribas has left #ocaml []
zzorn has joined #ocaml
pnou has joined #ocaml
smimou has quit [tolkien.freenode.net irc.freenode.net]
mellum has quit [tolkien.freenode.net irc.freenode.net]
mellum has joined #ocaml
smimou has joined #ocaml
smkl_ has joined #ocaml
smkl has quit [Read error: 110 (Connection timed out)]
mrvn_ has joined #ocaml
stef_ has quit [Read error: 60 (Operation timed out)]
mrvn has quit [Read error: 110 (Connection timed out)]
stef_ has joined #ocaml
mattam has joined #ocaml
smkl_ has quit [Read error: 110 (Connection timed out)]
_JusSx__ has joined #ocaml
pango has quit [Nick collision from services.]
pango_ has joined #ocaml
_JusSx_ has quit [Read error: 110 (Connection timed out)]
smkl_ has joined #ocaml
vezenchio has quit ["Computer Science is no more about computers than astronomy is about telescopes"]
dobrek has quit [tolkien.freenode.net irc.freenode.net]
haakonn_ has quit [tolkien.freenode.net irc.freenode.net]
xew has quit [tolkien.freenode.net irc.freenode.net]
Demitar has quit [tolkien.freenode.net irc.freenode.net]
mbh has quit [tolkien.freenode.net irc.freenode.net]
oracle1 has quit [tolkien.freenode.net irc.freenode.net]
dan2 has quit [tolkien.freenode.net irc.freenode.net]
Hipo has quit [tolkien.freenode.net irc.freenode.net]
skylan has quit [tolkien.freenode.net irc.freenode.net]
drewr has quit [tolkien.freenode.net irc.freenode.net]
dobrek has joined #ocaml
haakonn_ has joined #ocaml
xew has joined #ocaml
Demitar has joined #ocaml
drewr has joined #ocaml
mbh has joined #ocaml
oracle1 has joined #ocaml
dan2 has joined #ocaml
skylan has joined #ocaml
Hipo has joined #ocaml
dan2 has quit [Excess Flood]
Hipo has quit [Connection reset by peer]
Hipo has joined #ocaml
dan2 has joined #ocaml
Hipo has quit [tolkien.freenode.net irc.freenode.net]
oracle1 has quit [tolkien.freenode.net irc.freenode.net]
haakonn_ has quit [tolkien.freenode.net irc.freenode.net]
dobrek has quit [tolkien.freenode.net irc.freenode.net]
skylan has quit [tolkien.freenode.net irc.freenode.net]
mbh has quit [tolkien.freenode.net irc.freenode.net]
xew has quit [tolkien.freenode.net irc.freenode.net]
drewr has quit [tolkien.freenode.net irc.freenode.net]
Demitar has quit [tolkien.freenode.net irc.freenode.net]
Hipo has joined #ocaml
dobrek has joined #ocaml
haakonn_ has joined #ocaml
xew has joined #ocaml
Demitar has joined #ocaml
drewr has joined #ocaml
mbh has joined #ocaml
oracle1 has joined #ocaml
skylan has joined #ocaml
skylan_ has joined #ocaml
oracle1 has quit [tolkien.freenode.net irc.freenode.net]
haakonn_ has quit [tolkien.freenode.net irc.freenode.net]
dobrek has quit [tolkien.freenode.net irc.freenode.net]
skylan has quit [tolkien.freenode.net irc.freenode.net]
Hipo has quit [tolkien.freenode.net irc.freenode.net]
mbh has quit [tolkien.freenode.net irc.freenode.net]
xew has quit [tolkien.freenode.net irc.freenode.net]
drewr has quit [tolkien.freenode.net irc.freenode.net]
Demitar has quit [tolkien.freenode.net irc.freenode.net]
Hipo has joined #ocaml
dobrek has joined #ocaml
haakonn_ has joined #ocaml
xew has joined #ocaml
Demitar has joined #ocaml
drewr has joined #ocaml
mbh has joined #ocaml
oracle1 has joined #ocaml
skylan has joined #ocaml
skylan has quit [Remote closed the connection]
oracle1 has quit [tolkien.freenode.net irc.freenode.net]
haakonn_ has quit [tolkien.freenode.net irc.freenode.net]
dobrek has quit [tolkien.freenode.net irc.freenode.net]
Hipo has quit [tolkien.freenode.net irc.freenode.net]
mbh has quit [tolkien.freenode.net irc.freenode.net]
xew has quit [tolkien.freenode.net irc.freenode.net]
drewr has quit [tolkien.freenode.net irc.freenode.net]
Demitar has quit [tolkien.freenode.net irc.freenode.net]
dobrek has joined #ocaml
smkl_ has quit [Read error: 60 (Operation timed out)]
mbh has joined #ocaml
haakonn_ has joined #ocaml
oracle1 has joined #ocaml
Demitar has joined #ocaml
drewr has joined #ocaml
xew has joined #ocaml
skylan_ is now known as skylan
Hipo has joined #ocaml
Nutssh has joined #ocaml
<dross> hmmm
<dross> hey question, can someone optimise this even further? http://shootout.alioth.debian.org/benchmark.php?test=matrix&lang=ocaml
<Riastradh> Yes, it is unfortunate that it can probably be optimized by changing inner_loop to use a for loop instead of recursion.
<dross> Riastradh: I'm actually making a few tests
<dross> ocaml has been even gcc c for some odd reason, and c++ of course
<Smerdyakov> If you actually get an improvement with that, try MLton.
<Smerdyakov> It shouldn't make a difference there.
<dross> Riastradh: I'm no ocaml expert, however I like ocaml.. its very nice language
<dross> Smerdyakov: I like ocaml though ;)
<Smerdyakov> dross, reasons?
<dross> supported on more platforms
<Smerdyakov> Maybe slightly more.
<dross> Smerdyakov: I didn't see bytecode anywhere in the features list, unless I'm bliind
<Riastradh> OCaml has a REPL, even if it is crap compared to any decent Lisp environment.
<Smerdyakov> For MLton? You're blind. :)
<Smerdyakov> And, honestly, you are irrationally obsessed with "bytecode."
<dross> Smerdyakov: mind giving me eyes and pointing me out to where it says bytecode?
<dross> and does MLton support windows directly?
<dross> without cygwin.
<Smerdyakov> I don't know where to find info on MLton bytecode, because I've never cared to use it.
<Smerdyakov> And I don't care about avoiding Cygwin, either.
<dross> then I guess portability is a MLton issue
<Smerdyakov> Why?
<dross> Smerdyakov: for more people to actually use the compiler, it needs support for at least the most popular platforms
<Smerdyakov> MLton does. It has C and bytecode code generators.
<dross> windows counts as a popular platform
<dross> Don't know if you haven't noticed, but cygwin is a slow POS
<Smerdyakov> I don't think so.
<dross> Smerdyakov: who is the blind one :)
<Smerdyakov> Do you have any data to back that up?
<Submarine> Cygwin is supposedly slow when you do lots of I/O.
<Submarine> If you are concerned, use Mingw.
<dross> Smerdyakov: run just about any application, you can tell
<Smerdyakov> I prefer to avoid Windows, so I don't have much opportunity for that.
<dross> Smerdyakov: you might not use it, but it doesn't mean Windows doesn't need to be avoided
<Smerdyakov> I'm quite content to give Windows users an inferior experience to save time in the development community.
<dross> Smerdyakov: one of the best arguements of mine.. using a portable language
<Smerdyakov> This is NOT lack of portability, since SML programs port to Windows much more easily than, say, C programs.
<Smerdyakov> SML is the most portable language on the planet.
<dross> Smerdyakov: I don't wish to use another computer for windows
<Smerdyakov> There are social issues of developing tools for it to work with specific legacy systems.
<dross> Smerdyakov: I wish to use 1 compiler only.
<Submarine> I once compiled Astrée on Windows.
<Submarine> It was an experience.
<Smerdyakov> But SML is formally defined... nothing else comes close for being able to predict ahead of time how your programw ill work on a particular platform.
<Submarine> Next time I feel a bout of masochism, I'll do this again, or I'll do some Coq.
<dross> Submarine: hehe.
<Smerdyakov> Submarine, did you just diss Coq?
* dross hides
<Submarine> You can interpret what I said this way.
<Smerdyakov> Submarine, what are your grievances with Coq?
<Submarine> mmmh
<Submarine> picky decision procedures that for instance will see x < y (x and y being real) but not NOT (x >= y)
<Submarine> not enough automation
<Submarine> bad upwards compatibility
<Smerdyakov> Hm. So contribute patches for those procedures. :)
<Submarine> Why should I?
<Smerdyakov> Because it's easy!
<Submarine> I'm not the one saying that I made a usable proof assistant.
<Smerdyakov> You can also write a tactical to handle the example you gave. Easy as pie.
<Smerdyakov> Or just run intro before the dec. proc..
<Submarine> Intro won't help you.
<Submarine> what you essentially want to do is to use the lemma saying that <= is total and decidable
<Submarine> then in one branch you'll reach absurdity
<Submarine> and you get what you want in the other branch
<Submarine> the point is, the dec. proc should do this by itself
<Smerdyakov> Omega handles this stuff. Which real number procedure are you using?
<Submarine> Coq's Omega is for Presburger arithmetics, that is, integers, unless I'm greatly mistaken.
<Smerdyakov> I know.
<Submarine> Fourier should handle this.
<Smerdyakov> Is that included with the base distribution?
<Submarine> Yes.
<Smerdyakov> "intro; fourier." worked for me.
<Smerdyakov> (to prove ~(6 >= 7))
<Smerdyakov> Whoa.
<Smerdyakov> (to prove ~(6 >= 7)%R)
<Submarine> oh dear
<Submarine> ~(6 >= 7) in the hypotheses
<Smerdyakov> Ah, gotcha.
* Gahhh wonders if he is the only one predicting that Coq will at some point have a name change...
<Smerdyakov> Gahhh, it's decades old.
<Submarine> Why? The name is fine.
<Gahhh> Ugh. it has a vulgar meaning in english.
<Submarine> First, its original English meaning in English is "rooster", which is the same as the French meaning.
<dross> could someone optimise the ocaml shootout program for matrix?
<Submarine> Second, this is a French project largely funded by the French taxpayers, why should they care about hung-up English speakers.
<dross> the shootout is actually flawed because it uses I/O in the non-IO tests
<Submarine> Third, did you know that Mona (solver for Monadic logic) means female genitalia in Italian?
<dross> like matrix :)
<Submarine> x : R
<Submarine> y : R
<Submarine> H : ~ x <= y
<Submarine> ============================
<Submarine> x > y
<Submarine> fourier.
<Submarine> > ^^^^^^^
<Submarine> User error: The statement is not built from Leibniz' equality
<Smerdyakov> Submarine, I hear ya, man. It's kind of odd that you end up with hypotheses like that, though.
<dross> Submarine: thats not as bad as saying "Moshi-moshi" (japanese phone greeting to a german phone caller :)
<Smerdyakov> That's not as bad as cutting a baby in half with a sword.
<Submarine> Smerdyakov, Such hypotheses are trivially obtained in some circumstances, like when dealing with max and min, which use {x <= y} + {~ (x <= y)} or similar
<dross> which mushi mushi in japanese means pussy pussy in german :)
<Smerdyakov> Make your own max and min that don't use ~.
<Submarine> sure sure
<dross> *moshi moshi
<Submarine> but still, there's some kind of integration problem
<Smerdyakov> Well, it's never been an issue for me. I only do very limited reasoning about numbers.
<Gahhh> Well, if you start mixing people speaking different languages, some words will have unexpected meanings, yes. But Coq has documentation in English. I don't think it's meant to be for the French only...
<Gahhh> Anyway, I could very well be the only one predicting a name change.
<Smerdyakov> It would be terribly un-French to change the name.
<Submarine> I think they take a perverse pride in shocking people.
* Submarine notes that Americans organize tons of meetings with names like LogicCon
<Smerdyakov> Is that bad in French?
<Submarine> as you perhaps know, Con means "cunt" in French literally, and is usually rather used as a very vulgar insult for "very stupid"
<Smerdyakov> I didn't know that.
<Gahhh> Impressive. Lisp must be fun in French.
<Submarine> well... that's why you pronounce consse and not con
<Submarine> String is also quite bad.
<Smerdyakov> It means "boil retarded people in oil"?
<Submarine> "String", in French, is used solely for G-string... I mean, extra narrow panties.
<Smerdyakov> I was close.
<Submarine> Imagine teaching an introductory CS course.
<Gahhh> Your guess worries me, Smerdyakov.
smkl_ has joined #ocaml
_JusSx__ has quit ["leaving"]
<smimou> Submarine: btw (it's not really related), is there some code of astrée publicly available ?
<Submarine> not yet
<smimou> there will be ?
<Submarine> we may take out some libraries and make them available
<smimou> that's great
<Submarine> maybe there will be a free version without the aerospace-specific bells and whistles
<smimou> under a free licence ?
<Submarine> We don't know.
<Submarine> Remember, we're not the one making the decisions.
<dross> I hope they are Free and not free
<dross> or written for that matter.
<Submarine> We do not have the legal right to grant licenses on the IP of our employers.
<dross> Submarine: oh, you are employed by someone.. heh
<smimou> your employers = airbus ?
<dross> Submarine: why not be self employed? ;)
<Submarine> Our employers are our academic institutions.
<dross> Submarine: oh.
<dross> Submarine: well that sucks(tm)
<Submarine> For minor libraries, this is not an issue, but in that case, we'd have to clear things before.
<dross> erm.. I've forgotten a certain magazine
<dross> anyone know what the major supplier in electronics was besides digikey?
Submarine has quit ["Leaving"]
smkl_ has quit [Read error: 110 (Connection timed out)]
mlh has joined #ocaml
<dross> hmm~
<dross> I'm liking how ML is compared to otehr langauges I've used
<dross> real langauges, not php, perl , java ,a dn friends :P
mattam has quit [Read error: 110 (Connection timed out)]
smimou has quit ["?"]