diff options
Diffstat (limited to 'dev/build/windows/patches_coq/coq_new.nsi')
| -rw-r--r-- | dev/build/windows/patches_coq/coq_new.nsi | 191 |
1 files changed, 149 insertions, 42 deletions
diff --git a/dev/build/windows/patches_coq/coq_new.nsi b/dev/build/windows/patches_coq/coq_new.nsi index b88aa066..9947965c 100644 --- a/dev/build/windows/patches_coq/coq_new.nsi +++ b/dev/build/windows/patches_coq/coq_new.nsi @@ -9,13 +9,14 @@ ; ARCH The target architecture, either x86_64 or i686 ; COQ_SRC_PATH path of Coq installation in Windows or MinGW format (either \\ or /, but with drive letter) ; COQ_ICON path of Coq icon file in Windows or MinGW format +; COQ_ADDONS list of addons that are shipped ; Enable compression after debugging. ; SetCompress off SetCompressor lzma !define MY_PRODUCT "Coq" ;Define your own software name here -!define OUTFILE "coq-installer-${VERSION}-${ARCH}.exe" +!define OUTFILE "coq-${VERSION}-installer-windows-${ARCH}.exe" !include "MUI2.nsh" !include "FileAssociation.nsh" @@ -37,42 +38,20 @@ Var INSTDIR_DBS ; INSTDIR with \\ instead of \ ;Folder selection page InstallDir "C:\${MY_PRODUCT}" - + ;Remember install folder InstallDirRegKey HKCU "Software\${MY_PRODUCT}" "" ;-------------------------------- -;Modern UI Configuration - - !define MUI_ICON "${COQ_ICON}" - - !insertmacro MUI_PAGE_WELCOME - !insertmacro MUI_PAGE_LICENSE "${COQ_SRC_PATH}/license_readme/coq/License.txt" - !insertmacro MUI_PAGE_COMPONENTS - !define MUI_DIRECTORYPAGE_TEXT_TOP "Select where to install Coq. The path MUST NOT include spaces." - !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 +;Extra license pages - ;Description - LangString DESC_1 ${LANG_ENGLISH} "This package contains Coq and CoqIDE." - LangString DESC_2 ${LANG_ENGLISH} "This package contains an OCaml compiler for Coq native compute and plugin development." - LangString DESC_3 ${LANG_ENGLISH} "This package contains the development files needed in order to build a plugin for Coq." - LangString DESC_4 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for the current user." - LangString DESC_5 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for all users." +!macro MUI_PAGE_LICENSE_EXTRA Licensefile Header Subheader Bottom SelFunc + !define MUI_PAGE_HEADER_TEXT "${Header}" + !define MUI_PAGE_HEADER_SUBTEXT "${Subheader}" + !define MUI_LICENSEPAGE_TEXT_BOTTOM "${Bottom}" + !define MUI_PAGE_CUSTOMFUNCTION_PRE ${SelFunc} + !insertmacro MUI_PAGE_LICENSE "${Licensefile}" +!macroend ;-------------------------------- ; Check for white spaces @@ -93,7 +72,6 @@ FunctionEnd ;-------------------------------- ;Installer Sections - Section "Coq" Sec1 SetOutPath "$INSTDIR\" @@ -103,7 +81,7 @@ Section "Coq" Sec1 ;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" \ @@ -121,7 +99,7 @@ Section "Coq" Sec1 ; Create start menu entries ; SetOutPath is required for the path in the .lnk files - SetOutPath "$INSTDIR" + SetOutPath "$INSTDIR" CreateDirectory "$SMPROGRAMS\Coq" ; The first shortcut set here is treated as main application by Windows 7/8. ; Use CoqIDE as main application @@ -136,20 +114,24 @@ SectionEnd ;OCAML Section "Ocaml for native compute and plugin development" Sec2 ;OCAML SetOutPath "$INSTDIR\" ;OCAML !include "..\..\..\filelists\ocaml.nsh" -;OCAML +;OCAML ;OCAML ; Create a few slash / backslash variants of the source and install path ;OCAML ; Note: NSIS has variables, written as $VAR and defines, written as ${VAR} ;OCAML !insertmacro StrRep $COQ_SRC_PATH_BS ${COQ_SRC_PATH} "/" "\" ;OCAML !insertmacro StrRep $COQ_SRC_PATH_DBS ${COQ_SRC_PATH} "/" "\\" ;OCAML !insertmacro StrRep $INSTDIR_DBS $INSTDIR "\" "\\" -;OCAML +;OCAML ;OCAML ; Replace absolute paths in some OCaml config files ;OCAML ; These are not all, see ReadMe.txt ;OCAML !insertmacro ReplaceInFile "$INSTDIR\libocaml\ld.conf" "/" "\" ;OCAML !insertmacro ReplaceInFile "$INSTDIR\libocaml\ld.conf" "$COQ_SRC_PATH_BS" "$INSTDIR" ;OCAML !insertmacro ReplaceInFile "$INSTDIR\etc\findlib.conf" "$COQ_SRC_PATH_DBS" "$INSTDIR_DBS" ;OCAML SectionEnd - + +SectionGroup "Coq addons" Sec2 + !include "..\..\..\filelists\addon_sections.nsh" +SectionGroupEnd + Section "Coq files for plugin developers" Sec3 SetOutPath "$INSTDIR\" !include "..\..\..\filelists\coq_plugindev.nsh" @@ -172,23 +154,148 @@ SectionEnd ;OCAML SectionEnd ;-------------------------------- +;Section dependencies + +; Parameters on the stack: +; top-0 : section B on which section A dependencies +; top-1 : section A, which depends on section B +; top-2 : name of section B +; top-3 : name of section A + +Function CheckSectionDependency + ; stack=nameB nameA secB secA rest + Exch $R3 ; stack=$R3 nameA secB secA rest; $R3=nameB + Exch ; stack=nameA $R3 secB secA rest + Exch $R2 ; stack=$R2 $R3 secB secA rest; $R2=nameA + Exch 2 ; stack=secB $R3 $R2 secA rest + Exch $R1 ; stack=$R1 $R3 $R2 secA rest; $R1=secB + Exch 3 ; stack=secA $R3 $R2 $R1 rest; + Exch $R0 ; stack=$R0 $R3 $R2 $R1 rest; $R0=secA + ; Take care of save order when popping the stack! + Push $R4 + Push $R5 + + SectionGetFlags $R0 $R0 + IntOp $R0 $R0 & ${SF_SELECTED} + + SectionGetFlags $R1 $R4 + IntOp $R5 $R4 & ${SF_SELECTED} + + ${If} $R0 == ${SF_SELECTED} + ${AndIf} $R5 != ${SF_SELECTED} + + IntOp $R5 $R4 | ${SF_SELECTED} + SectionSetFlags $R1 $R5 + MessageBox MB_OK '"$R3" has been selected, because "$R2" depends on it' + + ${EndIf} + + Pop $R5 + Pop $R4 + Pop $R0 + Pop $R3 + Pop $R2 + Pop $R1 +FunctionEnd + +!macro CheckSectionDependency secA secB nameA nameB + Push "${secA}" + Push "${secB}" + Push "${nameA}" + Push "${nameB}" + Call CheckSectionDependency +!macroend + +!define CheckSectionDependency "!insertmacro CheckSectionDependency" + +Function .onSelChange + !include "..\..\..\filelists\addon_dependencies.nsh" +FunctionEnd + +;-------------------------------- +;Modern UI Configuration + +; Note: this must be placed after the sections, because below we need to check at compile time +; if sections exist (by !ifdef <section_index_var>) to decide if the license page must be included. +; The section index variables are only defined after the section definitions. + + !define MUI_ICON "${COQ_ICON}" + + !insertmacro MUI_PAGE_WELCOME + !insertmacro MUI_PAGE_LICENSE "${COQ_SRC_PATH}/license_readme/coq/License.txt" + !insertmacro MUI_PAGE_COMPONENTS + + !ifdef Sec_compcert + !define LicCompCert_Title "CompCert License Agreement" + !define LicCompCert_SubTitle "You selected the CompCert addon. CompCert is not open source. Please review the license terms before installing CompCert!" + !define LicCompCert_Bottom "If you accept the terms of the agreement, click I Agree to continue. Otherwise go back and unselect the CompCert addon." + !insertmacro MUI_PAGE_LICENSE_EXTRA "${COQ_SRC_PATH}/lib/coq/user-contrib/compcert/LICENSE" "${LicCompCert_Title}" "${LicCompCert_SubTitle}" "${LicCompCert_Bottom}" SelFuncCompCert + + Function SelFuncCompCert + ${Unless} ${SectionIsSelected} ${Sec_compcert} + Abort + ${EndUnless} + FunctionEnd + !endif + + !ifdef Sec_vst + !define LicVST_Title "Princeton VST License Agreement" + !define LicVST_SubTitle "You selected the VST addon. VST contains parts of CompCert which are not open source. Please review the license terms before installing VST!" + !define LicVST_Bottom "If you accept the terms of the agreement, click I Agree to continue. Otherwise go back and unselect the VST addon." + !insertmacro MUI_PAGE_LICENSE_EXTRA "${COQ_SRC_PATH}/lib/coq/user-contrib/VST/LICENSE" "${LicVST_Title}" "${LicVST_SubTitle}" "${LicVST_Bottom}" SelFuncVST + + Function SelFuncVST + ${Unless} ${SectionIsSelected} ${Sec_vst} + Abort + ${EndUnless} + FunctionEnd + !endif + + !define MUI_DIRECTORYPAGE_TEXT_TOP "Select where to install Coq. The path MUST NOT include spaces." + !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 following extra Coq packages: ${COQ_ADDONS}" + LangString DESC_3 ${LANG_ENGLISH} "This package contains the development files needed in order to build a plugin for Coq." + ; LangString DESC_4 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for the current user." + ; LangString DESC_5 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for all users." + !include "..\..\..\filelists\addon_strings.nsh" + +;-------------------------------- ;Descriptions !insertmacro MUI_FUNCTION_DESCRIPTION_BEGIN !insertmacro MUI_DESCRIPTION_TEXT ${Sec1} $(DESC_1) - ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec2} $(DESC_2) + !insertmacro MUI_DESCRIPTION_TEXT ${Sec2} $(DESC_2) !insertmacro MUI_DESCRIPTION_TEXT ${Sec3} $(DESC_3) ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec4} $(DESC_4) ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec5} $(DESC_5) + !include "..\..\..\filelists\addon_descriptions.nsh" !insertmacro MUI_FUNCTION_DESCRIPTION_END - + ;-------------------------------- ;Uninstaller Section Section "Uninstall" ; Files and folders RMDir /r "$INSTDIR\bin" - RMDir /r "$INSTDIR\dev" + RMDir /r "$INSTDIR\doc" RMDir /r "$INSTDIR\etc" RMDir /r "$INSTDIR\lib" RMDir /r "$INSTDIR\libocaml" @@ -207,7 +314,7 @@ Section "Uninstall" Delete "$SMPROGRAMS\Coq\The Coq HomePage.url" Delete "$SMPROGRAMS\Coq\The Coq Standard Library.url" Delete "$INSTDIR\Uninstall.exe" - + ; Registry keys DeleteRegKey HKCU "Software\${MY_PRODUCT}" DeleteRegKey HKLM "SOFTWARE\Coq" |