From ef3f9fac7cff820bd927d122caef2c37a68a55c8 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 8 Sep 2016 17:04:43 +0200
Subject: Avoid canonizing the same paths over and over.

The number of path canonizations was quadratic in the number of potential
plugin directories. This patch makes it linear; on a standard Coq tree,
this brings the number of chdir and getcwd system calls from more than
1,000 down to about 200 at startup.

This also fixes a bug where the Cd vernacular command could cause plugins
to break since relative paths were used to locate them.
---
 toplevel/mltop.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index fbd1e60336..f972959453 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -45,12 +45,12 @@ open System
    to build a dummy dynlink.cmxa, cf. dev/dynlink.ml. *)
 
 (* This path is where we look for .cmo *)
-let coq_mlpath_copy = ref ["."]
+let coq_mlpath_copy = ref [Sys.getcwd ()]
 let keep_copy_mlpath path =
   let cpath = CUnix.canonical_path_name path in
-  let filter path' = not (String.equal cpath (CUnix.canonical_path_name path'))
+  let filter path' = not (String.equal cpath path')
   in
-  coq_mlpath_copy := path :: List.filter filter !coq_mlpath_copy
+  coq_mlpath_copy := cpath :: List.filter filter !coq_mlpath_copy
 
 (* If there is a toplevel under Coq *)
 type toplevel = {
-- 
cgit v1.2.3