diff options
| author | Guillaume Melquiond | 2016-09-08 17:04:43 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-09-08 17:04:43 +0200 |
| commit | ef3f9fac7cff820bd927d122caef2c37a68a55c8 (patch) | |
| tree | 4f0edc4bab216df032f30d42261f407bb28b405a | |
| parent | 9f56baf7bb78a520dc2e7f5f0f94091ebf86dcaf (diff) | |
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.
| -rw-r--r-- | toplevel/mltop.ml | 6 |
1 files 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 = { |