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.
---
 engine/univGen.ml | 20 ++++++++------------
 1 file changed, 8 insertions(+), 12 deletions(-)

(limited to 'engine/univGen.ml')

diff --git a/engine/univGen.ml b/engine/univGen.ml
index 130aa06f53..5aa4734b23 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -14,25 +14,21 @@ open Constr
 open Univ
 
 (* Generator of levels *)
-type universe_id = DirPath.t * int
-
 let new_univ_id, set_remote_new_univ_id =
   RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
-    ~build:(fun n -> Global.current_dirpath (), n)
-
-let new_univ_level () =
-  let dp, id = new_univ_id () in
-  Univ.Level.make dp id
+    ~build:(fun n -> Level.Id.make n)
 
-let fresh_level () = new_univ_level ()
+let fresh_level () =
+  let id = new_univ_id () in
+  Univ.Level.make2 (Global.current_dirpath ()) id
 
 (* TODO: remove *)
-let new_univ dp = Univ.Universe.make (new_univ_level dp)
-let new_Type dp = mkType (new_univ dp)
-let new_Type_sort dp = Type (new_univ dp)
+let new_univ () = Univ.Universe.make (fresh_level ())
+let new_Type () = mkType (new_univ ())
+let new_Type_sort () = Type (new_univ ())
 
 let fresh_instance auctx =
-  let inst = Array.init (AUContext.size auctx) (fun _ -> new_univ_level()) in
+  let inst = Array.init (AUContext.size auctx) (fun _ -> fresh_level()) in
   let ctx = Array.fold_right LSet.add inst LSet.empty in
   let inst = Instance.of_array inst in
   inst, (ctx, AUContext.instantiate inst auctx)
-- 
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.
---
 engine/univGen.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'engine/univGen.ml')

diff --git a/engine/univGen.ml b/engine/univGen.ml
index 5aa4734b23..40c4c909fe 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -13,14 +13,17 @@ open Names
 open Constr
 open Univ
 
+type univ_unique_id = int
 (* Generator of levels *)
 let new_univ_id, set_remote_new_univ_id =
   RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
-    ~build:(fun n -> Level.Id.make n)
+    ~build:(fun n -> n)
+
+let new_univ_global () =
+  Univ.Level.UGlobal.make (Global.current_dirpath ()) (new_univ_id ())
 
 let fresh_level () =
-  let id = new_univ_id () in
-  Univ.Level.make2 (Global.current_dirpath ()) id
+  Univ.Level.make (new_univ_global ())
 
 (* TODO: remove *)
 let new_univ () = Univ.Universe.make (fresh_level ())
-- 
cgit v1.2.3