From: "Matej Košík" <mail@matej-kosik.net>
To: "Nicolás Ojeda Bär" <nicolas.ojeda.bar@lexifi.com>
Cc: OCaml Mailing List <caml-list@inria.fr>
Subject: Re: [Caml-list] a question about Ocaml toplevel behavior
Date: Mon, 12 Mar 2018 09:44:43 +0100 [thread overview]
Message-ID: <c5f0f1e5-9925-6293-1f17-3633f3f31a96@matej-kosik.net> (raw)
In-Reply-To: <CADK7aFNbNNx=3aFV7p_Xkf-47gof-Otr-iWvWZcYmJKkTE-wZg@mail.gmail.com>
Hi,
On 03/11/18 20:17, Nicolás Ojeda Bär wrote:
> Hello,
>
> I don't know if there is any deep design reason for this behaviour,
> but for one it enables a kind of information hiding: in order to hide
> modules which are private to a library and should not be exposed to
> the client code, simply do not install the corresponding .cmi files.
I am not sure if this is the right mechanism (not providing *.cmi files)
for information hiding (which is a valid goal) but that is a separate topic.
What I do not understand is the default behavior of coqtop if *.cmi files are present.
Why coqtop does not load them all eagerly?
Why does coqtop delays loading of them us much as possible?
What is here to be gained by this behavior?
Is this done on purpose or was it a random decision?
Does anybody have an idea?
Why isn't this documented?
Why are (non abstract) types printed (in case *.cmi files were temporarily ignored) printed as "<abstr>" instead of "<something-else>"?
next prev parent reply other threads:[~2018-03-12 8:44 UTC|newest]
Thread overview: 8+ messages / expand[flat|nested] mbox.gz Atom feed top
2018-03-10 17:55 Matej Košík
2018-03-11 13:30 ` Matej Košík
2018-03-11 15:06 ` Nicolás Ojeda Bär
2018-03-11 15:51 ` Matej Košík
2018-03-11 19:17 ` Nicolás Ojeda Bär
2018-03-12 8:44 ` Matej Košík [this message]
2018-03-12 8:50 ` Jacques Garrigue
2018-03-12 9:09 ` Matej Košík
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=c5f0f1e5-9925-6293-1f17-3633f3f31a96@matej-kosik.net \
--to=mail@matej-kosik.net \
--cc=caml-list@inria.fr \
--cc=nicolas.ojeda.bar@lexifi.com \
/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