From: "Harrison, John R" <johnh@ichips.intel.com>
To: "skaller" <skaller@users.sourceforge.net>
Cc: "Caml list" <caml-list@inria.fr>
Subject: RE: [Caml-list] toplevel with pre-installed printers
Date: Fri, 20 Jan 2006 12:19:48 -0800 [thread overview]
Message-ID: <196F1D996F92CD46A542EA519DB8CE4702F0D2D7@orsmsx409> (raw)
| Under "Linux" ckpt is not available. I tried this, since HOL Light
takes
| ages to load. I even tried to build ckpt from source with no luck.
| Maybe it works for x86 .. but I'm running an x86_64.
I wasn't aware of that problem. It works fine on 32-bit x86, though
there
are some peculiarities of certain Linux variants. I'll look into this,
since I suppose I'll want it myself one day.
| Is there some reason HOL Light doesn't load bytecode?
It's not so much the code (of automated proof procedures etc.) that
slows
the load down, but actually running the proofs to arrive at the basic
core of theorems. Loading as bytecode won't help that significantly.
It would be possible to restructure the code to completely separate data
(theorems) from code (proof procedures), load the former via marshalling
and the latter as bytecode. But it's not very natural to do so, since
one
often wants to introduce theorems and proof procedures in a tightly
interleaved manner.
John.
next reply other threads:[~2006-01-20 20:19 UTC|newest]
Thread overview: 14+ messages / expand[flat|nested] mbox.gz Atom feed top
2006-01-20 20:19 Harrison, John R [this message]
-- strict thread matches above, loose matches on Subject: below --
2006-01-19 19:40 Harrison, John R
2006-01-20 1:30 ` skaller
2006-01-19 16:28 Andrej Bauer
2006-01-19 16:53 ` [Caml-list] " Daniel Bünzli
2006-01-19 16:57 ` Eric Stokes
2006-01-19 17:08 ` Andrej Bauer
2006-01-19 17:49 ` Richard Jones
2006-01-19 19:12 ` Eric Cooper
2006-01-19 20:18 ` Richard Jones
2006-01-20 2:24 ` skaller
2006-01-20 16:49 ` David Brown
2006-01-20 19:29 ` skaller
2006-01-20 8:29 ` Jean-Christophe Filliatre
2006-01-20 13:13 ` Gerd Stolpmann
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=196F1D996F92CD46A542EA519DB8CE4702F0D2D7@orsmsx409 \
--to=johnh@ichips.intel.com \
--cc=caml-list@inria.fr \
--cc=skaller@users.sourceforge.net \
/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 a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox