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

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
new file mode 100755
index 000000000..c80220476
--- /dev/null
+++ b/dev/nsis/coq_splash.bmp