now using pdfsizeopt to decrease the size of the book pdf

Author: thomasWeise

README.md

@@ -13,6 +13,9 @@ Your feedback would help us to improve the book.
 ## 2. License
 This book is released under the Attribution-NonCommercial-ShareAlike 4.0 International license (CC BY‑NC‑SA 4.0), see [http://creativecommons.org/licenses/by-nc-sa/4.0/](http://creativecommons.org/licenses/by-nc-sa/4.0/) for a summary.
 
+We statically include the [pdfsizeopt](https://github.com/pts/pdfsizeopt) tool to compress the book pdf file.
+This tool is excluded from the license mentioned above; it is under the GNU GENERAL PUBLIC LICENSE Version 2, June 1991 and the copyright belongs to its authors.
+
 ## 3. Contact
 If you have any questions or suggestions, please contact
 Prof. Dr. [Thomas Weise](http://iao.hfuu.edu.cn/5) (汤卫思教授)

scripts/filterPdf.sh

@@ -1,6 +1,6 @@
 #!/bin/bash -
 
-# This script filters a PDF file and attempts to include as many fonts as possible.
+# This script filters a PDF file using ghostscript and attempts to include as many fonts as possible.
 
 # strict error handling
 set -o pipefail  # trace ERR through pipes

scripts/pdfsizeopt.sh

@@ -0,0 +1,47 @@
+#!/bin/bash -
+
+# This script applies the pdfsizeopt compressor to a pdf.
+# The pdfsizeopt compressor is open source and available at https://github.com/pts/pdfsizeopt.
+# We include it here in a single archive.
+
+# strict error handling
+set -o pipefail  # trace ERR through pipes
+set -o errtrace  # trace ERR through 'time command' and other functions
+set -o nounset   # set -u : exit the script if you try to use an uninitialized variable
+set -o errexit   # set -e : exit the script if any statement returns a non-true return value
+
+scriptDir="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+echo "Script directory is '$scriptDir'."
+
+currentDir="$(pwd)"
+echo "$(date +'%0Y-%0m-%0d %0R:%0S'): We are working in directory: '$currentDir'."
+
+fileIn="$(readlink -f "$1")"
+echo "$(date +'%0Y-%0m-%0d %0R:%0S'): The full input document path is '$fileIn'."
+
+fileOut="$2"
+echo "$(date +'%0Y-%0m-%0d %0R:%0S'): We will filter the input document '$fileIn' to '$fileOut'."
+
+tempDir="$(mktemp -d)"
+echo "$(date +'%0Y-%0m-%0d %0R:%0S'): We will use the temporary directory '$tempDir'."
+
+cd "$tempDir"
+
+echo "$(date +'%0Y-%0m-%0d %0R:%0S'): Unpacking pdfsizeopt to '$tempDir'."
+tar -C "$tempDir" -xf "$scriptDir/pdfsizeopt.tar.xz"
+pdfsizeoptdir="$tempDir/pdfsizeopt"
+chmod 777 -R "$pdfsizeoptdir"
+
+export PATH="$pdfsizeoptdir:$PATH"
+echo "$(date +'%0Y-%0m-%0d %0R:%0S'): PATH is now '$PATH'."
+
+pdfsizeopttemp="$pdfsizeoptdir/pdft"
+mkdir "$pdfsizeopttemp"
+echo "$(date +'%0Y-%0m-%0d %0R:%0S'): pdfsizeopt will use temp dir '$pdfsizeopttemp'."
+
+"$pdfsizeoptdir/pdfsizeopt.single" --do-double-check-type1c-output=yes --tmp-dir="$pdfsizeopttemp" "$fileIn" "$fileOut"
+
+echo "$(date +'%0Y-%0m-%0d %0R:%0S'): Now deleting temporary directory '$tempDir'."
+rm -rf "$tempDir"
+
+echo "$(date +'%0Y-%0m-%0d %0R:%0S'): Successfully finished filtering '$fileIn' to '$fileOut using pdfsizeopt."

scripts/pdfsizeopt.tar.xz

@@ -30,8 +30,14 @@ echo "$(date +'%0Y-%0m-%0d %0R:%0S'): First, we make sure that '$websiteDir' is
 rm -rf "$websiteDir" || true
 mkdir -p "$websiteDir"
 
-echo "$(date +'%0Y-%0m-%0d %0R:%0S'): Filtering the book into the website directory."
-"$scriptDir/filterPdf.sh" "$currentDir/book.pdf" "$websiteDir/programmingWithPython.pdf"
+# ghostscriptTemp="$(mktemp)"
+# echo "$(date +'%0Y-%0m-%0d %0R:%0S'): First filtering the book to a temp file '$ghostscriptTemp'."
+# "$scriptDir/filterPdf.sh" "$currentDir/book.pdf" "$ghostscriptTemp"
+# echo "$(date +'%0Y-%0m-%0d %0R:%0S'): Now compressing the book to the website directory."
+# "$scriptDir/pdfsizeopt.sh" "$ghostscriptTemp" "$websiteDir/programmingWithPython.pdf"
+# rm "$ghostscriptTemp"
+echo "$(date +'%0Y-%0m-%0d %0R:%0S'): Compressing the book from '$currentDir/book.pdf' to '$websiteDir/programmingWithPython.pdf' using pdfsizeopt."
+"$scriptDir/pdfsizeopt.sh" "$currentDir/book.pdf" "$websiteDir/programmingWithPython.pdf"
 
 echo "$(date +'%0Y-%0m-%0d %0R:%0S'): Put the LICENSE.md file into the website directory."
 licenseFile="$currentDir/LICENSE.md"