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

3 files changed, 424 insertions, 0 deletions

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