From d26535d6665879f77d39e790b4aa9ee0dcb63dcf Mon Sep 17 00:00:00 2001
From: Mohammad Akhlaghi <mohammad@akhlaghi.org>
Date: Wed, 14 Feb 2018 14:13:36 +0100
Subject: Sanity checks added, local settings now in LOCAL.mk.in

The choice of whether or not to make a PDF is now also a local system
issue, not a general pipeline issue. So it has been put in the new
`LOCAL.mk.in' file which replaces the old `DIRECTORIES.mk.in'. All local
settings (things that when changed should not be version-controlled) should
be defined in this file.

A sanity check was added to find if `./configure' has been run before
`make' or not (using the `LOCAL.mk' file which is an output of the
configuration step). If `LOCAL.mk' doesn't exist, an error will be printed
informing the user that `./configure' needs to be run first.

The configure script also provides more clear and hopefully better
information on its purpose and what must be done.

Since `make clean', it is executed even when `./configure' hasn't been run,
it will only delete the build directory and its contents when local
configuration has been done.

A `distclean' target was also added which will first "clean" the pipeline,
then delete the `LOCAL.mk.in' file.

To allow rules like `make' to be run even if `BDIR' isn't defined
(`./configure' hasn't been run yet), a fake `BDIR' is defined in such
cases.
---
 configure | 57 +++++++++++++++++++++++++++++++--------------------------
 1 file changed, 31 insertions(+), 26 deletions(-)

(limited to 'configure')

diff --git a/configure b/configure
index be18c25..8ecb8fa 100755
--- a/configure
+++ b/configure
@@ -28,43 +28,37 @@
 pdir=reproduce/config/pipeline
 
 
-# Message to print for editing
-function msg {
-    echo; echo "Top-level reproduction directories are set.";
-    echo "Please run the following command to start the pipeline:"
-    echo "(Replace '8' with the number of CPU threads available)"
-    echo; echo "    make -j8"
-    echo;
-}
 
 
-# If `DIRECTORIES.mk' is already created, then ignore this step.
-if [ -f $pdir/DIRECTORIES.mk ]; then
+
+# If `LOCAL.mk' is already created, then ignore this step.
+if [ -f $pdir/LOCAL.mk ]; then
     echo
-    echo "$pdir/DIRECTORIES.mk already exists."
+    echo "$pdir/LOCAL.mk already exists."
     echo "To change/correct the top-level directories, please remove/edit it manually."
     echo
 else
 
     # Copy the base file to the desired output file.
-    if cp $pdir/DIRECTORIES.mk.in $pdir/DIRECTORIES.mk; then
+    if cp $pdir/LOCAL.mk.in $pdir/LOCAL.mk; then
 
         # Tell the user to edit the directories.
         while [ "$userread" != "y" -a "$userread" != "n" ]
         do
-            echo "Top-level directories..."
             echo
-            echo "These directories define the input(s) location and the"
-            echo "directory to host the intermediate/processing files."
+            echo "------------------------------------"
+            echo "Reproduction pipeline local configuration"
+            echo "-----------------------------------------"
             echo
-            echo "To help in your ability to read and manage this pipeline,"
-            echo "it is recommended (but not mandatory) to change them to"
-            echo "a directory outside this reproduction pipeline."
+            echo "Local settings include things like top-level directories,"
+            echo "or processing steps (e.g., if you want a final PDF output)."
             echo
-            echo "More descriptions are provided within the file that is"
-            echo "opened if you choose to edit the directories."
+            echo "Pressing 'y' will open the local settings file in an editor"
+            echo "so you can modify the default values if you want. Each"
+            echo "variable is also thoroughly described in the comments (lines"
+            echo "starting with a '#') above it."
             echo
-            read -p"Edit the default top-level directories (y/n)? " userread
+            read -p"Edit the default local configuration (y/n)? " userread
         done
 
         # Only continue if the user wants to edit the top level
@@ -72,17 +66,28 @@ else
         if [ $userread = "y" ]; then
 
             # Open a text editor to set the given directories
-            if emacs $pdir/DIRECTORIES.mk;   then msg
-            elif gedit $pdir/DIRECTORIES.mk; then msg
-            elif vi $pdir/DIRECTORIES.mk;    then msg
+            if   emacs $pdir/LOCAL.mk; then junk=1
+            elif gedit $pdir/LOCAL.mk; then junk=1
+            elif vi    $pdir/LOCAL.mk; then junk=1
             else
                 echo
                 echo "No common text editor found on your system."
-                echo "Please set the values in '$pdir/DIRECTORIES.mk' manually."
+                echo "Please set the values in '$pdir/LOCAL.mk' manually."
                 echo
             fi
         fi
+        echo
+        echo "This reproduction pipeline has been configured for this system."
+        echo "Please run the following command to start the pipeline:"
+        echo "(Replace '8' with the number of CPU threads available)"
+        echo
+        echo "    make -j8"
+        echo
+        echo
+        echo "(you can always check/modify the default local settings"
+        echo " by editing this file: '$pdir/LOCAL.mk')"
+        echo
     else
-        echo; echo "Couldn't create $pdir/DIRECTORIES.mk"
+        echo; echo "Couldn't create $pdir/LOCAL.mk"
     fi
 fi
-- 
cgit v1.2.1