From 3e275d4bd1c3eb002b68c36ab116e5ab687d52f3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 4 Dec 2018 10:33:47 +0100
Subject: Fix race condition triggered by fresh universe generation

Remote counters were trying to build universe levels (as opposed to
simple integers), but did not have access to the right dirpath at
construction time. We fix it by constructing the level only at use time,
and we introduce some abstractions for qualified and unqualified level
names.
---
 library/nametab.ml  | 15 +++++----------
 library/nametab.mli | 12 +++++-------
 2 files changed, 10 insertions(+), 17 deletions(-)

(limited to 'library')

diff --git a/library/nametab.ml b/library/nametab.ml
index e29c7b2960..ab69da3467 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -347,12 +347,10 @@ module DirTab = Make(DirPath')(GlobDirRef)
 type dirtab = DirTab.t
 let the_dirtab = Summary.ref ~name:"dirtab" (DirTab.empty : dirtab)
 
-type universe_id = DirPath.t * int
-
 module UnivIdEqual =
 struct
-  type t = universe_id
-  let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i'
+  type t = Univ.Level.Qualid.t
+  let equal = Univ.Level.Qualid.equal
 end
 module UnivTab = Make(FullPath)(UnivIdEqual)
 type univtab = UnivTab.t
@@ -375,12 +373,9 @@ let the_modtyperevtab = Summary.ref ~name:"modtyperevtab" (MPmap.empty : mptrevt
 
 module UnivIdOrdered =
 struct
-  type t = universe_id
-  let hash (d, i) = i + DirPath.hash d
-  let compare (d, i) (d', i') =
-    let c = Int.compare i i' in
-    if Int.equal c 0 then DirPath.compare d d'
-    else c
+  type t = Univ.Level.Qualid.t
+  let hash = Univ.Level.Qualid.hash
+  let compare = Univ.Level.Qualid.compare
 end
 
 module UnivIdMap = HMap.Make(UnivIdOrdered)
diff --git a/library/nametab.mli b/library/nametab.mli
index 24af07619d..496c76d9b0 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -120,11 +120,9 @@ val push_modtype : visibility -> full_path -> ModPath.t -> unit
 val push_dir : visibility -> DirPath.t -> GlobDirRef.t -> unit
 val push_syndef : visibility -> full_path -> syndef_name -> unit
 
-type universe_id = DirPath.t * int
+module UnivIdMap : CMap.ExtS with type key = Univ.Level.Qualid.t
 
-module UnivIdMap : CMap.ExtS with type key = universe_id
-
-val push_universe : visibility -> full_path -> universe_id -> unit
+val push_universe : visibility -> full_path -> Univ.Level.Qualid.t -> unit
 
 (** {6 The following functions perform globalization of qualified names } *)
 
@@ -139,7 +137,7 @@ val locate_modtype : qualid -> ModPath.t
 val locate_dir : qualid -> GlobDirRef.t
 val locate_module : qualid -> ModPath.t
 val locate_section : qualid -> DirPath.t
-val locate_universe : qualid -> universe_id
+val locate_universe : qualid -> Univ.Level.Qualid.t
 
 (** These functions globalize user-level references into global
    references, like [locate] and co, but raise a nice error message
@@ -196,7 +194,7 @@ val path_of_modtype : ModPath.t -> full_path
 
 (** A universe_id might not be registered with a corresponding user name.
     @raise Not_found if the universe was not introduced by the user. *)
-val path_of_universe : universe_id -> full_path
+val path_of_universe : Univ.Level.Qualid.t -> full_path
 
 (** Returns in particular the dirpath or the basename of the full path
    associated to global reference *)
@@ -218,7 +216,7 @@ val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
 val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid
 val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid
 val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid
-val shortest_qualid_of_universe : ?loc:Loc.t -> universe_id -> qualid
+val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.Qualid.t -> qualid
 
 (** Deprecated synonyms *)
 
-- 
cgit v1.2.3


From cff3c5a7148afc722852bd01658fe49ffec1d967 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Dec 2018 15:52:37 +0100
Subject: Revise API for global universes.

Rename Univ.Level.{Qualid -> UGlobal}, remove Univ.Level.Id.

Remove the ability to split the argument of `Univ.Level.Level` into a
dirpath*int pair (except by going through string hacks like
detyping/pretyping(/funind) does).

Id.of_string_soft to turn unnamed universes into qualid is pushed up
to detyping. (TODO some followup PR clean up more)

This makes it pointless to have an opaque type for ints in
Univ.Level: it would only be used as argument to
Univ.Level.UGlobal.make, ie
~~~
open Univ.Level
let x = UGlobal.make dp (Id.make n)
(* vs *)
let x = UGlobal.make dp n
~~~

Remaining places which create levels from ints are various hacks (eg
the dummy in inductive.ml, the Type.n universes in ugraph
sort_universes) and univgen.

UnivGen does have an opaque type for ints used as univ ids since they
get manipulated by the stm.

NB: build breaks due to ocamldep issue if UGlobal is named Global instead.
---
 library/nametab.ml  | 10 +++++-----
 library/nametab.mli | 10 +++++-----
 2 files changed, 10 insertions(+), 10 deletions(-)

(limited to 'library')

diff --git a/library/nametab.ml b/library/nametab.ml
index ab69da3467..f0f643d9b5 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -349,8 +349,8 @@ let the_dirtab = Summary.ref ~name:"dirtab" (DirTab.empty : dirtab)
 
 module UnivIdEqual =
 struct
-  type t = Univ.Level.Qualid.t
-  let equal = Univ.Level.Qualid.equal
+  type t = Univ.Level.UGlobal.t
+  let equal = Univ.Level.UGlobal.equal
 end
 module UnivTab = Make(FullPath)(UnivIdEqual)
 type univtab = UnivTab.t
@@ -373,9 +373,9 @@ let the_modtyperevtab = Summary.ref ~name:"modtyperevtab" (MPmap.empty : mptrevt
 
 module UnivIdOrdered =
 struct
-  type t = Univ.Level.Qualid.t
-  let hash = Univ.Level.Qualid.hash
-  let compare = Univ.Level.Qualid.compare
+  type t = Univ.Level.UGlobal.t
+  let hash = Univ.Level.UGlobal.hash
+  let compare = Univ.Level.UGlobal.compare
 end
 
 module UnivIdMap = HMap.Make(UnivIdOrdered)
diff --git a/library/nametab.mli b/library/nametab.mli
index 496c76d9b0..b7926cf515 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -120,9 +120,9 @@ val push_modtype : visibility -> full_path -> ModPath.t -> unit
 val push_dir : visibility -> DirPath.t -> GlobDirRef.t -> unit
 val push_syndef : visibility -> full_path -> syndef_name -> unit
 
-module UnivIdMap : CMap.ExtS with type key = Univ.Level.Qualid.t
+module UnivIdMap : CMap.ExtS with type key = Univ.Level.UGlobal.t
 
-val push_universe : visibility -> full_path -> Univ.Level.Qualid.t -> unit
+val push_universe : visibility -> full_path -> Univ.Level.UGlobal.t -> unit
 
 (** {6 The following functions perform globalization of qualified names } *)
 
@@ -137,7 +137,7 @@ val locate_modtype : qualid -> ModPath.t
 val locate_dir : qualid -> GlobDirRef.t
 val locate_module : qualid -> ModPath.t
 val locate_section : qualid -> DirPath.t
-val locate_universe : qualid -> Univ.Level.Qualid.t
+val locate_universe : qualid -> Univ.Level.UGlobal.t
 
 (** These functions globalize user-level references into global
    references, like [locate] and co, but raise a nice error message
@@ -194,7 +194,7 @@ val path_of_modtype : ModPath.t -> full_path
 
 (** A universe_id might not be registered with a corresponding user name.
     @raise Not_found if the universe was not introduced by the user. *)
-val path_of_universe : Univ.Level.Qualid.t -> full_path
+val path_of_universe : Univ.Level.UGlobal.t -> full_path
 
 (** Returns in particular the dirpath or the basename of the full path
    associated to global reference *)
@@ -216,7 +216,7 @@ val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
 val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid
 val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid
 val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid
-val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.Qualid.t -> qualid
+val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.UGlobal.t -> qualid
 
 (** Deprecated synonyms *)
 
-- 
cgit v1.2.3