From 8050c90b1cfc755abb16c83df0eebaed85cd67d2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 14 Jan 2015 19:08:55 +0100
Subject: coq_makefile: chmod 755 on toplopp cmxs

---
 tools/coq_makefile.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index b73fdba1e6..ac3f6fc8b3 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -270,7 +270,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in
     if (not_empty cmxsfiles) then begin
       print "install-toploop: $(MLLIBFILES:.mllib=.cmxs)\n";
       printf "\t install -d \"$(DSTROOT)\"$(COQTOPINSTALL)/\n";
-      printf "\t install -m 0644 $?  \"$(DSTROOT)\"$(COQTOPINSTALL)/\n";
+      printf "\t install -m 0755 $?  \"$(DSTROOT)\"$(COQTOPINSTALL)/\n";
       print "\n";
     end;
     print "install:";
-- 
cgit v1.2.3


From 8f077f6d05d0c764e401ce6770f6b598523c33fc Mon Sep 17 00:00:00 2001
From: Pierre Boutillier
Date: Tue, 13 Jan 2015 23:26:13 +0100
Subject: coq_makefile installs native files

---
 tools/coq_makefile.ml | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index ac3f6fc8b3..d877ed564a 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -257,7 +257,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in
     let cmxsfiles = List.rev_append cmofiles mllibfiles in
     let where_what_cmxs = vars_to_put_by_root [("CMXSFILES",cmxsfiles)] inc in
     let where_what_oth = vars_to_put_by_root
-      [("VOFILES",vfiles);("CMOFILES",cmofiles);("CMIFILES",cmifiles);("CMAFILES",mllibfiles)]
+      [("VOFILES",vfiles);("NATIVEFILES",vfiles);("CMOFILES",cmofiles);("CMIFILES",cmifiles);("CMAFILES",mllibfiles)]
       inc in
     let doc_dir = where_put_doc inc in
     let () = if is_install = Project_file.UnspecInstall then
@@ -328,9 +328,7 @@ let clean sds sps =
   end;
   if !some_vfile then
     begin
-      print "\trm -f $(OBJFILES) $(OBJFILES:.o=.native)\n";
-      print "\trm -f $(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo)\n";
-      print "\trm -f $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)\n";
+      print "\trm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)\n";
       print "\trm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)\n"
     end;
   print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex\n";
@@ -577,8 +575,9 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
       print "GFILES:=$(VFILES:.v=.g)\n";
       print "HTMLFILES:=$(VFILES:.v=.html)\n";
       print "GHTMLFILES:=$(VFILES:.v=.g.html)\n";
-      print "OBJFILES:=$(call vo_to_obj,$(VOFILES))\n";
-      classify_files_by_root "OBJFILES" l inc
+      print "OBJFILES=$(call vo_to_obj,$(VOFILES))\n";
+      print "NATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)\n";
+      classify_files_by_root "NATIVEFILES" l inc
   end;
   decl_var "ML4FILES" ml4files;
   decl_var "MLFILES" mlfiles;
-- 
cgit v1.2.3


From 530dcf1e6cd008e89a527dacb836202bcb2d02db Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Jan 2015 07:49:27 +0100
Subject: Make installation of native files more robust.

---
 tools/coq_makefile.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index d877ed564a..28b86ddc78 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -505,7 +505,7 @@ let parameters () =
   print "TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))\n\n";
   print "vo_to_obj = $(addsuffix .o,$(foreach vo,$(1),\\\n";
   print "  $(addprefix $(dir $(vo)),$(addprefix .coq-native/,$(filter-out Warning: Error:,$(firstword \\\n";
-  print "    $(shell $(COQBIN)coqtop -batch -quiet -print-mod-uid $(vo))))))))\n\n"
+  print "    $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(vo))))))))\n\n"
 
 let include_dirs (inc_ml,inc_i,inc_r) =
   let parse_ml_includes l = List.map (fun (x,_) -> "-I \"" ^ x ^ "\"") l in
@@ -576,7 +576,8 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
       print "HTMLFILES:=$(VFILES:.v=.html)\n";
       print "GHTMLFILES:=$(VFILES:.v=.g.html)\n";
       print "OBJFILES=$(call vo_to_obj,$(VOFILES))\n";
-      print "NATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)\n";
+      print "ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)\n";
+      print "NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f))\n";
       classify_files_by_root "NATIVEFILES" l inc
   end;
   decl_var "ML4FILES" ml4files;
-- 
cgit v1.2.3


From d66b734336cf04a94ac3ef1bd129dfcd3bba92d2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Jan 2015 13:28:21 +0100
Subject: Make -print-mod-uid accept a list of files.

Solves an efficiency problem in Makefiles generated by coq_makefile.
---
 tools/coq_makefile.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 28b86ddc78..badaf280e4 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -503,9 +503,14 @@ let parameters () =
   print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n";
   print "TIMED=\nTIMECMD=\nSTDTIME?=/usr/bin/time -f \"$* (user: %U mem: %M ko)\"\n";
   print "TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))\n\n";
+  print "vo_to_obj = $(addsuffix .o,\\\n";
+  print "  $(filter-out Warning: Error:,\\\n";
+  print "  $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))\n\n"
+(*
   print "vo_to_obj = $(addsuffix .o,$(foreach vo,$(1),\\\n";
   print "  $(addprefix $(dir $(vo)),$(addprefix .coq-native/,$(filter-out Warning: Error:,$(firstword \\\n";
   print "    $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(vo))))))))\n\n"
+ *)
 
 let include_dirs (inc_ml,inc_i,inc_r) =
   let parse_ml_includes l = List.map (fun (x,_) -> "-I \"" ^ x ^ "\"") l in
-- 
cgit v1.2.3


From 93fa642fa5e4134d034a1f10fe6dffa4a36182cf Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Jan 2015 13:32:20 +0100
Subject: Remove left-over dead code in previous commit.

---
 tools/coq_makefile.ml | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index badaf280e4..e9bdb6caca 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -506,11 +506,6 @@ let parameters () =
   print "vo_to_obj = $(addsuffix .o,\\\n";
   print "  $(filter-out Warning: Error:,\\\n";
   print "  $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))\n\n"
-(*
-  print "vo_to_obj = $(addsuffix .o,$(foreach vo,$(1),\\\n";
-  print "  $(addprefix $(dir $(vo)),$(addprefix .coq-native/,$(filter-out Warning: Error:,$(firstword \\\n";
-  print "    $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(vo))))))))\n\n"
- *)
 
 let include_dirs (inc_ml,inc_i,inc_r) =
   let parse_ml_includes l = List.map (fun (x,_) -> "-I \"" ^ x ^ "\"") l in
-- 
cgit v1.2.3