aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/build
diff options
context:
space:
mode:
Diffstat (limited to 'dev/build')
-rwxr-xr-xdev/build/osx/make-macos-dmg.sh12
-rw-r--r--dev/build/windows/configure_profile.sh24
-rw-r--r--dev/build/windows/difftar-folder.sh22
-rw-r--r--dev/build/windows/makecoq_mingw.sh261
4 files changed, 164 insertions, 155 deletions
diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh
index dc33838f1..c450e8157 100755
--- a/dev/build/osx/make-macos-dmg.sh
+++ b/dev/build/osx/make-macos-dmg.sh
@@ -10,19 +10,19 @@ VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml)
APP=bin/CoqIDE_${VERSION}.app
# Create a .app file with CoqIDE, without signing it
-make PRIVATEBINARIES=$APP -j $NJOBS -l2 $APP
+make PRIVATEBINARIES="$APP" -j "$NJOBS" -l2 "$APP"
# Add Coq to the .app file
-make OLDROOT=$OUTDIR COQINSTALLPREFIX=$APP/Contents/Resources/ install-coq install-ide-toploop
+make OLDROOT="$OUTDIR" COQINSTALLPREFIX="$APP/Contents/Resources/" install-coq install-ide-toploop
# Create the dmg bundle
-mkdir -p $DMGDIR
-ln -sf /Applications $DMGDIR/Applications
-cp -r $APP $DMGDIR
+mkdir -p "$DMGDIR"
+ln -sf /Applications "$DMGDIR/Applications"
+cp -r "$APP" "$DMGDIR"
mkdir -p _build
# Temporary countermeasure to hdiutil error 5341
# head -c9703424 /dev/urandom > $DMGDIR/.padding
-hdiutil create -imagekey zlib-level=9 -volname coq-$VERSION-installer-macos -srcfolder $DMGDIR -ov -format UDZO _build/coq-$VERSION-installer-macos.dmg
+hdiutil create -imagekey zlib-level=9 -volname "coq-$VERSION-installer-macos" -srcfolder "$DMGDIR" -ov -format UDZO "_build/coq-$VERSION-installer-macos.dmg"
diff --git a/dev/build/windows/configure_profile.sh b/dev/build/windows/configure_profile.sh
index 16c972e80..7e606b554 100644
--- a/dev/build/windows/configure_profile.sh
+++ b/dev/build/windows/configure_profile.sh
@@ -14,30 +14,30 @@
rcfile=~/.bash_profile
donefile=~/.bash_profile.upated
+# to learn about `exec >> $file`, see https://www.tldp.org/LDP/abs/html/x17974.html
+exec >> $rcfile
+
if [ ! -f $donefile ] ; then
- echo >> $rcfile
-
- if [ "$1" != "" -a "$1" != " " ]; then
- echo export http_proxy="http://$1" >> $rcfile
- echo export https_proxy="http://$1" >> $rcfile
- echo export ftp_proxy="http://$1" >> $rcfile
+ if [ "$1" != "" ] && [ "$1" != " " ]; then
+ echo export http_proxy="http://$1"
+ echo export https_proxy="http://$1"
+ echo export ftp_proxy="http://$1"
fi
-
- mkdir -p $RESULT_INSTALLDIR_CFMT/bin
+
+ mkdir -p "$RESULT_INSTALLDIR_CFMT/bin"
# A tightly controlled path helps to avoid issues
# Note: the order is important: first have the cygwin binaries, then the mingw binaries in the path!
# Note: /bin is mounted at /usr/bin and /lib at /usr/lib and it is common to use /usr/bin in PATH
# See cat /proc/mounts
- echo "export PATH=/usr/local/bin:/usr/bin:$RESULT_INSTALLDIR_CFMT/bin:/usr/$TARGET_ARCH/sys-root/mingw/bin:/cygdrive/c/Windows/system32:/cygdrive/c/Windows" >> $rcfile
+ echo "export PATH=/usr/local/bin:/usr/bin:$RESULT_INSTALLDIR_CFMT/bin:/usr/$TARGET_ARCH/sys-root/mingw/bin:/cygdrive/c/Windows/system32:/cygdrive/c/Windows"
# find and xargs complain if the environment is larger than (I think) 8k.
# ORIGINAL_PATH (set by cygwin) can be a few k and exceed the limit
- echo unset ORIGINAL_PATH >> $rcfile
-
+ echo unset ORIGINAL_PATH
# Other installations of OCaml will mess up things
- echo unset OCAMLLIB >> $rcfile
+ echo unset OCAMLLIB
touch $donefile
fi
diff --git a/dev/build/windows/difftar-folder.sh b/dev/build/windows/difftar-folder.sh
index cbcf14ec2..3bba451ec 100644
--- a/dev/build/windows/difftar-folder.sh
+++ b/dev/build/windows/difftar-folder.sh
@@ -42,7 +42,7 @@ fi
if [ "$strip" -gt 0 ] ; then
# Get the path/name of the first file from teh tar and extract the first $strip path components
# This assumes that the first file in the tar file has at least $strip many path components
- prefix=$(tar -t -f $tarfile | head -1 | cut -d / -f -$strip)/
+ prefix=$(tar -t -f "$tarfile" | head -1 | cut -d / -f -$strip)/
else
prefix=
fi
@@ -60,13 +60,13 @@ mkdir -p "$empty"
# Print information (this is ignored by patch)
-echo diff/patch file created on $(date) with:
-echo difftar-folder.sh $@
-echo TARFILE= $tarfile
-echo FOLDER= $folder
-echo TARSTRIP= $strip
-echo TARPREFIX= $prefix
-echo ORIGFOLDER= $orig
+echo diff/patch file created on "$(date)" with:
+echo difftar-folder.sh "$@"
+echo TARFILE= "$tarfile"
+echo FOLDER= "$folder"
+echo TARSTRIP= "$strip"
+echo TARPREFIX= "$prefix"
+echo ORIGFOLDER= "$orig"
# Make sure tar uses english output (for Mod time differs)
export LC_ALL=C
@@ -76,14 +76,14 @@ tar --diff -a -f "$tarfile" --strip $strip --directory "$folder" | grep "Mod tim
# Substitute ': Mod time differs' with nothing
file=${file/: Mod time differs/}
# Check if file exists
- if [ -f "$folder/$file" ] ; then
+ if [ -f "$folder/$file" ] ; then
# Extract original file
tar -x -a -f "$tarfile" --strip $strip --directory "$orig" "$prefix$file"
# Compute diff
- diff -u "$orig/$file" "$folder/$file"
+ diff -u "$orig/$file" "$folder/$file"
fi
done
if [ -d "$new" ] ; then
- diff -u -r --unidirectional-new-file $empty $new
+ diff -u -r --unidirectional-new-file "$empty" "$new"
fi
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 8e0d2341d..e5a7b04a1 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -67,7 +67,7 @@ RMDIR_BEFORE_BUILD=1
###################### ARCHITECTURES #####################
# The OS on which the build of the tool/lib runs
-BUILD=`gcc -dumpmachine`
+BUILD=$(gcc -dumpmachine)
# The OS on which the tool runs
# "`find /bin -name "*mingw32-gcc.exe"`" -dumpmachine
@@ -132,34 +132,34 @@ CYGWIN_REPO_FOLDER=${CYGWIN_REPO_FOLDER//\//%2f}
# Copy files
cp "$CYGWIN_LOCAL_CACHE_WFMT/$CYGWIN_REPO_FOLDER/$CYGWINARCH/setup.ini" $TARBALLS
cp /etc/setup/installed.db $TARBALLS
-
+
###################### LOGGING #####################
# The folder which receives log files
mkdir -p buildlogs
-LOGS=`pwd`/buildlogs
+LOGS=$(pwd)/buildlogs
# The current log target (first part of the log file name)
LOGTARGET=other
log1() {
- "$@" > $LOGS/$LOGTARGET-$1.log 2> $LOGS/$LOGTARGET-$1.err
+ "$@" > "$LOGS/$LOGTARGET-$1.log" 2> "$LOGS/$LOGTARGET-$1.err"
}
log2() {
- "$@" > $LOGS/$LOGTARGET-$1-$2.log 2> $LOGS/$LOGTARGET-$1-$2.err
+ "$@" > "$LOGS/$LOGTARGET-$1-$2.log" 2> "$LOGS/$LOGTARGET-$1-$2.err"
}
log_1_3() {
- "$@" > $LOGS/$LOGTARGET-$1-$3.log 2> $LOGS/$LOGTARGET-$1-$3.err
+ "$@" > "$LOGS/$LOGTARGET-$1-$3.log" 2> "$LOGS/$LOGTARGET-$1-$3.err"
}
logn() {
LOGTARGETEX=$1
shift
- "$@" > $LOGS/$LOGTARGET-$LOGTARGETEX.log 2> $LOGS/$LOGTARGET-$LOGTARGETEX.err
+ "$@" > "$LOGS/$LOGTARGET-$LOGTARGETEX.log" 2> "$LOGS/$LOGTARGET-$LOGTARGETEX.err"
}
-
+
###################### 'UNFIX' SED #####################
# In Cygwin SED used to do CR-LF to LF conversion, but since sed 4.4-1 this was changed
@@ -183,7 +183,7 @@ logn() {
# - create build folder
# - extract source archive
# - patch source file if patch exists
-#
+#
# Parameters
# $1 file server name including protocol prefix
# $2 file name (without extension)
@@ -206,68 +206,68 @@ function get_expand_source_tar {
else
name=$2
fi
-
+
if [ "$#" -ge 6 ] ; then
folder=$6
else
folder=$name
fi
-
+
# Set logging target
logtargetold=$LOGTARGET
LOGTARGET=$name
-
+
# Get the source archive either from the source cache or online
- if [ ! -f $TARBALLS/$name.$3 ] ; then
+ if [ ! -f "$TARBALLS/$name.$3" ] ; then
if [ -f "$SOURCE_LOCAL_CACHE_CFMT/$name.$3" ] ; then
- cp "$SOURCE_LOCAL_CACHE_CFMT/$name.$3" $TARBALLS
+ cp "$SOURCE_LOCAL_CACHE_CFMT/$name.$3" "$TARBALLS"
else
- wget $1/$2.$3
- if file -i $2.$3 | grep text/html; then
- echo Download failed: $1/$2.$3
+ wget "$1/$2.$3"
+ if file -i "$2.$3" | grep text/html; then
+ echo Download failed: "$1/$2.$3"
echo The file wget downloaded is an html file:
- cat $2.$3
+ cat "$2.$3"
exit 1
fi
if [ ! "$2.$3" == "$name.$3" ] ; then
- mv $2.$3 $name.$3
+ mv "$2.$3" "$name.$3"
fi
- mv $name.$3 $TARBALLS
+ mv "$name.$3" "$TARBALLS"
# Save the source archive in the source cache
if [ -d "$SOURCE_LOCAL_CACHE_CFMT" ] ; then
- cp $TARBALLS/$name.$3 "$SOURCE_LOCAL_CACHE_CFMT"
+ cp "$TARBALLS/$name.$3" "$SOURCE_LOCAL_CACHE_CFMT"
fi
fi
fi
-
+
# Remove build directory (clean build)
if [ $RMDIR_BEFORE_BUILD -eq 1 ] ; then
- rm -f -r $folder
+ rm -f -r "$folder"
fi
-
+
# Create build directory and cd
- mkdir -p $folder
- cd $folder
-
+ mkdir -p "$folder"
+ cd "$folder"
+
# Extract source archive
if [ "$3" == "zip" ] ; then
- log1 unzip $TARBALLS/$name.$3
+ log1 unzip "$TARBALLS/$name.$3"
if [ "$strip" == "1" ] ; then
# Ok, this is dirty, but it works and it fails if there are name clashes
- mv */* .
+ mv -- */* .
else
echo "Unzip strip count not supported"
return 1
fi
else
- logn untar tar xvaf $TARBALLS/$name.$3 --strip $strip
+ logn untar tar xvaf "$TARBALLS/$name.$3" --strip $strip
fi
-
+
# Patch if patch file exists
- if [ -f $PATCHES/$name.patch ] ; then
- log1 patch -p1 -i $PATCHES/$name.patch
+ if [ -f "$PATCHES/$name.patch" ] ; then
+ log1 patch -p1 -i "$PATCHES/$name.patch"
fi
-
+
# Go back to base folder
cd ..
@@ -283,7 +283,7 @@ function get_expand_source_tar {
# - cd to build folder and extract source archive
# - create bin_special subfolder and add it to $PATH
# - remember things for build_post
-#
+#
# Parameters
# $1 file server name including protocol prefix
# $2 file name (without extension)
@@ -305,27 +305,27 @@ function build_prep {
else
name=$2
fi
-
+
# Check if build is already done
- if [ ! -f flagfiles/$name.finished ] ; then
+ if [ ! -f "flagfiles/$name.finished" ] ; then
BUILD_PACKAGE_NAME=$name
BUILD_OLDPATH=$PATH
- BUILD_OLDPWD=`pwd`
+ BUILD_OLDPWD=$(pwd)
LOGTARGET=$name
- touch flagfiles/$name.started
-
- get_expand_source_tar $1 $2 $3 $strip $name
-
- cd $name
-
+ touch "flagfiles/$name.started"
+
+ get_expand_source_tar "$1" "$2" "$3" "$strip" "$name"
+
+ cd "$name"
+
# Create a folder and add it to path, where we can put special binaries
# The path is restored in build_post
mkdir bin_special
- PATH=`pwd`/bin_special:$PATH
-
+ PATH=$(pwd)/bin_special:$PATH
+
return 0
- else
+ else
return 1
fi
}
@@ -337,9 +337,9 @@ function build_prep {
# ------------------------------------------------------------------------------
function build_post {
- if [ ! -f flagfiles/$BUILD_PACKAGE_NAME.finished ]; then
- cd $BUILD_OLDPWD
- touch flagfiles/$BUILD_PACKAGE_NAME.finished
+ if [ ! -f "flagfiles/$BUILD_PACKAGE_NAME.finished" ]; then
+ cd "$BUILD_OLDPWD"
+ touch "flagfiles/$BUILD_PACKAGE_NAME.finished"
PATH=$BUILD_OLDPATH
LOGTARGET=other
fi
@@ -362,9 +362,10 @@ function build_post {
# ------------------------------------------------------------------------------
function build_conf_make_inst {
- if build_prep $1 $2 $3 ; then
+ if build_prep "$1" "$2" "$3" ; then
$4
- logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIX" "${@:5}"
+ logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIX" "${@:5}"
+ # shellcheck disable=SC2086
log1 make $MAKE_OPT
log2 make install
log2 make clean
@@ -383,6 +384,7 @@ function build_conf_make_inst {
function install_glob {
# Check if any files matching the pattern exist
if [ "$(echo $1)" != "$1" ] ; then
+ # shellcheck disable=SC2086
install -D -t $2 $1
fi
}
@@ -398,7 +400,7 @@ function install_glob {
# ------------------------------------------------------------------------------
function install_rec {
- ( cd $1 && find -type f -name "$2" -exec install -D -T $1/{} $3/{} \; )
+ ( cd "$1" && find . -type f -name "$2" -exec install -D -T "$1"/{} "$3"/{} \; )
}
# ------------------------------------------------------------------------------
@@ -411,7 +413,7 @@ function install_rec {
function list_files {
if [ ! -e "/build/filelists/$1" ] ; then
- ( cd "$PREFIXCOQ" && find -type f | sort > /build/filelists/$1 )
+ ( cd "$PREFIXCOQ" && find . -type f | sort > /build/filelists/"$1" )
fi
}
@@ -439,7 +441,7 @@ function diff_files {
# ------------------------------------------------------------------------------
function filter_files {
- egrep "$3" "/build/filelists/$2" > "/build/filelists/$1"
+ grep -E "$3" "/build/filelists/$2" > "/build/filelists/$1"
}
# ------------------------------------------------------------------------------
@@ -453,7 +455,7 @@ function files_to_nsis {
# Split the path in the file list into path and filename and create SetOutPath and File instructions
# Note: File /oname cannot be used, because it does not create the paths as SetOutPath does
# Note: I didn't check if the redundant SetOutPath instructions have a bad impact on installer size or install time
- cat "/build/filelists/$1" | tr '/' '\\' | sed -r 's/^\.(.*)\\([^\\]+)$/SetOutPath $INSTDIR\\\1\nFile ${COQ_SRC_PATH}\\\1\\\2/' > "/build/filelists/$1.nsh"
+ tr '/' '\\' < "/build/filelists/$1" | sed -r 's/^\.(.*)\\([^\\]+)$/SetOutPath $INSTDIR\\\1\nFile ${COQ_SRC_PATH}\\\1\\\2/' > "/build/filelists/$1.nsh"
}
@@ -501,7 +503,7 @@ function make_fontconfig {
make_freetype
make_expat
# CONFIGURE PARAMETERS
- # build/install fails without --disable-docs
+ # build/install fails without --disable-docs
build_conf_make_inst http://www.freedesktop.org/software/fontconfig/release fontconfig-2.11.94 tar.gz true --disable-docs
}
@@ -532,7 +534,7 @@ function make_ncurses {
#
# CONFIGURE PARAMETERS
# --enable-term-driver --enable-sp-funcs is rewuired for mingw (see README.MinGW)
- # additional changes
+ # additional changes
# ADD --with-pkg-config
# ADD --enable-pc-files
# ADD --without-manpages
@@ -604,7 +606,7 @@ function make_gdk-pixbuf {
# CONFIGURE PARAMETERS
# --with-included-loaders=yes statically links the image file format handlers
# This avoids "Cannot open pixbuf loader module file '/usr/x86_64-w64-mingw32/sys-root/mingw/lib/gdk-pixbuf-2.0/2.10.0/loaders.cache': No such file or directory"
- build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.32 gdk-pixbuf-2.32.1 tar.xz true --with-included-loaders=yes
+ build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.32 gdk-pixbuf-2.32.1 tar.xz true --with-included-loaders=yes
}
##### CAIRO #####
@@ -657,8 +659,8 @@ function make_gtk3 {
build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/gtk+/3.16 gtk+-3.16.7 tar.xz true
# make all incl. tests and examples runs through fine
- # make install fails with issue with
- #
+ # make install fails with issue with
+ #
# make[5]: Entering directory '/home/soegtrop/GTK/gtk+-3.16.7/demos/gtk-demo'
# test -n "" || ../../gtk/gtk-update-icon-cache --ignore-theme-index --force "/usr/x86_64-w64-mingw32/sys-root/mingw/share/icons/hicolor"
# gtk-update-icon-cache.exe: Failed to open file /usr/x86_64-w64-mingw32/sys-root/mingw/share/icons/hicolor/.icon-theme.cache : No such file or directory
@@ -676,7 +678,8 @@ function make_libxml2 {
if build_prep https://git.gnome.org/browse/libxml2/snapshot libxml2-2.9.1 tar.xz ; then
# ./autogen.sh --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIX" --disable-shared --without-python
# shared library required by gtksourceview
- ./autogen.sh --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIX" --without-python
+ ./autogen.sh --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIX" --without-python
+ # shellcheck disable=SC2086
log1 make $MAKE_OPT all
log2 make install
log2 make clean
@@ -708,12 +711,12 @@ function make_gtk_sourceview2 {
# Install flexdll objects
function install_flexdll {
- cp flexdll.h /usr/$TARGET_ARCH/sys-root/mingw/include
+ cp flexdll.h "/usr/$TARGET_ARCH/sys-root/mingw/include"
if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
- cp flexdll*_mingw.o /usr/$TARGET_ARCH/bin
+ cp flexdll*_mingw.o "/usr/$TARGET_ARCH/bin"
cp flexdll*_mingw.o "$PREFIXOCAML/bin"
elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then
- cp flexdll*_mingw64.o /usr/$TARGET_ARCH/bin
+ cp flexdll*_mingw64.o "/usr/$TARGET_ARCH/bin"
cp flexdll*_mingw64.o "$PREFIXOCAML/bin"
else
echo "Unknown target architecture"
@@ -724,8 +727,8 @@ function install_flexdll {
# Install flexlink
function install_flexlink {
- cp flexlink.exe /usr/$TARGET_ARCH/bin
-
+ cp flexlink.exe "/usr/$TARGET_ARCH/bin"
+
cp flexlink.exe "$PREFIXOCAML/bin"
}
@@ -745,8 +748,10 @@ function get_flex_dll_link_bin {
function make_flex_dll_link {
if build_prep http://alain.frisch.fr/flexdll flexdll-0.34 tar.gz ; then
if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
+ # shellcheck disable=SC2086
log1 make $MAKE_OPT build_mingw flexlink.exe
elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then
+ # shellcheck disable=SC2086
log1 make $MAKE_OPT build_mingw64 flexlink.exe
else
echo "Unknown target architecture"
@@ -769,11 +774,11 @@ function make_ln {
if [ ! -f flagfiles/myln.finished ] ; then
touch flagfiles/myln.started
mkdir -p myln
- cd myln
+ ( cd myln
cp $PATCHES/ln.c .
- $TARGET_ARCH-gcc -DUNICODE -D_UNICODE -DIGNORE_SYMBOLIC -mconsole -o ln.exe ln.c
+ "$TARGET_ARCH-gcc" -DUNICODE -D_UNICODE -DIGNORE_SYMBOLIC -mconsole -o ln.exe ln.c
install -D ln.exe "$PREFIXCOQ/bin/ln.exe"
- cd ..
+ )
touch flagfiles/myln.finished
fi
}
@@ -799,14 +804,14 @@ function make_ocaml {
# Prefix is fixed in make file - replace it with the real one
# TODO: this might not work if PREFIX contains spaces
sed -i "s|^PREFIX=.*|PREFIX=$PREFIXOCAML|" config/Makefile
-
+
# We don't want to mess up Coq's directory structure so put the OCaml library in a separate folder
# If we refer to the make variable ${PREFIX} below, camlp5 ends up having the wrong path:
# D:\bin\coq64_buildtest_abs_ocaml4\bin>ocamlc -where => D:/bin/coq64_buildtest_abs_ocaml4/libocaml
# D:\bin\coq64_buildtest_abs_ocaml4\bin>camlp4 -where => ${PREFIX}/libocaml\camlp4
# So we put an explicit path in there
sed -i "s|^LIBDIR=.*|LIBDIR=$PREFIXOCAML/libocaml|" config/Makefile
-
+
# Note: ocaml doesn't support -j 8, so don't pass MAKE_OPT
# I verified that 4.02.3 still doesn't support parallel build
log2 make world -f Makefile.nt
@@ -815,12 +820,12 @@ function make_ocaml {
log2 make opt.opt -f Makefile.nt
log2 make install -f Makefile.nt
# TODO log2 make clean -f Makefile.nt Temporarily disabled for ocamlbuild development
-
+
# Move license files and other into into special folder
if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
mkdir -p "$PREFIXOCAML/license_readme/ocaml"
# 4.01 installs these files, 4.02 doesn't. So delete them and copy them from the sources.
- rm -f *.txt
+ rm -f ./*.txt
cp LICENSE "$PREFIXOCAML/license_readme/ocaml/License.txt"
cp INSTALL "$PREFIXOCAML/license_readme/ocaml/Install.txt"
cp README "$PREFIXOCAML/license_readme/ocaml/ReadMe.txt"
@@ -909,9 +914,10 @@ function make_camlp5 {
make_ocaml
make_findlib
if build_prep http://camlp5.gforge.inria.fr/distrib/src camlp5-6.14 tgz 1 ; then
- logn configure ./configure
+ logn configure ./configure
# Somehow my virus scanner has the boot.new/SAVED directory locked after the move for a second => repeat until success
sed -i 's/mv boot.new boot/until mv boot.new boot; do sleep 1; done/' Makefile
+ # shellcheck disable=SC2086
log1 make world.opt $MAKE_OPT
log2 make install
# For some reason gramlib.a is not copied, but it is required by Coq
@@ -939,15 +945,15 @@ function make_lablgtk {
make_gtk_sourceview2
if build_prep https://forge.ocamlcore.org/frs/download.php/1479 lablgtk-2.18.3 tar.gz 1 ; then
# configure should be fixed to search for $TARGET_ARCH-pkg-config.exe
- cp /bin/$TARGET_ARCH-pkg-config.exe bin_special/pkg-config.exe
- logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIXOCAML"
-
+ cp "/bin/$TARGET_ARCH-pkg-config.exe" bin_special/pkg-config.exe
+ logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIXOCAML"
+
# lablgtk shows occasional errors with -j, so don't pass $MAKE_OPT
-
+
# See https://sympa.inria.fr/sympa/arc/caml-list/2015-10/msg00204.html for the make || true + strip
logn make-world-pre make world || true
- $TARGET_ARCH-strip.exe --strip-unneeded src/dlllablgtk2.dll
-
+ "$TARGET_ARCH-strip.exe" --strip-unneeded src/dlllablgtk2.dll
+
log2 make world
log2 make install
log2 make clean
@@ -978,7 +984,7 @@ function make_stdint {
function copy_coq_dll {
if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
- cp /usr/${ARCH}-w64-mingw32/sys-root/mingw/bin/$1 "$PREFIXCOQ/bin/$1"
+ cp "/usr/${ARCH}-w64-mingw32/sys-root/mingw/bin/$1" "$PREFIXCOQ/bin/$1"
fi
}
@@ -994,7 +1000,7 @@ function copy_coq_dlls {
# Do this recursively until there are no further missing DLLs (File close + reopen)
# For running this quickly, just do "cd coq-<ver> ; call copy_coq_dlls ; cd .." at the end of this script.
# Do the same for coqc and ocamlc (usually doesn't result in additional files)
-
+
copy_coq_dll LIBATK-1.0-0.DLL
copy_coq_dll LIBCAIRO-2.DLL
copy_coq_dll LIBEXPAT-1.DLL
@@ -1018,7 +1024,7 @@ function copy_coq_dlls {
copy_coq_dll LIBXML2-2.DLL
copy_coq_dll ZLIB1.DLL
- # Depends on if GTK is built from sources
+ # Depends on if GTK is built from sources
if [ "$GTK_FROM_SOURCES" == "Y" ]; then
copy_coq_dll libiconv-2.dll
else
@@ -1036,21 +1042,21 @@ function copy_coq_dlls {
i686) copy_coq_dll LIBGCC_S_SJLJ-1.DLL ;;
*) false ;;
esac
-
+
# Win pthread version change
copy_coq_dll LIBWINPTHREAD-1.DLL
}
function copy_coq_objects {
# copy objects only from folders which exist in the target lib directory
- find . -type d | while read FOLDER ; do
+ find . -type d | while read -r FOLDER ; do
if [ -e "$PREFIXCOQ/lib/$FOLDER" ] ; then
- install_glob $FOLDER/'*.cmxa' "$PREFIXCOQ/lib/$FOLDER"
- install_glob $FOLDER/'*.cmi' "$PREFIXCOQ/lib/$FOLDER"
- install_glob $FOLDER/'*.cma' "$PREFIXCOQ/lib/$FOLDER"
- install_glob $FOLDER/'*.cmo' "$PREFIXCOQ/lib/$FOLDER"
- install_glob $FOLDER/'*.a' "$PREFIXCOQ/lib/$FOLDER"
- install_glob $FOLDER/'*.o' "$PREFIXCOQ/lib/$FOLDER"
+ install_glob "$FOLDER"/'*.cmxa' "$PREFIXCOQ/lib/$FOLDER"
+ install_glob "$FOLDER"/'*.cmi' "$PREFIXCOQ/lib/$FOLDER"
+ install_glob "$FOLDER"/'*.cma' "$PREFIXCOQ/lib/$FOLDER"
+ install_glob "$FOLDER"/'*.cmo' "$PREFIXCOQ/lib/$FOLDER"
+ install_glob "$FOLDER"/'*.a' "$PREFIXCOQ/lib/$FOLDER"
+ install_glob "$FOLDER"/'*.o' "$PREFIXCOQ/lib/$FOLDER"
fi
done
}
@@ -1066,7 +1072,7 @@ function copq_coq_gtk {
install_glob "$PREFIX/share/gtksourceview-2.0/language-specs/"'*' "$PREFIXCOQ/share/gtksourceview-2.0/language-specs"
install_glob "$PREFIX/share/gtksourceview-2.0/styles/"'*' "$PREFIXCOQ/share/gtksourceview-2.0/styles"
install_rec "$PREFIX/share/themes/" '*' "$PREFIXCOQ/share/themes"
-
+
# This below item look like a bug in make install
if [ -d "$PREFIXCOQ/share/coq/" ] ; then
COQSHARE="$PREFIXCOQ/share/coq/"
@@ -1111,11 +1117,11 @@ function make_coq {
case $COQ_VERSION in
# e.g. git-v8.6 => download from https://github.com/coq/coq/archive/v8.6.zip
# e.g. git-trunk => download from https://github.com/coq/coq/archive/trunk.zip
- git-*)
+ git-*)
COQ_BUILD_PATH=/build/coq-${COQ_VERSION}
- build_prep https://github.com/coq/coq/archive ${COQ_VERSION##git-} zip 1 coq-${COQ_VERSION}
+ build_prep https://github.com/coq/coq/archive "${COQ_VERSION##git-}" zip 1 "coq-${COQ_VERSION}"
;;
-
+
# e.g. /cygdrive/d/coqgit
/*)
# Todo: --exclude-vcs-ignores doesn't work because tools/coqdoc/coqdoc.sty is excluded => fix .gitignore
@@ -1124,11 +1130,11 @@ function make_coq {
tar -zcf $TARBALLS/coq-local.tar.gz --exclude-vcs -C "${COQ_VERSION%/*}" "${COQ_VERSION##*/}"
build_prep NEVER-DOWNLOADED coq-local tar.gz
;;
-
+
# e.g. 8.6 => https://coq.inria.fr/distrib/8.6/files/coq-8.6.tar.gz
*)
COQ_BUILD_PATH=/build/coq-$COQ_VERSION
- build_prep https://coq.inria.fr/distrib/V$COQ_VERSION/files coq-$COQ_VERSION tar.gz
+ build_prep "https://coq.inria.fr/distrib/V$COQ_VERSION/files" "coq-$COQ_VERSION" tar.gz
;;
esac
then
@@ -1142,16 +1148,17 @@ function make_coq {
fi
# The windows resource compiler binary name is hard coded
- sed -i "s/i686-w64-mingw32-windres/$TARGET_ARCH-windres/" Makefile.build
+ sed -i "s/i686-w64-mingw32-windres/$TARGET_ARCH-windres/" Makefile.build
sed -i "s/i686-w64-mingw32-windres/$TARGET_ARCH-windres/" Makefile.ide || true
# 8.4x doesn't support parallel make
if [[ $COQ_VERSION == 8.4* ]] ; then
log1 make
else
+ # shellcheck disable=SC2086
make $MAKE_OPT
fi
-
+
if [ "$INSTALLMODE" == "relocatable" ]; then
./configure -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man"
fi
@@ -1161,7 +1168,7 @@ function make_coq {
if [ "$INSTALLOCAML" == "Y" ]; then
copy_coq_objects
fi
-
+
copq_coq_gtk
copy_coq_license
@@ -1169,7 +1176,7 @@ function make_coq {
# 1.) find | xargs fails on cygwin, can be fixed by sed -i 's|\| xargs rm -f|-exec rm -fv \{\} \+|' Makefile
# 2.) clean of test suites fails with "cannot run complexity tests (no bogomips found)"
# make clean
-
+
build_post
fi
}
@@ -1180,7 +1187,7 @@ function make_mingw_make {
if build_prep http://ftp.gnu.org/gnu/make make-4.2 tar.bz2 ; then
# The config.h.win32 file is fine - don't edit it
# We need to copy the mingw gcc here as "gcc" - then the batch file will use it
- cp /usr/bin/${ARCH}-w64-mingw32-gcc-6.4.0.exe ./gcc.exe
+ cp "/usr/bin/${ARCH}-w64-mingw32-gcc-6.4.0.exe" ./gcc.exe
# By some magic cygwin bash can run batch files
logn build ./build_w32.bat gcc
# Copy make to Coq folder
@@ -1193,7 +1200,8 @@ function make_mingw_make {
function make_binutils {
if build_prep http://ftp.gnu.org/gnu/binutils binutils-2.27 tar.gz ; then
- logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIXCOQ" --program-prefix=$TARGET-
+ logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIXCOQ" --program-prefix="$TARGET-"
+ # shellcheck disable=SC2086
log1 make $MAKE_OPT
log2 make install
# log2 make clean
@@ -1219,12 +1227,13 @@ function make_gcc {
mkdir -p "$PREFIXCOQ/mingw/include"
# See https://gcc.gnu.org/install/configure.html
- logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET \
- --prefix="$PREFIXCOQ" --program-prefix=$TARGET- --disable-win32-registry --with-sysroot="$PREFIXCOQ" \
+ logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" \
+ --prefix="$PREFIXCOQ" --program-prefix="$TARGET-" --disable-win32-registry --with-sysroot="$PREFIXCOQ" \
--enable-languages=c --disable-nls \
--disable-libsanitizer --disable-libssp --disable-libquadmath --disable-libgomp --disable-libvtv --disable-lto
# --disable-decimal-float seems to be required
# --with-sysroot="$PREFIX" results in configure error that this is not an absolute path
+ # shellcheck disable=SC2086
log1 make $MAKE_OPT
log2 make install
# log2 make clean
@@ -1252,21 +1261,22 @@ function get_cygwin_mingw_sources {
# Take the 2nd field of the last line => ${SOURCE} = x86_64/release/mingw64-x86_64-gcc/mingw64-x86_64-gcc-5.4.0-2-src.tar.xz
# Remove that path part => ${SOURCEFILE} = mingw64-x86_64-gcc-5.4.0-2-src.tar.xz
- grep "mingw" /etc/setup/installed.db | sed 's/\.tar\.bz2 [0-1]$//' | sed 's/ /\//' | while read ARCHIVE ; do
+ grep "mingw" /etc/setup/installed.db | sed 's/\.tar\.bz2 [0-1]$//' | sed 's/ /\//' | while read -r ARCHIVE ; do
local ARCHIVEESC=${ARCHIVE//+/\\+}
- local SOURCE=`egrep -A 1 "install: ($CYGWINARCH|noarch)/release/[-+_/a-z0-9]*$ARCHIVEESC" $TARBALLS/setup.ini | tail -1 | cut -d " " -f 2`
+ local SOURCE
+ SOURCE=$(grep -E -A 1 "install: ($CYGWINARCH|noarch)/release/[-+_/a-z0-9]*$ARCHIVEESC" $TARBALLS/setup.ini | tail -1 | cut -d " " -f 2)
local SOURCEFILE=${SOURCE##*/}
# Get the source file (either from the source cache or online)
- if [ ! -f $TARBALLS/$SOURCEFILE ] ; then
+ if [ ! -f "$TARBALLS/$SOURCEFILE" ] ; then
if [ -f "$SOURCE_LOCAL_CACHE_CFMT/$SOURCEFILE" ] ; then
cp "$SOURCE_LOCAL_CACHE_CFMT/$SOURCEFILE" $TARBALLS
else
wget "$CYGWIN_REPOSITORY/$SOURCE"
- mv $SOURCEFILE $TARBALLS
+ mv "$SOURCEFILE" "$TARBALLS"
# Save the source archive in the source cache
if [ -d "$SOURCE_LOCAL_CACHE_CFMT" ] ; then
- cp $TARBALLS/$SOURCEFILE "$SOURCE_LOCAL_CACHE_CFMT"
+ cp "$TARBALLS/$SOURCEFILE" "$SOURCE_LOCAL_CACHE_CFMT"
fi
fi
fi
@@ -1288,19 +1298,19 @@ function make_coq_installer {
# ocaml: ocaml + menhir + camlp5 + findlib
# ocaml_coq: as above + coq
# ocaml_coq_addons: as above + lib/user-contrib/*
-
+
# Create coq file list as ocaml_coq / ocaml
diff_files coq ocaml_coq ocaml
-
+
# Filter out object files
- filter_files coq_objects coq '\.(cmxa|cmi|cma|cmo|a|o)$'
-
+ filter_files coq_objects coq '\.(cmxa|cmi|cma|cmo|a|o)$'
+
# Filter out plugin object files
filter_files coq_objects_plugins coq_objects '/lib/plugins/.*\.(cmxa|cmi|cma|cmo|a|o)$'
-
+
# Coq objects objects required for plugin development = coq objects except those for pre installed plugins
diff_files coq_plugindev coq_objects coq_objects_plugins
-
+
# Addons (TODO: including objects that could go to the plugindev thing, but
# then one would have to make that package depend on this one, so not
# implemented yet)
@@ -1308,27 +1318,27 @@ function make_coq_installer {
# Coq files, except objects needed only for plugin development
diff_files coq_base coq coq_plugindev
-
+
# Convert section files to NSIS format
files_to_nsis coq_base
files_to_nsis coq_addons
files_to_nsis coq_plugindev
files_to_nsis ocaml
-
+
# Get and extract NSIS Binaries
if build_prep http://downloads.sourceforge.net/project/nsis/NSIS%202/2.51 nsis-2.51 zip ; then
- NSIS=`pwd`/makensis.exe
+ NSIS=$(pwd)/makensis.exe
chmod u+x "$NSIS"
# Change to Coq folder
- cd $COQ_BUILD_PATH
+ cd "$COQ_BUILD_PATH"
# Copy patched nsi file
cp ../patches/coq_new.nsi dev/nsis
cp ../patches/StrRep.nsh dev/nsis
cp ../patches/ReplaceInFile.nsh dev/nsis
- VERSION=`grep '^VERSION=' config/Makefile | cut -d = -f 2 | tr -d '\r'`
+ VERSION=$(grep '^VERSION=' config/Makefile | cut -d = -f 2 | tr -d '\r')
cd dev/nsis
- logn nsis-installer "$NSIS" -DVERSION=$VERSION -DARCH=$ARCH -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coq.ico -DCOQ_ADDONS="$COQ_ADDONS" coq_new.nsi
-
+ logn nsis-installer "$NSIS" -DVERSION="$VERSION" -DARCH="$ARCH" -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coq.ico -DCOQ_ADDONS="$COQ_ADDONS" coq_new.nsi
+
build_post
fi
}
@@ -1346,7 +1356,7 @@ function make_addon_bignums {
function make_addons {
for addon in $COQ_ADDONS; do
- make_addon_$addon
+ "make_addon_$addon"
done
}
@@ -1374,4 +1384,3 @@ list_files ocaml_coq_addons
if [ "$MAKEINSTALLER" == "Y" ] ; then
make_coq_installer
fi
-
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 16:34:40 +0000