From 32e26090369e47e3e83e4313b3eefb321bc3311e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 7 Oct 2020 18:28:50 +0200
Subject: Store the resolver of required modules as functor parameters in
 safe_env.

The safe environment features two different sets of delta resolvers, one for
module parameters and one for the actual body of the module being built. The
purpose of this separations seems to have been to reduce the number of name
equations being added to the environment, since the one from the parameters
would already be present at instanciation time.

Semantically, required modules behave like parameters in this respect, i.e.
delta resolvers that come from modules dependend upon are guaranteed to be added
when that module is actually required. As such, there is no need to store the
quotient coming from the dependencies inside the vo file of a given library.

Yet, the previous code would precisely do that, leading to a potential quadratic
blowup in vo file size, similarly to the issue with vio files storing the whole
chain of dependency. This patch fixes the issue simply by segregating those
redundant constraints in the dedicated field, thus dropping them from the vo.
---
 kernel/safe_typing.ml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index da77a2882e..3dee3d2b2f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -79,8 +79,10 @@ module NamedDecl = Context.Named.Declaration
     * STRUCT (params,oldsenv) : inside a local module, with
       module parameters [params] and earlier environment [oldsenv]
     * SIG (params,oldsenv) : same for a local module type
-  - [modresolver] : delta_resolver concerning the module content
-  - [paramresolver] : delta_resolver concerning the module parameters
+  - [modresolver] : delta_resolver concerning the module content, that needs to
+    be marshalled on disk
+  - [paramresolver] : delta_resolver in scope but not part of the library per
+    se, that is from functor parameters and required libraries
   - [revstruct] : current module content, most recent declarations first
   - [modlabels] and [objlabels] : names defined in the current module,
       either for modules/modtypes or for constants/inductives.
@@ -1301,7 +1303,9 @@ let import lib cst vodigest senv =
   mp,
   { senv with
     env;
-    modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver;
+    (* Do NOT store the name quotient from the dependencies in the set of
+       constraints that will be marshalled on disk. *)
+    paramresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.paramresolver;
     required = DPmap.add lib.comp_name vodigest senv.required;
     loads = (mp,mb)::senv.loads;
     sections;
-- 
cgit v1.2.3