<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.