Isabelle
Posted by Skrud at Wednesday, November 30th 2005 at 1:03pm
Isabelle makes no sense. Isabelle isn’t a person (though I can only assume that, if she were human she’d be a female, and would still make no sense), it’s a “generic theorem proving environment”. It’s built on top of EMACS, and I’m a vi(m) man, and the two are opposites to the point of holy war. EMACS is bloated. The introductory tutorial for Isabelle is 235 pages. It’s written for mathematicians, not for programmers. All the documentation is written with LaTeX and makes extensive use of the greek alphabet which is not available to use in the syntax for the proofing language. In other words, a measure function uses the greek character lambda (λ) as an argument, however one cannot input λ as such into an emacs document. So instead the % character substitutes for λ. Why not just use the ‘%’ symbol in the documentation and save us all the trouble???!!! This goes on for many symbols. And it gets worse…
A “simple” factorial function would look something like this:
consts
factorial :: "nat => nat"
recdef measure(%n.n)
"factorial 0 = 1"
"factorial n = n * factorial(pred n)"Which is probably wrong, the prof erased and rewrote it about 3 times, and I still have no idea how it works. By comparison, in C:
int factorial( int n ) {
return ( n <= 0 ) ? 1 : factorial( n - 1 ) * n;
}You know something is wrong if it’s simpler to do in C.
Ah, enough ranting. I feel a little better now.
I like mathematicians. But I agree, vim > emacs. I’m a vim girl too.. Well when I’m forced to use unix that is…
Forced to use Unix?!
vi rules!
Dude, Isabelle is a bitch! And the whole emacs thing…WTF. Now I very rarely leave my windowed world, but EVEN I know emacs is shit. Vim is a bit tricky at 1st, but once you get the hang of it, it makes sense.
I’m a vimmer too, but for the past 1 or 2 months I use emacs, just to learn, because I already know the beauty of vim (the logic of it, the speed and productivity it offers, how light and fast it is etc.) and why so many people like it. For now, I think I understand why so many people love emacs; it is extremely customizable and extensible because it is a developement environement by itself, with a full-featured programming language within, which makes it extremely fun to use. I know it is slower to start and run (1.2 seconds to start on my machine. Wow. A lifetime), but this is the price to pay to have an interpreter to play with. As I said, I love both toys.
I think that the ‘war’ between vimmers and emacsens is a complete waste of time for everyone. It’s a joke that is not funny anymore because it was repeated so many times.
Guys, anybody who hasn’t already done so – try the editor you dislike for a couple of months with all the motivation to learn, so you can see that both are extremely cool and fun.
Here’s another view: http://www.io.com/~dierdorf/emacsvi.html
I still think it’s funny. :P
emacs is a great operating system, it just needs a good text editor!
(i still think it’s funny)
Ok, it’s funny, still. :)
What saved me was the well-hidden VI Emulation mode (in XEmacs at least) that’s enabled by a check box under Options -> Keyboard and Mouse.
It’s a standard vi so, e.g., it only has one level of undo. But it’s definitely better than having to use all those multicharacter M- and C- command sequences!