diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-09-05 15:04:49 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-09-09 13:11:38 +0200 |
commit | 938dd9ba81d0bba5a9358627405d3110fc4ee335 (patch) | |
tree | 463fb87ad733ae48fb2a5de022c44ebaf1ab7ae9 /dev | |
parent | 2b4fcf404228fbc67f1c137cd75805255c2581d4 (diff) |
Installer for win32
Not 100% functional, but coqide works.
The native compiler is embedded but:
- some path mangling problem prevents it from working even when run via
cygwin (like in the build process)
- CAMLLIB must be exported to ${COQ}\ocaml\lib to have it run
(coq should do it).
fix
Diffstat (limited to 'dev')
-rwxr-xr-x | dev/make-installer-win32.sh | 22 | ||||
-rwxr-xr-x | dev/make-sdk-win32.sh | 321 | ||||
-rw-r--r-- | dev/nsis/FileAssociation.nsh | 190 | ||||
-rwxr-xr-x | dev/nsis/coq.nsi | 234 | ||||
-rwxr-xr-x | dev/nsis/coq_splash.bmp | bin | 0 -> 360054 bytes |
5 files changed, 767 insertions, 0 deletions
diff --git a/dev/make-installer-win32.sh b/dev/make-installer-win32.sh new file mode 100755 index 000000000..acbcb040b --- /dev/null +++ b/dev/make-installer-win32.sh @@ -0,0 +1,22 @@ +#!/bin/sh + +NSIS="/cygdrive/c/Program Files/NSIS/makensis" +ZIP=_make.zip +URL1=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-bin.zip/download +URL2=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-dep.zip/download + +./configure -prefix ./ -with-doc no +make +if [ ! -e bin/make.exe ]; then + wget -O $ZIP $URL1 && 7z x $ZIP "bin/*" + wget -O $ZIP $URL2 && 7z x $ZIP "bin/*" + rm -rf $ZIP +fi +ocamlc unix.cma tools/mkwinapp.ml -o bin/mkwinapp.exe +bin/mkwinapp.exe bin/coqide.exe +bin/mkwinapp.exe bin/coqide.byte.exe +VERSION=`grep ^VERSION= config/Makefile | cut -d = -f 2` +cd dev/nsis +"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" coq.nsi +ls *exe +cd ../.. diff --git a/dev/make-sdk-win32.sh b/dev/make-sdk-win32.sh new file mode 100755 index 000000000..2c3713b5d --- /dev/null +++ b/dev/make-sdk-win32.sh @@ -0,0 +1,321 @@ +#!/bin/bash + +# To run this script install cygwin by running setup-x86.exe from cygwin.com +# Install the standard packages plus wget. Then run this script. + +# Sworn by Enrico Tassi <enrico.tassi@inra.fr> +# Modified to support other directories and almost support spaces in paths +# by Jason Gross <jgross@mit.edu> +# License: Expat/MIT http://opensource.org/licenses/MIT + +set -e +# set -x + +# Resources +ocaml=ocaml-4.01.0-i686-mingw64-installer3.exe +glib=base-windows-0.18.1.1.13.356@BUILD_ec06e9.txz +gtk=base-gtk-2.24.18.1.58@BUILD_594ca8.txz +lablgtk=lablgtk-2.18.0.tar.gz +camlp5=camlp5-6.11.tgz + +ocaml_URL='http://yquem.inria.fr/~protzenk/caml-installer/'$ocaml +lablgtk_URL='https://forge.ocamlcore.org/frs/download.php/1261/'$lablgtk +glib_URL='http://dl.arirux.de/5/binaries32/'$glib +gtk_URL='http://dl.arirux.de/5/binaries32/'$gtk +camlp5_URL='http://pauillac.inria.fr/~ddr/camlp5/distrib/src/'$camlp5 + +cygwin=setup-x86.exe +cygwin_URL='http://cygwin.com/'$cygwin +cygwin_PKGS=p7zip,zip,sed,make,mingw64-i686-gcc-g++,mingw64-i686-gcc-core,mingw64-i686-gcc,patch,rlwrap,libreadline6,diffutils + +has_spaces() { + test -z "$2" +} +# utilities +# http://www.dependencywalker.com/depends22_x86.zip + +# The SDK itself +REVISION=1 +BASE="/cygdrive/c/CoqSDK-$REVISION" + +WGET_ARGS="-N -q" + +if [ "$(has_spaces $BASE; echo $?)" -ne 0 ]; then + echo "ERROR: The current base directory ($BASE) has spaces." + echo "ERROR: building lablgtk would fail." + exit 1 +fi + +cyg_install() { + if [ ! -e "$cygwin" ]; then wget $WGET_ARGS "$cygwin_URL"; fi + chmod a+x "$cygwin" + cygstart -w "$cygwin" -q -P $@ +} + +sanity_check() { + echo "Check: wget." + (which wget) || \ + (echo "Please install wget using the cygwin installer and retry.";\ + exit 1) + echo "Check: 7z, gcc. If it fails wait for cygwin to complete and retry" + (which 7z && which i686-w64-mingw32-gcc) || \ + (echo "Some cygwin package is not installed.";\ + echo "Please wait for cygwin to finish and retry.";\ + cyg_install $cygwin_PKGS;\ + exit 1) +} + +install_base() { + echo "Setting up $BASE" + rm -rf "$BASE" + mkdir -p "$BASE" +} + +make_environ() { + echo "Setting up $BASE/environ" + pushd "$BASE" >/dev/null + cat > environ <<- EOF + cyg_install() { + if [ ! -e "$cygwin" ]; then wget $WGET_ARGS "$cygwin_URL"; fi + chmod a+x "$cygwin" + cygstart -w "$cygwin" -q -P \$@ + } + # Sanity checks: is the mingw64-i686-gcc package installed? + (which i686-w64-mingw32-gcc && which make && which sed) || \\ + (echo "Some cygwin package is not installed.";\\ + echo "Please wait for cygwin to finish and retry.";\\ + cyg_install $cygwin_PKGS;\\ + exit 1) || exit 1 + + export BASE="\$( cd "\$( dirname "\${BASH_SOURCE[0]}" )" && pwd )" + export PATH="\$BASE/bin:\$PATH" + export OCAMLLIB="\$(cygpath -m "\$BASE")/lib" + export OCAMLFIND_CONF="\$(cygpath -m "\$BASE")/etc/findlib.conf" + sed s"|@BASE@|\$(cygpath -m "\$BASE")|g" "\$BASE/lib/ld.conf.in" \\ + > "\$BASE/lib/ld.conf" + sed s"|@BASE@|\$(cygpath -m "\$BASE")|g" "\$BASE/lib/topfind.in" \\ + > "\$BASE/lib/topfind" + sed s"|@BASE@|\$(cygpath -m "\$BASE")|g" "\$BASE/etc/findlib.conf.in" \\ + > "\$BASE/etc/findlib.conf" + EOF + cat >> "$BASE/environ" <<- EOF + echo "Good. You can now build Coq and Coqide from cygwin." + EOF + popd >/dev/null +} + +download() { + echo "Downloading some software:" + if [ ! -e "$ocaml" ]; then + echo "- downloading OCaml..." + wget $WGET_ARGS "$ocaml_URL" + fi + chmod a+x "$ocaml" + if [ ! -e "$lablgtk" ]; then + echo "- downloading lablgtk..." + wget $WGET_ARGS --no-check-certificate "$lablgtk_URL" + fi + if [ ! -e "$gtk" ]; then + echo "- downloading gtk..." + wget $WGET_ARGS "$gtk_URL" + fi + if [ ! -e "$glib" ]; then + echo "- downloading glib..." + wget $WGET_ARGS "$glib_URL" + fi + if [ ! -e "$camlp5" ]; then + echo "- downloading camlp5..." + wget $WGET_ARGS "$camlp5_URL" + fi +} + +cleanup() { + rm -rf tmp build +} + +install_gtk() { + echo "Installing $glib" + tar -xJf "$glib" -C "$BASE" + echo "Installing $gtk" + tar -xJf "$gtk" -C "$BASE" +} + +install_ocaml() { + echo "Installing $ocaml" + mkdir -p tmp + 7z -otmp x "$ocaml" >/dev/null + cp -r tmp/\$_OUTDIR/bin "$BASE/" + cp -r tmp/bin "$BASE/" + cp -r tmp/\$_OUTDIR/lib "$BASE/" + cp -r tmp/lib "$BASE/" + cp -r tmp/\$_OUTDIR/etc "$BASE/" + find "$BASE" -name '*.dll' -o -name '*.exe' | tr '\n' '\0' \ + | xargs -0 chmod a+x + mv "$BASE/lib/topfind" "$BASE/lib/topfind.in" + sed -i 's|@SITELIB@|@BASE@/lib/site-lib|g' "$BASE/lib/topfind.in" + cat > "$BASE/lib/ld.conf.in" <<- EOF + @BASE@/lib + @BASE@/lib/stublibs + EOF + cat > "$BASE/etc/findlib.conf.in" <<- EOF + destdir="@BASE@/lib/site-lib" + path="@BASE@/lib/site-lib" + stdlib="@BASE@/lib" + ldconf="@BASE@/lib/ld.conf" + ocamlc="ocamlc.opt" + ocamlopt="ocamlopt.opt" + ocamldep="ocamldep.opt" + ocamldoc="ocamldoc.opt" + EOF + cp "$BASE/lib/topdirs.cmi" "$BASE/lib/compiler-libs/" +} + +build_install_lablgtk() { + echo "Building $lablgtk" + mkdir -p build + tar -xzf "$lablgtk" -C build + cd build/lablgtk-* + patch -p1 <<EOT +--- lablgtk-2.18.0/src/glib.mli 2013-10-01 01:31:50.000000000 -0700 ++++ lablgtk-2.18.0.new/src/glib.mli 2013-12-06 11:57:34.203675200 -0800 +@@ -75,6 +75,7 @@ + type condition = [ \`ERR | \`HUP | \`IN | \`NVAL | \`OUT | \`PRI] + type id + val channel_of_descr : Unix.file_descr -> channel ++ val channel_of_descr_socket : Unix.file_descr -> channel + val add_watch : + cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id + val remove : id -> unit +--- lablgtk-2.18.0/src/glib.ml 2013-10-01 01:31:50.000000000 -0700 ++++ lablgtk-2.18.0.new/src/glib.ml 2013-12-06 11:57:53.070804800 -0800 +@@ -72,6 +72,8 @@ + type id + external channel_of_descr : Unix.file_descr -> channel + = "ml_g_io_channel_unix_new" ++ external channel_of_descr_socket : Unix.file_descr -> channel ++ = "ml_g_io_channel_unix_new_socket" + external remove : id -> unit = "ml_g_source_remove" + external add_watch : + cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id +--- lablgtk-2.18.0/src/ml_glib.c 2013-10-01 01:31:50.000000000 -0700 ++++ lablgtk-2.18.0.new/src/ml_glib.c 2013-12-10 02:03:33.940371800 -0800 +@@ -25,6 +25,8 @@ + #include <string.h> + #include <locale.h> + #ifdef _WIN32 ++/* to kill a #warning: include winsock2.h before windows.h */ ++#include <winsock2.h> + #include "win32.h" + #include <wtypes.h> + #include <io.h> +@@ -38,6 +40,11 @@ + #include <caml/callback.h> + #include <caml/threads.h> + ++#ifdef _WIN32 ++/* for Socket_val */ ++#include <caml/unixsupport.h> ++#endif ++ + #include "wrappers.h" + #include "ml_glib.h" + #include "glib_tags.h" +@@ -325,14 +332,23 @@ + + #ifndef _WIN32 + ML_1 (g_io_channel_unix_new, Int_val, Val_GIOChannel_noref) ++CAMLprim value ml_g_io_channel_unix_new_socket (value arg1) { ++ return Val_GIOChannel_noref (g_io_channel_unix_new (Int_val (arg1))); ++} + + #else + CAMLprim value ml_g_io_channel_unix_new(value wh) + { + return Val_GIOChannel_noref +- (g_io_channel_unix_new ++ (g_io_channel_win32_new_fd + (_open_osfhandle((long)*(HANDLE*)Data_custom_val(wh), O_BINARY))); + } ++ ++CAMLprim value ml_g_io_channel_unix_new_socket(value wh) ++{ ++ return Val_GIOChannel_noref ++ (g_io_channel_win32_new_socket(Socket_val(wh))); ++} + #endif + + static gboolean ml_g_io_channel_watch(GIOChannel *s, GIOCondition c, +EOT + #sed -i s'/$PKG_CONFIG/"$PKG_CONFIG"/g' configure + #sed -i s'/""$PKG_CONFIG""/"$PKG_CONFIG"/g' configure + ./configure --disable-gtktest --prefix="$(cygpath -m "$BASE")" \ + >log-configure 2>&1 + sed -i 's?\\?/?g' config.make + make >log-make 2>&1 + make opt >>log-make 2>&1 + #echo "Testing $lablgtk" + #cd src + #./lablgtk2 ../examples/calc.ml + #./lablgtk2 -all ../examples/calc.ml + #cd .. + echo "Installing $lablgtk" + make install >>log-make 2>&1 + cd ../.. +} + +build_install_camlp5() { + echo "Building $camlp5" + mkdir -p build + tar -xzf "$camlp5" -C build + cd build/camlp5-* + ./configure >log-configure 2>&1 + sed -i 's/EXT_OBJ=.obj/EXT_OBJ=.o/' config/Makefile + sed -i 's/EXT_LIB=.lib/EXT_LIB=.a/' config/Makefile + make world.opt >log-make 2>&1 + echo "Installing $camlp5" + make install >>log-make 2>&1 + cd ../.. +} + +zip_sdk() { + echo "Generating CoqSDK-${REVISION}.zip" + here="`pwd`" + cd "$BASE/.." + rm -f "$here/CoqSDK-${REVISION}.zip" + zip -q -r "$here/CoqSDK-${REVISION}.zip" "$(basename "$BASE")" + cd "$here" +} + +diet_sdk() { + rm -rf "$BASE"/+* + rm -rf "$BASE"/bin/camlp4* + rm -rf "$BASE"/lib/camlp4/ + rm -rf "$BASE"/lib/site-lib/camlp4/ +} + +victory(){ + echo "Output file: CoqSDK-${REVISION}.zip "\ + "(`du -sh CoqSDK-${REVISION}.zip | cut -f 1`)" + echo "Usage: unpack and source the environ file at its root" +} + +if [ -z "$1" ]; then + sanity_check + download + cleanup + install_base + install_ocaml + install_gtk + make_environ + . "$BASE/environ" + build_install_lablgtk + build_install_camlp5 + diet_sdk + make_environ + zip_sdk + cleanup + victory +else + # just one step + $1 +fi diff --git a/dev/nsis/FileAssociation.nsh b/dev/nsis/FileAssociation.nsh new file mode 100644 index 000000000..b8c1e5ee7 --- /dev/null +++ b/dev/nsis/FileAssociation.nsh @@ -0,0 +1,190 @@ +/* +_____________________________________________________________________________ + + File Association +_____________________________________________________________________________ + + Based on code taken from http://nsis.sourceforge.net/File_Association + + Usage in script: + 1. !include "FileAssociation.nsh" + 2. [Section|Function] + ${FileAssociationFunction} "Param1" "Param2" "..." $var + [SectionEnd|FunctionEnd] + + FileAssociationFunction=[RegisterExtension|UnRegisterExtension] + +_____________________________________________________________________________ + + ${RegisterExtension} "[executable]" "[extension]" "[description]" + +"[executable]" ; executable which opens the file format + ; +"[extension]" ; extension, which represents the file format to open + ; +"[description]" ; description for the extension. This will be display in Windows Explorer. + ; + + + ${UnRegisterExtension} "[extension]" "[description]" + +"[extension]" ; extension, which represents the file format to open + ; +"[description]" ; description for the extension. This will be display in Windows Explorer. + ; + +_____________________________________________________________________________ + + Macros +_____________________________________________________________________________ + + Change log window verbosity (default: 3=no script) + + Example: + !include "FileAssociation.nsh" + !insertmacro RegisterExtension + ${FileAssociation_VERBOSE} 4 # all verbosity + !insertmacro UnRegisterExtension + ${FileAssociation_VERBOSE} 3 # no script +*/ + + +!ifndef FileAssociation_INCLUDED +!define FileAssociation_INCLUDED + +!include Util.nsh + +!verbose push +!verbose 3 +!ifndef _FileAssociation_VERBOSE + !define _FileAssociation_VERBOSE 3 +!endif +!verbose ${_FileAssociation_VERBOSE} +!define FileAssociation_VERBOSE `!insertmacro FileAssociation_VERBOSE` +!verbose pop + +!macro FileAssociation_VERBOSE _VERBOSE + !verbose push + !verbose 3 + !undef _FileAssociation_VERBOSE + !define _FileAssociation_VERBOSE ${_VERBOSE} + !verbose pop +!macroend + + + +!macro RegisterExtensionCall _EXECUTABLE _EXTENSION _DESCRIPTION + !verbose push + !verbose ${_FileAssociation_VERBOSE} + Push `${_DESCRIPTION}` + Push `${_EXTENSION}` + Push `${_EXECUTABLE}` + ${CallArtificialFunction} RegisterExtension_ + !verbose pop +!macroend + +!macro UnRegisterExtensionCall _EXTENSION _DESCRIPTION + !verbose push + !verbose ${_FileAssociation_VERBOSE} + Push `${_EXTENSION}` + Push `${_DESCRIPTION}` + ${CallArtificialFunction} UnRegisterExtension_ + !verbose pop +!macroend + + + +!define RegisterExtension `!insertmacro RegisterExtensionCall` +!define un.RegisterExtension `!insertmacro RegisterExtensionCall` + +!macro RegisterExtension +!macroend + +!macro un.RegisterExtension +!macroend + +!macro RegisterExtension_ + !verbose push + !verbose ${_FileAssociation_VERBOSE} + + Exch $R2 ;exe + Exch + Exch $R1 ;ext + Exch + Exch 2 + Exch $R0 ;desc + Exch 2 + Push $0 + Push $1 + + ReadRegStr $1 HKCR $R1 "" ; read current file association + StrCmp "$1" "" NoBackup ; is it empty + StrCmp "$1" "$R0" NoBackup ; is it our own + WriteRegStr HKCR $R1 "backup_val" "$1" ; backup current value +NoBackup: + WriteRegStr HKCR $R1 "" "$R0" ; set our file association + + ReadRegStr $0 HKCR $R0 "" + StrCmp $0 "" 0 Skip + WriteRegStr HKCR "$R0" "" "$R0" + WriteRegStr HKCR "$R0\shell" "" "open" + WriteRegStr HKCR "$R0\DefaultIcon" "" "$R2,0" +Skip: + WriteRegStr HKCR "$R0\shell\open\command" "" '"$R2" "%1"' + WriteRegStr HKCR "$R0\shell\edit" "" "Edit $R0" + WriteRegStr HKCR "$R0\shell\edit\command" "" '"$R2" "%1"' + + Pop $1 + Pop $0 + Pop $R2 + Pop $R1 + Pop $R0 + + !verbose pop +!macroend + + + +!define UnRegisterExtension `!insertmacro UnRegisterExtensionCall` +!define un.UnRegisterExtension `!insertmacro UnRegisterExtensionCall` + +!macro UnRegisterExtension +!macroend + +!macro un.UnRegisterExtension +!macroend + +!macro UnRegisterExtension_ + !verbose push + !verbose ${_FileAssociation_VERBOSE} + + Exch $R1 ;desc + Exch + Exch $R0 ;ext + Exch + Push $0 + Push $1 + + ReadRegStr $1 HKCR $R0 "" + StrCmp $1 $R1 0 NoOwn ; only do this if we own it + ReadRegStr $1 HKCR $R0 "backup_val" + StrCmp $1 "" 0 Restore ; if backup="" then delete the whole key + DeleteRegKey HKCR $R0 + Goto NoOwn + +Restore: + WriteRegStr HKCR $R0 "" $1 + DeleteRegValue HKCR $R0 "backup_val" + DeleteRegKey HKCR $R1 ;Delete key with association name settings + +NoOwn: + + Pop $1 + Pop $0 + Pop $R1 + Pop $R0 + + !verbose pop +!macroend + +!endif # !FileAssociation_INCLUDED
\ No newline at end of file diff --git a/dev/nsis/coq.nsi b/dev/nsis/coq.nsi new file mode 100755 index 000000000..84dbb193e --- /dev/null +++ b/dev/nsis/coq.nsi @@ -0,0 +1,234 @@ +; This script is used to build the Windows install program for Coq. + +;NSIS Modern User Interface +;Written by Joost Verburg +;Modified by Julien Narboux and Pierre Letouzey + +;SetCompress off +SetCompressor lzma +; Comment out after debuging. + +; The VERSION should be passed as an argument at compile time using : +; + +!define MY_PRODUCT "Coq" ;Define your own software name here +!define COQ_SRC_PATH "..\.." +!define OUTFILE "coq-installer-${VERSION}.exe" + +!include "MUI.nsh" +!include "FileAssociation.nsh" + +;-------------------------------- +;Configuration + + Name "Coq" + + ;General + OutFile "${OUTFILE}" + + ;Folder selection page + InstallDir "$PROGRAMFILES\${MY_PRODUCT}" + + ;Remember install folder + InstallDirRegKey HKCU "Software\${MY_PRODUCT}" "" + +;-------------------------------- +;Modern UI Configuration + + !insertmacro MUI_PAGE_WELCOME + !insertmacro MUI_PAGE_LICENSE "${COQ_SRC_PATH}/LICENSE" + !insertmacro MUI_PAGE_COMPONENTS + !insertmacro MUI_PAGE_DIRECTORY + !insertmacro MUI_PAGE_INSTFILES + !insertmacro MUI_PAGE_FINISH + + !insertmacro MUI_UNPAGE_WELCOME + !insertmacro MUI_UNPAGE_CONFIRM + !insertmacro MUI_UNPAGE_INSTFILES + !insertmacro MUI_UNPAGE_FINISH + +;-------------------------------- +;Languages + + !insertmacro MUI_LANGUAGE "English" + +;-------------------------------- +;Language Strings + + ;Description + LangString DESC_1 ${LANG_ENGLISH} "This package contains Coq and CoqIDE." + LangString DESC_2 ${LANG_ENGLISH} "This package contains the development files (*.cmi, *.cmo, *.cmx, ...) needed in order to build a plugin for Coq." + +;-------------------------------- +;Data + +Function .onInit + SetOutPath $TEMP + File /oname=coq_splash.bmp "coq_splash.bmp" + InitPluginsDir + + advsplash::show 1000 600 400 -1 $TEMP\coq_splash + + Pop $0 ; $0 has '1' if the user closed the splash screen early, + ; '0' if everything closed normal, and '-1' if some error occured. + + Delete $TEMP\coq_splash.bmp +FunctionEnd + + +;-------------------------------- +;Installer Sections + + +Section "Coq" Sec1 + + SetOutPath "$INSTDIR\" + + SetOutPath "$INSTDIR\bin" + File ${COQ_SRC_PATH}\bin\*.exe + ; make.exe and its dll + File ${COQ_SRC_PATH}\bin\make.exe + File ${COQ_SRC_PATH}\bin\libiconv2.dll + File ${COQ_SRC_PATH}\bin\libintl3.dll + + SetOutPath "$INSTDIR\lib\theories" + File /r ${COQ_SRC_PATH}\theories\*.vo + SetOutPath "$INSTDIR\lib\plugins" + File /r ${COQ_SRC_PATH}\plugins\*.vo + File /r ${COQ_SRC_PATH}\plugins\*.cmxs + SetOutPath "$INSTDIR\lib\tools\coqdoc" + File ${COQ_SRC_PATH}\tools\coqdoc\coqdoc.sty + File ${COQ_SRC_PATH}\tools\coqdoc\coqdoc.css + SetOutPath "$INSTDIR\emacs" + File ${COQ_SRC_PATH}\tools\*.el + SetOutPath "$INSTDIR\man" + File ${COQ_SRC_PATH}\man\*.1 + SetOutPath "$INSTDIR\lib\toploop" + File ${COQ_SRC_PATH}\stm\stmworkertop.cmxs + File ${COQ_SRC_PATH}\stm\tacworkertop.cmxs + File ${COQ_SRC_PATH}\ide\coqidetop.cmxs + + ; CoqIDE + SetOutPath "$INSTDIR\ide\" + File /r ${COQ_SRC_PATH}\ide\*.png + File /r ${COQ_SRC_PATH}\ide\*.lang + File /r ${COQ_SRC_PATH}\ide\*.xml + + ; Start Menu Entries + SetOutPath "$INSTDIR" + CreateShortCut "$SMPROGRAMS\Coq\CoqIde.lnk" "$INSTDIR\bin\coqide.exe" + + ${registerExtension} "$INSTDIR\bin\coqide.exe" ".v" "Coq Script File" + + SetOutPath "$INSTDIR" + File /r ${GTK_RUNTIME}\etc\gtk-2.0 + SetOutPath "$INSTDIR\bin" + File ${GTK_RUNTIME}\bin\*.dll + SetOutPath "$INSTDIR\lib" + File /r ${GTK_RUNTIME}\lib\gtk-2.0 ${GTK_RUNTIME}\lib\glib-2.0 + SetOutPath "$INSTDIR\share" + File /r ${GTK_RUNTIME}\share\themes + File /r ${GTK_RUNTIME}\share\gtksourceview-2.0 + + ;Store install folder + WriteRegStr HKCU "Software\${MY_PRODUCT}" "" $INSTDIR + + ;Create uninstaller + WriteUninstaller "$INSTDIR\Uninstall.exe" + WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \ + "DisplayName" "Coq Version ${VERSION}" + WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \ + "UninstallString" '"$INSTDIR\Uninstall.exe"' + + WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \ + "DisplayVersion" "${VERSION}" + + WriteRegDWORD HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \ + "NoModify" "1" + WriteRegDWORD HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \ + "NoRepair" "1" + + WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \ + "URLInfoAbout" "http://coq.inria.fr" + +; Start Menu Entries + +; for the path in the .lnk + SetOutPath "$INSTDIR" + + CreateDirectory "$SMPROGRAMS\Coq" + CreateShortCut "$SMPROGRAMS\Coq\Coq.lnk" "$INSTDIR\bin\coqtop.exe" + WriteINIStr "$SMPROGRAMS\Coq\The Coq HomePage.url" "InternetShortcut" "URL" "http://coq.inria.fr" + WriteINIStr "$SMPROGRAMS\Coq\The Coq Standard Library.url" "InternetShortcut" "URL" "http://coq.inria.fr/library" + CreateShortCut "$SMPROGRAMS\Coq\Uninstall.lnk" "$INSTDIR\Uninstall.exe" "" "$INSTDIR\Uninstall.exe" 0 + +SectionEnd + +Section "Coq files for plugin developers" Sec2 + + SetOutPath "$INSTDIR\lib\" + File /r ${COQ_SRC_PATH}\*.cmxa + File /r ${COQ_SRC_PATH}\*.cmi + File /r ${COQ_SRC_PATH}\*.cma + File /r ${COQ_SRC_PATH}\*.cmo + File /r ${COQ_SRC_PATH}\*.a + File /r ${COQ_SRC_PATH}\*.o + SetOutPath "$INSTDIR\bin\" + File ${GTK_RUNTIME}\bin\ocaml*.exe + File ${GTK_RUNTIME}\bin\camlp5*.exe + SetOutPath "$INSTDIR\ocaml\lib\" + File ${GTK_RUNTIME}\lib\*.cm* + File ${GTK_RUNTIME}\lib\*.a + File ${GTK_RUNTIME}\lib\stublibs\* + File ${GTK_RUNTIME}\lib\threads\* + File ${GTK_RUNTIME}\lib\compiler-libs\* + File ${GTK_RUNTIME}\lib\camlp5\* + +SectionEnd + +;-------------------------------- +;Descriptions + +!insertmacro MUI_FUNCTION_DESCRIPTION_BEGIN + !insertmacro MUI_DESCRIPTION_TEXT ${Sec1} $(DESC_1) + !insertmacro MUI_DESCRIPTION_TEXT ${Sec2} $(DESC_2) +!insertmacro MUI_FUNCTION_DESCRIPTION_END + +;-------------------------------- +;Uninstaller Section + +Section "Uninstall" + +;; We keep the settings +;; Delete "$INSTDIR\config\coqide-gtk2rc" + + RMDir /r "$INSTDIR\bin" + RMDir /r "$INSTDIR\dev" + RMDir /r "$INSTDIR\etc" + RMDir /r "$INSTDIR\lib" + RMDir /r "$INSTDIR\share" + + Delete "$INSTDIR\man\*.1" + RMDir "$INSTDIR\man" + + Delete "$INSTDIR\emacs\*.el" + RMDir "$INSTDIR\emacs" + +;; Start Menu + Delete "$SMPROGRAMS\Coq\Coq.lnk" + Delete "$SMPROGRAMS\Coq\CoqIde.lnk" + Delete "$SMPROGRAMS\Coq\Uninstall.lnk" + Delete "$SMPROGRAMS\Coq\The Coq HomePage.url" + Delete "$SMPROGRAMS\Coq\The Coq Standard Library.url" + Delete "$INSTDIR\Uninstall.exe" + + DeleteRegKey /ifempty HKCU "Software\${MY_PRODUCT}" + + DeleteRegKey HKEY_LOCAL_MACHINE "SOFTWARE\Coq" + DeleteRegKey HKEY_LOCAL_MACHINE "SOFTWARE\Microsoft\Windows\CurrentVersion\Uninstall\Coq" + RMDir "$INSTDIR" + RMDir "$SMPROGRAMS\Coq" + + ${unregisterExtension} ".v" "Coq Script File" + +SectionEnd diff --git a/dev/nsis/coq_splash.bmp b/dev/nsis/coq_splash.bmp Binary files differnew file mode 100755 index 000000000..c80220476 --- /dev/null +++ b/dev/nsis/coq_splash.bmp |