From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 0D9558239C for ; Mon, 12 Mar 2018 09:44:47 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mail@matej-kosik.net; spf=SoftFail smtp.mailfrom=mail@matej-kosik.net; spf=SoftFail smtp.helo=postmaster@matej-kosik.net Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of mail@matej-kosik.net) identity=pra; client-ip=145.239.83.105; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mail@matej-kosik.net"; x-sender="mail@matej-kosik.net"; x-conformance=sidf_compatible Received-SPF: SoftFail (mail3-smtp-sop.national.inria.fr: domain of mail@matej-kosik.net is inclined to not designate 145.239.83.105 as permitted sender) identity=mailfrom; client-ip=145.239.83.105; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mail@matej-kosik.net"; x-sender="mail@matej-kosik.net"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: SoftFail (mail3-smtp-sop.national.inria.fr: domain of postmaster@matej-kosik.net is inclined to not designate 145.239.83.105 as permitted sender) identity=helo; client-ip=145.239.83.105; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="mail@matej-kosik.net"; x-sender="postmaster@matej-kosik.net"; x-conformance=sidf_compatible; x-record-type="v=spf1" IronPort-PHdr: =?us-ascii?q?9a23=3A8SYygRNcIkHAhICAVmgl6mtUPXoX/o7sNwtQ0KIM?= =?us-ascii?q?zox0LfT9rarrMEGX3/hxlliBBdydt6ofzbKO+4nbGkU4qa6bt34DdJEeHzQksu?= =?us-ascii?q?4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1?= =?us-ascii?q?Ov71GonPhMiryuy+4ZLebxlGiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPde?= =?us-ascii?q?RWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbY?= =?us-ascii?q?UwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0vRz+s87lkRwPpiC?= =?us-ascii?q?cfNj427mfXitBrjKlGpB6tvgFzz5LIbI2QMvd1Y6HTcs4ARWdZQ8hfSSJBDIO/?= =?us-ascii?q?YYUBAeUOMuRXoJXyqVYVsRuzBhOhCP/zxjJGhHL727Ax3eQ7EQHB2QwtB9UAv2?= =?us-ascii?q?7IrNrrNqcZTOW7zK7HzjLdbPNdxDDw6I3SfRAgpfGBRrdwftDNyUYxFQPJl1aQ?= =?us-ascii?q?qYv+PzOU1eQBqW6b4PR8Ve+2jWMstgJ/oiC3y8sxhYTEhpgZxk7K+Ch92oo4Jt?= =?us-ascii?q?O1RFRmbdK4EJZcryWXOotsTs8/X21kpjw2xqMJtJO1ZiQG1poqywLZZveaaYaH?= =?us-ascii?q?+AjjW/yUITpghHJqZra/hxGq/Eil0OL8Ste70FRToipGldnMrXEN1x/J5siBVP?= =?us-ascii?q?R94l+t2TeJ1w/N9uFJOV04mKXbJpI73LI9mJ4evV7AEyL4gkn6kbOae0U89uit?= =?us-ascii?q?8evnY7HmppGGN49zjwHzKqEulda+AeQ8KQUOWnKU+fii273h5EH5Q7JKjuY3kq?= =?us-ascii?q?naqpzaI9oUprKhDw9Pzokj8wq/Dyuh0NkAgXYINldFeBaeg4jtOlHOO+z4AOyk?= =?us-ascii?q?g1WslTdr3+rJMqfgApXLNHjDka3ucaxz605Gm0IPyoV55plTDjgaF9XxV0P4g/?= =?us-ascii?q?ZUFFdtNQ2/xOLuE5N61I4SUCSFC7WxNK7CsFGJoOkoJr/fSpUSvWPYIuQo5bbN?= =?us-ascii?q?io28mhdJeKCo2bMSYWy1HLFlJF6YYjzqj8tXQjRChRY3UOG/0A7KajVUfXvnGv?= =?us-ascii?q?tkvmhqWrLjNp/KQ8WWuJLE2S66GpNMYWUfVQKJGGvldcCHXOwNa2SUL9MzyWVY?= =?us-ascii?q?B4jkcJco0FSVjCG/06Bud7WG/yQEuJCm199u5u6Vkxwup2QtUpatllqVRmQxpV?= =?us-ascii?q?smAj872Kcm/h54w0uO0+17hOdZFppV6u8bCQo=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0ADBwBsPaZa/2lT75FdGgEBAQEBAgEBA?= =?us-ascii?q?QEIAQEBAYNQaWyDeIsSjk4LKYEWlkeFLwKDEx0JBS8UAQIBAQEBAQEBAQFqJ4I?= =?us-ascii?q?4JAGCRwEFIw8BOQ0QCxgCAiYCAlcGDQgBAYUYqz6CJoRvg0YnghqBDYQogwKDE?= =?us-ascii?q?QyCeYgpgmIEmlYJiVOHCYkShVaSdDUhJoEsewo6gkSER4wiK4IeAQEB?= X-IPAS-Result: =?us-ascii?q?A0ADBwBsPaZa/2lT75FdGgEBAQEBAgEBAQEIAQEBAYNQaWy?= =?us-ascii?q?DeIsSjk4LKYEWlkeFLwKDEx0JBS8UAQIBAQEBAQEBAQFqJ4I4JAGCRwEFIw8BO?= =?us-ascii?q?Q0QCxgCAiYCAlcGDQgBAYUYqz6CJoRvg0YnghqBDYQogwKDEQyCeYgpgmIEmlY?= =?us-ascii?q?JiVOHCYkShVaSdDUhJoEsewo6gkSER4wiK4IeAQEB?= X-IronPort-AV: E=Sophos;i="5.47,460,1515452400"; d="scan'208";a="257836543" Received: from 105.ip-145-239-83.eu (HELO matej-kosik.net) ([145.239.83.105]) by mail3-smtp-sop.national.inria.fr with ESMTP; 12 Mar 2018 09:44:46 +0100 Received: from [192.168.1.11] (adsl-dyn-230.95-102-243.t-com.sk [95.102.243.230]) by matej-kosik.net (Postfix) with ESMTPSA id 24E82226F3; Mon, 12 Mar 2018 09:44:45 +0100 (CET) To: =?UTF-8?Q?Nicol=c3=a1s_Ojeda_B=c3=a4r?= Cc: OCaml Mailing List References: <97fc418b-c016-7a7f-77ae-3823bf4b8a12@matej-kosik.net> <81818a99-0a21-f5b3-8708-7a4c99d13935@matej-kosik.net> From: =?UTF-8?B?TWF0ZWogS2/FocOtaw==?= Openpgp: id=1CD41D0A52319DC7ABC1B79F50AFFA128CE48649; url=http://matej-kosik.net/doc/kosik.asc Message-ID: Date: Mon, 12 Mar 2018 09:44:43 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.6.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8 Content-Language: en-US Content-Transfer-Encoding: 8bit Subject: Re: [Caml-list] a question about Ocaml toplevel behavior 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 "" instead of ""?