From aa16865dd7a3ae1c123dfcf88c5f9dd7451a151d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 26 Nov 2020 09:22:25 +0100
Subject: [PATCH] [ccache] play safe with STM

---
 src/coq_elpi_vernacular.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml
index 4bae3fa65..58c45c177 100644
--- a/src/coq_elpi_vernacular.ml
+++ b/src/coq_elpi_vernacular.ml
@@ -622,7 +622,11 @@ let debug vl = debug_vars := List.fold_right EC.StrSet.add vl EC.StrSet.empty
 let bound_steps n =
   if n <= 0 then max_steps := default_max_step else max_steps := n
 
-let compiler_cache = ref SLMap.empty
+(* Units are marshalable, but programs are not *)
+let compiler_cache = Summary.ref
+  ~freeze:(fun ~marshallable x -> if marshallable then SLMap.empty else x)
+  ~name:"elpi-compiler-cache"
+  SLMap.empty
 
 let compile name baseul extra =
   try