#!/bin/sh # install.sh for the Metamath site (metamath.org) - version of 4-Dec-04 # Author: Norman Megill # This file (specifically, the version of this file with the above date) # is placed in the public domain per the Creative Commons Public Domain # Dedication. http://creativecommons.org/licenses/publicdomain/ # See http://www.faqs.org/docs/abs/HTML/index.html for bash language syntax # # This Linux bash shell script regenerates the automatically-generated parts # of the Metamath site. It should be run from the metamathsite directory (where # this script resides) by typing "./install.sh". # # # If you do not have LaTeX installed, some .pdf files will not be created. # In that case, at the end of the run you will be given an informational warning, # which will tell you which .pdf files to retrieve from the metamath.org site in # order to make your installation complete. # # # Suggestion: You might want to run with logging in order to detect any # problems that may have occurred. To do this, instead of "./install.sh" type: # # sh -x ./install.sh >install.log 2>&1 # # You can monitor the progress in another window with "tail -f install.log". # # After the run, check the log file for problems: # # egrep -i \ # "warning|error|no such|cannot|permission|denied|invalid|too long|can't" \ # install.log | egrep -v "No errors|Font Warn|label token|ignored" # # If all went OK there should be no output. # # If you are using Cygwin on Windows XP, see the "Note for Cygwin on Windows XP" # below for recovery from a Microsoft bug you might encounter. # # # This script can be run again to refresh the site. If the site is regenerated # on top of itself, up to 600MB of disk space may be needed temporarily. (This # is so site can be viewed while it is being regenerated.) # # The script is also intended to be robust in that it can be re-run if # it is aborted in the middle. # # Please report any problems to "nm at alum.mit.edu" (change " at " to "@"). # ############################################################################## # (The following notes are intended for N. Megill only) # QA checklist for official web site release # 1. nohup ./install.sh & check nohup.out for errors - Linux and Cygwin # 2. tar -xzf downloads/metamathsite.tar.gz, diff -rq with original # 2. nohup wget --mirror (url)/index.html & check nohup.out for "ERROR 404" # 3. diff -r between wget'ed and original # 4. check latex/metamath.log, latex/finiteaxiom.log for warnings # 5. http://validator.w3.org/ # index.html # mmsolitaire/mms.html # mmsolitaire/mmsviewer.html # mpegif/mmbiblio.html # mpegif/mmcomplex.html # mpegif/mmdeduction.html # mpegif/mmhil.html # mpegif/mmmusic.html # mpegif/mmrecent.html # mpegif/mmset.html # mpegif/mmzfcnd.html # qlegif/mmql.html # symbols/symbols.html # 6. tar -cf - * | gzip -9 > ../metamathmirror.tar.gz generates release file # (End of N.Megill-only stuff) ############################################################################## # The Metamath site-building script starts here # Check that necessary software is present DEPS="bash gcc tar gzip zip bzip2 find ls mv cp rm sed md5sum touch chmod" for item in $DEPS do if [ -z "`which $item`" ]; then echo "?Fatal error: $item (needed for build) is not installed on your system." exit 1 fi done # Cygwin support CYGWIN=false case "`uname`" in # Match the conventional Cygwin naming scheme returned from uname CYGWIN*) CYGWIN=true ;; esac ######## Recover if a previous run was aborted in the middle ####### # # ############ Note for Cygwin on Windows XP ########## # # Sometimes Windows XP will "lock" a file or directory randomly for no # apparent reason, such that if an attempt to delete/rename the file or # is made from the Windows Explorer, the error message "Cannot rename/delete # xxx - access is denied. Make sure the disk is not full or write-protected." # appears, even if all applications are closed. Rebooting sometimes works. # Other times, the following manual procedure (found on a newsgroup and # verified to work) is needed to delete the file: # # "Open a Command Prompt window and leave it open. Close all open programs. # Click Start, Run and enter TASKMGR.EXE Go to the Processes tab and End # Process on Explorer.exe. Leave Task Manager open. Go back to the Command # Prompt window and change to the directory the AVI (or other undeletable # file) is located in. At the command prompt type DEL where # is the file you wish to delete. Go back to Task Manager, click # File, New Task and enter EXPLORER.EXE to restart the GUI shell. Close Task # Manager." # # In this script we attempt to detect all such cases of this problem, so # that hopefully this script will never terminate with a false "success" # message. Unfortunately this Windows bug makes this script much more # complex than it would otherwise have to be. # if [ -d tmpmetamathsite ] ; then # If the subdirectory tmpmetamathsite exists, the site master # backup was not finished, so just delete it. Nothing else was # touched yet. echo "Recovering from an earlier aborted run..." rm -rf tmpmetamathsite if [ -d tmpmetamathsite ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not delete the subdirectory 'tmpmetamathsite'." echo "Is someone else using that subdirectory?" echo "If this is Windows, please reboot before running install.sh again." exit 1 fi # If there was an aborted failure to delete the metamathsite directory # at the end of this script in an earlier run, we should try to delete it # now because it may be corrupted and shouldn't be reused. rm -rf metamathsite if [ -d metamathsite ] ; then # If the rm -rf failed, some files in 'metamathsite' may be gone but not # others. However, everything else completed OK. We must prevent # metamathsite from being used for recovery, so we create a dummy # tmpmetamathsite file for use by install.sh recovery the next time around. mkdir tmpmetamathsite # See comment about Windows XP above. echo "?Fatal error: Could not delete the subdirectory 'metamathsite'." echo "Is someone else using that subdirectory?" echo "On Windows, please reboot before running install.sh again." exit 1 fi elif [ -d metamathsite ] ; then # If the subdirectory metamathsite exists, we finished the # site master backup but everything else is in an unknown state # and may be corrupted. Recover from the site master backup. echo "Recovering from an earlier aborted run..." if [ -d metamathsite/metamathsite ] ; then # Bad bad user ... but even so he/she can still recover... echo "A run was aborted inside the metamathsite subdirectory of an earlier" echo "aborted run. You must first cd to the metamathsite subdirectory then" echo "run ./install.sh from there to recover, then come back here and" echo "run ./install.sh again to complete the recovery." exit 1 fi # This will delete files but leave directories intact # Of course, we don't want to delete the install.sh we're running from # nor any files we're logging to rm -f `ls | egrep -v "install.sh|install.log|nohup.out"` # Now delete all directories except the metamathsite recovery directory. # The "-name "?*" filters the empty "." directory. for i in `find . -type d -name "?*" | egrep -v "metamathsite"` do rm -rf $i if [ -d $i ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not delete the subdirectory '$i'." echo "Is someone else using that subdirectory?" echo "On Windows, please reboot before running install.sh again." exit 1 fi done cd metamathsite # Finally, move all files up a level where they are expected, then delete the # metamathsite recovery directory mv `ls | grep -v install.sh` .. cd .. rm -rf metamathsite if [ -d metamathsite ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not delete the subdirectory 'metamathsite'." echo "Is someone else using that subdirectory?" echo "If this is Windows, please reboot before running install.sh again." exit 1 fi fi ######## End of recover if a previous run was aborted in the middle ####### echo "Creating subdirectories..." # Remove "backup" version of set.mm if any [ -f metamathsite/set.mm~1 ] && rm -f metamathsite/set.mm~1 # Remove "working" version of set.mm if any [ -f metamathsite/set.mm ] && rm -f metamathsite/set.mm ##### Recreate the minimal site master for recovery and archiving ##### # The minimal site recovery files are placed in a temporary subdirectory # called metamathsite, which persists until the end in case this script # is aborted. Before deleting the metamathsite subdirectory, it is # archived into metamathsite.tar.gz which will allow the site to be # rebuilt on another machine. # Remove old tmp directory (if it exists) and create new one rm -rf tmpmetamathsite if [ -d tmpmetamathsite ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not delete the subdirectory 'tmpmetamathsite'." echo "Is someone else using that subdirectory?" echo "If this is Windows, please reboot before running install.sh again." exit 1 fi mkdir tmpmetamathsite # Copy home directory files; create needed subdirectories for i in * do [ -f $i ] && cp -p $i tmpmetamathsite/ done # We skip the tmpmetamathsite we're working on, of course; also, mpeuni # and qleuni are fully automatically generated so we skip them too for i in `find . -type d -name "?*" | egrep -v "tmpmetamathsite|mpeuni|qleuni"` do mkdir tmpmetamathsite/$i done # Remove any log files from previous (or this) run [ -f tmpmetamathsite/install.log ] && rm -f tmpmetamathsite/install.log [ -f tmpmetamathsite/nohup.out ] && rm -f tmpmetamathsite/nohup.out # Copy subdirectories but omit the two "Explorer"s for now for i in `find . -type d -name "?*" | egrep -v \ "tmpmetamathsite|mpegif|mpeuni|qlegif|qleuni"` do cp -p $i/* tmpmetamathsite/$i/ done # Copy only manually-created files from the "Explorer"s # Metamath Proof Explorer cd mpegif # Copy all the non-html files find . -type f ! -name "*.html" -exec cp -p {} ../tmpmetamathsite/mpegif/ \; # Delete any non-custom symbols that exist in the symbols directory for i in *.gif do [ -f ../symbols/$i ] && rm -f ../tmpmetamathsite/mpegif/$i done # Delete files that will be copied from home directory [ -f mm.gif ] && rm -f ../tmpmetamathsite/mpegif/mm.gif [ -f favicon.ico ] && rm -f ../tmpmetamathsite/mpegif/favicon.ico [ -f _nmemail.gif ] && rm -f ../tmpmetamathsite/mpegif/_nmemail.gif # Our convention is that all manually-created html files begin with "mm" cp -p mm*.html ../tmpmetamathsite/mpegif/ # But some of them are automatically generated, so we don't include them # Omit the automatically-generated mm*.html files [ -f mmtheorems.html ] && rm -f ../tmpmetamathsite/mpegif/mmtheorems.html [ -f mmdefinitions.html ] && rm -f ../tmpmetamathsite/mpegif/mmdefinitions.html [ -f mmascii.html ] && rm -f ../tmpmetamathsite/mpegif/mmascii.html cd .. # Quantum Logic Explorer cd qlegif # Copy all the non-html files find . -type f ! -name "*.html" -exec cp -p {} ../tmpmetamathsite/qlegif/ \; # Delete any non-custom symbols that exist in the symbols directory for i in *.gif do [ -f ../symbols/$i ] && rm -f ../tmpmetamathsite/qlegif/$i done # Delete any non-custom symbols that exist in the mpegif directory for i in *.gif do [ -f ../mpegif/$i ] && rm -f ../tmpmetamathsite/qlegif/$i done # Delete files that will be copied from home directory [ -f favicon.ico ] && rm -f ../tmpmetamathsite/qlegif/favicon.ico [ -f _nmemail.gif ] && rm -f ../tmpmetamathsite/qlegif/_nmemail.gif # Our convention is that all manually-created html files begin with "mm" cp -p mm*.html ../tmpmetamathsite/qlegif/ # Omit the automatically-generated mm*.html files [ -f mmtheorems.html ] && rm -f ../tmpmetamathsite/qlegif/mmtheorems.html [ -f mmdefinitions.html ] && rm -f ../tmpmetamathsite/qlegif/mmdefinitions.html [ -f mmascii.html ] && rm -f ../tmpmetamathsite/qlegif/mmascii.html cd .. # Metamath Solitaire cd mmsolitaire # Delete any non-custom symbols that exist in the symbols directory for i in *.gif do [ -f ../symbols/$i ] && rm -f ../tmpmetamathsite/mmsolitaire/$i done # Delete any symbols that exist in the mpegif directory for i in *.gif do [ -f ../mpegif/$i ] && rm -f ../tmpmetamathsite/mmsolitaire/$i done # Delete files that will be copied from home directory [ -f mm.gif ] && rm -f ../tmpmetamathsite/mmsolitaire/mm.gif [ -f favicon.ico ] && rm -f ../tmpmetamathsite/mmsolitaire/favicon.ico [ -f _nmemail.gif ] && rm -f ../tmpmetamathsite/mmsolitaire/_nmemail.gif cd .. # GIF Images for Math Symbols cd symbols # Delete files that will be copied from home directory [ -f mm.gif ] && rm -f ../tmpmetamathsite/symbols/mm.gif [ -f favicon.ico ] && rm -f ../tmpmetamathsite/symbols/favicon.ico [ -f _nmemail.gif ] && rm -f ../tmpmetamathsite/symbols/_nmemail.gif #[ -f valid-html401.png ] && rm -f ../tmpmetamathsite/symbols/valid-html401.png cd .. # LaTeX directory cd latex # Remove auxilliary files created by LaTeX (all files but *.tex) find . -type f ! -name "*.tex" -exec rm -f ../tmpmetamathsite/latex/{} \; cd .. # Download directory # Remove the automatically-generated compressed downloads; by convention these # are ones whose prefix is a directory name for i in mpegif mpeuni qlegif qleuni mmsolitaire symbols metamathsite metamath do [ -f downloads/${i}.tar.bz2 ] && rm -f tmpmetamathsite/downloads/${i}.tar.bz2 [ -f downloads/${i}.tar.gz ] && rm -f tmpmetamathsite/downloads/${i}.tar.gz [ -f downloads/${i}.zip ] && rm -f tmpmetamathsite/downloads/${i}.zip done # Remove the automatically-created .pdf files for i in metamath finiteaxiom megillaward2003 megillaward2004 do [ -f downloads/${i}.pdf ] && rm -f tmpmetamathsite/downloads/${i}.pdf done # Remove all but one compressed quantum-logic - leave the .bz2 [ -f downloads/quantum-logic.tar.gz ] && rm -f tmpmetamathsite/downloads/quantum-logic.tar.gz [ -f downloads/quantum-logic.zip ] && rm -f tmpmetamathsite/downloads/quantum-logic.zip # Remove any previous (platform-dependent) metamath compilation left # over from an aborted run [ -f metamath/metamath ] && rm -f tmpmetamathsite/metamath/metamath # We're now done creating the minimal site master backup; rename it # First delete any old metamathsite (shouldn't exist but just in case) rm -rf metamathsite if [ -d metamathsite ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not delete the subdirectory 'metamathsite'." echo "Is someone else using that subdirectory?" echo "On Windows, please reboot before running install.sh again." exit 1 fi mv tmpmetamathsite metamathsite if [ -d tmpmetamathsite ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not rename the subdirectory 'tmpmetamathsite'." echo "Is someone else using that subdirectory?" echo "On Windows, please reboot before running install.sh again." exit 1 fi ########### End of creating minimal site master ############### ########### Compile Metamath ############# cd metamath # Make sure the Windows version is executable under Cygwin [ -f metamath.exe ] && chmod +x metamath.exe echo "Compiling Metamath..." if $CYGWIN ; then # Save the original Windows metamath.exe in case we're running on Cygwin, # because in Cygwin, gcc appends .exe to the compiled file name [ -f metamath.exe ] && mv metamath.exe metamath.exe-save fi gcc m*.c -o metamath -O3 -funroll-loops -finline-functions \ -fomit-frame-pointer -Wall -ansi -pedantic cd .. ######## Generate Metamath Proof Explorer ############ # Copy manually-created files. The mpegif directory is assumed to contain # the lastest "master" versions of them. The mpeuni directory is discarded. mkdir mpegif-new cp -p metamathsite/mpegif/* mpegif-new/ [ -f favicon.ico ] && cp -p favicon.ico mpegif-new/ [ -f _nmemail.gif ] && cp -p _nmemail.gif mpegif-new/ [ -f mm.gif ] && cp -p mm.gif mpegif-new/ # Copy the non-custom symbols from the symbols subdirectory, plus mm.gif for i in \ 0 1 2 3 4 5 6 7 8 9 amp approx ast backquote backtick bang bbc bbn bbq \ bbr bbz bigcap bigcup bigto caln calp calq calr cap cdot ce ci circ colon \ comma cup cv diagup eq exists forall uparrow i im in langle \ lbrace lbrack leftrightarrow le lnot longrightarrow lp lt minus ne notin \ omega onetoone onetooneonto onto perp plus preccurlyeq prec rangle \ rbrace rbrack re restriction rightsquigarrow rp scrh scrp setminus \ shortminus smallsmile solidus subseteq subset supast surd times to \ varnothing vee vert wedge varaleph lessdot mm do [ -f symbols/${i}.gif ] && cp -p symbols/${i}.gif mpegif-new/ done # All manually-created files are the same for both gif and symbol-font versions mkdir mpeuni-new cp -p mpegif-new/* mpeuni-new/ cd mpegif-new # show statement... = regenerate proof pages # write bibliography... = refresh bibiographic cross-reference # write recent_additions... = refresh recent additions ../metamath/metamath "read '../metamath/set.mm'" \ "show statement */html" \ "write theorem_list /theorems_per_page 100" \ "write bibliography mmbiblio.html" \ "write recent_additions mmrecent.html / limit 100" \ "exit" rm -f mmtheorems.html~1 rm -f mmbiblio.html~1 rm -f mmrecent.html~1 cd .. # There should not be an old one, but just in case rm -rf mpegif-old if [ -d mpegif-old ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not delete the subdirectory 'mpegif-old'." echo "Is someone else using that subdirectory?" echo "If this is Windows, please reboot before running install.sh again." exit 1 fi mv mpegif mpegif-old if [ -d mpegif ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not rename the subdirectory 'mpegif'." echo "Is someone else using that subdirectory?" echo "If this is Windows, please reboot before running install.sh again." exit 1 fi mv mpegif-new mpegif if [ -d mpegif-new ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not rename the subdirectory 'mpegif-new'." echo "Is someone else using that subdirectory?" echo "If this is Windows, please reboot before running install.sh again." exit 1 fi rm -rf mpegif-old if [ -d mpegif-old ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not delete the subdirectory 'mpegif-old'." echo "Is someone else using that subdirectory?" echo "On Windows, please reboot before running install.sh again." exit 1 fi cd mpeuni-new # show statement... = regenerate proof pages (alt_html = Unicode version) # write bibliography... = refresh bibiographic cross-reference # write recent_additions... = refresh recent additions ../metamath/metamath "read '../metamath/set.mm'" \ "show statement */alt_html" \ "write theorem_list /theorems_per_page 100" \ "write bibliography mmbiblio.html" \ "write recent_additions mmrecent.html / limit 100" \ "exit" rm -f mmtheorems.html~1 rm -f mmbiblio.html~1 rm -f mmrecent.html~1 cd .. if ! [ -d mpeuni ] ; then # We're doing an initial build, not a rebuild mkdir mpeuni fi # There should not be an old one, but just in case rm -rf mpeuni-old if [ -d mpeuni-old ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not delete the subdirectory 'mpeuni-old'." echo "Is someone else using that subdirectory?" echo "If this is Windows, please reboot before running install.sh again." exit 1 fi mv mpeuni mpeuni-old if [ -d mpeuni ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not rename the subdirectory 'mpeuni'." echo "Is someone else using that subdirectory?" echo "If this is Windows, please reboot before running install.sh again." exit 1 fi mv mpeuni-new mpeuni if [ -d mpeuni-new ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not rename the subdirectory 'mpeuni-new'." echo "Is someone else using that subdirectory?" echo "If this is Windows, please reboot before running install.sh again." exit 1 fi rm -rf mpeuni-old if [ -d mpeuni-old ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not delete the subdirectory 'mpeuni-old'." echo "Is someone else using that subdirectory?" echo "On Windows, please reboot before running install.sh again." exit 1 fi ######## Generate Quantum Logic Explorer ############ # Copy manually-created files. The qlegif directory is assumed to contain # the lastest "master" versions of them. The qleuni directory is discarded. mkdir qlegif-new cp -p metamathsite/qlegif/* qlegif-new/ [ -f favicon.ico ] && cp -p favicon.ico qlegif-new/ [ -f _nmemail.gif ] && cp -p _nmemail.gif qlegif-new/ # Copy the non-custom symbols needed from the symbols subdirectory for i in \ 0 1 amp bigto cap cc comma cup eq equiv le lnot lp rp to \ vee supperp langle rangle perp do [ -f symbols/${i}.gif ] && cp -p symbols/${i}.gif qlegif-new/ done # Copy the custom symbols needed from the mpegif subdirectory for i in _scrch _veeh _vdash _wff bn65_20 spacer do [ -f mpegif/${i}.gif ] && cp -p mpegif/${i}.gif qlegif-new/ done # All manually-created files are the same for both gif and symbol-font versions mkdir qleuni-new cp -p qlegif-new/* qleuni-new/ # Regenerate proof pages cd qlegif-new ../metamath/metamath "read '../metamath/ql.mm'" \ "show statement */html" \ "write theorem_list /theorems_per_page 100" \ "exit" rm -f mmtheorems.html~1 cd .. # There should not be an old one, but just in case rm -rf qlegif-old if [ -d qlegif-old ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not delete the subdirectory 'qlegif-old'." echo "Is someone else using that subdirectory?" echo "If this is Windows, please reboot before running install.sh again." exit 1 fi mv qlegif qlegif-old if [ -d qlegif ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not rename the subdirectory 'qlegif'." echo "Is someone else using that subdirectory?" echo "If this is Windows, please reboot before running install.sh again." exit 1 fi mv qlegif-new qlegif if [ -d qlegif-new ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not rename the subdirectory 'qlegif-new'." echo "Is someone else using that subdirectory?" echo "If this is Windows, please reboot before running install.sh again." exit 1 fi rm -rf qlegif-old if [ -d qlegif-old ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not delete the subdirectory 'qlegif-old'." echo "Is someone else using that subdirectory?" echo "On Windows, please reboot before running install.sh again." exit 1 fi cd qleuni-new ../metamath/metamath "read '../metamath/ql.mm'" \ "show statement */alt_html" \ "write theorem_list /theorems_per_page 100" \ "exit" rm -f mmtheorems.html~1 cd .. if ! [ -d qleuni ] ; then # We're doing an initial build, not a rebuild mkdir qleuni fi # There should not be an old one, but just in case rm -rf qleuni-old if [ -d qleuni-old ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not delete the subdirectory 'qleuni-old'." echo "Is someone else using that subdirectory?" echo "If this is Windows, please reboot before running install.sh again." exit 1 fi mv qleuni qleuni-old if [ -d qleuni ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not rename the subdirectory 'qleuni'." echo "Is someone else using that subdirectory?" echo "If this is Windows, please reboot before running install.sh again." exit 1 fi mv qleuni-new qleuni if [ -d qleuni-new ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not rename the subdirectory 'qleuni-new'." echo "Is someone else using that subdirectory?" echo "If this is Windows, please reboot before running install.sh again." exit 1 fi rm -rf qleuni-old if [ -d qleuni-old ] ; then # See comment about Windows XP above. echo "?Fatal error: Could not delete the subdirectory 'qleuni-old'." echo "Is someone else using that subdirectory?" echo "On Windows, please reboot before running install.sh again." exit 1 fi ########### Get files needed for Metamath Solitaire ########### [ -f mm.gif ] && cp -p mm.gif mmsolitaire/ [ -f favicon.ico ] && cp -p favicon.ico mmsolitaire/ [ -f _nmemail.gif ] && cp -p _nmemail.gif mmsolitaire/ # Copy the non-custom symbols from the symbols subdirectory for i in \ bigcap bigcup cap cup eq exists forall in lbrace leftrightarrow lnot \ lp rbrace rp subseteq to varnothing vee vert wedge do [ -f symbols/${i}.gif ] && cp -p symbols/${i}.gif mmsolitaire/ done # Copy the custom symbols from the mpegif subdirectory for i in _ca _cb _x _y _z _varphi _psi do [ -f mpegif/${i}.gif ] && cp -p mpegif/${i}.gif mmsolitaire/ done ########### Get files needed for GIF Images for Math Symbols ########### [ -f mm.gif ] && cp -p mm.gif symbols/ [ -f favicon.ico ] && cp -p favicon.ico symbols/ [ -f _nmemail.gif ] && cp -p _nmemail.gif symbols/ # This was taken out 10-Aug-03 since the directory is pubic domain # and we don't want to include copyrighted images #[ -f valid-html401.png ] && cp -p valid-html401.png symbols/ ########### Generate PDF files from LaTeX sources ########### # Since not all systems will have LaTeX, we will just warn if it is missing. # But the user will have to get the PDF files from the Metamath site. # Check that LaTeX software is present LATEX_OK=true LATEX_DEPS="touch sed grep makeindex bibtex pdflatex" LATEX_WRN2="?Therefore PDF files 'metamath.pdf', 'finiteaxiom.pdf'," LATEX_WRN3="?'megillaward2003.pdf', and 'megillaward2003.pdf' may not have" LATEX_WRN4="?been created. You should download them from http://metamath.org" LATEX_WRN5="?and put them in the 'downloads' subdirectory." for item in $LATEX_DEPS do if [ -z "`which $item`" ]; then LATEX_OK=false LATEX_WRN1="?Warning: '$item' (needed for LaTeX) is not present on your system." fi done if $LATEX_OK ; then cd latex # Compile metamath.pdf - ignore warnings from initial runs grep "^%realref.sty%" metamath.tex | sed -e s/^%realref.sty%// > realref.sty grep "^%bib%" metamath.tex | sed -e s/^%bib%// > metamath.bib touch metamath.ind pdflatex metamath > /dev/null 2>&1 pdflatex metamath > /dev/null 2>&1 bibtex metamath makeindex metamath > /dev/null 2>&1 pdflatex metamath > /dev/null 2>&1 pdflatex metamath # Compile finiteaxiom.pdf pdflatex finiteaxiom > /dev/null 2>&1 pdflatex finiteaxiom # Compile megillaward2003.pdf pdflatex megillaward2003 > /dev/null 2>&1 pdflatex megillaward2003 # Compile megillaward2004.pdf pdflatex megillaward2004 > /dev/null 2>&1 pdflatex megillaward2004 # Move the PDF files to the downloads directory if [ -f metamath.pdf ] ; then mv metamath.pdf ../downloads else LATEX_OK=false LATEX_WRN1="?Warning: There was a problem creating 'metamath.pdf'." fi if [ -f finiteaxiom.pdf ] ; then mv finiteaxiom.pdf ../downloads else LATEX_OK=false LATEX_WRN1="?Warning: There was a problem creating 'finiteaxiom.pdf'." fi if [ -f megillaward2003.pdf ] ; then mv megillaward2003.pdf ../downloads else LATEX_OK=false LATEX_WRN1="?Warning: There was a problem creating 'megillaward2003.pdf'." fi if [ -f megillaward2004.pdf ] ; then mv megillaward2004.pdf ../downloads else LATEX_OK=false LATEX_WRN1="?Warning: There was a problem creating 'megillaward2004.pdf'." fi cd .. fi ########### Final cleanup ########### # A file name with ~ is a previous version of a file created by Metamath # (There should be none, but just in case...) find . -name '*~[1-9]' -exec rm -f {} \; # We don't keep the compiled code because it is platform-dependent if $CYGWIN ; then # Cygwin [ -f metamath/metamath.exe ] && rm -f metamath/metamath.exe # Restore the original Windows exe # Note: the original was compiled with lcc: # lc -O m*.c -o metamath.exe # because it has a small size and doesn't require the Cygwin dll [ -f metamath/metamath.exe-save ] && mv metamath/metamath.exe-save \ metamath/metamath.exe else # Unix # (8/1/03: I decided to keep it for convenience. The drawback is # that it may not run on all systems without recompiling. # I put a note about this in metamath/README.TXT. - nm) # [ -f metamath/metamath ] && rm -f metamath/metamath # Dummy statement - bash doesn't like empty else..fi echo ' ' > /dev/null fi echo "Creating compressed downloads..." # Create the download files linked on the home page # Copy the README.TXT file to DOS-format __README.TXT # (This sed command changes LF to CRLF) sed -e "s/\$/`echo -e '\r'`/" metamath/README.TXT > metamath/__README.TXT tar -cjf downloads/metamath.tar.bz2 metamath tar -cf - metamath | gzip -9 > downloads/metamath.tar.gz [ -f downloads/metamath.zip ] && rm -f downloads/metamath.zip zip -r9 downloads/metamath.zip metamath # Now restore the original files rm -f metamath/__README.TXT # Change out-of-directory links in the mpegif download to # absolute URLs so that it won't have broken links # (The links to the "Symbol font version" will still be broken, # but the user is told that on index.html.) FILE_LIST="mmset.html mmhil.html mmmusic.html" mkdir tmp for i in $FILE_LIST ; do cp -p mpegif/$i tmp/ # The 2nd sed removes the web bug. sed -e 's/HREF=\"..\//HREF=\"http:\/\/us.metamath.org\//g' \ < tmp/$i \ | sed -e 's/http:\/\/us2.metamath.org:8888\/mpegif\/short/short/g' \ > mpegif/$i done # Copy the README.TXT file to DOS-format __README.TXT # (This sed command changes LF to CRLF) sed -e "s/\$/`echo -e '\r'`/" mpegif/README.TXT > mpegif/__README.TXT # Create the download files tar -cjf downloads/mpegif.tar.bz2 mpegif tar -cf - mpegif | gzip -9 > downloads/mpegif.tar.gz [ -f downloads/mpegif.zip ] && rm -f downloads/mpegif.zip zip -r9 downloads/mpegif.zip mpegif # Now restore the original files mv tmp/* mpegif/ rmdir tmp/ rm -f mpegif/__README.TXT # Change out-of-directory links in the qlegif download to # absolute URLs so that it won't have broken links mkdir tmp/ cp -p qlegif/mmql.html tmp/ sed -e 's/HREF=\"..\//HREF=\"http:\/\/us.metamath.org\//g' \ < tmp/mmql.html > qlegif/mmql.html # Copy the README.TXT file to DOS-format __README.TXT # (This sed command changes LF to CRLF) sed -e "s/\$/`echo -e '\r'`/" qlegif/README.TXT > qlegif/__README.TXT # Create the download files tar -cjf downloads/qlegif.tar.bz2 qlegif tar -cf - qlegif | gzip -9 > downloads/qlegif.tar.gz [ -f downloads/qlegif.zip ] && rm -f downloads/qlegif.zip zip -r9 downloads/qlegif.zip qlegif # Now restore the original mmql.html mv tmp/* qlegif/ rmdir tmp/ rm -f qlegif/__README.TXT # The Unicode versions are not presently downloadable #tar -cf - mpeuni | gzip -9 > downloads/mpeuni.tar.gz #tar -cf - qleuni | gzip -9 > downloads/qleuni.tar.gz # Change out-of-directory links in the mmsolitaire download to # absolute URLs so that it won't have broken links mkdir tmp/ cp -p mmsolitaire/mms.html tmp/ sed -e 's/HREF=\"..\//HREF=\"http:\/\/us.metamath.org\//g' \ < tmp/mms.html > mmsolitaire/mms.html # Copy the README.TXT file to DOS-format __README.TXT # (This sed command changes LF to CRLF) sed -e "s/\$/`echo -e '\r'`/" mmsolitaire/README.TXT > mmsolitaire/__README.TXT # Create the download files tar -cjf downloads/mmsolitaire.tar.bz2 mmsolitaire tar -cf - mmsolitaire | gzip -9 > downloads/mmsolitaire.tar.gz [ -f downloads/mmsolitaire.zip ] && rm -f downloads/mmsolitaire.zip zip -r9 downloads/mmsolitaire.zip mmsolitaire # Now restore the original mmsolitaire directory mv tmp/* mmsolitaire/ rmdir tmp/ rm -f mmsolitaire/__README.TXT # Our goal in the following section is to have a consistent md5sum # for symbols.zip after rebuilding, so that the md5sum can identify # the symbols.zip version (and not just the day of that particular build). # 21-Mar-04: I gave up on getting a consistent checksum from the zip # program version 2.3. On Linux Debian it doesn't reproduce the exact # same binary when run multiple times on the same set of files, even # though it did on RedHat 7.2. Multiple versions are sometimes off by one # bit per file, perhaps a redundant bit that doesn't get initialized in # memory by the program. Therefore I took out the section of symbols.html # that used to be updated by the code below, but I'm leaving in the code # (it does no harm) because it would probably work for tar.gz files if we # want that later on. For historical purposes this section read as follows: #

