From 3b917b7b9a201b511a56f55102077199868212e7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 1 Jun 2015 13:39:16 +0200
Subject: Making Coq compile with ocp-memprof.

Patch provided by Çagdas Bozman.
---
 kernel/byterun/coq_gc.h | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
index c7b18b9006..f06275862c 100644
--- a/kernel/byterun/coq_gc.h
+++ b/kernel/byterun/coq_gc.h
@@ -12,6 +12,7 @@
 #define _COQ_CAML_GC_
 #include <caml/mlvalues.h>
 #include <caml/alloc.h>
+#include <caml/memory.h>
 
 typedef void (*scanning_action) (value, value *);
 
@@ -24,12 +25,22 @@ CAMLextern void minor_collection (void);
 #define Caml_white (0 << 8)
 #define Caml_black (3 << 8)
 
+#ifdef HAS_OCP_MEMPROF
+
+/*  This code is necessary to make the OCamlPro memory profiling branch of
+    OCaml compile. */
+
+#define Make_header(wosize, tag, color)                                 \
+  caml_make_header(wosize, tag, color)
+
+#else
+
 #define Make_header(wosize, tag, color)                                 \
   (((header_t) (((header_t) (wosize) << 10)                             \
 		+ (color)                                               \
 		+ (tag_t) (tag)))   					\
    )
-
+#endif
 
 #define Alloc_small(result, wosize, tag) do{                            \
   young_ptr -= Bhsize_wosize (wosize);                                  \
-- 
cgit v1.2.3


From 48a6ce6e7cbdc2a03767c61696425cd5d5827f4f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 8 Jun 2015 22:34:07 +0200
Subject: Fix native compilation of primitive projections. Closes #4210.

---
 kernel/nativecode.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index ada7ae737f..f56b6f83e7 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -2015,9 +2015,13 @@ let rec compile_deps env sigma prefix ~interactive init t =
         || (Cmap_env.mem c const_updates)
       then init
       else
-      let comp_stack, (mind_updates, const_updates) = match cb.const_body with
-        | Def t ->
+      let comp_stack, (mind_updates, const_updates) =
+	match cb.const_proj, cb.const_body with
+        | None, Def t ->
 	   compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t)
+	| Some pb, _ ->
+	   let mind = pb.proj_ind in
+	   compile_mind_deps env prefix ~interactive init mind
         | _ -> init
       in
       let code, name =
-- 
cgit v1.2.3


From c78e8d35d6431fa9119c863c3b58aed1f53ed4a5 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sat, 13 Jun 2015 00:36:02 +0200
Subject: Native compiler: do not catch exceptions not related to dynlink.

Was making the study of bugs like #4139 painful.
Now printing a better error message when a compiled file is missing.
---
 kernel/nativelib.ml | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

(limited to 'kernel')

diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 29b6bf6de7..7cb01b6955 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -105,22 +105,23 @@ let compile_library dir code fn =
   r
 
 (* call_linker links dynamically the code for constants in environment or a  *)
-(* conversion test. Silently fails if the file does not exist in bytecode    *)
-(* mode, since the standard library is not compiled to bytecode with default *)
-(* settings.                                                                 *)
+(* conversion test. *)
 let call_linker ?(fatal=true) prefix f upds =
   rt1 := dummy_value ();
   rt2 := dummy_value ();
-  if Dynlink.is_native || Sys.file_exists f then
+  if not (Sys.file_exists f) then
+    let msg = "Cannot find native compiler file " ^ f in
+    if fatal then Errors.error msg
+    else Pp.msg_warning (Pp.str msg)
+  else
   (try
     if Dynlink.is_native then Dynlink.loadfile f else !load_obj f;
     register_native_file prefix
-   with | Dynlink.Error e ->
-          let msg = "Dynlink error, " ^ Dynlink.error_message e in
-          if fatal then anomaly (Pp.str msg) else Pp.msg_warning (Pp.str msg)
-        | e when Errors.noncritical e ->
-          if fatal then anomaly (Errors.print e)
-	  else Pp.msg_warning (Errors.print_no_report e));
+   with Dynlink.Error e as exn ->
+     let exn = Errors.push exn in
+     let msg = "Dynlink error, " ^ Dynlink.error_message e in
+     if fatal then (Pp.msg_error (Pp.str msg); iraise exn)
+     else Pp.msg_warning (Pp.str msg));
   match upds with Some upds -> update_locations upds | _ -> ()
 
 let link_library ~prefix ~dirname ~basename =
-- 
cgit v1.2.3