# HG changeset patch # User wenzelm # Date 1544035360 -3600 # Node ID 7a1b7b737c0283f99e906a16551c8274b4aefb2a # Parent c19b7b56599856e8a74b459c2e43acf80e836803 eliminated old makedist_bundle and remote_dmg: build_release does everything in Scala; more robust components and classpath via Other_Isabelle; updated macos_app to include full dmg template; misc tuning and clarification; diff -r c19b7b565998 -r 7a1b7b737c02 Admin/MacOS/Info.plist --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/MacOS/Info.plist Wed Dec 05 19:42:40 2018 +0100 @@ -0,0 +1,69 @@ + + + + +CFBundleDevelopmentRegion +English +CFBundleExecutable +JavaAppLauncher +CFBundleIconFile +isabelle.icns +CFBundleIdentifier +de.tum.in.isabelle.{ISABELLE_NAME} +CFBundleDisplayName +{ISABELLE_NAME} +CFBundleInfoDictionaryVersion +6.0 +CFBundleName +{ISABELLE_NAME} +CFBundlePackageType +APPL +CFBundleShortVersionString +1.0 +CFBundleSignature +???? +CFBundleVersion +1 +NSHumanReadableCopyright + +LSMinimumSystemVersion +10.7 +LSApplicationCategoryType +public.app-category.developer-tools +NSHighResolutionCapable +true +NSSupportsAutomaticGraphicsSwitching +true +JVMRuntime +bundled.jdk +JVMMainClassName +isabelle.Main +CFBundleDocumentTypes + + +CFBundleTypeExtensions + +thy + +CFBundleTypeIconFile +theory.icns +CFBundleTypeName +Isabelle theory file +CFBundleTypeRole +Editor +LSTypeIsPackage + + + +JVMOptions + +{JAVA_OPTIONS} +-Dapple.awt.application.name={ISABELLE_NAME} +-Disabelle.root=$APP_ROOT/Contents/Resources/{ISABELLE_NAME} +-Disabelle.app=true + +JVMArguments + + + + diff -r c19b7b565998 -r 7a1b7b737c02 Admin/MacOS/Info.plist-part1 --- a/Admin/MacOS/Info.plist-part1 Tue Dec 04 16:11:52 2018 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,59 +0,0 @@ - - - - -CFBundleDevelopmentRegion -English -CFBundleExecutable -JavaAppLauncher -CFBundleIconFile -isabelle.icns -CFBundleIdentifier -de.tum.in.isabelle.{ISABELLE_NAME} -CFBundleDisplayName -{ISABELLE_NAME} -CFBundleInfoDictionaryVersion -6.0 -CFBundleName -{ISABELLE_NAME} -CFBundlePackageType -APPL -CFBundleShortVersionString -1.0 -CFBundleSignature -???? -CFBundleVersion -1 -NSHumanReadableCopyright - -LSMinimumSystemVersion -10.7 -LSApplicationCategoryType -public.app-category.developer-tools -NSHighResolutionCapable -true -NSSupportsAutomaticGraphicsSwitching -true -JVMRuntime -bundled.jdk -JVMMainClassName -isabelle.Main -CFBundleDocumentTypes - - -CFBundleTypeExtensions - -thy - -CFBundleTypeIconFile -theory.icns -CFBundleTypeName -Isabelle theory file -CFBundleTypeRole -Editor -LSTypeIsPackage - - - -JVMOptions - diff -r c19b7b565998 -r 7a1b7b737c02 Admin/MacOS/Info.plist-part2 --- a/Admin/MacOS/Info.plist-part2 Tue Dec 04 16:11:52 2018 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ --Disabelle.root=$APP_ROOT/Contents/Resources/{ISABELLE_NAME} --Disabelle.app=true - -JVMArguments - - - - diff -r c19b7b565998 -r 7a1b7b737c02 Admin/MacOS/README --- a/Admin/MacOS/README Tue Dec 04 16:11:52 2018 +0100 +++ b/Admin/MacOS/README Wed Dec 05 19:42:40 2018 +0100 @@ -5,4 +5,3 @@ see appbundler-1.0.jar see com/oracle/appbundler/JavaAppLauncher - diff -r c19b7b565998 -r 7a1b7b737c02 Admin/MacOS/Resources/en.lproj/Localizable.strings --- a/Admin/MacOS/Resources/en.lproj/Localizable.strings Tue Dec 04 16:11:52 2018 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -"JRELoadError" = "Unable to load Java Runtime Environment."; -"MainClassNameRequired" = "Main class name is required."; -"JavaDirectoryNotFound" = "Unable to enumerate Java directory contents."; diff -r c19b7b565998 -r 7a1b7b737c02 Admin/MacOS/Resources/isabelle.icns Binary file Admin/MacOS/Resources/isabelle.icns has changed diff -r c19b7b565998 -r 7a1b7b737c02 Admin/MacOS/Resources/theory.icns Binary file Admin/MacOS/Resources/theory.icns has changed diff -r c19b7b565998 -r 7a1b7b737c02 Admin/MacOS/dmg/DS_Store Binary file Admin/MacOS/dmg/DS_Store has changed diff -r c19b7b565998 -r 7a1b7b737c02 Admin/MacOS/dmg/background.png Binary file Admin/MacOS/dmg/background.png has changed diff -r c19b7b565998 -r 7a1b7b737c02 Admin/components/bundled-macos --- a/Admin/components/bundled-macos Tue Dec 04 16:11:52 2018 +0100 +++ b/Admin/components/bundled-macos Wed Dec 05 19:42:40 2018 +0100 @@ -1,2 +1,2 @@ #additional components to be bundled for release -macos_app-20130716 +macos_app-20181205 diff -r c19b7b565998 -r 7a1b7b737c02 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Tue Dec 04 16:11:52 2018 +0100 +++ b/Admin/components/components.sha1 Wed Dec 05 19:42:40 2018 +0100 @@ -151,6 +151,7 @@ 377e36efb8608e6c828c7718d890e97fde2006a4 linux_app-20131007.tar.gz 0aab4f73ff7f5e36f33276547e10897e1e56fb1d macos_app-20130716.tar.gz ad5d0e640ce3609a885cecab645389a2204e03bb macos_app-20150916.tar.gz +400af57ec5cd51f96928d9de00d077524a6fe316 macos_app-20181205.tar.gz 26df569cee9c2fd91b9ac06714afd43f3b37a1dd nunchaku-0.3.tar.gz e573f2cbb57eb7b813ed5908753cfe2cb41033ca nunchaku-0.5.tar.gz fe57793aca175336deea4f5e9c0d949a197850ac opam-1.2.2.tar.gz diff -r c19b7b565998 -r 7a1b7b737c02 Admin/lib/Tools/makedist_bundle --- a/Admin/lib/Tools/makedist_bundle Tue Dec 04 16:11:52 2018 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,394 +0,0 @@ -#!/usr/bin/env bash -# -# DESCRIPTION: re-package Isabelle distribution with add-on components - -## diagnostics - -PRG=$(basename "$0") - -function usage() -{ - echo - echo "Usage: isabelle $PRG ARCHIVE PLATFORM_FAMILY [REMOTE_MAC]" - echo - echo " Re-package Isabelle source distribution with add-on components and" - echo " post-hoc patches for platform family linux, windows, macos." - echo - echo " The optional remote Mac OS X system is used for dmg build." - echo - echo " Add-on components are that of the running Isabelle version!" - echo - exit 1 -} - -function fail() -{ - echo "$1" >&2 - exit 2 -} - - -## arguments - -[ "$#" -ne 2 -a "$#" -ne 3 ] && usage - -ARCHIVE="$1"; shift -PLATFORM_FAMILY="$1"; shift -REMOTE_MAC="$1"; shift - -[ -f "$ARCHIVE" ] || fail "Bad source archive: $ARCHIVE" - -ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")" -ISABELLE_NAME="$(basename "$ARCHIVE" .tar.gz)" - - -## main - -#GNU tar (notably on Mac OS X) -type -p gnutar >/dev/null && function tar() { gnutar "$@"; } - -TMP="/var/tmp/isabelle-makedist$$" -mkdir "$TMP" || fail "Cannot create directory $TMP" - -ISABELLE_TARGET="$TMP/$ISABELLE_NAME" - -tar -C "$TMP" -x -z -f "$ARCHIVE" || exit 2 - - -# distribution classpath (based on educated guesses) - -splitarray ":" "$ISABELLE_CLASSPATH"; CLASSPATH_ENTRIES=("${SPLITARRAY[@]}") -declare -a DISTRIBUTION_CLASSPATH=() - -for ENTRY in "${CLASSPATH_ENTRIES[@]}" -do - ENTRY=$(echo "$ENTRY" | perl -n -e " - if (m,$ISABELLE_HOME/(.*)\$,) { print qq{\$1}; } - elsif (m,$USER_HOME/.isabelle/contrib/(.*)\$,) { print qq{contrib/\$1}; } - elsif (m,/home/isabelle/contrib/(.*)\$,) { print qq{contrib/\$1}; } - else { print; }; - print qq{\n};") - DISTRIBUTION_CLASSPATH["${#DISTRIBUTION_CLASSPATH[@]}"]="$ENTRY" -done - -DISTRIBUTION_CLASSPATH["${#DISTRIBUTION_CLASSPATH[@]}"]="src/Tools/jEdit/dist/jedit.jar" - -echo "classpath" -for ENTRY in "${DISTRIBUTION_CLASSPATH[@]}" -do - echo " $ENTRY" -done - - -# bundled components - -if [ ! -e "$ARCHIVE_DIR/contrib" ]; then - if [ ! -e "$ARCHIVE_DIR/../contrib" ]; then - mkdir -p "$ARCHIVE_DIR/contrib" - else - ln -s "../contrib" "$ARCHIVE_DIR/contrib" - fi -fi - -echo "#bundled components" >> "$ISABELLE_TARGET/etc/components" - -for CATALOG in main "$PLATFORM_FAMILY" bundled "bundled-$PLATFORM_FAMILY" -do - CATALOG_FILE="$ISABELLE_HOME/Admin/components/$CATALOG" - if [ -f "$CATALOG_FILE" ] - then - echo "catalog ${CATALOG}" - { - while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; } - do - case "$REPLY" in - \#* | "") ;; - *) - COMPONENT="$REPLY" - COMPONENT_DIR="$ISABELLE_TARGET/contrib/$COMPONENT" - case "$COMPONENT" in - jedit_build*) ;; - *) - echo " component $COMPONENT" - CONTRIB="$ARCHIVE_DIR/contrib/${COMPONENT}.tar.gz" - if [ ! -f "$CONTRIB" ]; then - type -p curl > /dev/null || fail "Cannot download files: missing curl" - REMOTE="$ISABELLE_COMPONENT_REPOSITORY/${COMPONENT}.tar.gz" - echo " downloading $REMOTE" - curl --fail --silent "$REMOTE" > "$CONTRIB" || \ - fail "Failed to download \"$REMOTE\"" - perl -e "exit((stat('${CONTRIB}'))[7] == 0 ? 0 : 1);" && exit 2 - fi - - tar -C "$ISABELLE_TARGET/contrib" -x -z -f "$CONTRIB" || exit 2 - if [ -f "$COMPONENT_DIR/etc/settings" -o -f "$COMPONENT_DIR/etc/components" ] - then - case "$COMPONENT" in - jdk-*) - mv "$ISABELLE_TARGET/contrib/$COMPONENT" "$ISABELLE_TARGET/contrib/jdk" - echo "contrib/jdk" >> "$ISABELLE_TARGET/etc/components" - ;; - *) - echo "contrib/$COMPONENT" >> "$ISABELLE_TARGET/etc/components" - ;; - esac - fi - ;; - esac - ;; - esac - done - } < "$CATALOG_FILE" - fi -done - - -# purge other platforms - -function purge_target -{ - ( - cd "$ISABELLE_TARGET" - for DIR in $(eval find "$@" | sort) - do - echo "removing $DIR" - rm -rf "$DIR" - done - ) -} - - -# platform-specific setup (inside archive) - -case "$PLATFORM_FAMILY" in - linux) - purge_target 'contrib -name "x86*-darwin" -o -name "x86*-cygwin" -o -name "x86*-windows"' - - ( - init_component "$JEDIT_HOME" - - echo "# Java runtime options" - eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" - for ARG in "${JAVA_ARGS[@]}" - do - echo "$ARG" - done - echo "-Disabelle.jedit_server=${ISABELLE_NAME}" - ) > "$ISABELLE_TARGET/${ISABELLE_NAME}.options" - - LINUX_CLASSPATH="" - for ENTRY in "${DISTRIBUTION_CLASSPATH[@]}" - do - if [ -z "$LINUX_CLASSPATH" ]; then - LINUX_CLASSPATH="\\\$ISABELLE_HOME/$ENTRY" - else - LINUX_CLASSPATH="$LINUX_CLASSPATH:\\\$ISABELLE_HOME/$ENTRY" - fi - done - - cat "$ISABELLE_HOME/Admin/Linux/Isabelle.run" | \ - perl -p > "$ISABELLE_TARGET/${ISABELLE_NAME}.run" -e "s,{CLASSPATH},$LINUX_CLASSPATH,;" - chmod +x "$ISABELLE_TARGET/${ISABELLE_NAME}.run" - - mv "$ISABELLE_TARGET/contrib/linux_app" "$TMP/." - cp "$TMP/linux_app/Isabelle" "$ISABELLE_TARGET/$ISABELLE_NAME" - ;; - macos) - purge_target 'contrib -name "x86*-linux" -o -name "x86*-cygwin" -o -name "x86*-windows"' - mv "$ISABELLE_TARGET/contrib/macos_app" "$TMP/." - - perl -pi \ - -e "s,lookAndFeel=.*,lookAndFeel=com.apple.laf.AquaLookAndFeel,g;" \ - -e "s,delete-line.shortcut=.*,delete-line.shortcut=C+d,g;" \ - -e "s,delete.shortcut2=.*,delete.shortcut2=A+d,g;" \ - -e "s,plugin-blacklist.MacOSX.jar=true,plugin-blacklist.MacOSX.jar=,g;" \ - "$ISABELLE_TARGET/src/Tools/jEdit/dist/properties/jEdit.props" - ;; - windows) - purge_target 'contrib -name "x86*-linux" -o -name "x86*-darwin" -o -name "x86-cygwin"' - - mv "$ISABELLE_TARGET/contrib/windows_app" "$TMP/." - - perl -pi \ - -e "s,lookAndFeel=.*,lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel,g;" \ - -e "s,foldPainter=.*,foldPainter=Square,g;" \ - "$ISABELLE_TARGET/src/Tools/jEdit/dist/properties/jEdit.props" - - ( - init_component "$JEDIT_HOME" - - echo -e "# Java runtime options\r" - eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" - for ARG in "${JAVA_ARGS[@]}" - do - echo -e "$ARG\r" - done - echo -e "-Disabelle.jedit_server=${ISABELLE_NAME}\r" - ) > "$ISABELLE_TARGET/${ISABELLE_NAME}.l4j.ini" - - ( - cd "$TMP" - - APP_TEMPLATE="$ISABELLE_HOME/Admin/Windows/launch4j" - - ( - for ENTRY in "${DISTRIBUTION_CLASSPATH[@]}" - do - ENTRY=$(echo "$ENTRY" | perl -p -e 's,/,\\\\,g;') - echo " %EXEDIR%\\\\$ENTRY" - done - ) > exe_classpath - EXE_CLASSPATH="$(cat exe_classpath)" - - perl -p \ - -e "s,{OUTFILE},$ISABELLE_TARGET/${ISABELLE_NAME}.exe,g;" \ - -e "s,{ICON},$APP_TEMPLATE/isabelle_transparent.ico,g;" \ - -e "s,{SPLASH},$APP_TEMPLATE/isabelle.bmp,g;" \ - -e "s,{CLASSPATH},$EXE_CLASSPATH,g;" \ - -e "s,{ISABELLE_NAME},$ISABELLE_NAME,g;" \ - "$APP_TEMPLATE/isabelle.xml" > isabelle.xml - - "windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j" isabelle.xml - - cp "$APP_TEMPLATE/manifest.xml" "$ISABELLE_TARGET/${ISABELLE_NAME}.exe.manifest" - ) - - ( - cd "$ISABELLE_TARGET" - - cp "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Terminal.bat" . - - CYGWIN_MIRROR="$(cat contrib/cygwin/isabelle/cygwin_mirror)" - cat "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Setup.bat" | \ - perl -p > "Cygwin-Setup.bat" -e "s,{MIRROR},$CYGWIN_MIRROR,;" - chmod +x "Cygwin-Setup.bat" - - for NAME in postinstall rebaseall - do - cp -a "$ISABELLE_HOME/Admin/Windows/Cygwin/isabelle/$NAME" \ - "contrib/cygwin/isabelle/." - done - - if [ "$ISABELLE_PLATFORM_FAMILY" = macos ]; then - find . -type f -not -name '*.exe' -not -name '*.dll' -perm +100 \ - -print0 > "contrib/cygwin/isabelle/executables" - else - find . -type f -not -name '*.exe' -not -name '*.dll' -executable \ - -print0 > "contrib/cygwin/isabelle/executables" - fi - - find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" \ - > "contrib/cygwin/isabelle/symlinks" - find . -type l -exec rm "{}" ";" - - touch "contrib/cygwin/isabelle/uninitialized" - ) - ;; - *) - ;; -esac - - -# archive - -BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_${PLATFORM_FAMILY}.tar.gz" - -echo "packaging $(basename "$BUNDLE_ARCHIVE")" -tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" "$ISABELLE_NAME" || exit 2 - - -# platform-specific setup (outside archive) - -case "$PLATFORM_FAMILY" in - linux) - echo "application for $PLATFORM_FAMILY" - ln -s "${ISABELLE_NAME}_linux.tar.gz" "${ARCHIVE_DIR}/${ISABELLE_NAME}_app.tar.gz" - ;; - macos) - echo "application for $PLATFORM_FAMILY" - ( - cd "$TMP" - - APP_TEMPLATE="$ISABELLE_HOME/Admin/MacOS" - APP="dmg/${ISABELLE_NAME}.app" - - mkdir -p "dmg/.background" - cp "$APP_TEMPLATE/dmg/background.png" "dmg/.background/" - cp "$APP_TEMPLATE/dmg/DS_Store" "dmg/.DS_Store" - ln -s /Applications "dmg/." - - for NAME in Java MacOS PlugIns Resources - do - mkdir -p "$APP/Contents/$NAME" - done - - ( - init_component "$JEDIT_HOME" - - cat "$APP_TEMPLATE/Info.plist-part1" - - declare -a OPTIONS=() - eval "OPTIONS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" - for OPT in "${OPTIONS[@]}" - do - echo "$OPT" - done - echo "-Disabelle.jedit_server={ISABELLE_NAME}" - echo "-Dapple.awt.application.name={ISABELLE_NAME}" - - cat "$APP_TEMPLATE/Info.plist-part2" - ) | perl -p -e "s,{ISABELLE_NAME},${ISABELLE_NAME},g;" > "$APP/Contents/Info.plist" - - for ENTRY in "${DISTRIBUTION_CLASSPATH[@]}" - do - ln -sf "../Resources/${ISABELLE_NAME}/$ENTRY" "$APP/Contents/Java" - done - - cp -R "$APP_TEMPLATE/Resources/." "$APP/Contents/Resources/." - - ln -sf "../Resources/${ISABELLE_NAME}/contrib/jdk/x86_64-darwin" \ - "$APP/Contents/PlugIns/bundled.jdk" - - cp macos_app/JavaAppLauncher "$APP/Contents/MacOS/." && \ - chmod +x "$APP/Contents/MacOS/JavaAppLauncher" - - mv "$ISABELLE_NAME" "$APP/Contents/Resources/." - ln -sf "../../Info.plist" "$APP/Contents/Resources/$ISABELLE_NAME/${ISABELLE_NAME}.plist" - ln -sf "Contents/Resources/$ISABELLE_NAME" "$APP/Isabelle" - - rm -f "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg" - tar -C dmg -czf "${ARCHIVE_DIR}/${ISABELLE_NAME}_dmg.tar.gz" . - - if [ -n "$REMOTE_MAC" ] - then - echo -n "$REMOTE_MAC: building dmg ..." - isabelle remote_dmg -V Isabelle "$REMOTE_MAC" \ - "${ARCHIVE_DIR}/${ISABELLE_NAME}_dmg.tar.gz" "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg" && - echo " done" - fi - ) - ;; - windows) - ( - cd "$TMP" - rm -f "$TMP/${ISABELLE_NAME}.7z" - 7z -y -bd a "$TMP/${ISABELLE_NAME}.7z" "$ISABELLE_NAME" - [ -f "$TMP/${ISABELLE_NAME}.7z" ] || exit 2 - - echo "application for $PLATFORM_FAMILY" - ( - cat "windows_app/7zsd_All_x64.sfx" - cat "$ISABELLE_HOME/Admin/Windows/Installer/sfx.txt" | \ - perl -p -e "s,{ISABELLE_NAME},${ISABELLE_NAME},g;" - cat "$TMP/${ISABELLE_NAME}.7z" - ) > "${ARCHIVE_DIR}/${ISABELLE_NAME}.exe" - chmod +x "${ARCHIVE_DIR}/${ISABELLE_NAME}.exe" - ) - ;; - *) - ;; -esac - - -# clean up -rm -rf "$TMP" diff -r c19b7b565998 -r 7a1b7b737c02 src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala Tue Dec 04 16:11:52 2018 +0100 +++ b/src/Pure/Admin/build_release.scala Wed Dec 05 19:42:40 2018 +0100 @@ -21,6 +21,7 @@ } class Release private[Build_Release]( + progress: Progress, val date: Date, val dist_name: String, val dist_dir: Path, @@ -31,7 +32,10 @@ val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz") val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz") - val other_isabelle_identifier: String = dist_name + "-build" + def other_isabelle(dir: Path): Other_Isabelle = + Other_Isabelle(dir + Path.explode(dist_name), + isabelle_identifier = dist_name + "-build", + progress = progress) def bundle_info(platform_family: String): Bundle_Info = platform_family match { @@ -168,10 +172,17 @@ } yield bundled(line)).toList)) } - def get_bundled_components(dir: Path, platform: String): List[String] = + def get_bundled_components(dir: Path, platform: String): (List[String], String) = { val Bundled = new Bundled(platform) - for (Bundled(name) <- Components.read_components(dir)) yield name + val components = + for { + Bundled(name) <- Components.read_components(dir) + if !name.startsWith("jedit_build") + } yield name + val jdk_component = + components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component") + (components, jdk_component) } def activate_bundled_components(dir: Path, platform: String) @@ -202,28 +213,6 @@ /** build_release **/ - def distribution_classpath( - components_base: Path, - isabelle_home: Path, - isabelle_classpath: String): List[Path] = - { - val base = isabelle_home.absolute - val contrib_base = components_base.absolute - - Path.split(isabelle_classpath).map(path => - { - val abs_path = path.absolute - File.relative_path(base, abs_path) match { - case Some(rel_path) => rel_path - case None => - File.relative_path(contrib_base, abs_path) match { - case Some(rel_path) => Components.contrib() + rel_path - case None => error("Bad ISABELLE_CLASSPATH element: " + path) - } - } - }) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar")) - } - private def execute(dir: Path, script: String): Unit = Isabelle_System.bash(script, cwd = dir.file).check @@ -236,6 +225,7 @@ private val default_platform_families = List("linux", "windows", "macos") def build_release(base_dir: Path, + options: Options, components_base: Option[Path] = None, progress: Progress = No_Progress, rev: String = "", @@ -267,7 +257,7 @@ case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date) } - new Release(date, dist_name, dist_dir, dist_version, ident) + new Release(progress, date, dist_name, dist_dir, dist_version, ident) } @@ -320,13 +310,12 @@ execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""") + record_bundled_components(release.isabelle_dir) + /* build tools and documentation */ - val other_isabelle = - Other_Isabelle(release.isabelle_dir, - isabelle_identifier = release.other_isabelle_identifier, - progress = progress) + val other_isabelle = release.other_isabelle(release.dist_dir) other_isabelle.init_settings( other_isabelle.init_components(base = components_base, catalogs = List("main"))) @@ -406,13 +395,262 @@ if (bundle_archive.is_file) progress.echo_warning("Application bundle already exists: " + bundle_archive) else { - progress.echo( - "\nApplication bundle for " + bundle_info.platform_family + ": " + bundle_archive) - progress.bash( - "isabelle makedist_bundle " + File.bash_path(release.isabelle_archive) + - " " + Bash.string(bundle_info.platform_family) + - (if (remote_mac == "") "" else " " + Bash.string(remote_mac)), - echo = true).check + val isabelle_name = release.dist_name + val platform = bundle_info.platform_family + + progress.echo("\nApplication bundle for " + platform + ": " + bundle_archive) + + Isabelle_System.with_tmp_dir("build_release")(tmp_dir => + { + // release archive + + execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive)) + val other_isabelle = release.other_isabelle(tmp_dir) + val isabelle_target = other_isabelle.isabelle_home + + + // bundled components + + progress.echo("Bundled components:") + + val contrib_dir = Components.contrib(isabelle_target) + + val (components, jdk_component) = get_bundled_components(isabelle_target, platform) + + Components.resolve(other_isabelle.components_base(components_base), + components, target_dir = Some(contrib_dir), progress = progress) + + Components.purge(contrib_dir, platform) + + activate_bundled_components(isabelle_target, platform) + + + // Java parameters + + val java_options_title = "# Java runtime options" + val java_options: List[String] = + (for { + variable <- + List( + "ISABELLE_JAVA_SYSTEM_OPTIONS", + "JEDIT_JAVA_SYSTEM_OPTIONS", + "JEDIT_JAVA_OPTIONS") + opt <- Word.explode(other_isabelle.getenv(variable)) + } yield opt) ::: List("-Disabelle.jedit_server=" + isabelle_name) + + val classpath: List[Path] = + { + val base = isabelle_target.absolute + Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path => + { + val abs_path = path.absolute + File.relative_path(base, abs_path) match { + case Some(rel_path) => rel_path + case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path) + } + }) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar")) + } + + val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props") + + + // platform-specific setup (inside archive) + + if (platform == "linux") { + File.write(isabelle_target + Path.explode(isabelle_name + ".options"), + terminate_lines(java_options_title :: java_options)) + + val isabelle_run = isabelle_target + Path.explode(isabelle_name + ".run") + File.write(isabelle_run, + File.read(Path.explode("~~/Admin/Linux/Isabelle.run")) + .replaceAllLiterally("{CLASSPATH}", + classpath.map("$ISABELLE_HOME/" + _).mkString(":")) + .replaceAllLiterally("/jdk/", "/" + jdk_component + "/")) + Isabelle_System.bash("chmod +x " + File.bash_path(isabelle_run)).check + + val linux_app = isabelle_target + Path.explode("contrib/linux_app") + File.move(linux_app + Path.explode("Isabelle"), + isabelle_target + Path.explode(isabelle_name)) + Isabelle_System.rm_tree(linux_app) + } + else if (platform == "macos") { + File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir) + File.write(isabelle_target + jedit_props, + File.read(isabelle_target + jedit_props) + .replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel") + .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d") + .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d") + .replaceAll("plugin-blacklist.MacOSX.jar=true", "plugin-blacklist.MacOSX.jar=")) + } + else if (platform == "windows") { + val app_template = Path.explode("~~/Admin/Windows/launch4j") + val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin") + + File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir) + + File.write(isabelle_target + jedit_props, + File.read(isabelle_target + jedit_props) + .replaceAll("lookAndFeel=.*", + "lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel") + .replaceAll("foldPainter=.*", "foldPainter=Square")) + + File.write(isabelle_target + Path.explode(isabelle_name + ".l4j.ini"), + (java_options_title :: java_options).map(_ + "\r\n").mkString) + + val isabelle_xml = Path.explode("isabelle.xml") + val isabelle_exe = Path.explode(isabelle_name + ".exe") + + File.write(tmp_dir + isabelle_xml, + File.read(app_template + isabelle_xml) + .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name) + .replaceAllLiterally("{OUTFILE}", File.platform_path(isabelle_target + isabelle_exe)) + .replaceAllLiterally("{ICON}", + File.platform_path(app_template + Path.explode("isabelle_transparent.ico"))) + .replaceAllLiterally("{SPLASH}", + File.platform_path(app_template + Path.explode("isabelle.bmp"))) + .replaceAllLiterally("{CLASSPATH}", + cat_lines(classpath.map(cp => + " %EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + ""))) + .replaceAllLiterally("\\jdk\\", "\\" + jdk_component + "\\")) + + Isabelle_System.bash( + "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml", + cwd = tmp_dir.file).check + + File.copy(app_template + Path.explode("manifest.xml"), + isabelle_target + isabelle_exe.ext("manifest")) + + + File.copy(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target) + + val cygwin_mirror = + File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror")) + + val cygwin_bat = Path.explode("Cygwin-Setup.bat") + File.write(isabelle_target + cygwin_bat, + File.read(cygwin_template + cygwin_bat) + .replaceAllLiterally("{MIRROR}", cygwin_mirror)) + + Isabelle_System.bash("chmod +x " + File.bash_path(isabelle_target + cygwin_bat)).check + + for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) { + val path = Path.explode(name) + File.copy(cygwin_template + path, + isabelle_target + Path.explode("contrib/cygwin") + path) + } + + Isabelle_System.bash("""find . -type f -not -name "*.exe" -not -name "*.dll" """ + + (if (Platform.is_macos) "-perm +100" else "-executable") + + " -print0 > contrib/cygwin/isabelle/executables", + cwd = isabelle_target.file).check + + Isabelle_System.bash("""find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ + + """> contrib/cygwin/isabelle/symlinks""", + cwd = isabelle_target.file).check + + Isabelle_System.bash("""find . -type l -exec rm "{}" ";" """, + cwd = isabelle_target.file).check + + File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "") + } + + + // archive + + val archive_name = isabelle_name + "_" + platform + ".tar.gz" + progress.echo("Packaging " + archive_name) + execute_tar(tmp_dir, + "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " + + Bash.string(isabelle_name)) + + + // platform-specific application (outside archive) + + progress.echo("Application for " + platform) + + if (platform == "linux") { + Isabelle_System.bash( + "ln -s " + Bash.string(isabelle_name + "_linux.tar.gz") + " " + + File.bash_path(release.dist_dir + Path.explode(isabelle_name + "_app.tar.gz"))).check + } + else if (platform == "macos") { + val dmg_dir = tmp_dir + Path.explode("macos_app/dmg") + val app_dir = dmg_dir + Path.explode(isabelle_name + ".app") + File.move(dmg_dir + Path.explode("Isabelle.app"), app_dir) + + val app_contents = app_dir + Path.explode("Contents") + val app_resources = app_contents + Path.explode("Resources") + File.move(tmp_dir + Path.explode(isabelle_name), app_resources) + + File.write(app_contents + Path.explode("Info.plist"), + File.read(Path.explode("~~/Admin/MacOS/Info.plist")) + .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name) + .replaceAllLiterally("{JAVA_OPTIONS}", + terminate_lines(java_options.map(opt => "" + opt + "")))) + + for (cp <- classpath) { + Isabelle_System.bash( + "ln -sf " + + Bash.string("../Resources/" + isabelle_name + "/") + File.bash_path(cp) + " " + + File.bash_path(app_contents + Path.explode("Java"))).check + } + + Isabelle_System.bash("ln -sf ../Resources/" + Bash.string(isabelle_name) + + "/contrib/" + Bash.string(jdk_component) + "/x86_64-darwin " + + File.bash_path(app_contents + Path.explode("PlugIns/bundled.jdk"))).check + + Isabelle_System.bash("ln -sf ../../Info.plist " + + File.bash_path(app_resources + Path.explode(isabelle_name) + + Path.explode(isabelle_name + ".plist"))).check + Isabelle_System.bash("ln -sf Contents/Resources/" + Bash.string(isabelle_name) + " " + + File.bash_path(app_dir) + "/Isabelle").check + + val dmg = Path.explode(isabelle_name + ".dmg") + (release.dist_dir + dmg).file.delete + + val dmg_archive = Path.explode(isabelle_name + "_dmg.tar.gz") + execute_tar(dmg_dir, "-czf " + File.bash_path(release.dist_dir + dmg_archive) + " .") + + remote_mac match { + case SSH.Target(user, host) => + progress.echo("Building dmg on " + quote(host) + " ...") + using(SSH.open_session(options, host = host, user = user))(ssh => + { + ssh.with_tmp_dir(remote_dir => + { + val cd = "cd " + ssh.bash_path(remote_dir) + "; " + ssh.write_file(remote_dir + dmg_archive, release.dist_dir + dmg_archive) + ssh.execute( + cd + "mkdir root && tar -C root -xzf " + ssh.bash_path(dmg_archive)).check + ssh.execute( + cd + "hdiutil create -srcfolder root -volname Isabelle " + + ssh.bash_path(dmg)).check + ssh.read_file(remote_dir + dmg, release.dist_dir + dmg) + }) + }) + case _ => + } + } + else if (platform == "windows") { + val exe_archive = tmp_dir + Path.explode(isabelle_name + ".7z") + exe_archive.file.delete + + Isabelle_System.bash("7z -y -bd a " + File.bash_path(exe_archive) + " " + + Bash.string(isabelle_name), cwd = tmp_dir.file).check + if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive) + + val isabelle_exe = Path.explode(isabelle_name + ".exe") + val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx") + val sfx_txt = + File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt")). + replaceAllLiterally("{ISABELLE_NAME}", isabelle_name) + + Bytes.write(release.dist_dir + isabelle_exe, + Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive)) + + Isabelle_System.bash("chmod +x " + (release.dist_dir + isabelle_exe)).check + } + }) } } @@ -452,14 +690,12 @@ else { Isabelle_System.with_tmp_dir("build_release")(tmp_dir => { - val name = release.dist_name val platform = Isabelle_System.getenv_strict("ISABELLE_PLATFORM_FAMILY") - val bundle = release.dist_dir + Path.explode(name + "_" + platform + ".tar.gz") + val bundle = + release.dist_dir + Path.explode(release.dist_name + "_" + platform + ".tar.gz") execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle)) - val other_isabelle = - Other_Isabelle(tmp_dir + Path.explode(name), - isabelle_identifier = release.other_isabelle_identifier, progress = progress) + val other_isabelle = release.other_isabelle(tmp_dir) Isabelle_System.mkdirs(other_isabelle.etc) File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n") @@ -469,11 +705,11 @@ " -s -c -a -d '~~/src/Benchmarks'", echo = true).check other_isabelle.isabelle_home_user.file.delete - execute(tmp_dir, "chmod -R a+r " + Bash.string(name)) - execute(tmp_dir, "chmod -R g=o " + Bash.string(name)) + execute(tmp_dir, "chmod -R a+r " + Bash.string(release.dist_name)) + execute(tmp_dir, "chmod -R g=o " + Bash.string(release.dist_name)) execute_tar(tmp_dir, tar_options + " -czf " + File.bash_path(release.isabelle_library_archive) + - " " + Bash.string(name + "/browser_info")) + " " + Bash.string(release.dist_name + "/browser_info")) }) } } @@ -496,6 +732,7 @@ var website: Option[Path] = None var parallel_jobs = 1 var build_library = false + var options = Options.init() var platform_families = default_platform_families var rev = "" @@ -511,6 +748,7 @@ -W WEBSITE produce minimal website in given directory -j INT maximum number of parallel jobs (default 1) -l build library + -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -p NAMES platform families (default: """ + default_platform_families.mkString(",") + """) -r REV Mercurial changeset id (default: RELEASE or tip) @@ -524,6 +762,7 @@ "W:" -> (arg => website = Some(Path.explode(arg))), "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)), "l" -> (_ => build_library = true), + "o:" -> (arg => options = options + arg), "p:" -> (arg => platform_families = space_explode(',', arg)), "r:" -> (arg => rev = arg)) @@ -532,8 +771,8 @@ val progress = new Console_Progress() - build_release(Path.explode(base_dir), components_base = components_base, progress = progress, - rev = rev, afp_rev = afp_rev, official_release = official_release, + build_release(Path.explode(base_dir), options, components_base = components_base, + progress = progress, rev = rev, afp_rev = afp_rev, official_release = official_release, proper_release_name = proper_release_name, website = website, platform_families = if (platform_families.isEmpty) default_platform_families diff -r c19b7b565998 -r 7a1b7b737c02 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Tue Dec 04 16:11:52 2018 +0100 +++ b/src/Pure/Admin/isabelle_cronjob.scala Wed Dec 05 19:42:40 2018 +0100 @@ -75,7 +75,7 @@ val build_release = Logger_Task("build_release", logger => { - Isabelle_Devel.release_snapshot( + Isabelle_Devel.release_snapshot(logger.options, rev = get_rev(), afp_rev = get_afp_rev(), remote_mac = "macbroy30") }) diff -r c19b7b565998 -r 7a1b7b737c02 src/Pure/Admin/isabelle_devel.scala --- a/src/Pure/Admin/isabelle_devel.scala Tue Dec 04 16:11:52 2018 +0100 +++ b/src/Pure/Admin/isabelle_devel.scala Wed Dec 05 19:42:40 2018 +0100 @@ -51,6 +51,7 @@ /* release snapshot */ def release_snapshot( + options: Options, rev: String = "", afp_rev: String = "", parallel_jobs: Int = 1, @@ -60,7 +61,7 @@ { Isabelle_System.update_directory(root + Path.explode(RELEASE_SNAPSHOT), website_dir => - Build_Release.build_release(base_dir, rev = rev, afp_rev = afp_rev, + Build_Release.build_release(base_dir, options, rev = rev, afp_rev = afp_rev, parallel_jobs = parallel_jobs, remote_mac = remote_mac, website = Some(website_dir))) }) } diff -r c19b7b565998 -r 7a1b7b737c02 src/Pure/Admin/other_isabelle.scala --- a/src/Pure/Admin/other_isabelle.scala Tue Dec 04 16:11:52 2018 +0100 +++ b/src/Pure/Admin/other_isabelle.scala Wed Dec 05 19:42:40 2018 +0100 @@ -68,12 +68,15 @@ /* components */ + def components_base(base: Option[Path]): Path = + base getOrElse Components.contrib(isabelle_home_user.absolute.dir) + def init_components( base: Option[Path] = None, catalogs: List[String] = Nil, components: List[String] = Nil): List[String] = { - val base_dir = base getOrElse Components.contrib(isabelle_home_user.absolute.dir) + val base_dir = components_base(base) val dir = Components.admin(isabelle_home.absolute) catalogs.map(name => "init_components " + File.bash_path(base_dir) + " " + File.bash_path(dir + Path.basic(name))) ::: diff -r c19b7b565998 -r 7a1b7b737c02 src/Pure/Admin/remote_dmg.scala --- a/src/Pure/Admin/remote_dmg.scala Tue Dec 04 16:11:52 2018 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,64 +0,0 @@ -/* Title: Pure/Admin/remote_dmg.scala - Author: Makarius - -Build dmg on remote Mac OS X system. -*/ - -package isabelle - - -object Remote_DMG -{ - def remote_dmg(ssh: SSH.Session, tar_gz_file: Path, dmg_file: Path, volume_name: String = "") - { - ssh.with_tmp_dir(remote_dir => - { - val cd = "cd " + ssh.bash_path(remote_dir) + "; " - - ssh.write_file(remote_dir + Path.explode("dmg.tar.gz"), tar_gz_file) - ssh.execute(cd + "mkdir root && tar -C root -xzf dmg.tar.gz").check - ssh.execute( - cd + "hdiutil create -srcfolder root" + - (if (volume_name == "") "" else " -volname " + Bash.string(volume_name)) + - " dmg.dmg").check - ssh.read_file(remote_dir + Path.explode("dmg.dmg"), dmg_file) - }) - } - - - /* Isabelle tool wrapper */ - - val isabelle_tool = - Isabelle_Tool("remote_dmg", "build dmg on remote Mac OS X system", args => - { - Command_Line.tool0 { - var port = 0 - var volume_name = "" - - val getopts = Getopts(""" -Usage: isabelle remote_dmg [OPTIONS] USER@HOST TAR_GZ_FILE DMG_FILE - - Options are: - -p PORT alternative SSH port - -V NAME specify volume name - - Turn the contents of a tar.gz file into a dmg file -- produced on a remote - Mac OS X system. -""", - "p:" -> (arg => port = Value.Int.parse(arg)), - "V:" -> (arg => volume_name = arg)) - - val more_args = getopts(args) - val (user, host, tar_gz_file, dmg_file) = - more_args match { - case List(SSH.Target(user, host), tar_gz_file, dmg_file) => - (user, host, Path.explode(tar_gz_file), Path.explode(dmg_file)) - case _ => getopts.usage() - } - - val options = Options.init() - using(SSH.open_session(options, host = host, user = user, port = port))( - remote_dmg(_, tar_gz_file, dmg_file, volume_name)) - } - }) -} diff -r c19b7b565998 -r 7a1b7b737c02 src/Pure/System/components.scala --- a/src/Pure/System/components.scala Tue Dec 04 16:11:52 2018 +0100 +++ b/src/Pure/System/components.scala Wed Dec 05 19:42:40 2018 +0100 @@ -7,6 +7,9 @@ package isabelle +import java.io.{File => JFile} + + object Components { /* component collections */ @@ -16,20 +19,43 @@ def contrib(dir: Path = Path.current, name: String = ""): Path = dir + Path.explode("contrib") + Path.explode(name) - def download(dir: Path, names: List[String], progress: Progress = No_Progress) + def resolve(base_dir: Path, names: List[String], + target_dir: Option[Path] = None, + progress: Progress = No_Progress) { - Isabelle_System.mkdirs(dir) + Isabelle_System.mkdirs(base_dir) for (name <- names) { - val archive = name + ".tar.gz" - val target = dir + Path.explode(archive) - if (!target.is_file) { - val remote = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") + "/" + archive - progress.echo("Getting " + quote(remote)) - Bytes.write(target, Url.read_bytes(Url(remote))) + val archive_name = name + ".tar.gz" + val archive = base_dir + Path.explode(archive_name) + if (!archive.is_file) { + val remote = Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") + "/" + archive_name + progress.echo("Getting " + remote) + Bytes.write(archive, Url.read_bytes(Url(remote))) } + progress.echo("Unpacking " + archive_name) + Isabelle_System.gnutar( + "-C " + File.bash_path(target_dir getOrElse base_dir) + + " -xzf " + File.bash_path(archive)).check } } + def purge(dir: Path, platform: String) + { + def purge_platforms(platforms: String*): Set[String] = + platforms.flatMap(name => List("x86-" + name, "x86_64-" + name)).toSet + "ppc-darwin" + val purge_set = + platform match { + case "linux" => purge_platforms("darwin", "cygwin", "windows") + case "windows" => purge_platforms("linux", "darwin") + case "macos" => purge_platforms("linux", "cygwin", "windows") + case _ => error("Bad platform: " + quote(platform)) + } + + File.find_files(dir.file, + (file: JFile) => file.isDirectory && purge_set(file.getName), + include_dirs = true).foreach(Isabelle_System.rm_tree) + } + /* component directory content */ diff -r c19b7b565998 -r 7a1b7b737c02 src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Tue Dec 04 16:11:52 2018 +0100 +++ b/src/Pure/System/isabelle_tool.scala Wed Dec 05 19:42:40 2018 +0100 @@ -172,5 +172,4 @@ Build_PolyML.isabelle_tool2, Build_Status.isabelle_tool, Check_Sources.isabelle_tool, - Remote_DMG.isabelle_tool, isabelle.vscode.Build_VSCode.isabelle_tool) diff -r c19b7b565998 -r 7a1b7b737c02 src/Pure/build-jars --- a/src/Pure/build-jars Tue Dec 04 16:11:52 2018 +0100 +++ b/src/Pure/build-jars Wed Dec 05 19:42:40 2018 +0100 @@ -25,7 +25,6 @@ Admin/isabelle_devel.scala Admin/jenkins.scala Admin/other_isabelle.scala - Admin/remote_dmg.scala Concurrent/consumer_thread.scala Concurrent/counter.scala Concurrent/event_timer.scala