Copyright Disclaimer    # #

For the purpose of this disclaimer, "this work" refers # to exactly and only the contents of the compressed folder "symbols.zip", # including all text and images contained therein, in its original form # # downloaded from the URL "http://us.metamath.org/downloads/symbols.zip" (0.6MB), with MD5 # checksum 7cfe8a4137cb7dd5b8ea0185e4f7b914 # (computed by the program "md5sum"). # #

This work was created by Norman Megill, who # explicitly abandons in perpetuity any copyright or other proprietary # interest in this work, thereby granting it to the public domain. This # means it may be used for any purpose whatsoever, with or without # acknowledgement, commercial or non-commercial, including use in a # separate or derivative copyrighted work. No warranty of any kind is # expressed or implied. Any trademarks mentioned in this work belong to # their respective owners and must be treated accordingly in any # derivative work. # #

Any modification to a public-domain work will # result in a new work that is copyrighted, unless the new author chooses # to abandon the copyright. The MD5 checksum helps assure you that you # are not inadvertently infringing the copyright of a derivative # work. mkdir tmp/ cp -p symbols/symbols.html tmp/ # Change out-of-directory links in the symbols download to # absolute URLs so that it won't have broken links # Also, comment out the (old) MD5 sum (that will no longer be valid) WEB=", with MD5 checksum as shown on the web page" WEB="${WEB} \\\"/' \ > symbols/symbols.html # Remove the checksum so we will have a consistent md5sum in the future cp -p symbols/symbols.html 1.tmp sed -e \ 's/^checksum [0-9a-fA-F]*/checksum 00000000000000000000000000000000/' \ < 1.tmp \ > symbols/symbols.html rm -f 1.tmp # Restore the time to prevent different md5sum upon rebuild touch -r tmp/symbols.html symbols/symbols.html # Copy the README.TXT file to DOS-format __README.TXT # (This sed command changes LF to CRLF) sed -e "s/\$/`echo -e '\r'`/" symbols/README.TXT > symbols/__README.TXT # Restore the time to prevent different md5sum upon rebuild touch -r symbols/README.TXT symbols/__README.TXT # Create the downloads tar -cjf downloads/symbols.tar.bz2 symbols tar -cf - symbols | gzip -9 > downloads/symbols.tar.gz [ -f downloads/symbols.zip ] && rm -f downloads/symbols.zip # Fix protection of new files for consistent md5sum (umask may be different # running from login vs. cron) for i in __README.TXT symbols.html do [ -f symbols/${i} ] && chmod 644 symbols/${i} done # # Fix all access times to a constant for consistent md5sum find symbols/ -type f -exec touch -a -t 200212312359 {} \; # # We can't use 'zip -r downloads/symbols.zip symbols' because it puts # the files in an unpredicatable order, causing an inconsistent md5sum # from run to run. Instead, we do the following: # (This old version causes argument list overflow on Cygwin:) # zip -r downloads/symbols.zip `LC_COLLATE=C ls symbols/*` # (This newer version seems to work on all systems:) LC_COLLATE=C ls symbols | sed -e 's/^/symbols\//' | \ xargs zip -r9 downloads/symbols.zip # (Note that LC_COLLATE=C above forces a standard sorting order for 'ls', # regardless of the system setting that can be seen with the 'locale' # program. [The 'locale' program doesn't seem to be available on Cygwin.]) # # Now restore the original symbols directory # Also, compute the new MD5 sum MD5CHECKSUM=`md5sum downloads/symbols.zip | cut -f1 -d " "` sed -e \ "s/^checksum [0-9a-fA-F]*/checksum ${MD5CHECKSUM}/" \ < tmp/symbols.html \ > symbols/symbols.html # Restore the time to prevent different md5sum upon future rebuild touch -r tmp/symbols.html symbols/symbols.html # Remove the temporary directory rm -f tmp/symbols.html rmdir tmp/ # Remove the unofficial __README.TXT rm -f symbols/__README.TXT # Create the alternate quantum-logic downloads (only .bz2 is permanent) tar -xjf downloads/quantum-logic.tar.bz2 tar -cf - quantum-logic | gzip -9 > downloads/quantum-logic.tar.gz [ -f downloads/quantum-logic.zip ] && rm -f downloads/quantum-logic.zip zip -r9 downloads/quantum-logic.zip quantum-logic rm -rf quantum-logic/ # Create final minimal site master file # Copy the updated MD5 sum to the site build directory - just to be nitpicky cp -p symbols/symbols.html metamathsite/symbols/ # Copy the README.TXT file to DOS-format __README.TXT # (This sed command changes LF to CRLF) sed -e "s/\$/`echo -e '\r'`/" metamathsite/README.TXT \ > metamathsite/__README.TXT tar -cjf downloads/metamathsite.tar.bz2 metamathsite tar -cf - metamathsite | gzip -9 > downloads/metamathsite.tar.gz [ -f downloads/metamathsite.zip ] && rm -f downloads/metamathsite.zip zip -r9 downloads/metamathsite.zip metamathsite # Put in instructions for after the build echo "To navigate this directory, open index.html in your browser." > \ __README.TXT # Now delete the minimal site master directory rm -rf metamathsite/ if [ -d metamathsite ] ; then # If the rm -rf failed, some files in 'metamathsite' may be gone but not # others. However, everything else completed OK. We must prevent # metamathsite from being used for recovery, so we create a dummy # tmpmetamathsite file for use by install.sh recovery the next time around. mkdir tmpmetamathsite # See comment about Windows XP above. echo "?Fatal error: Could not delete the subdirectory 'metamathsite'." echo "Is someone else using that subdirectory?" echo "On Windows, please reboot before running install.sh again." exit 1 fi ########### Create compressed site for metamath.planetmirror.com ########## #tar -cf - * | gzip -9 > ../metamathmirror.tar.gz echo "" # Produce a warning if LaTeX is not installed if $LATEX_OK ; then echo "The installation completed successfully. The home page is index.html." else echo "The installation completed (mostly) successfully, except the following:" echo "" echo $LATEX_WRN1 echo $LATEX_WRN2 echo $LATEX_WRN3 echo $LATEX_WRN4 echo $LATEX_WRN5 fi