All of lore.kernel.org
 help / color / mirror / Atom feed
From: esr@thyrsus.com
To: Aaron Lehmann <aaronl@vitelus.com>
Cc: Michael Elizabeth Chastain <chastain@cygnus.com>,
	kbuild-devel@lists.sourceforge.net, linux-kernel@vger.kernel.org
Subject: Re: [kbuild-devel] Re: CML2 1.0.0 release announcement
Date: Wed, 11 Apr 2001 21:53:20 -0400	[thread overview]
Message-ID: <20010411215320.G9081@thyrsus.com> (raw)
In-Reply-To: <200104112056.NAA20872@bosch.cygnus.com> <20010411174609.A8410@thyrsus.com> <20010411180138.A27597@vitelus.com>
In-Reply-To: <20010411180138.A27597@vitelus.com>; from aaronl@vitelus.com on Wed, Apr 11, 2001 at 06:01:38PM -0700

Aaron Lehmann <aaronl@vitelus.com>:
> Maybe you could kill two birds with one stone by calling 1.0.0 the
> prototype and rewriting it in C.

If I were to become absolutely convinced that I can't get acceptable speed
out of Python, I might do that.  There's a gcml project that tracked the CML2
compiler up to about 0.72 level that might make a decent starting point.

Unfortunately, I'm fairly sure that finishing gcml would take long
enough to render the point moot, because by the time it was done the
average Linux machine would have sped up enough for the Python
implementation not to be laggy anymore :-).

No joke -- *you* try writing a theorem-prover in a language with only
fixed-extent data types.  Go on.  Try it.  I think you will (as Mark
Twain put it about the consequences of teasing a cat) acquire a
valuable education, the facts of which will never grow dim or
doubtful.

I'm pretty sure that tuning the Python implementation (coming up with
faster algorithms, perhaps by reorganizing the data structures to do
more precomputation) will be a more effective use of my time.
-- 
		<a href="http://www.tuxedo.org/~esr/">Eric S. Raymond</a>

"One of the ordinary modes, by which tyrants accomplish their purposes
without resistance, is, by disarming the people, and making it an
offense to keep arms."
        -- Constitutional scholar and Supreme Court Justice Joseph Story, 1840

  reply	other threads:[~2001-04-12  1:52 UTC|newest]

Thread overview: 12+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2001-04-11 20:56 [kbuild-devel] Re: CML2 1.0.0 release announcement Michael Elizabeth Chastain
2001-04-11 21:46 ` esr
2001-04-12  1:01   ` Aaron Lehmann
2001-04-12  1:53     ` esr [this message]
2001-04-12 12:07       ` Dave Jones
2001-04-12 12:00         ` Steven Cole
2001-04-12 13:12           ` Dave Jones
2001-04-12 16:51           ` Horst von Brand
2001-04-12 16:12             ` Steven Cole
2001-04-12 17:59           ` Jochen Striepe
2001-04-11 22:25 ` Alan Cox
2001-04-12  0:40   ` esr

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20010411215320.G9081@thyrsus.com \
    --to=esr@thyrsus.com \
    --cc=aaronl@vitelus.com \
    --cc=chastain@cygnus.com \
    --cc=kbuild-devel@lists.sourceforge.net \
    --cc=linux-kernel@vger.kernel.org \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.