From 4c9eb2e3f41eb42a1d4fb74a76aaa0b62870ca01 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 7 May 2015 18:43:10 -0400
Subject: [PATCH] chore(scripts): update documentation of port.pl, port.sh and
 rename.pl

---
 script/port.pl   | 39 ++++++++++-----------------------------
 script/port.sh   | 13 +------------
 script/rename.pl | 14 +++++++++-----
 3 files changed, 20 insertions(+), 46 deletions(-)

diff --git a/script/port.pl b/script/port.pl
index 6ac83a291..499efce49 100755
--- a/script/port.pl
+++ b/script/port.pl
@@ -4,36 +4,17 @@
 #
 # This perl script is for porting files from the standard library to the HoTT library
 #
-# (1) create a file "port.txt", with a list of entries "foo:bar" (or "foo;bar"),
-#     one per line
-# (2) put this script and port.txt in the same directory, and make sure
-#     the script is executable.
-# (3) use "[path]/port.pl [path]/source [path]/target" to do the renaming.
-#     On a Unix system, at least, you can use wildcards.
+# To use: first make it executable (chmod u+x port.pl). Then type
 #
-# -> You can write foo;bar to replace all occurrences,
-#    even if they are a substring of a longer expression (useful for e.g. notation)
-#
-# Example: if you put rename.pl and port.txt in lean/library, then
-# from that directory type
-#
-#   ./rename.pl data/nat/*.lean
-#
-# to do all the renamings in data/nat. Alternative, change to that directory,
-# and type
-#
-# ../../rename.pl *.lean
-#
-# Notes:
-#
-# We assume identifiers have only letters, numbers, _, or "'" or ".".
-#
-# See http://perldoc.perl.org/perlfaq5.html, "How can I use Perl's i option from
-# within a program?" for information on the method used to change a file in place.
-#
-# See also http://perldoc.perl.org/File/Find.html for information on how to write
-# a subroutine that will traverse a directory tree.
+#  ./port.pl ../library/path/to/source.lean ../hott/path/to/destination.hlean ["from1" "to1" "from2" "to2" ...]
 #
+# This will port the file ../library/path/to/source.lean to ../hott/path/to/destination.hlean
+# renaming core definitions form the standard library to core definitions in the HoTT library.
+# These renamings are specified in port.txt. See the documentation in rename.pl for the syntax.
+# The arguments "fromi" and "toi" are optional, but should be provided in pairs.
+# These arguments will replace "fromi" by "toi" in the specified file,
+# before doing any other renamings.
+
 use strict;
 use warnings;
 use Cwd 'abs_path';
@@ -102,7 +83,7 @@ sub rename_in_file {
 
 my $oldfile = shift;
 my $newfile = shift;
-if (-e $newfile) {move($newfile,$newfile.".orig") or die "Move failed: $!"; } 
+if (-e $newfile) {move($newfile,$newfile.".orig") or die "Move failed: $!"; }
 print "copying ", $oldfile, " to ",$newfile, ".\n";
 copy($oldfile,$newfile) or die "Copy failed: $!";
 get_renamings;
diff --git a/script/port.sh b/script/port.sh
index 6d962c577..a50a0b3de 100755
--- a/script/port.sh
+++ b/script/port.sh
@@ -6,18 +6,7 @@
 #
 # WARNING: This will overwrite all destination files without warning!
 #
-# to add a new file to port to this file, add a new line of the form 
-#
-#  ./port.pl ../library/path/to/source.lean ../hott/path/to/destination.hlean "from1" "to1" "from2" "to2" [...]
-#
-# This will port the file ../library/path/to/source.lean to ../hott/path/to/destination.hlean 
-# renaming core definitions form the standard library to core definitions in the HoTT library. 
-# These renamings are specified in port.txt. Additional changes can be added by the extra arguments.
-# The extra arguments will replace "fromi" by "toi" in the specified file, 
-# before doing any other renamings.
-#
-# Note: parentheses (and other characters with a special meaning in regular expressions)
-# have to be escaped
+# See port.pl for the syntax, if you want to add new files to port.
 
 now=$(date +"%B %d, %Y")
 ./port.pl ../library/data/nat/basic.lean ../hott/types/nat/basic2.hlean "Module: data.nat.basic" "Module: types.nat.basic
diff --git a/script/rename.pl b/script/rename.pl
index 08726f6fb..b37052405 100755
--- a/script/rename.pl
+++ b/script/rename.pl
@@ -9,9 +9,6 @@
 # (3) use "[path]/rename.pl [path]/file" to do the renaming.
 #     On a Unix system, at least, you can use wildcards.
 #
-# -> You can write foo;bar to replace all occurrences,
-#    even if they are a substring of a longer expression (useful for e.g. notation)
-#
 # Example: if you put rename.pl and renamings.txt in lean/library, then
 # from that directory type
 #
@@ -24,14 +21,21 @@
 #
 # Notes:
 #
-# We assume identifiers have only letters, numbers, _, or "'" or ".".
+# For lines "foo:bar" we assume that foo has only letters, numbers, _, or "'" or ".".
+#
+# Lines "foo;bar" replaces every occurrence of "foo" by "bar",
+# even if "foo" is a substring of a bigger expression.
+# "foo" can contain whitespace or special characters, but cannot contain newlines.
+#
+# Parentheses (and other characters with a special meaning in regular expressions)
+# have to be escaped
 #
 # See http://perldoc.perl.org/perlfaq5.html, "How can I use Perl's i option from
 # within a program?" for information on the method used to change a file in place.
 #
 # See also http://perldoc.perl.org/File/Find.html for information on how to write
 # a subroutine that will traverse a directory tree.
-#
+
 use strict;
 use warnings;
 use Cwd 'abs_path';