From 5e2574cbef1ba132aacc73b4a079cc0b5584f589 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Thu, 23 Feb 2017 14:57:59 +0100
Subject: [safe-string] Enable -safe-string !

We now build Coq with `-safe-string`, which enforces functional use
of the `string` datatype. Coq was pretty safe in these regard so only
a few tweaks were needed.

- coq_makefile: build plugins with -safe-string too.
- `names.ml`: we remove `String.copy` uses, as they are not needed.
---
 .merlin               |  2 +-
 configure.ml          |  9 ++++++++-
 kernel/names.ml       |  4 +---
 tools/coq_makefile.ml | 14 +++++++-------
 4 files changed, 17 insertions(+), 12 deletions(-)

diff --git a/.merlin b/.merlin
index bda18d549..394db528d 100644
--- a/.merlin
+++ b/.merlin
@@ -1,4 +1,4 @@
-FLG -rectypes -thread
+FLG -rectypes -thread -safe-string
 
 S ltac
 B ltac
diff --git a/configure.ml b/configure.ml
index 82ce931d6..dfc6724a2 100644
--- a/configure.ml
+++ b/configure.ml
@@ -264,6 +264,10 @@ module Prefs = struct
   let debug = ref true
   let profile = ref false
   let annotate = ref false
+  (* Note, disabling this should be OK, but be careful with the
+     sharing invariants.
+  *)
+  let safe_string = ref true
   let nativecompiler = ref (not (os_type_win32 || os_type_cygwin))
   let coqwebsite = ref "http://coq.inria.fr/"
   let force_caml_version = ref false
@@ -386,6 +390,9 @@ let coq_annotate_flag =
   then if program_in_path "ocamlmerlin" then "-bin-annot" else "-annot"
   else ""
 
+let coq_safe_string =
+  if !Prefs.safe_string then "-safe-string" else ""
+
 let cflags = "-Wall -Wno-unused -g -O2"
 
 (** * Architecture *)
@@ -1118,7 +1125,7 @@ let write_makefile f =
   pr "CAMLHLIB=%S\n\n" camllib;
   pr "# Caml link command and Caml make top command\n";
   pr "# Caml flags\n";
-  pr "CAMLFLAGS=-rectypes %s\n" coq_annotate_flag;
+  pr "CAMLFLAGS=-rectypes %s %s\n" coq_annotate_flag coq_safe_string;
   pr "# User compilation flag\n";
   pr "USERFLAGS=\n\n";
   pr "# Flags for GCC\n";
diff --git a/kernel/names.ml b/kernel/names.ml
index 831b6ad46..ee8d838da 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -57,15 +57,13 @@ struct
 
   let of_string s =
     let () = check_soft s in
-    let s = String.copy s in
     String.hcons s
 
   let of_string_soft s =
     let () = check_soft ~warn:false s in
-    let s = String.copy s in
     String.hcons s
 
-  let to_string id = String.copy id
+  let to_string id = id
 
   let print id = str id
 
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 23479aee5..4dfb7af6a 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -521,10 +521,10 @@ let variables is_install opt (args,defs) =
     List.iter (fun c -> print " \\
   -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n";
     print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n";
-    print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread\n";
-    print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread\n";
-    print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread\n";
-    print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread\n";
+    print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread -safe-string\n";
+    print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread -safe-string\n";
+    print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread -safe-string\n";
+    print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread -safe-string\n";
     print "CAMLDEP?=$(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack\n";
     print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n";
     print "GRAMMARS?=grammar.cma\n";
@@ -764,9 +764,9 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
     begin
       print "mlihtml: $(MLIFILES:.mli=.cmi)\n";
       print "\t mkdir $@ || rm -rf $@/*\n";
-      print "\t$(OCAMLFIND) ocamldoc -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
+      print "\t$(OCAMLFIND) ocamldoc -html -safe-string -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
       print "all-mli.tex: $(MLIFILES:.mli=.cmi)\n";
-      print "\t$(OCAMLFIND) ocamldoc -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
+      print "\t$(OCAMLFIND) ocamldoc -latex -safe-string -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)\n\n";
     end;
   if !some_vfile then
     begin
@@ -882,7 +882,7 @@ let check_overlapping_include (_,inc_i,inc_r) =
  *)
 let merlin targets (ml_inc,_,_) =
   print ".merlin:\n";
-  print "\t@echo 'FLG -rectypes' > .merlin\n" ;
+  print "\t@echo 'FLG -rectypes -safe-string' > .merlin\n" ;
   List.iter (fun c ->
       printf "\t@echo \"B $(COQLIB)%s\" >> .merlin\n" c)
     lib_dirs ;
-- 
cgit v1.2.3