1.1 --- a/Admin/Linux/Isabelle.c Sat Apr 11 11:28:31 2015 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,41 +0,0 @@
1.4 -/* Author: Makarius
1.5 -
1.6 -Main Isabelle application executable.
1.7 -*/
1.8 -
1.9 -#include <stdlib.h>
1.10 -#include <stdio.h>
1.11 -#include <string.h>
1.12 -#include <sys/types.h>
1.13 -#include <unistd.h>
1.14 -
1.15 -
1.16 -static void fail(const char *msg)
1.17 -{
1.18 - fprintf(stderr, "%s\n", msg);
1.19 - exit(2);
1.20 -}
1.21 -
1.22 -
1.23 -int main(int argc, char *argv[])
1.24 -{
1.25 - char **cmd_line = NULL;
1.26 - int i = 0;
1.27 -
1.28 - cmd_line = malloc(sizeof(char *) * (argc + 1));
1.29 - if (cmd_line == NULL) fail("Failed to allocate command line");
1.30 -
1.31 - cmd_line[0] = malloc(strlen(argv[0]) + 5);
1.32 - if (cmd_line[0] == NULL) fail("Failed to allocate command line");
1.33 -
1.34 - strcpy(cmd_line[0], argv[0]);
1.35 - strcat(cmd_line[0], ".run");
1.36 -
1.37 - for (i = 1; i < argc; i++) cmd_line[i] = argv[i];
1.38 -
1.39 - cmd_line[argc] = NULL;
1.40 -
1.41 - execvp(cmd_line[0], cmd_line);
1.42 - fail("Failed to execute application script");
1.43 -}
1.44 -
2.1 --- a/Admin/Linux/Isabelle.run Sat Apr 11 11:28:31 2015 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,31 +0,0 @@
2.4 -#!/usr/bin/env bash
2.5 -#
2.6 -# Author: Makarius
2.7 -#
2.8 -# Main Isabelle application script.
2.9 -
2.10 -# dereference executable
2.11 -if [ -L "$0" ]; then
2.12 - TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
2.13 - exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
2.14 -fi
2.15 -
2.16 -
2.17 -# minimal Isabelle environment
2.18 -
2.19 -ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; pwd)"
2.20 -source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
2.21 -
2.22 -
2.23 -# main
2.24 -
2.25 -#paranoia setting -- avoid problems of Java/Swing versus XIM/IBus etc.
2.26 -unset XMODIFIERS
2.27 -
2.28 -exec "$ISABELLE_HOME/contrib/jdk/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/bin/java" \
2.29 - "-Disabelle.home=$ISABELLE_HOME" \
2.30 - {JAVA_ARGS} \
2.31 - -classpath "{CLASSPATH}" \
2.32 - "-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \
2.33 - isabelle.Main "$@"
2.34 -
3.1 --- a/Admin/Linux/build Sat Apr 11 11:28:31 2015 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,4 +0,0 @@
3.4 -#!/usr/bin/env bash
3.5 -
3.6 -cc -static -m32 Isabelle.c -o Isabelle
3.7 -
4.1 --- a/Admin/MacOS/Info.plist-part1 Sat Apr 11 11:28:31 2015 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,38 +0,0 @@
4.4 -<?xml version="1.0" ?>
4.5 -<!DOCTYPE plist PUBLIC "-//Apple//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">
4.6 -<plist version="1.0">
4.7 -<dict>
4.8 -<key>CFBundleDevelopmentRegion</key>
4.9 -<string>English</string>
4.10 -<key>CFBundleExecutable</key>
4.11 -<string>JavaAppLauncher</string>
4.12 -<key>CFBundleIconFile</key>
4.13 -<string>isabelle.icns</string>
4.14 -<key>CFBundleIdentifier</key>
4.15 -<string>de.tum.in.isabelle</string>
4.16 -<key>CFBundleDisplayName</key>
4.17 -<string>{ISABELLE_NAME}</string>
4.18 -<key>CFBundleInfoDictionaryVersion</key>
4.19 -<string>6.0</string>
4.20 -<key>CFBundleName</key>
4.21 -<string>{ISABELLE_NAME}</string>
4.22 -<key>CFBundlePackageType</key>
4.23 -<string>APPL</string>
4.24 -<key>CFBundleShortVersionString</key>
4.25 -<string>1.0</string>
4.26 -<key>CFBundleSignature</key>
4.27 -<string>????</string>
4.28 -<key>CFBundleVersion</key>
4.29 -<string>1</string>
4.30 -<key>NSHumanReadableCopyright</key>
4.31 -<string></string>
4.32 -<key>LSApplicationCategoryType</key>
4.33 -<string>public.app-category.developer-tools</string>
4.34 -<key>NSHighResolutionCapable</key>
4.35 -<string>true</string>
4.36 -<key>JVMRuntime</key>
4.37 -<string>jdk</string>
4.38 -<key>JVMMainClassName</key>
4.39 -<string>isabelle.Main</string>
4.40 -<key>JVMOptions</key>
4.41 -<array>
5.1 --- a/Admin/MacOS/Info.plist-part2 Sat Apr 11 11:28:31 2015 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,8 +0,0 @@
5.4 -<string>-Disabelle.home=$APP_ROOT/Contents/Resources/{ISABELLE_NAME}</string>
5.5 -<string>-Disabelle.app=true</string>
5.6 -</array>
5.7 -<key>JVMArguments</key>
5.8 -<array>
5.9 -</array>
5.10 -</dict>
5.11 -</plist>
6.1 --- a/Admin/MacOS/README Sat Apr 11 11:28:31 2015 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,8 +0,0 @@
6.4 -Isabelle/JVM application bundle for Mac OS X
6.5 -============================================
6.6 -
6.7 -* http://java.net/projects/appbundler
6.8 -
6.9 - see appbundler-1.0.jar
6.10 - see com/oracle/appbundler/JavaAppLauncher
6.11 -
7.1 --- a/Admin/MacOS/Resources/en.lproj/Localizable.strings Sat Apr 11 11:28:31 2015 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,3 +0,0 @@
7.4 -"JRELoadError" = "Unable to load Java Runtime Environment.";
7.5 -"MainClassNameRequired" = "Main class name is required.";
7.6 -"JavaDirectoryNotFound" = "Unable to enumerate Java directory contents.";
8.1 Binary file Admin/MacOS/Resources/isabelle.icns has changed
9.1 Binary file Admin/MacOS/Resources/theory.icns has changed
10.1 Binary file Admin/MacOS/dmg/DS_Store has changed
11.1 Binary file Admin/MacOS/dmg/background.png has changed
12.1 --- a/Admin/Mercurial/Central/Mercurial Sat Apr 11 11:28:31 2015 +0200
12.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
12.3 @@ -1,2 +0,0 @@
12.4 -This is the main Isabelle Mercurial repository.
12.5 -All the meta data is in .hg/
13.1 --- a/Admin/Mercurial/Central/README Sat Apr 11 11:28:31 2015 +0200
13.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
13.3 @@ -1,52 +0,0 @@
13.4 -Notes on central Isabelle repository
13.5 -====================================
13.6 -
13.7 -* direct file-system access (locally or remotely via ssh)
13.8 -
13.9 -* permissions via dedicated Unix group "isabelle"
13.10 -
13.11 -* See http://mercurial.selenic.com/wiki/RequiresFile on physical format, with
13.12 - conservative requirements for Mercurial 1.3 as lowest common denominator:
13.13 -
13.14 - revlogv1
13.15 - store
13.16 - fncache
13.17 -
13.18 -* See http://mercurial.selenic.com/wiki/MultipleCommitters for old-fashioned
13.19 - CVS-like multiple committers configuration, "The filesystem method".
13.20 -
13.21 - A fresh multi-user clone is initialized like this:
13.22 -
13.23 - hg --config format.dotencode=0 init isabelle-clone
13.24 - cd isabelle-clone
13.25 - chgrp -R isabelle .hg
13.26 - chmod g+s .hg .hg/store
13.27 - mkdir .hg/strip-backup ## Not to be used under normal circumstances!
13.28 - chmod -R g+w .hg
13.29 -
13.30 - Now isabelle-clone is ready for push of repository data (without making
13.31 - a working directory).
13.32 -
13.33 -* Addressing technical issues: according to
13.34 - http://mercurial.selenic.com/wiki/PublishingRepositories our shared disk
13.35 - configuration (after regular ssh login) is characterized as follows:
13.36 -
13.37 - Advantages: can use existing setup
13.38 -
13.39 - Disadvantages: generally restricted to intranets, not generally
13.40 - recommended due to general issues with network filesystem reliability
13.41 -
13.42 - Due to NFS instabilities of unknown origin at TUM, drop-outs have
13.43 - happened before. The following measures of last resort can be applied:
13.44 -
13.45 - (a) "hg verify" to find offending changesets
13.46 - "hg strip REV" to remove parts of the public history by vivisection
13.47 -
13.48 - (b) fresh clone from known-good source as explained above
13.49 -
13.50 - Note that any such non-monotonic changes on the central push area work
13.51 - under the assumption of sequential single-user mode!!
13.52 -
13.53 - See also http://mercurial.selenic.com/wiki/RepositoryCorruption for
13.54 - further background information.
13.55 -
14.1 --- a/Admin/Mercurial/Central/hgrc Sat Apr 11 11:28:31 2015 +0200
14.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
14.3 @@ -1,7 +0,0 @@
14.4 -[web]
14.5 -style = isabelle
14.6 -contact = isabelle
14.7 -description = The Isabelle repository
14.8 -allow_archive = gz
14.9 -maxfiles = 50
14.10 -encoding = UTF-8
15.1 --- a/Admin/PLATFORMS Sat Apr 11 11:28:31 2015 +0200
15.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
15.3 @@ -1,127 +0,0 @@
15.4 -Some notes on multi-platform support of Isabelle
15.5 -================================================
15.6 -
15.7 -Preamble
15.8 ---------
15.9 -
15.10 -The general programming model is that of a stylized ML + Scala + POSIX
15.11 -environment, with as little system-specific code in user-space tools
15.12 -as possible.
15.13 -
15.14 -The basic Isabelle system infrastructure provides some facilities to
15.15 -make this work, e.g. see the ML and Scala modules File and Path, or
15.16 -functions like Isabelle_System.bash. The settings environment also
15.17 -provides some means for portability, e.g. the bash function "jvmpath"
15.18 -to keep the impression that Java on Windows/Cygwin adheres to
15.19 -Isabelle/POSIX standards, although inside the JVM itself there are
15.20 -many Windows-specific things.
15.21 -
15.22 -When producing add-on tools, it is important to stay within this clean
15.23 -room of Isabelle, and refrain from overly ambitious system hacking.
15.24 -The existing Isabelle scripts follow a peculiar style that reflects
15.25 -long years of experience in getting system plumbing right.
15.26 -
15.27 -
15.28 -Supported platforms
15.29 --------------------
15.30 -
15.31 -The following hardware and operating system platforms are officially
15.32 -supported by the Isabelle distribution (and bundled tools), with the
15.33 -following reference versions (which have been selected to be neither
15.34 -too old nor too new):
15.35 -
15.36 - x86-linux Ubuntu 10.04 LTS
15.37 - x86_64-linux Ubuntu 10.04 LTS
15.38 -
15.39 - x86_64-darwin Mac OS X Lion (macbroy6)
15.40 - Mac OS X Mountain Lion (macbroy30)
15.41 - Mac OS X Mavericks (macbroy2)
15.42 -
15.43 - x86-cygwin Cygwin 1.7 (vmbroy9)
15.44 -
15.45 -All of the above platforms are 100% supported by Isabelle -- end-users
15.46 -should not have to care about the differences (at least in theory).
15.47 -
15.48 -Fringe platforms like BSD or Solaris are unsupported.
15.49 -
15.50 -
15.51 -32 bit vs. 64 bit platforms
15.52 ----------------------------
15.53 -
15.54 -Most users have 64 bit hardware and are running a 64 bit operating
15.55 -system by default. For Linux this usually means missing 32 bit shared
15.56 -libraries, so native x86_64-linux needs to be used by default, despite
15.57 -its doubled space requirements for Poly/ML heaps. For Mac OS X, the
15.58 -x86-darwin personality usually works seamlessly for C/C++ programs,
15.59 -but the Java 7 platform is only available for x86_64-darwin.
15.60 -
15.61 -Add-on executables are expected to work without manual user
15.62 -configuration. Each component settings script needs to determine the
15.63 -platform details appropriately.
15.64 -
15.65 -The Isabelle settings environment provides the following variables to
15.66 -help configuring platform-dependent tools:
15.67 -
15.68 - ISABELLE_PLATFORM64 (potentially empty)
15.69 - ISABELLE_PLATFORM32
15.70 - ISABELLE_PLATFORM
15.71 -
15.72 -The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
15.73 -the platform, even on 64 bit hardware. Using regular bash notation,
15.74 -tools may express their preference for 64 bit with a fall-back for 32
15.75 -bit as follows:
15.76 -
15.77 - "${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
15.78 -
15.79 -Moreover note that ML and JVM usually have a different idea of the
15.80 -platform, depending on the respective binaries that are actually run.
15.81 -Poly/ML 5.5.x performs best in 32 bit mode, even for large
15.82 -applications, thanks to its sophisticated heap management. The JVM
15.83 -usually works better in 64 bit mode, which allows its heap to grow
15.84 -beyond 2 GB.
15.85 -
15.86 -The traditional "uname" Unix tool usually only tells about its own
15.87 -executable format, not the underlying platform!
15.88 -
15.89 -
15.90 -Dependable system tools
15.91 ------------------------
15.92 -
15.93 -The following portable system tools can be taken for granted:
15.94 -
15.95 -* GNU bash as uniform shell on all platforms. The POSIX "standard"
15.96 - shell /bin/sh is *not* appropriate, because there are too many
15.97 - non-standard implementations of it.
15.98 -
15.99 -* Perl as largely portable system programming language. In some
15.100 - situations Python may serve as an alternative, but it usually
15.101 - performs not as well in addressing various delicate details of
15.102 - operating system concepts (processes, signals, sockets etc.).
15.103 -
15.104 -* Scala with Java 1.7. Isabelle/Scala irons out many oddities and
15.105 - portability issues of the Java platform.
15.106 -
15.107 -
15.108 -Known problems
15.109 ---------------
15.110 -
15.111 -* Mac OS X: If MacPorts is installed there is some danger that
15.112 - accidental references to its shared libraries are created
15.113 - (e.g. libgmp). Use otool -L to check if compiled binaries also work
15.114 - without MacPorts.
15.115 -
15.116 -* Mac OS X: If MacPorts is installed and its version of Perl takes
15.117 - precedence over /usr/bin/perl in the PATH, then the end-user needs
15.118 - to take care of installing extra modules, e.g. for HTTP support.
15.119 - Such add-ons are usually included in Apple's /usr/bin/perl by
15.120 - default.
15.121 -
15.122 -* The Java runtime has its own idea about the underlying platform,
15.123 - which affects Java native libraries in particular. In
15.124 - Isabelle/Scala the function isabelle.Platform.jvm_platform
15.125 - identifies the JVM platform. Since a particular Java version is
15.126 - always bundled with Isabelle, the resulting settings also provide
15.127 - some clues about its platform, without running it.
15.128 -
15.129 -* Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are
15.130 - notoriously non-portable an should be avoided.
15.131 \ No newline at end of file
16.1 --- a/Admin/README Sat Apr 11 11:28:31 2015 +0200
16.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
16.3 @@ -1,2 +0,0 @@
16.4 -This directory contains some administrative tools for clones of the
16.5 -Isabelle repository. They do not appear in proper distributions.
17.1 --- a/Admin/Release/CHECKLIST Sat Apr 11 11:28:31 2015 +0200
17.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
17.3 @@ -1,93 +0,0 @@
17.4 -Checklist for official releases
17.5 -===============================
17.6 -
17.7 -- check latest polyml, smlnj, jdk, scala, jedit;
17.8 -
17.9 -- check Admin/components;
17.10 -
17.11 -- test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0, smlnj;
17.12 -
17.13 -- test Isabelle/jEdit on single-core;
17.14 -
17.15 -- test Isabelle/jEdit on airy device;
17.16 -
17.17 -- test 'display_drafts' command;
17.18 -
17.19 -- test "#!/usr/bin/env isabelle_scala_script";
17.20 -
17.21 -- check sources:
17.22 - isabelle java isabelle.Check_Source '~~' '$AFP_BASE'
17.23 -
17.24 -- run isabelle update_keywords;
17.25 -
17.26 -- check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS;
17.27 -
17.28 -- check funny base directory, e.g. "Test ä¸å›½";
17.29 -
17.30 -- check scalable fonts, e.g. src/Doc/Prog_Prove (NOTE: T1 encoding
17.31 - requires cm-super fonts, which are usually available on MacTeX or
17.32 - Cygwin, but not on Ubuntu/Debian);
17.33 -
17.34 -- diff NEWS wrt. last official release, which is read-only;
17.35 -
17.36 -- update https://bitbucket.org/isabelle_project/isabelle-website
17.37 -
17.38 -- maintain doc/Contents;
17.39 -
17.40 -- maintain Logics:
17.41 - ROOTS
17.42 - lib/html/library_index_content.template
17.43 -
17.44 -- check HTML header of library;
17.45 -
17.46 -- test separate compilation of Isabelle/Scala PIDE sources:
17.47 - Admin/build jars_test
17.48 -
17.49 -- test Isabelle/jEdit:
17.50 - print buffer
17.51 -
17.52 -- test contrib components:
17.53 - x86_64-linux without 32bit C/C++ libraries
17.54 -
17.55 -- check "Handler catches all exceptions", using
17.56 - PolyML.Compiler.reportExhaustiveHandlers := true;
17.57 -
17.58 -- Mac OS X: check app bundle with Retina display;
17.59 -
17.60 -- Windows: check dpi scaling with high-definition display;
17.61 -
17.62 -
17.63 -Repository fork
17.64 -===============
17.65 -
17.66 -- isabelle: finalize NEWS / CONTRIBUTORS -- proper headers for named release;
17.67 -
17.68 -- isabelle-release: hg tag;
17.69 -
17.70 -- isabelle: back to post-release mode -- after fork point;
17.71 -
17.72 -
17.73 -Packaging
17.74 -=========
17.75 -
17.76 -- fully-automated packaging (requires Mac OS X with gnutar, avoid Mavericks):
17.77 -
17.78 - hg up -r DISTNAME && Admin/Release/build -O -l -r DISTNAME /home/isabelle/dist
17.79 -
17.80 -
17.81 -Final release stage
17.82 -===================
17.83 -
17.84 -- various .hg/hgrc files:
17.85 - default = http://bitbucket.org/isabelle_project/isabelle-release
17.86 - default = ssh://hg@bitbucket.org/isabelle_project/isabelle-release
17.87 -
17.88 -- isatest@macbroy28:hg-isabelle/.hg/hgrc
17.89 -- isatest@macbroy28:devel-page/content/index.content
17.90 -
17.91 -
17.92 -Post-release
17.93 -============
17.94 -
17.95 -- update /home/isabelle and /home/isabelle/html-data
17.96 -
18.1 --- a/Admin/Release/build Sat Apr 11 11:28:31 2015 +0200
18.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
18.3 @@ -1,157 +0,0 @@
18.4 -#!/usr/bin/env bash
18.5 -#
18.6 -# Author: Makarius
18.7 -#
18.8 -# build full Isabelle distribution from repository
18.9 -
18.10 -THIS="$(cd "$(dirname "$0")"; pwd)"
18.11 -PRG="$(basename "$0")"
18.12 -
18.13 -
18.14 -## diagnostics
18.15 -
18.16 -PRG="$(basename "$0")"
18.17 -
18.18 -function usage()
18.19 -{
18.20 - echo
18.21 - echo "Usage: isabelle $PRG [OPTIONS] DIR [VERSION]"
18.22 - echo
18.23 - echo " Options are:"
18.24 - echo " -O official release (not release-candidate)"
18.25 - echo " -j INT maximum number of parallel jobs (default 1)"
18.26 - echo " -l build library"
18.27 - echo " -r RELEASE proper release with name"
18.28 - echo
18.29 - echo " Make Isabelle distribution DIR, using the local repository clone."
18.30 - echo
18.31 - echo " VERSION identifies the snapshot, using usual Mercurial terminology;"
18.32 - echo " the default is RELEASE if given, otherwise \"tip\"."
18.33 - echo
18.34 - exit 1
18.35 -}
18.36 -
18.37 -function fail()
18.38 -{
18.39 - echo "$1" >&2
18.40 - exit 2
18.41 -}
18.42 -
18.43 -function check_number()
18.44 -{
18.45 - [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
18.46 -}
18.47 -
18.48 -
18.49 -## process command line
18.50 -
18.51 -# options
18.52 -
18.53 -OFFICIAL_RELEASE=""
18.54 -JOBS=""
18.55 -LIBRARY=""
18.56 -RELEASE=""
18.57 -
18.58 -while getopts "Oj:lr:" OPT
18.59 -do
18.60 - case "$OPT" in
18.61 - O)
18.62 - OFFICIAL_RELEASE="-O"
18.63 - ;;
18.64 - j)
18.65 - check_number "$OPTARG"
18.66 - JOBS="-j $OPTARG"
18.67 - ;;
18.68 - l)
18.69 - LIBRARY="true"
18.70 - ;;
18.71 - r)
18.72 - RELEASE="$OPTARG"
18.73 - ;;
18.74 - \?)
18.75 - usage
18.76 - ;;
18.77 - esac
18.78 -done
18.79 -
18.80 -shift $(($OPTIND - 1))
18.81 -
18.82 -
18.83 -# args
18.84 -
18.85 -BASE_DIR=""
18.86 -[ "$#" -gt 0 ] && { BASE_DIR="$1"; shift; }
18.87 -[ -z "$BASE_DIR" ] && usage
18.88 -
18.89 -VERSION=""
18.90 -[ "$#" -gt 0 ] && { VERSION="$1"; shift; }
18.91 -[ -z "$VERSION" ] && VERSION="$RELEASE"
18.92 -[ -z "$VERSION" ] && VERSION="tip"
18.93 -
18.94 -[ "$#" -gt 0 ] && usage
18.95 -
18.96 -
18.97 -## Isabelle settings
18.98 -
18.99 -ISABELLE_TOOL="$THIS/../../bin/isabelle"
18.100 -ISABELLE_PLATFORM_FAMILY="$("$ISABELLE_TOOL" getenv -b ISABELLE_PLATFORM_FAMILY)"
18.101 -
18.102 -
18.103 -## main
18.104 -
18.105 -# make dist
18.106 -
18.107 -if [ -z "$RELEASE" ]; then
18.108 - DISTNAME="Isabelle_$(env LC_ALL=C date "+%d-%b-%Y")"
18.109 - "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS $OFFICIAL_RELEASE
18.110 -else
18.111 - DISTNAME="$RELEASE"
18.112 - "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS $OFFICIAL_RELEASE -r "$RELEASE"
18.113 -fi
18.114 -[ "$?" = 0 ] || exit "$?"
18.115 -
18.116 -DISTBASE="$BASE_DIR/dist-${DISTNAME}"
18.117 -
18.118 -
18.119 -# make bundles
18.120 -
18.121 -for PLATFORM_FAMILY in linux macos windows
18.122 -do
18.123 -
18.124 -echo
18.125 -echo "*** $PLATFORM_FAMILY ***"
18.126 -
18.127 -"$ISABELLE_TOOL" makedist_bundle "$DISTBASE/${DISTNAME}.tar.gz" "$PLATFORM_FAMILY"
18.128 -[ "$?" = 0 ] || exit "$?"
18.129 -
18.130 -done
18.131 -
18.132 -
18.133 -# minimal index
18.134 -
18.135 -cat > "$DISTBASE/index.html" <<EOF
18.136 -<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 3.2//EN">
18.137 -<html>
18.138 -<head>
18.139 -<title>${DISTNAME}</title>
18.140 -</head>
18.141 -
18.142 -<body>
18.143 -<h1>${DISTNAME}</h1>
18.144 -<ul>
18.145 -<li><a href="${DISTNAME}_linux.tar.gz">Linux</a></li>
18.146 -<li><a href="${DISTNAME}.exe">Windows</a></li>
18.147 -<li><a href="${DISTNAME}.dmg">Mac OS X</a></li>
18.148 -</ul>
18.149 -</body>
18.150 -
18.151 -</html>
18.152 -EOF
18.153 -
18.154 -
18.155 -# HTML library
18.156 -
18.157 -if [ -n "$LIBRARY" ]; then
18.158 - "$THIS/build_library" $JOBS "$DISTBASE/${DISTNAME}_${ISABELLE_PLATFORM_FAMILY}.tar.gz"
18.159 -fi
18.160 -
19.1 --- a/Admin/Release/build_library Sat Apr 11 11:28:31 2015 +0200
19.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
19.3 @@ -1,99 +0,0 @@
19.4 -#!/usr/bin/env bash
19.5 -#
19.6 -# build Isabelle HTML library from platform bundle
19.7 -
19.8 -## diagnostics
19.9 -
19.10 -PRG=$(basename "$0")
19.11 -
19.12 -function usage()
19.13 -{
19.14 - echo
19.15 - echo "Usage: $PRG [OPTIONS] ARCHIVE"
19.16 - echo
19.17 - echo " Options are:"
19.18 - echo " -j INT maximum number of parallel jobs (default 1)"
19.19 - echo
19.20 - echo " Build Isabelle HTML library from platform bundle."
19.21 - echo
19.22 - exit 1
19.23 -}
19.24 -
19.25 -function fail()
19.26 -{
19.27 - echo "$1" >&2
19.28 - exit 2
19.29 -}
19.30 -
19.31 -
19.32 -## process command line
19.33 -
19.34 -# options
19.35 -
19.36 -JOBS=""
19.37 -
19.38 -while getopts "j:" OPT
19.39 -do
19.40 - case "$OPT" in
19.41 - j)
19.42 - JOBS="-j $OPTARG"
19.43 - ;;
19.44 - \?)
19.45 - usage
19.46 - ;;
19.47 - esac
19.48 -done
19.49 -
19.50 -shift $(($OPTIND - 1))
19.51 -
19.52 -
19.53 -# args
19.54 -
19.55 -[ "$#" -ne 1 ] && usage
19.56 -
19.57 -ARCHIVE="$1"; shift
19.58 -
19.59 -[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
19.60 -ARCHIVE_BASE="$(basename "$ARCHIVE")"
19.61 -ARCHIVE_DIR="$(cd "$(dirname "$ARCHIVE")"; echo "$PWD")"
19.62 -ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
19.63 -
19.64 -
19.65 -## main
19.66 -
19.67 -#GNU tar (notably on Mac OS X)
19.68 -if [ -x /usr/bin/gnutar ]; then
19.69 - function tar() { /usr/bin/gnutar "$@"; }
19.70 -fi
19.71 -
19.72 -TMP="/var/tmp/isabelle-makedist$$"
19.73 -mkdir "$TMP" || fail "Cannot create directory: \"$TMP\""
19.74 -
19.75 -cd "$TMP"
19.76 -tar -x -z -f "$ARCHIVE_FULL"
19.77 -
19.78 -cd *
19.79 -ISABELLE_NAME="$(basename "$PWD")"
19.80 -
19.81 -echo "Z3_NON_COMMERCIAL=yes" >> etc/settings
19.82 -echo "ISABELLE_FULL_TEST=true" >> etc/settings
19.83 -
19.84 -echo -n > src/Doc/ROOT
19.85 -
19.86 -env ISABELLE_IDENTIFIER="${ISABELLE_NAME}-build" \
19.87 - ./bin/isabelle build $JOBS -s -c -a -o browser_info \
19.88 - -o "document=pdf" -o "document_variants=document:outline=/proof,/ML"
19.89 -RC="$?"
19.90 -
19.91 -cd ..
19.92 -
19.93 -if [ "$RC" = 0 ]; then
19.94 - chmod -R g=o "$ISABELLE_NAME"
19.95 - tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"
19.96 -fi
19.97 -
19.98 -# clean up
19.99 -cd /tmp
19.100 -rm -rf "$TMP"
19.101 -
19.102 -exit "$RC"
20.1 --- a/Admin/Release/isasync Sat Apr 11 11:28:31 2015 +0200
20.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
20.3 @@ -1,129 +0,0 @@
20.4 -#!/usr/bin/env bash
20.5 -#
20.6 -# mirror script for Isabelle distribution or website
20.7 -
20.8 -
20.9 -## diagnostics
20.10 -
20.11 -PRG=`basename "$0"`
20.12 -
20.13 -usage()
20.14 -{
20.15 - echo
20.16 - echo "Usage: $PRG [OPTIONS] DEST"
20.17 - echo
20.18 - echo " Options are:"
20.19 - echo " -h print help message"
20.20 - echo " -n dry run, don't do anything, just report what would happen"
20.21 - echo " -w (ignored for backward compatibility)"
20.22 - echo " -d delete files that are not on the server (BEWARE!)"
20.23 - echo
20.24 - exit 1
20.25 -}
20.26 -
20.27 -fail()
20.28 -{
20.29 - echo "$1" >&2
20.30 - exit 2
20.31 -}
20.32 -
20.33 -
20.34 -## process command line
20.35 -
20.36 -# options
20.37 -
20.38 -HELP=""
20.39 -ARGS=""
20.40 -SRC="isabelle-website"
20.41 -
20.42 -while getopts "hnwd" OPT
20.43 -do
20.44 - case "$OPT" in
20.45 - h)
20.46 - HELP=true
20.47 - ;;
20.48 - n)
20.49 - ARGS="$ARGS -n"
20.50 - ;;
20.51 - w)
20.52 - echo "option -w ignored"
20.53 - ;;
20.54 - d)
20.55 - ARGS="$ARGS --delete"
20.56 - ;;
20.57 - \?)
20.58 - usage
20.59 - ;;
20.60 - esac
20.61 -done
20.62 -
20.63 -shift `expr $OPTIND - 1`
20.64 -
20.65 -
20.66 -# help
20.67 -
20.68 -if [ -n "$HELP" ]; then
20.69 - cat <<EOF
20.70 -
20.71 -Mirroring the Isabelle distribution or website
20.72 -==============================================
20.73 -
20.74 -The Munich site maintains an rsync server for the Isabelle
20.75 -distribution or website.
20.76 -
20.77 -The rsync tool is very smart and efficient in mirroring large
20.78 -directory hierarchies. See http://rsync.samba.org/ for more
20.79 -information. The $PRG script provides a simple front-end
20.80 -for easy access to the Isabelle distribution.
20.81 -
20.82 -The script can be either run in conservative or clean-sweep mode.
20.83 -
20.84 -1) Basic mirroring works like this:
20.85 -
20.86 - $PRG /foo/bar
20.87 -
20.88 -where /foo/bar refers to your local copy of the Isabelle distribution
20.89 -(the base directory has to exist already). This operation is
20.90 -conservative in the sense that files are never deleted, thus garbage
20.91 -may accumulate over time as our master copy is changed.
20.92 -
20.93 -Avoiding garbage in your local copy requires some care. Rsync
20.94 -provides a way to delete all additional local files that are absent in
20.95 -the master copy. This provides an efficient way to purge large
20.96 -directory hierarchies, even unwillingly in case that a wrong
20.97 -destination is given!
20.98 -
20.99 -2a) This will invoke a safe dry-run of clean-sweep mirroring:
20.100 -
20.101 - $PRG -dn /foo/bar
20.102 -
20.103 -where additions and deletions will be printed without any actual
20.104 -changes performed so far.
20.105 -
20.106 -2b) Exact mirroring with actual deletion of garbage may be performed
20.107 -like this:
20.108 -
20.109 - $PRG -d /foo/bar
20.110 -
20.111 -
20.112 -After gaining some confidence in the workings of $PRG one
20.113 -would usually set up some automatic mirror scheme, e.g. a daily cron
20.114 -job run by the 'nobody' user.
20.115 -
20.116 -Add -w to the option list in order to mirror the whole Isabelle website
20.117 -
20.118 -EOF
20.119 - exit 0
20.120 -fi
20.121 -
20.122 -
20.123 -# arguments
20.124 -
20.125 -[ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; }
20.126 -
20.127 -DEST="$1"; shift;
20.128 -
20.129 -
20.130 -## main
20.131 -
20.132 -exec rsync -va $ARGS "rsync://isabelle.in.tum.de/$SRC" "$DEST/"
21.1 --- a/Admin/Release/mirror-website Sat Apr 11 11:28:31 2015 +0200
21.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
21.3 @@ -1,21 +0,0 @@
21.4 -#!/usr/bin/env bash
21.5 -#
21.6 -# mirrors the Isabelle website
21.7 -
21.8 -HOST=$(hostname)
21.9 -
21.10 -case ${HOST} in
21.11 - sunbroy* | atbroy* | macbroy* | lxbroy*)
21.12 - DEST=/home/html/isabelle/html-data
21.13 - ;;
21.14 - *.cl.cam.ac.uk)
21.15 - USER=paulson
21.16 - DEST=/anfs/bigdisc/lp15/Isabelle
21.17 - ;;
21.18 - *)
21.19 - echo "Unknown destination directory for ${HOST}"
21.20 - exit 2
21.21 - ;;
21.22 -esac
21.23 -
21.24 -exec $(dirname $0)/isasync $DEST
22.1 --- a/Admin/Windows/Cygwin/Cygwin-Setup.bat Sat Apr 11 11:28:31 2015 +0200
22.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
22.3 @@ -1,4 +0,0 @@
22.4 -@echo off
22.5 -
22.6 -"%CD%\contrib\cygwin\isabelle\cygwin" --site http://isabelle.in.tum.de/cygwin_2014 --no-verify --only-site --local-package-dir "%TEMP%" --root "%CD%\contrib\cygwin"
22.7 -
23.1 --- a/Admin/Windows/Cygwin/Cygwin-Terminal.bat Sat Apr 11 11:28:31 2015 +0200
23.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
23.3 @@ -1,9 +0,0 @@
23.4 -@echo off
23.5 -
23.6 -set HOME=%HOMEDRIVE%%HOMEPATH%
23.7 -set PATH=%CD%\bin;%PATH%
23.8 -set CHERE_INVOKING=true
23.9 -
23.10 -echo This is the GNU Bash interpreter of Cygwin.
23.11 -echo Use command "isabelle" to invoke Isabelle tools.
23.12 -"%CD%\contrib\cygwin\bin\bash" --login -i
24.1 --- a/Admin/Windows/Cygwin/README Sat Apr 11 11:28:31 2015 +0200
24.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
24.3 @@ -1,15 +0,0 @@
24.4 -Cygwin
24.5 -======
24.6 -
24.7 -* http://www.cygwin.com/
24.8 -
24.9 -* Mirror with many old versions (not setup.ini)
24.10 - http://ftp.eq.uc.pt/software/pc/prog/cygwin
24.11 -
24.12 -* Local snapshots:
24.13 - http://isabelle.in.tum.de/cygwin (Isabelle2012)
24.14 - http://isabelle.in.tum.de/cygwin_2013 (Isabelle2013)
24.15 - http://isabelle.in.tum.de/cygwin_2013-1 (Isabelle2013-1 and Isabelle2013-2)
24.16 - http://isabelle.in.tum.de/cygwin_2014 (Isabelle2014)
24.17 -
24.18 -* Quasi-component: "isabelle makedist_cygwin" (as administrator)
25.1 --- a/Admin/Windows/Cygwin/isabelle/postinstall Sat Apr 11 11:28:31 2015 +0200
25.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
25.3 @@ -1,14 +0,0 @@
25.4 -#!/bin/bash
25.5 -
25.6 -export PATH=/bin
25.7 -
25.8 -bash /etc/postinstall/base-files-mketc.sh.done
25.9 -
25.10 -mkpasswd -l >/etc/passwd
25.11 -mkgroup -l >/etc/group
25.12 -
25.13 -find -type d -exec chmod 755 '{}' +
25.14 -find -type f \( -name '*.exe' -o -name '*.dll' \) -exec chmod 755 '{}' +
25.15 -find -type f -not -name '*.exe' -not -name '*.dll' -exec chmod 644 '{}' +
25.16 -xargs -0 < contrib/cygwin/isabelle/executables chmod 755
25.17 -
26.1 --- a/Admin/Windows/Cygwin/isabelle/rebaseall Sat Apr 11 11:28:31 2015 +0200
26.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
26.3 @@ -1,15 +0,0 @@
26.4 -#!/bin/dash
26.5 -
26.6 -export PATH=/bin
26.7 -
26.8 -FILE_LIST="$(mktemp)"
26.9 -
26.10 -for DIR in contrib/polyml*
26.11 -do
26.12 - find "$DIR" -name "*.dll" >> "$FILE_LIST"
26.13 -done
26.14 -
26.15 -dash /bin/rebaseall -T "$FILE_LIST"
26.16 -
26.17 -rm -f "$FILE_LIST"
26.18 -
27.1 --- a/Admin/Windows/Installer/README Sat Apr 11 11:28:31 2015 +0200
27.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
27.3 @@ -1,11 +0,0 @@
27.4 -Windows installer (based on 7zip)
27.5 -=================================
27.6 -
27.7 -* 7zip: http://www.7-zip.org/
27.8 -
27.9 -* 7zip self-extracting installer: http://www.7zsfx.info
27.10 -
27.11 -* final packaging:
27.12 -
27.13 - cat 7zsd_All.sfx sfx.txt Isabelle.7z > Isabelle.exe
27.14 -
28.1 --- a/Admin/Windows/Installer/sfx.txt Sat Apr 11 11:28:31 2015 +0200
28.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
28.3 @@ -1,9 +0,0 @@
28.4 -;!@Install@!UTF-8!
28.5 -GUIFlags="64"
28.6 -InstallPath="%UserDesktop%"
28.7 -BeginPrompt="Unpack {ISABELLE_NAME}?"
28.8 -ExtractPathText="Target directory"
28.9 -ExtractTitle="Unpacking {ISABELLE_NAME} ..."
28.10 -Shortcut="Du,{%%T\{ISABELLE_NAME}\{ISABELLE_NAME}.exe},{},{},{},{{ISABELLE_NAME}},{%%T\{ISABELLE_NAME}}"
28.11 -RunProgram="\"%%T\{ISABELLE_NAME}\{ISABELLE_NAME}.exe\""
28.12 -;!@InstallEnd@!
29.1 --- a/Admin/Windows/WinRun4J/Isabelle.ini Sat Apr 11 11:28:31 2015 +0200
29.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
29.3 @@ -1,4 +0,0 @@
29.4 -main.class=isabelle.Main
29.5 -vm.location=contrib\jdk\x86-cygwin\jre\bin\server\jvm.dll
29.6 -splash.image=lib\logo\isabelle.bmp
29.7 -vmarg.1=-Disabelle.home=%INI_DIR%
30.1 --- a/Admin/Windows/WinRun4J/README Sat Apr 11 11:28:31 2015 +0200
30.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
30.3 @@ -1,9 +0,0 @@
30.4 -Java application wrapper for Windows
30.5 -====================================
30.6 -
30.7 -* http://winrun4j.sourceforge.net/
30.8 -
30.9 -cp winrun4j/bin/WinRun4J.exe Isabelle.exe
30.10 -winrun4j/bin/RCEDIT /C Isabelle.exe
30.11 -winrun4j/bin/RCEDIT /I Isabelle.exe isabelle_transparent.ico
30.12 -
31.1 Binary file Admin/Windows/WinRun4J/isabelle.ico has changed
32.1 Binary file Admin/Windows/WinRun4J/isabelle_transparent.ico has changed
33.1 --- a/Admin/Windows/WinRun4J/manifest.xml Sat Apr 11 11:28:31 2015 +0200
33.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
33.3 @@ -1,9 +0,0 @@
33.4 -<?xml version="1.0" encoding="UTF-8" standalone="yes"?>
33.5 -<assembly xmlns="urn:schemas-microsoft-com:asm.v1" manifestVersion="1.0" xmlns:asmv3="urn:schemas-microsoft-com:asm.v3" >
33.6 - <asmv3:application>
33.7 - <asmv3:windowsSettings xmlns="http://schemas.microsoft.com/SMI/2005/WindowsSettings">
33.8 - <dpiAware>true</dpiAware>
33.9 - </asmv3:windowsSettings>
33.10 - </asmv3:application>
33.11 -</assembly>
33.12 -
34.1 --- a/Admin/build Sat Apr 11 11:28:31 2015 +0200
34.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
34.3 @@ -1,92 +0,0 @@
34.4 -#!/usr/bin/env bash
34.5 -#
34.6 -# Administrative build for Isabelle source distribution.
34.7 -
34.8 -## directory layout
34.9 -
34.10 -if [ -z "$ISABELLE_HOME" ]; then
34.11 - ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
34.12 - ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
34.13 -fi
34.14 -
34.15 -
34.16 -## diagnostics
34.17 -
34.18 -PRG="$(basename "$0")"
34.19 -
34.20 -function usage()
34.21 -{
34.22 - cat <<EOF
34.23 -
34.24 -Usage: $PRG [MODULES]
34.25 -
34.26 - Produce Isabelle distribution modules from current repository sources.
34.27 - The MODULES list may contain any of the following:
34.28 -
34.29 - all all modules below
34.30 - browser graph browser (requires jdk)
34.31 - jars Isabelle/Scala (requires \$ISABELLE_JDK_HOME and \$SCALA_HOME)
34.32 - jars_test test separate build of jars
34.33 - jars_fresh fresh build of jars
34.34 -
34.35 -EOF
34.36 - exit 1
34.37 -}
34.38 -
34.39 -function fail()
34.40 -{
34.41 - echo "$1" >&2
34.42 - exit 2
34.43 -}
34.44 -
34.45 -
34.46 -## process command line
34.47 -
34.48 -[ "$#" -eq 0 ] && usage
34.49 -
34.50 -MODULES="$@"; shift "$#"
34.51 -
34.52 -
34.53 -## modules
34.54 -
34.55 -function build_all ()
34.56 -{
34.57 - build_browser
34.58 - build_jars
34.59 -}
34.60 -
34.61 -
34.62 -function build_browser ()
34.63 -{
34.64 - pushd "$ISABELLE_HOME/lib/browser" >/dev/null
34.65 - "$ISABELLE_TOOL" env ./build || exit $?
34.66 - popd >/dev/null
34.67 -}
34.68 -
34.69 -
34.70 -function build_jars ()
34.71 -{
34.72 - pushd "$ISABELLE_HOME/src/Pure" >/dev/null
34.73 - "$ISABELLE_TOOL" env ./build-jars "$@" || exit $?
34.74 - popd >/dev/null
34.75 -}
34.76 -
34.77 -
34.78 -## main
34.79 -
34.80 -#FIXME workarounds for scalac 2.11.0
34.81 -export CYGWIN="nodosfilewarning"
34.82 -function stty() { :; }
34.83 -export -f stty
34.84 -
34.85 -for MODULE in $MODULES
34.86 -do
34.87 - case $MODULE in
34.88 - all) build_all;;
34.89 - browser) build_browser;;
34.90 - jars) build_jars;;
34.91 - jars_fresh) build_jars -f;;
34.92 - jars_test) build_jars -t;;
34.93 - *) fail "Bad module $MODULE"
34.94 - esac
34.95 -done
35.1 --- a/Admin/components/README Sat Apr 11 11:28:31 2015 +0200
35.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
35.3 @@ -1,62 +0,0 @@
35.4 -Some notes on maintaining the Isabelle component repository at TUM
35.5 -==================================================================
35.6 -
35.7 -Quick reference
35.8 ----------------
35.9 -
35.10 - $ install /home/isabelle/components/screwdriver-3.14.tar.gz
35.11 - $ install /home/isabelle/contrib/screwdriver-3.14/
35.12 - $ edit Admin/components/main: screwdriver-3.14
35.13 - $ isabelle components_checksum -u
35.14 - $ hg diff
35.15 - $ hg commit
35.16 -
35.17 -
35.18 -Unique names
35.19 -------------
35.20 -
35.21 -Component names are globally unique over time and space: names of
35.22 -published components are never re-used. If some component needs to be
35.23 -re-packaged, extra indices may be added to the official version number
35.24 -like this:
35.25 -
35.26 - screwdriver-3.14 #default packaging/publishing, no index
35.27 - screwdriver-3.14-1 #another refinement of the same
35.28 - screwdriver-3.14-2 #yet another refinement of the same
35.29 -
35.30 -There is no standard format for the structure of component names: they
35.31 -are compared for equality only, without any guess at an ordering.
35.32 -
35.33 -Components are registered in Admin/components/main (or similar) for
35.34 -use of that particular Isabelle repository version, subject to regular
35.35 -Mercurial history. This allows to bisect Isabelle versions with full
35.36 -record of the required components for testing.
35.37 -
35.38 -
35.39 -Authentic archives
35.40 -------------------
35.41 -
35.42 -Isabelle components are managed as authentic .tar.gz archives in
35.43 -/home/isabelle/components from where they are made publicly available
35.44 -on http://isabelle.in.tum.de/components/.
35.45 -
35.46 -Visibility on the HTTP server depends on local Unix file permission:
35.47 -nonfree components should omit "read" mode for the Unix group/other;
35.48 -regular components should be world-readable.
35.49 -
35.50 -The file Admin/components/components.sha1 contains SHA1 identifiers
35.51 -within the Isabelle repository, for integrity checking of the archives
35.52 -that are exposed to the public file-system. The components_checksum
35.53 -tool helps to update these hash-keys wrt. the information within the
35.54 -Isabelle repository.
35.55 -
35.56 -
35.57 -Unpacked copy
35.58 --------------
35.59 -
35.60 -A second unpacked copy is provided in /home/isabelle/contrib/. This
35.61 -allows users within the TUM network to activate arbitrary snapshots of
35.62 -the repository with all standard components being available, without
35.63 -extra copying or unpacking of the authentic archives. Testing
35.64 -services like "isatest" and "mira" do this routinely, and will break
35.65 -accordingly if this is omitted.
36.1 --- a/Admin/components/bundled Sat Apr 11 11:28:31 2015 +0200
36.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
36.3 @@ -1,2 +0,0 @@
36.4 -#additional components to be bundled for release
36.5 -
37.1 --- a/Admin/components/bundled-linux Sat Apr 11 11:28:31 2015 +0200
37.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
37.3 @@ -1,2 +0,0 @@
37.4 -#additional components to be bundled for release
37.5 -linux_app-20131007
38.1 --- a/Admin/components/bundled-macos Sat Apr 11 11:28:31 2015 +0200
38.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
38.3 @@ -1,2 +0,0 @@
38.4 -#additional components to be bundled for release
38.5 -macos_app-20130716
39.1 --- a/Admin/components/bundled-windows Sat Apr 11 11:28:31 2015 +0200
39.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
39.3 @@ -1,3 +0,0 @@
39.4 -#additional components to be bundled for release
39.5 -cygwin-20140813
39.6 -windows_app-20131201
40.1 --- a/Admin/components/components.sha1 Sat Apr 11 11:28:31 2015 +0200
40.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
40.3 @@ -1,111 +0,0 @@
40.4 -2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7 cvc3-2.4.1.tar.gz
40.5 -842d9526f37b928cf9e22f141884365129990d63 cygwin-20130110.tar.gz
40.6 -cb3b0706d208f104b800267697204f6d82f7b48a cygwin-20130114.tar.gz
40.7 -3b44cca04855016d5f8cfb5101b2e0579ab80197 cygwin-20130117.tar.gz
40.8 -1fde9ddf0fa4f398965113d0c0c4f0e97c78d008 cygwin-20130716.tar.gz
40.9 -a03735a53c2963eb0b453f6a7282d3419f28bf38 cygwin-20130916.tar.gz
40.10 -7470125fc46e24ee188bdaacc6d560e01b6fa839 cygwin-20140520.tar.gz
40.11 -db4dedae026981c5f001be283180abc1962b79ad cygwin-20140521.tar.gz
40.12 -acbc4bf161ad21e96ecfe506266ccdbd288f8a6f cygwin-20140530.tar.gz
40.13 -3dc680d9eb85276e8c3e9f6057dad0efe2d5aa41 cygwin-20140626.tar.gz
40.14 -8e562dfe57a2f894f9461f4addedb88afa108152 cygwin-20140725.tar.gz
40.15 -238d8e30e8e22495b7ea3f5ec36e852e97fe8bbf cygwin-20140813.tar.gz
40.16 -0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz
40.17 -2e293256a134eb8e5b1a283361b15eb812fbfbf1 e-1.6-1.tar.gz
40.18 -e1919e72416cbd7ac8de5455caba8901acc7b44d e-1.6-2.tar.gz
40.19 -b98a98025d1f7e560ca6864a53296137dae736b4 e-1.6.tar.gz
40.20 -c11b25c919e2ec44fe2b6ac2086337b456344e97 e-1.8.tar.gz
40.21 -6d34b18ca0aa1e10bab6413045d079188c0e2dfb exec_process-1.0.1.tar.gz
40.22 -8b9bffd10e396d965e815418295f2ee2849bea75 exec_process-1.0.2.tar.gz
40.23 -e6aada354da11e533af2dee3dcdd96c06479b053 exec_process-1.0.3.tar.gz
40.24 -ae7ee5becb26512f18c609e83b34612918bae5f0 exec_process-1.0.tar.gz
40.25 -59a71e08c34ff01f3f5c4af00db5e16369527eb7 Haskabelle-2013.tar.gz
40.26 -23a96ff4951d72f4024b6e8843262eda988bc151 Haskabelle-2014.tar.gz
40.27 -683acd94761ef460cca1a628f650355370de5afb hol-light-bundle-0.5-126.tar.gz
40.28 -8d83e433c1419e0c0cc5fd1762903d11b4a5752c jdk-6u31.tar.gz
40.29 -38d2d2a91c66714c18430e136e7e5191af3996e6 jdk-7u11.tar.gz
40.30 -d765bc4ad2f34d494429b2a8c1563c49db224944 jdk-7u13.tar.gz
40.31 -13a265e4b706ece26fdfa6fc9f4a3dd1366016d2 jdk-7u21.tar.gz
40.32 -5080274f8721a18111a7f614793afe6c88726739 jdk-7u25.tar.gz
40.33 -dd24d63afd6d17b29ec9cb2b2464d4ff2e02de2c jdk-7u40.tar.gz
40.34 -71b629b2ce83dbb69967c4785530afce1bec3809 jdk-7u60.tar.gz
40.35 -e119f4cbfa2a39a53b9578d165d0dc44b59527b7 jdk-7u65.tar.gz
40.36 -d6d1c42989433839fe64f34eb77298ef6627aed4 jdk-7u67.tar.gz
40.37 -ec740ee9ffd43551ddf1e5b91641405116af6291 jdk-7u6.tar.gz
40.38 -7d5b152ac70f720bb9e783fa45ecadcf95069584 jdk-7u9.tar.gz
40.39 -5442f1015a0657259be0590b04572cd933431df7 jdk-8u11.tar.gz
40.40 -c95ebf7777beb3e7ef10c0cf3f734cb78f9828e4 jdk-8u5.tar.gz
40.41 -44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
40.42 -a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
40.43 -4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
40.44 -9c221fe71af8a063fcffcce21672a97aea0a8d5b jedit_build-20120313.tar.gz
40.45 -ed72630f307729df08fdedb095f0af8725f81b9c jedit_build-20120327.tar.gz
40.46 -6425f622625024c1de27f3730d6811f6370a19cd jedit_build-20120414.tar.gz
40.47 -7b012f725ec1cc102dc259df178d511cc7890bba jedit_build-20120813.tar.gz
40.48 -8e1d36f5071e3def2cb281f7fefe9f52352cb88f jedit_build-20120903.tar.gz
40.49 -8fa0c67f59beba369ab836562eed4e56382f672a jedit_build-20121201.tar.gz
40.50 -06e9be2627ebb95c45a9bcfa025d2eeef086b408 jedit_build-20130104.tar.gz
40.51 -c85c0829b8170f25aa65ec6852f505ce2a50639b jedit_build-20130628.tar.gz
40.52 -5de3e399be2507f684b49dfd13da45228214bbe4 jedit_build-20130905.tar.gz
40.53 -87136818fd5528d97288f5b06bd30c787229eb0d jedit_build-20130910.tar.gz
40.54 -c63189cbe39eb8104235a0928f579d9523de78a9 jedit_build-20130925.tar.gz
40.55 -65cc13054be20d3a60474d406797c32a976d7db7 jedit_build-20130926.tar.gz
40.56 -30ca171f745adf12b65c798c660ac77f9c0f9b4b jedit_build-20131106.tar.gz
40.57 -054c1300128f8abd0f46a3e92c756ccdb96ff2af jedit_build-20140405.tar.gz
40.58 -4a963665537ea66c69de4d761846541ebdbf69f2 jedit_build-20140511.tar.gz
40.59 -a9d637a30f6a87a3583f265da51e63e3619cff52 jedit_build-20140722.tar.gz
40.60 -0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz
40.61 -8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
40.62 -c8a19a36adf6cefa779d85f22ded2f4654e68ea5 jortho-1.0-1.tar.gz
40.63 -2155e0bdbd29cd3d2905454de2e7203b9661d239 jortho-1.0-2.tar.gz
40.64 -ffe179867cf5ffaabbb6bb096db9bdc0d7110065 jortho-1.0.tar.gz
40.65 -6c737137cc597fc920943783382e928ea79e3feb kodkodi-1.2.16.tar.gz
40.66 -5f95c96bb99927f3a026050f85bd056f37a9189e kodkodi-1.5.2.tar.gz
40.67 -377e36efb8608e6c828c7718d890e97fde2006a4 linux_app-20131007.tar.gz
40.68 -0aab4f73ff7f5e36f33276547e10897e1e56fb1d macos_app-20130716.tar.gz
40.69 -1c8cb6a8f4cbeaedce2d6d1ba8fc7e2ab3663aeb polyml-5.4.1.tar.gz
40.70 -a3f9c159a0ee9a63b7a5d0c835ed9c2c908f8b56 polyml-5.5.0-1.tar.gz
40.71 -7d604a99355efbfc1459d80db3279ffa7ade3e39 polyml-5.5.0-2.tar.gz
40.72 -b3d776e6744f0cd2773d467bc2cfe1de3d1ca2fd polyml-5.5.0-3.tar.gz
40.73 -1812e9fa6d163f63edb93e37d1217640a166cf3e polyml-5.5.0.tar.gz
40.74 -36f5b8224f484721749682a3655c796a55a2718d polyml-5.5.1-1.tar.gz
40.75 -36f78f27291a9ceb13bf1120b62a45625afd44a6 polyml-5.5.1.tar.gz
40.76 -a588640dbf5da9ae15455b02ef709764a48637dc polyml-5.5.2-1.tar.gz
40.77 -532f6e8814752aeb406c62fabcfd2cc05f8a7ca8 polyml-5.5.2.tar.gz
40.78 -8ee375cfc38972f080dbc78f07b68dac03efe968 ProofGeneral-3.7.1.1.tar.gz
40.79 -847b52c0676b5eb0fbf0476f64fc08c2d72afd0c ProofGeneral-4.1.tar.gz
40.80 -8e0b2b432755ef11d964e20637d1bc567d1c0477 ProofGeneral-4.2-1.tar.gz
40.81 -51e1e0f399e934020565b2301358452c0bcc8a5e ProofGeneral-4.2-2.tar.gz
40.82 -8472221c876a430cde325841ce52893328302712 ProofGeneral-4.2.tar.gz
40.83 -0885e1f1d8feaca78d2f204b6487e6eec6dfab4b scala-2.10.0.tar.gz
40.84 -f7dc7a4e1aea46408fd6e44b8cfacb33af61afbc scala-2.10.1.tar.gz
40.85 -207e4916336335386589c918c5e3f3dcc14698f2 scala-2.10.2.tar.gz
40.86 -21c8ee274ffa471ab54d4196ecd827bf3d43e591 scala-2.10.3.tar.gz
40.87 -d4688ddaf83037ca43b5bf271325fc53ae70e3aa scala-2.10.4.tar.gz
40.88 -44d12297a78988ffd34363535e6a8e0d94c1d8b5 scala-2.11.0.tar.gz
40.89 -14f20de82b25215a5e055631fb147356400625e6 scala-2.11.1.tar.gz
40.90 -4fe9590d08e55760b86755d3fab750e90ac6c380 scala-2.11.2.tar.gz
40.91 -b447017e81600cc5e30dd61b5d4962f6da01aa80 scala-2.8.1.final.tar.gz
40.92 -5659440f6b86db29f0c9c0de7249b7e24a647126 scala-2.9.2.tar.gz
40.93 -43b5afbcad575ab6817d2289756ca22fd2ef43a9 spass-3.8ds.tar.gz
40.94 -1f4a2053cc1f34fa36c4d9d2ac906ad4ebc863fd sumatra_pdf-2.1.1.tar.gz
40.95 -601e08d048d8e50b0729429c8928b667d9b6bde9 sumatra_pdf-2.3.2.tar.gz
40.96 -14d46c2eb1a34821703da59d543433f581e91df3 sumatra_pdf-2.4.tar.gz
40.97 -44d67b6742919ce59a42368fc60e2afa210a3e42 sumatra_pdf-2.5.2.tar.gz
40.98 -869ea6d8ea35c8ba68d7fcb028f16b2b7064c5fd vampire-1.0.tar.gz
40.99 -81d21dfd0ea5c58f375301f5166be9dbf8921a7a windows_app-20130716.tar.gz
40.100 -fe15e1079cf5ad86f3cbab4553722a0d20002d11 windows_app-20130905.tar.gz
40.101 -e6a43b7b3b21295853bd2a63b27ea20bd6102f5f windows_app-20130906.tar.gz
40.102 -8fe004aead867d4c82425afac481142bd3f01fb0 windows_app-20130908.tar.gz
40.103 -d273abdc7387462f77a127fa43095eed78332b5c windows_app-20130909.tar.gz
40.104 -c368908584e2bca38b3bcb20431d0c69399fc2f0 windows_app-20131130.tar.gz
40.105 -c3f5285481a95fde3c1961595b4dd0311ee7ac1f windows_app-20131201.tar.gz
40.106 -1c36a840320dfa9bac8af25fc289a4df5ea3eccb xz-java-1.2-1.tar.gz
40.107 -2ae13aa17d0dc95ce254a52f1dba10929763a10d xz-java-1.2.tar.gz
40.108 -4530a1aa6f4498ee3d78d6000fa71a3f63bd077f yices-1.0.28.tar.gz
40.109 -3a8f77822278fe9250890e357248bc678d8fac95 z3-3.2-1.tar.gz
40.110 -12ae71acde43bd7bed1e005c43034b208c0cba4c z3-3.2.tar.gz
40.111 -d94a716502c8503d63952bcb4d4176fac8b28704 z3-4.0.tar.gz
40.112 -86e721296c400ada440e4a9ce11b9e845eec9e25 z3-4.3.0.tar.gz
40.113 -a8917c31b31c182edeec0aaa48870844960c8a61 z3-4.3.2pre-1.tar.gz
40.114 -06b30757ff23aefbc30479785c212685ffd39f4d z3-4.3.2pre.tar.gz
41.1 --- a/Admin/components/main Sat Apr 11 11:28:31 2015 +0200
41.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
41.3 @@ -1,16 +0,0 @@
41.4 -#main components for everyday use, without big impact on overall build time
41.5 -cvc3-2.4.1
41.6 -e-1.8
41.7 -exec_process-1.0.3
41.8 -Haskabelle-2014
41.9 -jdk-7u67
41.10 -jedit_build-20140722
41.11 -jfreechart-1.0.14-1
41.12 -jortho-1.0-2
41.13 -kodkodi-1.5.2
41.14 -polyml-5.5.2-1
41.15 -scala-2.11.2
41.16 -spass-3.8ds
41.17 -z3-3.2-1
41.18 -z3-4.3.2pre-1
41.19 -xz-java-1.2-1
42.1 --- a/Admin/components/nonfree Sat Apr 11 11:28:31 2015 +0200
42.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
42.3 @@ -1,3 +0,0 @@
42.4 -#special components for internal testing only
42.5 -vampire-1.0
42.6 -yices-1.0.28
43.1 --- a/Admin/components/optional Sat Apr 11 11:28:31 2015 +0200
43.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
43.3 @@ -1,3 +0,0 @@
43.4 -#optional components that could impact build time significantly
43.5 -hol-light-bundle-0.5-126
43.6 -ProofGeneral-4.2-2
44.1 --- a/Admin/components/windows Sat Apr 11 11:28:31 2015 +0200
44.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
44.3 @@ -1,2 +0,0 @@
44.4 -#components for "windows" platform family
44.5 -sumatra_pdf-2.5.2
45.1 --- a/Admin/etc/settings Sat Apr 11 11:28:31 2015 +0200
45.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
45.3 @@ -1,3 +0,0 @@
45.4 -# -*- shell-script -*- :mode=shellscript:
45.5 -
45.6 -ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
46.1 --- a/Admin/exec_process/build Sat Apr 11 11:28:31 2015 +0200
46.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
46.3 @@ -1,53 +0,0 @@
46.4 -#!/usr/bin/env bash
46.5 -#
46.6 -# Multi-platform build script
46.7 -
46.8 -THIS="$(cd "$(dirname "$0")"; pwd)"
46.9 -PRG="$(basename "$0")"
46.10 -
46.11 -
46.12 -# diagnostics
46.13 -
46.14 -function usage()
46.15 -{
46.16 - echo
46.17 - echo "Usage: $PRG TARGET"
46.18 - echo
46.19 - exit 1
46.20 -}
46.21 -
46.22 -function fail()
46.23 -{
46.24 - echo "$1" >&2
46.25 - exit 2
46.26 -}
46.27 -
46.28 -
46.29 -# command line args
46.30 -
46.31 -[ "$#" -eq 0 ] && usage
46.32 -TARGET="$1"; shift
46.33 -
46.34 -[ "$#" -eq 0 ] || usage
46.35 -
46.36 -
46.37 -# main
46.38 -
46.39 -mkdir -p "$TARGET"
46.40 -
46.41 -case "$TARGET" in
46.42 - x86_64-linux | x86_64-darwin)
46.43 - cc -m64 exec_process.c -o "$TARGET/exec_process"
46.44 - ;;
46.45 - x86-linux | x86-darwin)
46.46 - cc -m32 exec_process.c -o "$TARGET/exec_process"
46.47 - ;;
46.48 - x86-cygwin)
46.49 - cc exec_process.c -o "$TARGET/exec_process.exe"
46.50 - ;;
46.51 - *)
46.52 - cc exec_process.c -o "$TARGET/exec_process"
46.53 - ;;
46.54 -esac
46.55 -
46.56 -
47.1 --- a/Admin/exec_process/etc/settings Sat Apr 11 11:28:31 2015 +0200
47.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
47.3 @@ -1,3 +0,0 @@
47.4 -# -*- shell-script -*- :mode=shellscript:
47.5 -
47.6 -EXEC_PROCESS="$COMPONENT/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/exec_process"
48.1 --- a/Admin/exec_process/exec_process.c Sat Apr 11 11:28:31 2015 +0200
48.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
48.3 @@ -1,61 +0,0 @@
48.4 -/* Author: Makarius
48.5 -
48.6 -Bash process group invocation.
48.7 -*/
48.8 -
48.9 -#include <stdlib.h>
48.10 -#include <stdio.h>
48.11 -#include <sys/types.h>
48.12 -#include <unistd.h>
48.13 -
48.14 -
48.15 -static void fail(const char *msg)
48.16 -{
48.17 - fprintf(stderr, "%s\n", msg);
48.18 - exit(2);
48.19 -}
48.20 -
48.21 -
48.22 -int main(int argc, char *argv[])
48.23 -{
48.24 - /* args */
48.25 -
48.26 - if (argc != 3) {
48.27 - fprintf(stderr, "Bad arguments\n");
48.28 - exit(1);
48.29 - }
48.30 - char *pid_name = argv[1];
48.31 - char *script = argv[2];
48.32 -
48.33 -
48.34 - /* setsid */
48.35 -
48.36 - if (setsid() == -1) {
48.37 - pid_t pid = fork();
48.38 - if (pid == -1) fail("Cannot set session id (failed to fork)");
48.39 - else if (pid != 0) exit(0);
48.40 - else if (setsid() == -1) fail("Cannot set session id (after fork)");
48.41 - }
48.42 -
48.43 -
48.44 - /* report pid */
48.45 -
48.46 - FILE *pid_file;
48.47 - pid_file = fopen(pid_name, "w");
48.48 - if (pid_file == NULL) fail("Cannot open pid file");
48.49 - fprintf(pid_file, "%d", getpid());
48.50 - fclose(pid_file);
48.51 -
48.52 -
48.53 - /* exec */
48.54 -
48.55 - char *cmd_line[4];
48.56 - cmd_line[0] = "bash";
48.57 - cmd_line[1] = "-c";
48.58 - cmd_line[2] = script;
48.59 - cmd_line[3] = NULL;
48.60 -
48.61 - execvp(cmd_line[0], cmd_line);
48.62 - fail("Cannot exec process");
48.63 -}
48.64 -
49.1 --- a/Admin/isatest/crontab.lxbroy2 Sat Apr 11 11:28:31 2015 +0200
49.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
49.3 @@ -1,7 +0,0 @@
49.4 -03 00 * * * $HOME/bin/checkout-admin
49.5 -17 00 * * * $HOME/bin/isatest-makedist
49.6 -01 08 * * * $HOME/bin/isatest-check
49.7 -
49.8 -04 23 31 1,3,5,7,8,10,12 * $HOME/bin/logmove
49.9 -04 23 30 4,6,9,11 * $HOME/bin/logmove
49.10 -04 23 28 2 * $HOME/bin/logmove
50.1 --- a/Admin/isatest/crontab.macbroy2 Sat Apr 11 11:28:31 2015 +0200
50.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
50.3 @@ -1,7 +0,0 @@
50.4 -MAILTO=isatest@mailbroy.informatik.tu-muenchen.de
50.5 -
50.6 -28 06 * * 0-5 $HOME/afp/devel/admin/regression -
50.7 -28 06 * * 6 export ISABELLE_FULL_TEST=true && $HOME/afp/devel/admin/regression -
50.8 -# 17 11 * * 6 $HOME/afp/devel/admin/regression -f -
50.9 -# 32 11 * * 0 $HOME/afp/release/admin/regression Isabelle2011-1
50.10 -
51.1 --- a/Admin/isatest/isatest-makeall Sat Apr 11 11:28:31 2015 +0200
51.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
51.3 @@ -1,158 +0,0 @@
51.4 -#!/usr/bin/env bash
51.5 -#
51.6 -# Author: Gerwin Klein, TU Muenchen
51.7 -#
51.8 -# DESCRIPTION: Run isabelle build from specified distribution and settings.
51.9 -
51.10 -## global settings
51.11 -. ~/admin/isatest/isatest-settings
51.12 -
51.13 -# max time until test is aborted (in sec)
51.14 -MAXTIME=28800
51.15 -
51.16 -
51.17 -## diagnostics
51.18 -
51.19 -PRG="$(basename "$0")"
51.20 -
51.21 -function usage()
51.22 -{
51.23 - echo
51.24 - echo "Usage: $PRG [-l targets] settings1 [settings2 ...]"
51.25 - echo
51.26 - echo " Runs isabelle build for specified settings."
51.27 - echo " Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
51.28 - echo
51.29 - echo "Examples:"
51.30 - echo " $PRG ~/settings/at-poly ~/settings/at-sml"
51.31 - echo " $PRG -l \"HOL-Library HOL-Bali\" ~/settings/at-poly"
51.32 - exit 1
51.33 -}
51.34 -
51.35 -function fail()
51.36 -{
51.37 - echo "$1" >&2
51.38 - log "FAILED, $1"
51.39 - exit 2
51.40 -}
51.41 -
51.42 -
51.43 -## main
51.44 -
51.45 -# argument checking
51.46 -
51.47 -[ "$1" = "-?" ] && usage
51.48 -[ "$#" -lt "1" ] && usage
51.49 -
51.50 -[ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
51.51 -
51.52 -# build args and nice setup for different target platforms
51.53 -BUILD_ARGS="-v"
51.54 -NICE="nice"
51.55 -case $HOSTNAME in
51.56 - macbroy2 | macbroy6 | macbroy30)
51.57 - NICE=""
51.58 - ;;
51.59 - lxbroy[234])
51.60 - BUILD_ARGS="$BUILD_ARGS -j 2"
51.61 - NICE=""
51.62 - ;;
51.63 -
51.64 -esac
51.65 -
51.66 -ISABELLE_TOOL="$DISTPREFIX/Isabelle/bin/isabelle"
51.67 -[ -x $ISABELLE_TOOL ] || fail "Cannot run $ISABELLE_TOOL"
51.68 -
51.69 -ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)"
51.70 -
51.71 -if [ "$1" = "-l" ]; then
51.72 - shift
51.73 - [ "$#" -lt 2 ] && usage
51.74 - BUILD_ARGS="$BUILD_ARGS $1"
51.75 - shift
51.76 -else
51.77 - BUILD_ARGS="$BUILD_ARGS -a"
51.78 -fi
51.79 -
51.80 -IDENT=$(cat "$DISTPREFIX/ISABELLE_IDENT")
51.81 -
51.82 -
51.83 -# main test loop
51.84 -
51.85 -log "starting [$@]"
51.86 -
51.87 -for SETTINGS in $@; do
51.88 -
51.89 - [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
51.90 -
51.91 - case "$SETTINGS" in
51.92 - *sml*)
51.93 - BUILD_ARGS="-o timeout=36000 $BUILD_ARGS"
51.94 - ;;
51.95 - *)
51.96 - BUILD_ARGS="-o timeout=3600 $BUILD_ARGS"
51.97 - ;;
51.98 - esac
51.99 -
51.100 - # logfile setup
51.101 -
51.102 - DATE=$(date "+%Y-%m-%d")
51.103 - SHORT=${SETTINGS##*/}
51.104 -
51.105 - if [ "${SHORT%-e}" == "$SHORT" ]; then
51.106 - # normal test
51.107 - TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
51.108 - else
51.109 - # experimental test
51.110 - TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME-e.log
51.111 - fi
51.112 -
51.113 - # the test
51.114 -
51.115 - touch $RUNNING/$SHORT.running
51.116 -
51.117 - echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
51.118 -
51.119 - echo "Isabelle version: $IDENT" >> $TESTLOG 2>&1
51.120 -
51.121 - if [ "${ISABELLE_HOME_USER:0:14}" == "/tmp/isabelle-" ]; then
51.122 - echo "--- cleaning up old $ISABELLE_HOME_USER"
51.123 - rm -rf $ISABELLE_HOME_USER
51.124 - fi
51.125 -
51.126 - cp $DISTPREFIX/Isabelle/etc/settings.orig $DISTPREFIX/Isabelle/etc/settings
51.127 - cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
51.128 - (ulimit -t $MAXTIME; $NICE "$ISABELLE_TOOL" build $BUILD_ARGS >> $TESTLOG 2>&1)
51.129 -
51.130 - if [ $? -eq 0 ]
51.131 - then
51.132 - # test log and cleanup
51.133 - echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
51.134 - gzip -f $TESTLOG
51.135 - else
51.136 - # test log
51.137 - echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
51.138 -
51.139 - # error log
51.140 - echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG
51.141 - echo "[...]" >> $ERRORLOG
51.142 - tail -4 $TESTLOG >> $ERRORLOG
51.143 - echo >> $ERRORLOG
51.144 -
51.145 - FAIL="$FAIL$SHORT "
51.146 - (cd $ERRORDIR; cp $TESTLOG .)
51.147 - fi
51.148 -
51.149 - rm -f $RUNNING/$SHORT.running
51.150 -done
51.151 -
51.152 -# time and success/failure to master log
51.153 -ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
51.154 -
51.155 -if [ -z "$FAIL" ]; then
51.156 - log "all tests successful, elapsed time $ELAPSED."
51.157 -else
51.158 - log "targets ${FAIL}FAILED, elapsed time $ELAPSED."
51.159 - exit 1
51.160 -fi
51.161 -
52.1 --- a/Admin/isatest/isatest-makedist Sat Apr 11 11:28:31 2015 +0200
52.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
52.3 @@ -1,128 +0,0 @@
52.4 -#!/usr/bin/env bash
52.5 -#
52.6 -# Author: Gerwin Klein, TU Muenchen
52.7 -#
52.8 -# DESCRIPTION: Build distribution and run isatest-make for lots of platforms.
52.9 -
52.10 -## global settings
52.11 -. "$HOME/hg-isabelle/Admin/isatest/isatest-settings"
52.12 -
52.13 -TMP=/tmp/isatest-makedist.$$
52.14 -MAIL=$HOME/bin/pmail
52.15 -
52.16 -MAKEALL=$HOME/bin/isatest-makeall
52.17 -TAR=tar
52.18 -
52.19 -SSH="ssh -f"
52.20 -
52.21 -export THIS_IS_ISATEST_MAKEDIST=true
52.22 -
52.23 -
52.24 -## diagnostics
52.25 -
52.26 -PRG="$(basename "$0")"
52.27 -
52.28 -function usage()
52.29 -{
52.30 - echo
52.31 - echo "Usage: $PRG"
52.32 - echo
52.33 - echo " Build distribution and run isatest-make for lots of platforms."
52.34 - echo
52.35 - exit 1
52.36 -}
52.37 -
52.38 -function fail()
52.39 -{
52.40 - echo "$1" >&2
52.41 - exit 2
52.42 -}
52.43 -
52.44 -
52.45 -## main
52.46 -
52.47 -# cleanup old error log and test-still-running files
52.48 -rm -f $ERRORLOG
52.49 -rm -f $ERRORDIR/isatest-*.log
52.50 -rm -f $RUNNING/*.runnning
52.51 -
52.52 -export DISTPREFIX
52.53 -
52.54 -DATE=$(date "+%Y-%m-%d")
52.55 -DISTLOG=$LOGPREFIX/isatest-makedist-$DATE.log
52.56 -
52.57 -echo ------------------- preparing test release --- `date` --- $HOSTNAME > $DISTLOG 2>&1
52.58 -
52.59 -echo "### cleaning up old dist directory" >> $DISTLOG 2>&1
52.60 -rm -rf $DISTPREFIX >> $DISTLOG 2>&1
52.61 -
52.62 -echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1
52.63 -rm -rf $HOME/isabelle-*
52.64 -
52.65 -echo "### building distribution" >> $DISTLOG 2>&1
52.66 -mkdir -p $DISTPREFIX
52.67 -"$HOME/hg-isabelle/bin/isabelle" makedist >> $DISTLOG 2>&1
52.68 -
52.69 -if [ $? -ne 0 ]
52.70 -then
52.71 - echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
52.72 - ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
52.73 - log "dist build FAILED, elapsed time $ELAPSED."
52.74 -
52.75 - echo "Could not build isabelle distribution. Log file available at" > $TMP
52.76 - echo "$HOSTNAME:$DISTLOG" >> $TMP
52.77 -
52.78 - for R in $MAILTO; do
52.79 - $MAIL "isabelle dist build failed" $R $TMP
52.80 - done
52.81 -
52.82 - rm $TMP
52.83 -
52.84 - exit 1
52.85 -fi
52.86 -
52.87 -cd $DISTPREFIX >> $DISTLOG 2>&1
52.88 -ISABELLE_DIST=`cat $DISTPREFIX/ISABELLE_DIST`
52.89 -$TAR xvzf $ISABELLE_DIST >> $DISTLOG 2>&1
52.90 -ln -sf $(basename $ISABELLE_DIST .tar.gz) Isabelle
52.91 -cp Isabelle/etc/settings Isabelle/etc/settings.orig
52.92 -
52.93 -echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
52.94 -
52.95 -ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
52.96 -log "dist build successful, elapsed time $ELAPSED."
52.97 -
52.98 -
52.99 -## clean up var/running
52.100 -rm -f $RUNNING/*
52.101 -mkdir -p $RUNNING
52.102 -
52.103 -
52.104 -## spawn test runs
52.105 -
52.106 -$SSH lxbroy10 "$MAKEALL $HOME/settings/at64-poly"
52.107 -sleep 15
52.108 -$SSH lxbroy4 "
52.109 - $MAKEALL $HOME/settings/at-poly;
52.110 - $MAKEALL $HOME/settings/at-poly-test"
52.111 -sleep 15
52.112 -$SSH lxbroy3 "$MAKEALL -l HOL-Library $HOME/settings/at-sml-dev-e"
52.113 -sleep 15
52.114 -$SSH macbroy23 "$MAKEALL $HOME/settings/at-poly-e"
52.115 -sleep 15
52.116 -$SSH macbroy2 "
52.117 - $MAKEALL $HOME/settings/mac-poly64-M4;
52.118 - $MAKEALL $HOME/settings/mac-poly64-M8;
52.119 - $MAKEALL $HOME/settings/mac-poly-M4;
52.120 - $MAKEALL $HOME/settings/mac-poly-M8;
52.121 - $MAKEALL $HOME/settings/mac-poly-M8-skip_proofs;
52.122 - $MAKEALL $HOME/settings/mac-poly-M8-quick_and_dirty"
52.123 -sleep 15
52.124 -$SSH macbroy6 "$MAKEALL $HOME/settings/mac-poly64-M2"
52.125 -sleep 15
52.126 -$SSH macbroy30 "$MAKEALL $HOME/settings/mac-poly-M2"
52.127 -
52.128 -echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
52.129 -
52.130 -gzip -f $DISTLOG
52.131 -
53.1 --- a/Admin/isatest/isatest-settings Sat Apr 11 11:28:31 2015 +0200
53.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
53.3 @@ -1,51 +0,0 @@
53.4 -# -*- shell-script -*- :mode=shellscript:
53.5 -#
53.6 -# Author: Gerwin Klein, NICTA
53.7 -#
53.8 -# DESCRIPTION: common settings for the isatest-* scripts
53.9 -
53.10 -# source bashrc, we're called by cron
53.11 -. ~/.bashrc
53.12 -
53.13 -# canoncical home for all platforms
53.14 -HOME=/home/isatest
53.15 -
53.16 -## send email on failure to
53.17 -MAILTO="\
53.18 -kleing@cse.unsw.edu.au \
53.19 -nipkow@in.tum.de \
53.20 -berghofe@in.tum.de \
53.21 -lp15@cam.ac.uk \
53.22 -makarius@sketis.net \
53.23 -blanchet@in.tum.de \
53.24 -boehmes@in.tum.de \
53.25 -bulwahn@in.tum.de \
53.26 -hoelzl@in.tum.de \
53.27 -krauss@in.tum.de \
53.28 -noschinl@in.tum.de \
53.29 -kuncar@in.tum.de \
53.30 -ns441@cam.ac.uk"
53.31 -
53.32 -LOGPREFIX=$HOME/log
53.33 -MASTERLOG=$LOGPREFIX/isatest.log
53.34 -LOGSERVER=lxbroy2.informatik.tu-muenchen.de
53.35 -
53.36 -ERRORDIR=$HOME/var
53.37 -ERRORLOG=$ERRORDIR/error.log
53.38 -
53.39 -RUNNING=$HOME/var/running
53.40 -
53.41 -DISTPREFIX=$HOME/isadist
53.42 -
53.43 -HOSTNAME="$(hostname -s)"
53.44 -
53.45 -# this function avoids NFS inconsistencies with multiple writers by
53.46 -# sshing to one central machine and writing locally. There is stil a
53.47 -# race condition, but at least it should not corrupt a whole set of entries
53.48 -# any more.
53.49 -function log()
53.50 -{
53.51 - MSG="$1"
53.52 - TIMESTAMP="$(date)"
53.53 - echo "[$TIMESTAMP $HOSTNAME $PRG]: $MSG" | ssh $LOGSERVER "cat >> $MASTERLOG"
53.54 -}
54.1 --- a/Admin/isatest/isatest-statistics Sat Apr 11 11:28:31 2015 +0200
54.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
54.3 @@ -1,112 +0,0 @@
54.4 -#!/usr/bin/env bash
54.5 -#
54.6 -# Author: Makarius
54.7 -#
54.8 -# DESCRIPTION: Produce statistics from isatest session logs.
54.9 -
54.10 -## platform settings
54.11 -
54.12 -case $(uname) in
54.13 - SunOS)
54.14 - ZGREP=xgrep
54.15 - TE="png color"
54.16 - ;;
54.17 - *)
54.18 - ZGREP=zgrep
54.19 - TE="png"
54.20 - ;;
54.21 -esac
54.22 -
54.23 -
54.24 -## diagnostics
54.25 -
54.26 -PRG="$(basename "$0")"
54.27 -
54.28 -function usage()
54.29 -{
54.30 - echo
54.31 - echo "Usage: $PRG DIR PLATFORM TIMESPAN SESSIONS..."
54.32 - echo
54.33 - echo " Produce statistics from isatest session logs, looking TIMESPAN"
54.34 - echo " days into the past. Outputs .png files into DIR."
54.35 - echo
54.36 - exit 1
54.37 -}
54.38 -
54.39 -function fail()
54.40 -{
54.41 - echo "$1" >&2
54.42 - exit 2
54.43 -}
54.44 -
54.45 -
54.46 -## arguments
54.47 -
54.48 -[ "$1" = "-?" ] && usage
54.49 -[ "$#" -lt "4" ] && usage
54.50 -
54.51 -DIR="$1"; shift
54.52 -PLATFORM="$1"; shift
54.53 -TIMESPAN="$1"; shift
54.54 -SESSIONS="$@"
54.55 -
54.56 -case "$PLATFORM" in
54.57 - *para* | *-M* | afp)
54.58 - PARALLEL=true
54.59 - ;;
54.60 - *)
54.61 - PARALLEL=false
54.62 - ;;
54.63 -esac
54.64 -
54.65 -if [ "$PLATFORM" = afp ]; then
54.66 - LOG_DIR=~isatest/afp/log
54.67 - LOG_NAME="afp-test-devel*"
54.68 -else
54.69 - LOG_DIR=~isatest/log
54.70 - LOG_NAME="isatest-makeall-${PLATFORM}*"
54.71 -fi
54.72 -
54.73 -
54.74 -## main
54.75 -
54.76 -ALL_DATA="/tmp/isatest-all$$.dat"
54.77 -SESSION_DATA="/tmp/isatest$$.dat"
54.78 -mkdir -p "$DIR" || fail "Bad directory: $DIR"
54.79 -
54.80 -$ZGREP "^Finished .*elapsed" \
54.81 - $(find "$LOG_DIR" -name "$LOG_NAME" -mtime "-${TIMESPAN}") | \
54.82 -perl -e '
54.83 - while (<>) {
54.84 - if (m/(\d\d\d\d)-(\d\d)-(\d\d).*:Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time/) {
54.85 - my $year = $1;
54.86 - my $month = $2;
54.87 - my $day = $3;
54.88 - my $name = $4;
54.89 - my $elapsed_time = ($5 * 3600 + $6 * 60 + $7) / 60;
54.90 - my $cpu_time = ($8 * 3600 + $9 * 60 + $10) / 60;
54.91 -
54.92 - printf "$name $year-$month-$day %.2f %.2f\n", $cpu_time, $elapsed_time;
54.93 - }
54.94 - }' > "$ALL_DATA"
54.95 -
54.96 -for SESSION in $SESSIONS
54.97 -do
54.98 - grep "^${SESSION} " "$ALL_DATA" > "$SESSION_DATA"
54.99 - PLOT="plot [] [0:] \"$SESSION_DATA\" using 2:3 smooth sbezier title \"interpolated cpu time\", \"$SESSION_DATA\" using 2:3 smooth csplines title \"cpu time\""
54.100 - if [ "$PARALLEL" = true ]; then
54.101 - PLOT="${PLOT}, \"$SESSION_DATA\" using 2:4 smooth sbezier title \"interpolated elapsed time\", \"$SESSION_DATA\" using 2:4 smooth csplines title \"elapsed time\""
54.102 - fi
54.103 - gnuplot <<EOF
54.104 -set terminal $TE
54.105 -set output "$DIR/${SESSION}.png"
54.106 -set xdata time
54.107 -set timefmt "%Y-%m-%d"
54.108 -set format x "%d-%b"
54.109 -set xlabel "$SESSION"
54.110 -set key left top
54.111 -$PLOT
54.112 -EOF
54.113 -done
54.114 -
54.115 -rm -f "$ALL_DATA" "$SESSION_DATA"
55.1 --- a/Admin/isatest/isatest-stats Sat Apr 11 11:28:31 2015 +0200
55.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
55.3 @@ -1,269 +0,0 @@
55.4 -#!/usr/bin/env bash
55.5 -#
55.6 -# Author: Makarius
55.7 -#
55.8 -# DESCRIPTION: Standard statistics.
55.9 -
55.10 -THIS="$(cd "$(dirname "$0")"; pwd)"
55.11 -
55.12 -PLATFORMS="at-poly at-poly-test afp at64-poly mac-poly-M2 mac-poly-M4 mac-poly64-M2 mac-poly64-M4 mac-poly-M8 mac-poly-M8-skip_proofs mac-poly64-M8 at-sml-dev"
55.13 -
55.14 -ISABELLE_SESSIONS="
55.15 - HOL
55.16 - HOL-Algebra
55.17 - HOL-Auth
55.18 - HOL-BNF
55.19 - HOL-BNF-Examples
55.20 - HOL-BNF-LFP
55.21 - HOL-BNF-Nitpick_Examples
55.22 - HOL-Bali
55.23 - HOL-Cardinals
55.24 - HOL-Cardinals-Base
55.25 - HOL-Codegenerator_Test
55.26 - HOL-Datatype_Benchmark
55.27 - HOL-Decision_Procs
55.28 - HOL-Hahn_Banach
55.29 - HOL-Hoare
55.30 - HOL-Hoare_Parallel
55.31 - HOL-IMP
55.32 - HOL-IMPP
55.33 - HOL-IOA
55.34 - HOL-Imperative_HOL
55.35 - HOL-Import
55.36 - HOL-Induct
55.37 - HOL-Isar_Examples
55.38 - HOL-Lattice
55.39 - HOL-Library
55.40 - HOL-Matrix_LP
55.41 - HOL-Metis_Examples
55.42 - HOL-MicroJava
55.43 - HOL-Mirabelle
55.44 - HOL-Mirabelle-ex
55.45 - HOL-Multivariate_Analysis
55.46 - HOL-Mutabelle
55.47 - HOL-NSA
55.48 - HOL-NSA-Examples
55.49 - HOL-NanoJava
55.50 - HOL-Nominal
55.51 - HOL-Nominal-Examples
55.52 - HOL-Number_Theory
55.53 - HOL-Old_Number_Theory
55.54 - HOL-Predicate_Compile_Examples
55.55 - HOL-Probability
55.56 - HOL-Prolog
55.57 - HOL-Proofs
55.58 - HOL-Proofs-Extraction
55.59 - HOL-Proofs-Lambda
55.60 - HOL-Proofs-ex
55.61 - HOL-Quickcheck_Benchmark
55.62 - HOL-Quickcheck_Examples
55.63 - HOL-Quotient_Examples
55.64 - HOL-Record_Benchmark
55.65 - HOL-SET_Protocol
55.66 - HOL-SPARK
55.67 - HOL-SPARK-Examples
55.68 - HOL-SPARK-Manual
55.69 - HOL-Statespace
55.70 - HOL-TLA
55.71 - HOL-TLA-Buffer
55.72 - HOL-TLA-Inc
55.73 - HOL-TLA-Memory
55.74 - HOL-TPTP
55.75 - HOL-UNITY
55.76 - HOL-Unix
55.77 - HOL-Word
55.78 - HOL-Word-Examples
55.79 - HOL-Word-SMT_Examples
55.80 - HOL-ZF
55.81 - HOL-ex
55.82 - HOLCF
55.83 - HOLCF-FOCUS
55.84 - HOLCF-IMP
55.85 - HOLCF-Library
55.86 - HOLCF-Tutorial
55.87 - HOLCF-ex
55.88 - IOA
55.89 - IOA-ABP
55.90 - IOA-NTP
55.91 - IOA-Storage
55.92 - IOA-ex
55.93 - Pure
55.94 - Spec_Check
55.95 - ZF
55.96 - ZF-AC
55.97 - ZF-Coind
55.98 - ZF-Constructible
55.99 - ZF-IMP
55.100 - ZF-Induct
55.101 - ZF-Resid
55.102 - ZF-UNITY
55.103 - ZF-ex
55.104 -"
55.105 -
55.106 -AFP_SESSIONS="
55.107 - AVL-Trees
55.108 - Abortable_Linearizable_Modules
55.109 - Abstract-Hoare-Logics
55.110 - Abstract-Rewriting
55.111 - ArrowImpossibilityGS
55.112 - AutoFocus-Stream
55.113 - BDD
55.114 - BinarySearchTree
55.115 - Binomial-Heaps
55.116 - Binomial-Queues
55.117 - Bondy
55.118 - BytecodeLogicJmlTypes
55.119 - CCS
55.120 - Category
55.121 - Category2
55.122 - Cauchy
55.123 - Circus
55.124 - ClockSynchInst
55.125 - CofGroups
55.126 - Coinductive
55.127 - Collections
55.128 - Compiling-Exceptions-Correctly
55.129 - Completeness
55.130 - Containers
55.131 - CoreC++
55.132 - DPT-SAT-Solver
55.133 - DataRefinementIBP
55.134 - Datatype_Order_Generator
55.135 - Depth-First-Search
55.136 - Dijkstra_Shortest_Path
55.137 - DiskPaxos
55.138 - Efficient-Mergesort
55.139 - Example-Submission
55.140 - FFT
55.141 - FOL-Fitting
55.142 - FeatherweightJava
55.143 - Fermat3_4
55.144 - FileRefinement
55.145 - FinFun
55.146 - Finger-Trees
55.147 - Flyspeck-Tame
55.148 - Free-Boolean-Algebra
55.149 - Free-Groups
55.150 - FunWithFunctions
55.151 - FunWithTilings
55.152 - Functional-Automata
55.153 - Gauss-Jordan-Elim-Fun
55.154 - GenClock
55.155 - General-Triangle
55.156 - Girth_Chromatic
55.157 - GraphMarkingIBP
55.158 - Graph_Theory
55.159 - Group-Ring-Module
55.160 - HRB-Slicing
55.161 - Heard_Of
55.162 - HotelKeyCards
55.163 - Huffman
55.164 - Impossible_Geometry
55.165 - Inductive_Confidentiality
55.166 - InformationFlowSlicing
55.167 - Integration
55.168 - Jinja
55.169 - JinjaThreads
55.170 - JiveDataStoreModel
55.171 - KBPs
55.172 - Kleene_Algebra
55.173 - Lam-ml-Normalization
55.174 - LatticeProperties
55.175 - Launchbury
55.176 - Lazy-Lists-II
55.177 - LightweightJava
55.178 - LinearQuantifierElim
55.179 - List-Index
55.180 - List-Infinite
55.181 - Locally-Nameless-Sigma
55.182 - Lower_Semicontinuous
55.183 - Markov_Models
55.184 - Marriage
55.185 - Matrix
55.186 - Max-Card-Matching
55.187 - MiniML
55.188 - MonoBoolTranAlgebra
55.189 - MuchAdoAboutTwo
55.190 - Myhill-Nerode
55.191 - Nat-Interval-Logic
55.192 - Nominal2
55.193 - NormByEval
55.194 - Open_Induction
55.195 - Ordinal
55.196 - Ordinals_and_Cardinals
55.197 - Ordinary_Differential_Equations
55.198 - PCF
55.199 - POPLmark-deBruijn
55.200 - Perfect-Number-Thm
55.201 - Pi_Calculus
55.202 - Polynomials
55.203 - Possibilistic_Noninterference
55.204 - Presburger-Automata
55.205 - Program-Conflict-Analysis
55.206 - PseudoHoops
55.207 - Psi_Calculi
55.208 - RIPEMD-160-SPARK
55.209 - RSAPSS
55.210 - Ramsey-Infinite
55.211 - Rank_Nullity_Theorem
55.212 - Recursion-Theory-I
55.213 - Refine_Monadic
55.214 - Regular-Sets
55.215 - Ribbon_Proofs
55.216 - Robbins-Conjecture
55.217 - SATSolverVerification
55.218 - SIFPL
55.219 - SenSocialChoice
55.220 - Separation_Algebra
55.221 - Separation_Logic_Imperative_HOL
55.222 - SequentInvertibility
55.223 - Shivers-CFA
55.224 - ShortestPath
55.225 - Simpl
55.226 - Slicing
55.227 - Sqrt_Babylonian
55.228 - Statecharts
55.229 - Stream-Fusion
55.230 - Stuttering_Equivalence
55.231 - SumSquares
55.232 - TLA
55.233 - Tarskis_Geometry
55.234 - Topology
55.235 - Transitive-Closure
55.236 - Transitive-Closure-II
55.237 - Tree-Automata
55.238 - Tycon
55.239 - Valuation
55.240 - Verified-Prover
55.241 - VolpanoSmith
55.242 - Well_Quasi_Orders
55.243 - WorkerWrapper
55.244 -"
55.245 -
55.246 -for PLATFORM in $PLATFORMS
55.247 -do
55.248 - if [ "$PLATFORM" = afp ]; then
55.249 - SESSIONS="$AFP_SESSIONS"
55.250 - else
55.251 - SESSIONS="$ISABELLE_SESSIONS"
55.252 - fi
55.253 -
55.254 - "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
55.255 - cat > "stats/$PLATFORM.html" <<EOF
55.256 -<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
55.257 -<html>
55.258 -<head><title>Development Snapshot -- Performance Statistics</title></head>
55.259 -
55.260 -<body>
55.261 -<h1>$PLATFORM</h1>
55.262 -EOF
55.263 -
55.264 -for SESSION in $SESSIONS
55.265 -do
55.266 - echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
55.267 -done
55.268 -
55.269 -echo "</body>" >> "stats/$PLATFORM.html"
55.270 -echo "</html>" >> "stats/$PLATFORM.html"
55.271 -
55.272 -done
56.1 --- a/Admin/isatest/pmail Sat Apr 11 11:28:31 2015 +0200
56.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
56.3 @@ -1,111 +0,0 @@
56.4 -#!/usr/bin/env bash
56.5 -#
56.6 -# Author: Gerwin Klein, TU Muenchen
56.7 -#
56.8 -# DESCRIPTION: send email with text attachments.
56.9 -# (works for "mail" command of SunOS 5.8)
56.10 -#
56.11 -
56.12 -PRG="$(basename "$0")"
56.13 -
56.14 -MIME_BOUNDARY="==PM_=_37427935"
56.15 -
56.16 -function usage()
56.17 -{
56.18 - echo
56.19 - echo "Usage: $PRG subject recipient <body> [<attachments>]"
56.20 - echo
56.21 - echo " Send email with text attachments. <body> is a file."
56.22 - echo
56.23 - exit 1
56.24 -}
56.25 -
56.26 -function fail()
56.27 -{
56.28 - echo "$1" >&2
56.29 - exit 2
56.30 -}
56.31 -
56.32 -#
56.33 -# print_attachment <file>
56.34 -#
56.35 -# print mime "encoded" <file> to stdout (text/plain, 8bit)
56.36 -#
56.37 -function print_attachment()
56.38 -{
56.39 - local FILE=$1
56.40 - local NAME=${FILE##*/}
56.41 -
56.42 - cat <<EOF
56.43 ---$MIME_BOUNDARY
56.44 -Content-Type: text/plain
56.45 -Content-Transfer-Encoding: 8bit
56.46 -Content-Disposition: attachment; filename="$NAME"
56.47 -
56.48 -EOF
56.49 - cat $FILE
56.50 - echo
56.51 -}
56.52 -
56.53 -
56.54 -#
56.55 -# print_body subject <message-file> [<attachments>]
56.56 -#
56.57 -# prints mime "encoded" message with text attachments to stdout
56.58 -#
56.59 -function print_body()
56.60 -{
56.61 - local SUBJECT=$1
56.62 - local BODY=$2
56.63 - local TO=$3
56.64 - shift 3
56.65 -
56.66 - cat <<EOF
56.67 -Subject: $SUBJECT
56.68 -To: $TO
56.69 -Mime-Version: 1.0
56.70 -Content-Type: multipart/mixed; boundary="$MIME_BOUNDARY"
56.71 -
56.72 ---$MIME_BOUNDARY
56.73 -Content-Type: text/plain
56.74 -Content-Transfer-Encoding: 8bit
56.75 -
56.76 -EOF
56.77 - cat $BODY
56.78 - echo
56.79 -
56.80 - for a in $@; do print_attachment $a; done
56.81 -
56.82 - echo "--$MIME_BOUNDARY--"
56.83 - echo
56.84 -}
56.85 -
56.86 -## main
56.87 -
56.88 -# argument checking
56.89 -
56.90 -[ "$1" = "-?" ] && usage
56.91 -[ "$#" -lt "3" ] && usage
56.92 -
56.93 -SUBJECT="$1"
56.94 -TO="$2"
56.95 -BODY="$3"
56.96 -
56.97 -shift 3
56.98 -
56.99 -[ -r "$BODY" ] || fail "could not read $BODY"
56.100 -
56.101 -case `hostname` in
56.102 - lxbroy*)
56.103 - print_body "$SUBJECT" "$BODY" "$TO" $@ | sendmail "$TO"
56.104 - ;;
56.105 - macbroy*) for F in $@; do ATTACH="$ATTACH -a $F"; done
56.106 - cat "$BODY" | mail -s "$SUBJECT" $ATTACH "$TO"
56.107 - ;;
56.108 - sunbroy*)
56.109 - print_body "$SUBJECT" "$BODY" "$TO" $@ | mail -t "$TO"
56.110 - ;;
56.111 - *)
56.112 - fail "unknown host/platform"
56.113 - ;;
56.114 -esac
57.1 --- a/Admin/isatest/settings/afp-poly Sat Apr 11 11:28:31 2015 +0200
57.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
57.3 @@ -1,27 +0,0 @@
57.4 -# -*- shell-script -*- :mode=shellscript:
57.5 -
57.6 -init_components /home/isabelle/contrib "$HOME/admin/components/main"
57.7 -
57.8 -# to be retired:
57.9 -# JINJATHREADS_OPTIONS="-M 1 -q 0 -p 0"
57.10 -
57.11 -ISABELLE_GHC=ghc
57.12 -
57.13 -ISABELLE_HOME_USER=~/afp/isabelle-afp-poly
57.14 -
57.15 -# Where to look for isabelle tools (multiple dirs separated by ':').
57.16 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
57.17 -
57.18 -# Location for temporary files (should be on a local file system).
57.19 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
57.20 -
57.21 -
57.22 -# Heap input locations. ML system identifier is included in lookup.
57.23 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
57.24 -
57.25 -# Heap output location. ML system identifier is appended automatically later on.
57.26 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
57.27 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
57.28 -
57.29 -ISABELLE_BUILD_OPTIONS="browser_info=false document=false threads=4 parallel_proofs=2"
57.30 -
58.1 --- a/Admin/isatest/settings/at-poly Sat Apr 11 11:28:31 2015 +0200
58.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
58.3 @@ -1,30 +0,0 @@
58.4 -# -*- shell-script -*- :mode=shellscript:
58.5 -
58.6 -init_components /home/isabelle/contrib "$HOME/admin/components/main"
58.7 -
58.8 - POLYML_HOME="/home/polyml/polyml-5.3.0"
58.9 - ML_SYSTEM="polyml-5.3.0"
58.10 - ML_PLATFORM="x86-linux"
58.11 - ML_HOME="$POLYML_HOME/$ML_PLATFORM"
58.12 - ML_OPTIONS="-H 500"
58.13 -
58.14 -ISABELLE_GHC=/usr/bin/ghc
58.15 -
58.16 -ISABELLE_HOME_USER=~/isabelle-at-poly
58.17 -
58.18 -# Where to look for isabelle tools (multiple dirs separated by ':').
58.19 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
58.20 -
58.21 -# Location for temporary files (should be on a local file system).
58.22 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
58.23 -
58.24 -
58.25 -# Heap input locations. ML system identifier is included in lookup.
58.26 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
58.27 -
58.28 -# Heap output location. ML system identifier is appended automatically later on.
58.29 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
58.30 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
58.31 -
58.32 -ISABELLE_BUILD_OPTIONS="browser_info=true document=pdf"
58.33 -
59.1 --- a/Admin/isatest/settings/at-poly-e Sat Apr 11 11:28:31 2015 +0200
59.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
59.3 @@ -1,30 +0,0 @@
59.4 -# -*- shell-script -*- :mode=shellscript:
59.5 -
59.6 -init_components /home/isabelle/contrib "$HOME/admin/components/main"
59.7 -
59.8 - POLYML_HOME="/home/polyml/polyml-5.3.0"
59.9 - ML_SYSTEM="polyml-5.3.0"
59.10 - ML_PLATFORM="x86-linux"
59.11 - ML_HOME="$POLYML_HOME/$ML_PLATFORM"
59.12 - ML_OPTIONS="-H 500"
59.13 -
59.14 -ISABELLE_GHC=/usr/bin/ghc
59.15 -
59.16 -ISABELLE_HOME_USER=~/isabelle-at-poly-e
59.17 -
59.18 -# Where to look for isabelle tools (multiple dirs separated by ':').
59.19 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
59.20 -
59.21 -# Location for temporary files (should be on a local file system).
59.22 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
59.23 -
59.24 -
59.25 -# Heap input locations. ML system identifier is included in lookup.
59.26 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
59.27 -
59.28 -# Heap output location. ML system identifier is appended automatically later on.
59.29 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
59.30 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
59.31 -
59.32 -ISABELLE_BUILD_OPTIONS="browser_info=true document=pdf"
59.33 -
60.1 --- a/Admin/isatest/settings/at-poly-test Sat Apr 11 11:28:31 2015 +0200
60.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
60.3 @@ -1,34 +0,0 @@
60.4 -# -*- shell-script -*- :mode=shellscript:
60.5 -
60.6 -init_components /home/isabelle/contrib "$HOME/admin/components/main"
60.7 -
60.8 - POLYML_HOME="/home/polyml/polyml-svn"
60.9 - ML_SYSTEM="polyml-5.5.2"
60.10 - ML_PLATFORM="x86-linux"
60.11 - ML_HOME="$POLYML_HOME/$ML_PLATFORM"
60.12 - ML_OPTIONS="-H 500 --gcthreads 4"
60.13 -
60.14 -ISABELLE_GHC=/usr/bin/ghc
60.15 -
60.16 -ISABELLE_HOME_USER=~/isabelle-at-poly-test
60.17 -
60.18 -# Where to look for isabelle tools (multiple dirs separated by ':').
60.19 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
60.20 -
60.21 -# Location for temporary files (should be on a local file system).
60.22 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
60.23 -
60.24 -
60.25 -# Heap input locations. ML system identifier is included in lookup.
60.26 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
60.27 -
60.28 -# Heap output location. ML system identifier is appended automatically later on.
60.29 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
60.30 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
60.31 -
60.32 -ISABELLE_BUILD_OPTIONS="browser_info=true document=pdf threads=4 parallel_proofs=2"
60.33 -
60.34 -ISABELLE_GHC="/usr/bin/ghc"
60.35 -ISABELLE_OCAML="/usr/bin/ocaml"
60.36 -ISABELLE_SWIPL="/usr/bin/swipl"
60.37 -
61.1 --- a/Admin/isatest/settings/at-sml-dev-e Sat Apr 11 11:28:31 2015 +0200
61.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
61.3 @@ -1,29 +0,0 @@
61.4 -# -*- shell-script -*- :mode=shellscript:
61.5 -
61.6 -init_components /home/isabelle/contrib "$HOME/admin/components/main"
61.7 -
61.8 -ML_SYSTEM=smlnj
61.9 -ML_HOME="/home/smlnj/110.76/bin"
61.10 -ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
61.11 -ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
61.12 -
61.13 -ISABELLE_GHC=/usr/bin/ghc
61.14 -
61.15 -ISABELLE_HOME_USER="$HOME/isabelle-at-sml-dev-e"
61.16 -
61.17 -# Where to look for isabelle tools (multiple dirs separated by ':').
61.18 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
61.19 -
61.20 -# Location for temporary files (should be on a local file system).
61.21 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
61.22 -
61.23 -
61.24 -# Heap input locations. ML system identifier is included in lookup.
61.25 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
61.26 -
61.27 -# Heap output location. ML system identifier is appended automatically later on.
61.28 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
61.29 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
61.30 -
61.31 -ISABELLE_BUILD_OPTIONS="browser_info=true document=pdf"
61.32 -
62.1 --- a/Admin/isatest/settings/at64-poly Sat Apr 11 11:28:31 2015 +0200
62.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
62.3 @@ -1,30 +0,0 @@
62.4 -# -*- shell-script -*- :mode=shellscript:
62.5 -
62.6 -init_components /home/isabelle/contrib "$HOME/admin/components/main"
62.7 -
62.8 - POLYML_HOME="/home/polyml/polyml-5.5.1"
62.9 - ML_SYSTEM="polyml-5.5.1"
62.10 - ML_PLATFORM="x86_64-linux"
62.11 - ML_HOME="$POLYML_HOME/$ML_PLATFORM"
62.12 - ML_OPTIONS="--minheap 1000 --maxheap 3000 --gcthreads 1"
62.13 -
62.14 -ISABELLE_GHC=/usr/bin/ghc
62.15 -
62.16 -ISABELLE_HOME_USER=~/isabelle-at64-poly
62.17 -
62.18 -# Where to look for isabelle tools (multiple dirs separated by ':').
62.19 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
62.20 -
62.21 -# Location for temporary files (should be on a local file system).
62.22 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
62.23 -
62.24 -
62.25 -# Heap input locations. ML system identifier is included in lookup.
62.26 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
62.27 -
62.28 -# Heap output location. ML system identifier is appended automatically later on.
62.29 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
62.30 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
62.31 -
62.32 -ISABELLE_BUILD_OPTIONS="browser_info=true document=pdf"
62.33 -
63.1 --- a/Admin/isatest/settings/mac-poly-M2 Sat Apr 11 11:28:31 2015 +0200
63.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
63.3 @@ -1,31 +0,0 @@
63.4 -# -*- shell-script -*- :mode=shellscript:
63.5 -
63.6 -init_components /home/isabelle/contrib "$HOME/admin/components/main"
63.7 -init_components /home/isabelle/contrib "$HOME/admin/components/optional"
63.8 -init_components /home/isabelle/contrib "$HOME/admin/components/nonfree"
63.9 -
63.10 -ML_SYSTEM="polyml-5.5.0"
63.11 -ML_PLATFORM="x86-darwin"
63.12 -ML_HOME="/home/polyml/polyml-5.5.0/$ML_PLATFORM"
63.13 -ML_OPTIONS="-H 500"
63.14 -
63.15 -ISABELLE_GHC=ghc
63.16 -
63.17 -ISABELLE_HOME_USER=~/isabelle-mac-poly-M2
63.18 -
63.19 -# Where to look for isabelle tools (multiple dirs separated by ':').
63.20 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
63.21 -
63.22 -# Location for temporary files (should be on a local file system).
63.23 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
63.24 -
63.25 -
63.26 -# Heap input locations. ML system identifier is included in lookup.
63.27 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
63.28 -
63.29 -# Heap output location. ML system identifier is appended automatically later on.
63.30 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
63.31 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
63.32 -
63.33 -ISABELLE_BUILD_OPTIONS="browser_info=true document=pdf threads=2 parallel_proofs=2"
63.34 -
64.1 --- a/Admin/isatest/settings/mac-poly-M4 Sat Apr 11 11:28:31 2015 +0200
64.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
64.3 @@ -1,34 +0,0 @@
64.4 -# -*- shell-script -*- :mode=shellscript:
64.5 -
64.6 -init_components /home/isabelle/contrib "$HOME/admin/components/main"
64.7 -
64.8 - POLYML_HOME="/home/polyml/polyml-5.5.2"
64.9 - ML_SYSTEM="polyml-5.5.2"
64.10 - ML_PLATFORM="x86-darwin"
64.11 - ML_HOME="$POLYML_HOME/$ML_PLATFORM"
64.12 - ML_OPTIONS="-H 500 --gcthreads 4"
64.13 -
64.14 -ISABELLE_GHC=ghc
64.15 -
64.16 -ISABELLE_HOME_USER=~/isabelle-mac-poly-M4
64.17 -
64.18 -# Where to look for isabelle tools (multiple dirs separated by ':').
64.19 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
64.20 -
64.21 -# Location for temporary files (should be on a local file system).
64.22 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
64.23 -
64.24 -
64.25 -# Heap input locations. ML system identifier is included in lookup.
64.26 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
64.27 -
64.28 -# Heap output location. ML system identifier is appended automatically later on.
64.29 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
64.30 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
64.31 -
64.32 -ISABELLE_BUILD_OPTIONS="browser_info=false document=pdf document_variants=document:outline=/proof,/ML threads=4 parallel_proofs=2"
64.33 -
64.34 -ISABELLE_FULL_TEST=true
64.35 -
64.36 -Z3_NON_COMMERCIAL="yes"
64.37 -
65.1 --- a/Admin/isatest/settings/mac-poly-M8 Sat Apr 11 11:28:31 2015 +0200
65.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
65.3 @@ -1,34 +0,0 @@
65.4 -# -*- shell-script -*- :mode=shellscript:
65.5 -
65.6 -init_components /home/isabelle/contrib "$HOME/admin/components/main"
65.7 -
65.8 - POLYML_HOME="/home/polyml/polyml-5.5.2"
65.9 - ML_SYSTEM="polyml-5.5.2"
65.10 - ML_PLATFORM="x86-darwin"
65.11 - ML_HOME="$POLYML_HOME/$ML_PLATFORM"
65.12 - ML_OPTIONS="-H 500 --gcthreads 8"
65.13 -
65.14 -ISABELLE_GHC=ghc
65.15 -
65.16 -ISABELLE_HOME_USER=~/isabelle-mac-poly-M8
65.17 -
65.18 -# Where to look for isabelle tools (multiple dirs separated by ':').
65.19 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
65.20 -
65.21 -# Location for temporary files (should be on a local file system).
65.22 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
65.23 -
65.24 -
65.25 -# Heap input locations. ML system identifier is included in lookup.
65.26 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
65.27 -
65.28 -# Heap output location. ML system identifier is appended automatically later on.
65.29 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
65.30 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
65.31 -
65.32 -ISABELLE_BUILD_OPTIONS="browser_info=false document=pdf document_variants=document:outline=/proof,/ML threads=8 parallel_proofs=2"
65.33 -
65.34 -ISABELLE_FULL_TEST=true
65.35 -
65.36 -Z3_NON_COMMERCIAL="yes"
65.37 -
66.1 --- a/Admin/isatest/settings/mac-poly-M8-quick_and_dirty Sat Apr 11 11:28:31 2015 +0200
66.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
66.3 @@ -1,32 +0,0 @@
66.4 -# -*- shell-script -*- :mode=shellscript:
66.5 -
66.6 -init_components /home/isabelle/contrib "$HOME/admin/components/main"
66.7 -
66.8 - POLYML_HOME="/home/polyml/polyml-5.4.1"
66.9 - ML_SYSTEM="polyml-5.4.1"
66.10 - ML_PLATFORM="x86-darwin"
66.11 - ML_HOME="$POLYML_HOME/$ML_PLATFORM"
66.12 - ML_OPTIONS="-H 1000"
66.13 -
66.14 -ISABELLE_GHC=ghc
66.15 -
66.16 -ISABELLE_HOME_USER=~/isabelle-mac-poly-M8-quick_and_dirty
66.17 -
66.18 -# Where to look for isabelle tools (multiple dirs separated by ':').
66.19 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
66.20 -
66.21 -# Location for temporary files (should be on a local file system).
66.22 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
66.23 -
66.24 -
66.25 -# Heap input locations. ML system identifier is included in lookup.
66.26 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
66.27 -
66.28 -# Heap output location. ML system identifier is appended automatically later on.
66.29 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
66.30 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
66.31 -
66.32 -ISABELLE_BUILD_OPTIONS="threads=8 quick_and_dirty"
66.33 -
66.34 -Z3_NON_COMMERCIAL="yes"
66.35 -
67.1 --- a/Admin/isatest/settings/mac-poly-M8-skip_proofs Sat Apr 11 11:28:31 2015 +0200
67.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
67.3 @@ -1,32 +0,0 @@
67.4 -# -*- shell-script -*- :mode=shellscript:
67.5 -
67.6 -init_components /home/isabelle/contrib "$HOME/admin/components/main"
67.7 -
67.8 - POLYML_HOME="/home/polyml/polyml-5.5.0"
67.9 - ML_SYSTEM="polyml-5.5.0"
67.10 - ML_PLATFORM="x86-darwin"
67.11 - ML_HOME="$POLYML_HOME/$ML_PLATFORM"
67.12 - ML_OPTIONS="-H 1000 --gcthreads 8"
67.13 -
67.14 -ISABELLE_GHC=ghc
67.15 -
67.16 -ISABELLE_HOME_USER=~/isabelle-mac-poly-M8-skip_proofs
67.17 -
67.18 -# Where to look for isabelle tools (multiple dirs separated by ':').
67.19 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
67.20 -
67.21 -# Location for temporary files (should be on a local file system).
67.22 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
67.23 -
67.24 -
67.25 -# Heap input locations. ML system identifier is included in lookup.
67.26 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
67.27 -
67.28 -# Heap output location. ML system identifier is appended automatically later on.
67.29 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
67.30 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
67.31 -
67.32 -ISABELLE_BUILD_OPTIONS="threads=8 skip_proofs"
67.33 -
67.34 -Z3_NON_COMMERCIAL="yes"
67.35 -
68.1 --- a/Admin/isatest/settings/mac-poly64-M2 Sat Apr 11 11:28:31 2015 +0200
68.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
68.3 @@ -1,30 +0,0 @@
68.4 -# -*- shell-script -*- :mode=shellscript:
68.5 -
68.6 -init_components /home/isabelle/contrib "$HOME/admin/components/main"
68.7 -
68.8 - POLYML_HOME="/home/polyml/polyml-5.4.0"
68.9 - ML_SYSTEM="polyml-5.4.0"
68.10 - ML_PLATFORM="x86_64-darwin"
68.11 - ML_HOME="$POLYML_HOME/$ML_PLATFORM"
68.12 - ML_OPTIONS="-H 1000"
68.13 -
68.14 -ISABELLE_GHC=ghc
68.15 -
68.16 -ISABELLE_HOME_USER=~/isabelle-at-mac-poly64-M2
68.17 -
68.18 -# Where to look for isabelle tools (multiple dirs separated by ':').
68.19 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
68.20 -
68.21 -# Location for temporary files (should be on a local file system).
68.22 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
68.23 -
68.24 -
68.25 -# Heap input locations. ML system identifier is included in lookup.
68.26 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
68.27 -
68.28 -# Heap output location. ML system identifier is appended automatically later on.
68.29 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
68.30 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
68.31 -
68.32 -ISABELLE_BUILD_OPTIONS="browser_info=false document=false threads=2 parallel_proofs=2"
68.33 -
69.1 --- a/Admin/isatest/settings/mac-poly64-M4 Sat Apr 11 11:28:31 2015 +0200
69.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
69.3 @@ -1,30 +0,0 @@
69.4 -# -*- shell-script -*- :mode=shellscript:
69.5 -
69.6 -init_components /home/isabelle/contrib "$HOME/admin/components/main"
69.7 -
69.8 - POLYML_HOME="/home/polyml/polyml-5.5.2"
69.9 - ML_SYSTEM="polyml-5.5.2"
69.10 - ML_PLATFORM="x86_64-darwin"
69.11 - ML_HOME="$POLYML_HOME/$ML_PLATFORM"
69.12 - ML_OPTIONS="-H 2000 --gcthreads 4"
69.13 -
69.14 -ISABELLE_GHC=ghc
69.15 -
69.16 -ISABELLE_HOME_USER=~/isabelle-mac-poly64-M4
69.17 -
69.18 -# Where to look for isabelle tools (multiple dirs separated by ':').
69.19 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
69.20 -
69.21 -# Location for temporary files (should be on a local file system).
69.22 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
69.23 -
69.24 -
69.25 -# Heap input locations. ML system identifier is included in lookup.
69.26 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
69.27 -
69.28 -# Heap output location. ML system identifier is appended automatically later on.
69.29 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
69.30 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
69.31 -
69.32 -ISABELLE_BUILD_OPTIONS="browser_info=false document=false threads=4 parallel_proofs=2"
69.33 -
70.1 --- a/Admin/isatest/settings/mac-poly64-M8 Sat Apr 11 11:28:31 2015 +0200
70.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
70.3 @@ -1,30 +0,0 @@
70.4 -# -*- shell-script -*- :mode=shellscript:
70.5 -
70.6 -init_components /home/isabelle/contrib "$HOME/admin/components/main"
70.7 -
70.8 - POLYML_HOME="/home/polyml/polyml-5.5.2"
70.9 - ML_SYSTEM="polyml-5.5.2"
70.10 - ML_PLATFORM="x86_64-darwin"
70.11 - ML_HOME="$POLYML_HOME/$ML_PLATFORM"
70.12 - ML_OPTIONS="-H 2000 --gcthreads 8"
70.13 -
70.14 -ISABELLE_GHC=ghc
70.15 -
70.16 -ISABELLE_HOME_USER=~/isabelle-mac-poly64-M8
70.17 -
70.18 -# Where to look for isabelle tools (multiple dirs separated by ':').
70.19 -ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
70.20 -
70.21 -# Location for temporary files (should be on a local file system).
70.22 -ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
70.23 -
70.24 -
70.25 -# Heap input locations. ML system identifier is included in lookup.
70.26 -ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
70.27 -
70.28 -# Heap output location. ML system identifier is appended automatically later on.
70.29 -ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
70.30 -ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
70.31 -
70.32 -ISABELLE_BUILD_OPTIONS="browser_info=false document=false threads=8 parallel_proofs=2"
70.33 -
71.1 --- a/Admin/java/build Sat Apr 11 11:28:31 2015 +0200
71.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
71.3 @@ -1,128 +0,0 @@
71.4 -#!/usr/bin/env bash
71.5 -
71.6 -## diagnostics
71.7 -
71.8 -function fail()
71.9 -{
71.10 - echo "$1" >&2
71.11 - exit 2
71.12 -}
71.13 -
71.14 -
71.15 -## parameters
71.16 -
71.17 -VERSION="7u67"
71.18 -FULL_VERSION="1.7.0_67"
71.19 -
71.20 -ARCHIVE_LINUX32="jdk-${VERSION}-linux-i586.tar.gz"
71.21 -ARCHIVE_LINUX64="jdk-${VERSION}-linux-x64.tar.gz"
71.22 -ARCHIVE_DARWIN="jdk${FULL_VERSION}.jdk.tar.gz"
71.23 -ARCHIVE_WINDOWS="jdk${FULL_VERSION}.tar.gz"
71.24 -
71.25 -
71.26 -## main
71.27 -
71.28 -DIR="jdk-${VERSION}"
71.29 -mkdir "$DIR" || fail "Cannot create fresh directory: \"$DIR\""
71.30 -
71.31 -
71.32 -# README
71.33 -
71.34 -cat >> "$DIR/README" << EOF
71.35 -This is JDK $FULL_VERSION as required for Isabelle.
71.36 -
71.37 -See http://www.oracle.com/technetwork/java/javase/downloads/index.html
71.38 -for the original downloads, which are covered by the Oracle Binary
71.39 -Code License Agreement for Java SE.
71.40 -
71.41 -Linux, Mac OS X, Windows work uniformly, depending on certain
71.42 -platform-specific subdirectories.
71.43 -EOF
71.44 -
71.45 -
71.46 -# settings
71.47 -
71.48 -mkdir "$DIR/etc"
71.49 -cat >> "$DIR/etc/settings" << EOF
71.50 -# -*- shell-script -*- :mode=shellscript:
71.51 -
71.52 -case "\${ISABELLE_PLATFORM64:-\$ISABELLE_PLATFORM32}" in
71.53 - x86-darwin)
71.54 - echo "### Java unavailable on 32bit Macintosh!" >&2
71.55 - ;;
71.56 - x86_64-darwin)
71.57 - ISABELLE_JDK_HOME="\$COMPONENT/\$ISABELLE_PLATFORM64/Contents/Home"
71.58 - ;;
71.59 - *)
71.60 - ISABELLE_JDK_HOME="\$COMPONENT/\${ISABELLE_PLATFORM64:-\$ISABELLE_PLATFORM32}"
71.61 - ;;
71.62 -esac
71.63 -
71.64 -if [ -n "\$ISABELLE_JDK_HOME" ]; then
71.65 - if [ -d "\$ISABELLE_JDK_HOME" ]; then
71.66 - ISABELLE_JAVA_EXT="\${ISABELLE_JDK_HOME}/jre/lib/ext"
71.67 - else
71.68 - echo "### Missing Java platform directory: \"\$ISABELLE_JDK_HOME\"" >&2
71.69 - unset ISABELLE_JDK_HOME
71.70 - fi
71.71 -fi
71.72 -EOF
71.73 -
71.74 -
71.75 -# content
71.76 -
71.77 -#GNU tar (notably on Mac OS X)
71.78 -if [ -x /usr/bin/gnutar ]; then
71.79 - function tar() { /usr/bin/gnutar "$@"; }
71.80 -fi
71.81 -
71.82 -mkdir "$DIR/x86-linux" "$DIR/x86_64-linux" "$DIR/x86_64-darwin" "$DIR/x86-cygwin"
71.83 -
71.84 -tar -C "$DIR/x86-linux" -xf "$ARCHIVE_LINUX32"
71.85 -tar -C "$DIR/x86_64-linux" -xf "$ARCHIVE_LINUX64"
71.86 -tar -C "$DIR/x86_64-darwin" -xf "$ARCHIVE_DARWIN"
71.87 -tar -C "$DIR/x86-cygwin" -xf "$ARCHIVE_WINDOWS"
71.88 -
71.89 -(
71.90 - cd "$DIR"
71.91 - for PLATFORM in x86-linux x86_64-linux x86-cygwin
71.92 - do
71.93 - mv "$PLATFORM/jdk${FULL_VERSION}"/* "$PLATFORM"/.
71.94 - rmdir "$PLATFORM/jdk${FULL_VERSION}"
71.95 - done
71.96 - PLATFORM=x86_64-darwin
71.97 - mv "$PLATFORM/jdk${FULL_VERSION}.jdk"/* "$PLATFORM"/.
71.98 - rmdir "$PLATFORM/jdk${FULL_VERSION}.jdk"
71.99 -)
71.100 -
71.101 -chgrp -R isabelle "$DIR"
71.102 -chmod -R a+r "$DIR"
71.103 -chmod -R a+X "$DIR"
71.104 -
71.105 -find "$DIR/x86_64-darwin" -name "._*" -exec rm -f {} ";"
71.106 -
71.107 -echo "Sharing ..."
71.108 -(
71.109 - cd "$DIR/x86-linux"
71.110 - for FILE in $(find . -type f)
71.111 - do
71.112 - for OTHER in \
71.113 - "../x86_64-linux/$FILE" \
71.114 - "../x86_64-darwin/Contents/Home/$FILE" \
71.115 - "../x86-cygwin/$FILE"
71.116 - do
71.117 - if cmp -s "$FILE" "$OTHER"
71.118 - then
71.119 - echo -n "*"
71.120 - ln -f "$FILE" "$OTHER"
71.121 - fi
71.122 - done
71.123 - done
71.124 -)
71.125 -echo
71.126 -
71.127 -
71.128 -# create archive
71.129 -
71.130 -echo "Archiving ..."
71.131 -tar -c -z -f "${DIR}.tar.gz" "$DIR" && echo "${DIR}.tar.gz"
72.1 --- a/Admin/lib/Tools/build_doc Sat Apr 11 11:28:31 2015 +0200
72.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
72.3 @@ -1,78 +0,0 @@
72.4 -#!/usr/bin/env bash
72.5 -#
72.6 -# Author: Makarius
72.7 -#
72.8 -# DESCRIPTION: build Isabelle documentation
72.9 -
72.10 -
72.11 -## diagnostics
72.12 -
72.13 -PRG="$(basename "$0")"
72.14 -
72.15 -function usage()
72.16 -{
72.17 - echo
72.18 - echo "Usage: isabelle $PRG [OPTIONS] [DOCS ...]"
72.19 - echo
72.20 - echo " Options are:"
72.21 - echo " -a select all documentation sessions"
72.22 - echo " -j INT maximum number of parallel jobs (default 1)"
72.23 - echo " -s system build mode"
72.24 - echo
72.25 - echo " Build Isabelle documentation from documentation sessions with"
72.26 - echo " suitable document_variants entry."
72.27 - echo
72.28 - exit 1
72.29 -}
72.30 -
72.31 -function fail()
72.32 -{
72.33 - echo "$1" >&2
72.34 - exit 2
72.35 -}
72.36 -
72.37 -function check_number()
72.38 -{
72.39 - [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
72.40 -}
72.41 -
72.42 -
72.43 -## process command line
72.44 -
72.45 -ALL_DOCS="false"
72.46 -MAX_JOBS="1"
72.47 -SYSTEM_MODE="false"
72.48 -
72.49 -while getopts "aj:s" OPT
72.50 -do
72.51 - case "$OPT" in
72.52 - a)
72.53 - ALL_DOCS="true"
72.54 - ;;
72.55 - j)
72.56 - check_number "$OPTARG"
72.57 - MAX_JOBS="$OPTARG"
72.58 - ;;
72.59 - s)
72.60 - SYSTEM_MODE="true"
72.61 - ;;
72.62 - \?)
72.63 - usage
72.64 - ;;
72.65 - esac
72.66 -done
72.67 -
72.68 -shift $(($OPTIND - 1))
72.69 -
72.70 -[ "$ALL_DOCS" = false -a "$#" -eq 0 ] && usage
72.71 -
72.72 -
72.73 -## main
72.74 -
72.75 -isabelle_admin_build jars || exit $?
72.76 -
72.77 -declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
72.78 -
72.79 -"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Doc \
72.80 - "$ALL_DOCS" "$MAX_JOBS" "$SYSTEM_MODE" "$@"
72.81 -
73.1 --- a/Admin/lib/Tools/churn Sat Apr 11 11:28:31 2015 +0200
73.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
73.3 @@ -1,12 +0,0 @@
73.4 -#!/usr/bin/env bash
73.5 -#
73.6 -# Author: Florian Haftmann, TU Muenchen
73.7 -#
73.8 -# DESCRIPTION: mercurial churn statistics for specified aliases file
73.9 -
73.10 -ALIAS="${1:-$ISABELLE_HOME/Admin/user-aliases}"
73.11 -shift
73.12 -
73.13 -cd "$(dirname "$ALIAS")"
73.14 -
73.15 -hg churn --aliases "$ALIAS" "$@"
74.1 --- a/Admin/lib/Tools/churn_pie Sat Apr 11 11:28:31 2015 +0200
74.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
74.3 @@ -1,14 +0,0 @@
74.4 -#!/usr/bin/env bash
74.5 -#
74.6 -# Author: Florian Haftmann, TU Muenchen
74.7 -#
74.8 -# DESCRIPTION: pie chart with Mercurial churn statistics
74.9 -
74.10 -ALIAS="${1:-$ISABELLE_HOME/Admin/user-aliases}"
74.11 -shift
74.12 -
74.13 -SCRIPT="$ISABELLE_HOME/Admin/lib/scripts/churn_pie"
74.14 -
74.15 -cd "$(dirname "$ALIAS")"
74.16 -
74.17 -hg churn --aliases "$ALIAS" | "$SCRIPT" "$@"
75.1 --- a/Admin/lib/Tools/components_checksum Sat Apr 11 11:28:31 2015 +0200
75.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
75.3 @@ -1,80 +0,0 @@
75.4 -#!/usr/bin/env bash
75.5 -#
75.6 -# Author: Alexander Krauss
75.7 -#
75.8 -# DESCRIPTION: compute and validate checksums for component repository
75.9 -
75.10 -
75.11 -## diagnostics
75.12 -
75.13 -PRG="$(basename "$0")"
75.14 -
75.15 -function usage()
75.16 -{
75.17 - echo
75.18 - echo "Usage: $PRG [OPTIONS] [DIR]"
75.19 - echo
75.20 - echo " Options are:"
75.21 - echo " -u update the recorded checksums in the repository"
75.22 - echo " -c compare the actual checksums with the recorded ones"
75.23 - echo
75.24 - echo " Compute the checksums of component .tar.gz archives in DIR"
75.25 - echo " (default \"/home/isabelle/components\") and synchronize them"
75.26 - echo " with the Isabelle repository."
75.27 - echo
75.28 - exit 1
75.29 -}
75.30 -
75.31 -function fail()
75.32 -{
75.33 - echo "$1" >&2
75.34 - exit 2
75.35 -}
75.36 -
75.37 -
75.38 -## process command line
75.39 -
75.40 -# options
75.41 -
75.42 -UPDATE=""
75.43 -CHECK=""
75.44 -COMPONENTS_DIR="/home/isabelle/components"
75.45 -
75.46 -while getopts "uc" OPT
75.47 -do
75.48 - case "$OPT" in
75.49 - u)
75.50 - UPDATE=true
75.51 - ;;
75.52 - c)
75.53 - CHECK=true
75.54 - ;;
75.55 - esac
75.56 -done
75.57 -
75.58 -shift $(($OPTIND - 1))
75.59 -
75.60 -[ -n "$UPDATE" ] || [ -n "$CHECK" ] || usage
75.61 -
75.62 -
75.63 -# args
75.64 -
75.65 -[ "$#" -ge 1 ] && { COMPONENTS_DIR="$1"; shift; }
75.66 -[ "$#" -ne 0 ] && usage
75.67 -
75.68 -
75.69 -## compute checksums
75.70 -
75.71 -CHECKSUM_DIR="$ISABELLE_HOME/Admin/components"
75.72 -CHECKSUM_FILE="$CHECKSUM_DIR/components.sha1"
75.73 -CHECKSUM_TMP="$CHECKSUM_DIR/components.sha1.tmp"
75.74 -
75.75 -(
75.76 - cd "$COMPONENTS_DIR"
75.77 - sha1sum *.tar.gz | sort -k2 -f > "$CHECKSUM_TMP"
75.78 -)
75.79 -
75.80 -[ -n "$UPDATE" ] && mv "$CHECKSUM_TMP" "$CHECKSUM_FILE"
75.81 -[ -n "$CHECK" ] && {
75.82 - diff "$CHECKSUM_FILE" "$CHECKSUM_TMP" || fail "Integrity error"
75.83 -}
76.1 --- a/Admin/lib/Tools/makedist Sat Apr 11 11:28:31 2015 +0200
76.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
76.3 @@ -1,231 +0,0 @@
76.4 -#!/usr/bin/env bash
76.5 -#
76.6 -# Author: Makarius
76.7 -#
76.8 -# DESCRIPTION: make Isabelle distribution from repository
76.9 -
76.10 -## global parameters
76.11 -
76.12 -umask 022
76.13 -
76.14 -HG="${HG:-hg}"
76.15 -
76.16 -DISTPREFIX="${DISTPREFIX:-$HOME/tmp/isadist}"
76.17 -
76.18 -
76.19 -## diagnostics
76.20 -
76.21 -PRG="$(basename "$0")"
76.22 -
76.23 -function usage()
76.24 -{
76.25 - echo
76.26 - echo "Usage: isabelle $PRG [OPTIONS] [VERSION]"
76.27 - echo
76.28 - echo " Options are:"
76.29 - echo " -O official release (not release-candidate)"
76.30 - echo " -d DIR global directory prefix (default: \"$DISTPREFIX\")"
76.31 - echo " -j INT maximum number of parallel jobs (default 1)"
76.32 - echo " -r RELEASE proper release with name"
76.33 - echo
76.34 - echo " Make Isabelle distribution from the local repository clone."
76.35 - echo
76.36 - echo " VERSION identifies the snapshot, using usual Mercurial terminology;"
76.37 - echo " the default is RELEASE if given, otherwise \"tip\"."
76.38 - echo
76.39 - echo " Add-on components are that of the running Isabelle version!"
76.40 - echo
76.41 - exit 1
76.42 -}
76.43 -
76.44 -function fail()
76.45 -{
76.46 - echo "$1" >&2
76.47 - exit 2
76.48 -}
76.49 -
76.50 -function check_number()
76.51 -{
76.52 - [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
76.53 -}
76.54 -
76.55 -
76.56 -## process command line
76.57 -
76.58 -# options
76.59 -
76.60 -OFFICIAL_RELEASE="false"
76.61 -JOBS=""
76.62 -RELEASE=""
76.63 -
76.64 -while getopts "Od:j:r:" OPT
76.65 -do
76.66 - case "$OPT" in
76.67 - O)
76.68 - OFFICIAL_RELEASE="true"
76.69 - ;;
76.70 - d)
76.71 - DISTPREFIX="$OPTARG"
76.72 - ;;
76.73 - j)
76.74 - check_number "$OPTARG"
76.75 - JOBS="-j $OPTARG"
76.76 - ;;
76.77 - r)
76.78 - RELEASE="$OPTARG"
76.79 - ;;
76.80 - \?)
76.81 - usage
76.82 - ;;
76.83 - esac
76.84 -done
76.85 -
76.86 -shift $(($OPTIND - 1))
76.87 -
76.88 -
76.89 -# args
76.90 -
76.91 -VERSION=""
76.92 -[ "$#" -gt 0 ] && { VERSION="$1"; shift; }
76.93 -[ -z "$VERSION" ] && VERSION="$RELEASE"
76.94 -[ -z "$VERSION" ] && VERSION="tip"
76.95 -
76.96 -[ "$#" -gt 0 ] && usage
76.97 -
76.98 -IDENT=$("$HG" --repository "$ISABELLE_HOME" id -r "$VERSION" -i)
76.99 -[ -z "$IDENT" ] && fail "Bad repository version: \"$VERSION\""
76.100 -
76.101 -
76.102 -## main
76.103 -
76.104 -# dist name
76.105 -
76.106 -DATE=$(env LC_ALL=C date "+%d-%b-%Y")
76.107 -DISTDATE=$(env LC_ALL=C date "+%B %Y")
76.108 -
76.109 -if [ -z "$RELEASE" ]; then
76.110 - DISTNAME="Isabelle_$DATE"
76.111 - DISTVERSION="Isabelle repository snapshot $IDENT $DATE"
76.112 -else
76.113 - DISTNAME="$RELEASE"
76.114 - DISTVERSION="$DISTNAME: $DISTDATE"
76.115 -fi
76.116 -
76.117 -DISTPREFIX="$(cd "$DISTPREFIX"; pwd)"
76.118 -DISTBASE="$DISTPREFIX/dist-$DISTNAME"
76.119 -mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir \"$DISTBASE\""
76.120 -
76.121 -DIR="$DISTBASE/$DISTNAME"
76.122 -[ -e "$DIR" ] && fail "Directory \"$DIR\" already exists"
76.123 -
76.124 -
76.125 -# retrieve repository archive
76.126 -
76.127 -echo "### Retrieving Mercurial repository $VERSION"
76.128 -
76.129 -"$HG" --repository "$ISABELLE_HOME" archive --type files -r "$IDENT" "$DIR" || \
76.130 - fail "Failed to retrieve $VERSION"
76.131 -
76.132 -rm -f "$DIR/.hg_archival.txt"
76.133 -rm -f "$DIR/.hgtags"
76.134 -rm -f "$DIR/.hgignore"
76.135 -rm -f "$DIR/README_REPOSITORY"
76.136 -
76.137 -
76.138 -# partial context switch to new version
76.139 -
76.140 -cd "$DIR"
76.141 -
76.142 -unset ISABELLE_SETTINGS_PRESENT
76.143 -unset ISABELLE_SITE_SETTINGS_PRESENT
76.144 -
76.145 -if [ -z "$RELEASE" ]; then
76.146 - {
76.147 - echo
76.148 - echo "IMPORTANT NOTE"
76.149 - echo "=============="
76.150 - echo
76.151 - echo "This is a snapshot of Isabelle/${IDENT} from the repository."
76.152 - echo
76.153 - } >ANNOUNCE
76.154 -fi
76.155 -
76.156 -if [ -n "$RELEASE" -a "$OFFICIAL_RELEASE" = true ]; then
76.157 - IS_OFFICIAL="true"
76.158 -else
76.159 - IS_OFFICIAL="false"
76.160 -fi
76.161 -
76.162 -perl -pi \
76.163 - -e "s,val is_identified = false,val is_identified = true,g;" \
76.164 - -e "s,val is_official = false,val is_official = ${IS_OFFICIAL},g;" \
76.165 - src/Pure/ROOT.ML src/Pure/ROOT.scala
76.166 -
76.167 -perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings
76.168 -perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
76.169 -perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
76.170 -perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML src/Pure/ROOT.scala lib/Tools/version
76.171 -perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README
76.172 -
76.173 -mkdir -p contrib
76.174 -cat >contrib/README <<EOF
76.175 -This directory contains add-on components that contribute to the main
76.176 -Isabelle distribution. Separate licensing conditions apply, see each
76.177 -directory individually.
76.178 -EOF
76.179 -
76.180 -
76.181 -# prepare dist for release
76.182 -
76.183 -echo "### Preparing distribution $DISTNAME"
76.184 -
76.185 -find . "(" -name \*.thy -o -name \*.ML -o -name \*.scala ")" -perm +111 -print | xargs chmod -f -x
76.186 -find . -print | xargs chmod -f u+rw
76.187 -
76.188 -export CLASSPATH="$ISABELLE_CLASSPATH"
76.189 -
76.190 -./Admin/build all || fail "Failed to build distribution"
76.191 -
76.192 -./bin/isabelle jedit -b || fail "Failed to build Isabelle/jEdit"
76.193 -
76.194 -cp -a src src.orig
76.195 -env ISABELLE_IDENTIFIER="${DISTNAME}-build" \
76.196 - ./bin/isabelle build_doc $JOBS -s -a || fail "Failed to build documentation"
76.197 -rm -rf src
76.198 -mv src.orig src
76.199 -
76.200 -rm -rf Admin browser_info heaps
76.201 -
76.202 -
76.203 -# create archive
76.204 -
76.205 -echo "### Creating archive"
76.206 -
76.207 -cd "$DISTBASE"
76.208 -
76.209 -echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
76.210 -echo "$IDENT" >../ISABELLE_IDENT
76.211 -
76.212 -chown -R "$LOGNAME" "$DISTNAME"
76.213 -chmod -R u+w "$DISTNAME"
76.214 -chmod -R g=o "$DISTNAME"
76.215 -
76.216 -echo "$DISTBASE/$DISTNAME.tar.gz"
76.217 -tar -c -z -f "$DISTNAME.tar.gz" "$DISTNAME"
76.218 -[ "$?" = 0 ] || exit "$?"
76.219 -
76.220 -
76.221 -# cleanup dist
76.222 -
76.223 -mv "$DISTNAME" "${DISTNAME}-old"
76.224 -mkdir "$DISTNAME"
76.225 -
76.226 -mv "${DISTNAME}-old/README" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" \
76.227 - "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" "$DISTNAME"
76.228 -mkdir "$DISTNAME/doc"
76.229 -mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
76.230 -
76.231 -rm -f Isabelle && ln -sf "$DISTNAME" Isabelle
76.232 -
76.233 -rm -rf "${DISTNAME}-old"
76.234 -
77.1 --- a/Admin/lib/Tools/makedist_bundle Sat Apr 11 11:28:31 2015 +0200
77.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
77.3 @@ -1,338 +0,0 @@
77.4 -#!/usr/bin/env bash
77.5 -#
77.6 -# DESCRIPTION: re-package Isabelle distribution with add-on components
77.7 -
77.8 -## diagnostics
77.9 -
77.10 -PRG=$(basename "$0")
77.11 -
77.12 -function usage()
77.13 -{
77.14 - echo
77.15 - echo "Usage: isabelle $PRG ARCHIVE PLATFORM_FAMILY"
77.16 - echo
77.17 - echo " Re-package Isabelle source distribution with add-on components"
77.18 - echo " and post-hoc patches for platform family linux, macos, windows."
77.19 - echo
77.20 - echo " Add-on components are that of the running Isabelle version!"
77.21 - echo
77.22 - exit 1
77.23 -}
77.24 -
77.25 -function fail()
77.26 -{
77.27 - echo "$1" >&2
77.28 - exit 2
77.29 -}
77.30 -
77.31 -
77.32 -## arguments
77.33 -
77.34 -[ "$#" -ne 2 ] && usage
77.35 -
77.36 -ARCHIVE="$1"; shift
77.37 -PLATFORM_FAMILY="$1"; shift
77.38 -
77.39 -[ -f "$ARCHIVE" ] || fail "Bad source archive: $ARCHIVE"
77.40 -
77.41 -ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
77.42 -ISABELLE_NAME="$(basename "$ARCHIVE" .tar.gz)"
77.43 -
77.44 -
77.45 -## main
77.46 -
77.47 -TMP="/var/tmp/isabelle-makedist$$"
77.48 -mkdir "$TMP" || fail "Cannot create directory $TMP"
77.49 -
77.50 -ISABELLE_TARGET="$TMP/$ISABELLE_NAME"
77.51 -
77.52 -tar -C "$TMP" -x -z -f "$ARCHIVE" || exit 2
77.53 -
77.54 -
77.55 -# distribution classpath (based on educated guesses)
77.56 -
77.57 -splitarray ":" "$ISABELLE_CLASSPATH"; CLASSPATH_ENTRIES=("${SPLITARRAY[@]}")
77.58 -declare -a DISTRIBITION_CLASSPATH=()
77.59 -
77.60 -for ENTRY in "${CLASSPATH_ENTRIES[@]}"
77.61 -do
77.62 - ENTRY=$(echo "$ENTRY" | perl -n -e "
77.63 - if (m,$ISABELLE_HOME/(.*)\$,) { print qq{\$1}; }
77.64 - elsif (m,$USER_HOME/.isabelle/contrib/(.*)\$,) { print qq{contrib/\$1}; }
77.65 - else { print; };
77.66 - print qq{\n};")
77.67 - DISTRIBITION_CLASSPATH["${#DISTRIBITION_CLASSPATH[@]}"]="$ENTRY"
77.68 -done
77.69 -
77.70 -DISTRIBITION_CLASSPATH["${#DISTRIBITION_CLASSPATH[@]}"]="src/Tools/jEdit/dist/jedit.jar"
77.71 -
77.72 -echo "classpath"
77.73 -for ENTRY in "${DISTRIBITION_CLASSPATH[@]}"
77.74 -do
77.75 - echo " $ENTRY"
77.76 -done
77.77 -
77.78 -
77.79 -# bundled components
77.80 -
77.81 -init_component "$JEDIT_HOME"
77.82 -
77.83 -mkdir -p "$ARCHIVE_DIR/contrib"
77.84 -
77.85 -echo "#bundled components" >> "$ISABELLE_TARGET/etc/components"
77.86 -
77.87 -for CATALOG in main "$PLATFORM_FAMILY" bundled "bundled-$PLATFORM_FAMILY"
77.88 -do
77.89 - CATALOG_FILE="$ISABELLE_HOME/Admin/components/$CATALOG"
77.90 - if [ -f "$CATALOG_FILE" ]
77.91 - then
77.92 - echo "catalog ${CATALOG}"
77.93 - {
77.94 - while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
77.95 - do
77.96 - case "$REPLY" in
77.97 - \#* | "") ;;
77.98 - *)
77.99 - COMPONENT="$REPLY"
77.100 - COMPONENT_DIR="$ISABELLE_TARGET/contrib/$COMPONENT"
77.101 - case "$COMPONENT" in
77.102 - jedit_build*) ;;
77.103 - *)
77.104 - echo " component $COMPONENT"
77.105 - CONTRIB="$ARCHIVE_DIR/contrib/${COMPONENT}.tar.gz"
77.106 - if [ ! -f "$CONTRIB" ]; then
77.107 - REMOTE="$ISABELLE_COMPONENT_REPOSITORY/${COMPONENT}.tar.gz"
77.108 - echo " download $REMOTE"
77.109 - perl -MLWP::Simple -e "getprint '$REMOTE';" > "$CONTRIB"
77.110 - perl -e "exit((stat('${CONTRIB}'))[7] == 0 ? 0 : 1);" && exit 2
77.111 - fi
77.112 -
77.113 - tar -C "$ISABELLE_TARGET/contrib" -x -z -f "$CONTRIB" || exit 2
77.114 - if [ -f "$COMPONENT_DIR/etc/settings" -o -f "$COMPONENT_DIR/etc/components" ]
77.115 - then
77.116 - case "$COMPONENT" in
77.117 - jdk-*)
77.118 - mv "$ISABELLE_TARGET/contrib/$COMPONENT" "$ISABELLE_TARGET/contrib/jdk"
77.119 - echo "contrib/jdk" >> "$ISABELLE_TARGET/etc/components"
77.120 - ;;
77.121 - *)
77.122 - echo "contrib/$COMPONENT" >> "$ISABELLE_TARGET/etc/components"
77.123 - ;;
77.124 - esac
77.125 - fi
77.126 - ;;
77.127 - esac
77.128 - ;;
77.129 - esac
77.130 - done
77.131 - } < "$CATALOG_FILE"
77.132 - fi
77.133 -done
77.134 -
77.135 -
77.136 -# purge other platforms
77.137 -
77.138 -function purge_contrib
77.139 -{
77.140 - (
77.141 - cd "$ISABELLE_TARGET"
77.142 - for DIR in $(eval find contrib "$@" | sort)
77.143 - do
77.144 - echo "removing $DIR"
77.145 - rm -rf "$DIR"
77.146 - done
77.147 - )
77.148 -}
77.149 -
77.150 -
77.151 -# platform-specific setup (inside archive)
77.152 -
77.153 -perl -pi -e "s,view.title=Isabelle/jEdit,view.title=${ISABELLE_NAME},g;" \
77.154 - "$ISABELLE_TARGET/src/Tools/jEdit/dist/properties/jEdit.props"
77.155 -
77.156 -case "$PLATFORM_FAMILY" in
77.157 - linux)
77.158 - purge_contrib '-name "x86*-darwin" -o -name "x86*-cygwin" -o -name "x86*-windows"'
77.159 -
77.160 - LINUX_CLASSPATH=""
77.161 - for ENTRY in "${DISTRIBITION_CLASSPATH[@]}"
77.162 - do
77.163 - if [ -z "$LINUX_CLASSPATH" ]; then
77.164 - LINUX_CLASSPATH="\\\$ISABELLE_HOME/$ENTRY"
77.165 - else
77.166 - LINUX_CLASSPATH="$LINUX_CLASSPATH:\\\$ISABELLE_HOME/$ENTRY"
77.167 - fi
77.168 - done
77.169 - cat "$ISABELLE_HOME/Admin/Linux/Isabelle.run" | \
77.170 - perl -p > "$ISABELLE_TARGET/${ISABELLE_NAME}.run" \
77.171 - -e "s,{JAVA_ARGS},$JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS,g; s,{CLASSPATH},$LINUX_CLASSPATH,;"
77.172 - chmod +x "$ISABELLE_TARGET/${ISABELLE_NAME}.run"
77.173 -
77.174 - mv "$ISABELLE_TARGET/contrib/linux_app" "$TMP/."
77.175 - cp "$TMP/linux_app/Isabelle" "$ISABELLE_TARGET/$ISABELLE_NAME"
77.176 - ;;
77.177 - macos)
77.178 - purge_contrib '-name "x86*-linux" -o -name "x86*-cygwin" -o -name "x86*-windows"'
77.179 - mv "$ISABELLE_TARGET/contrib/macos_app" "$TMP/."
77.180 -
77.181 - perl -pi \
77.182 - -e 's,\Qaction-bar.shortcut=C+ENTER\E,action-bar.shortcut=\naction-bar.shortcut2=C+ENTER,g;' \
77.183 - -e "s,lookAndFeel=.*,lookAndFeel=com.apple.laf.AquaLookAndFeel,g;" \
77.184 - -e "s,delete-line.shortcut=.*,delete-line.shortcut=C+d,g;" \
77.185 - -e "s,delete.shortcut2=.*,delete.shortcut2=A+d,g;" \
77.186 - -e "s,plugin-blacklist.MacOSX.jar=true,plugin-blacklist.MacOSX.jar=,g;" \
77.187 - "$ISABELLE_TARGET/src/Tools/jEdit/dist/properties/jEdit.props"
77.188 - ;;
77.189 - windows)
77.190 - purge_contrib '-name "x86*-linux" -o -name "x86*-darwin"'
77.191 - mv "$ISABELLE_TARGET/contrib/windows_app" "$TMP/."
77.192 -
77.193 - perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel,g;" \
77.194 - "$ISABELLE_TARGET/src/Tools/jEdit/dist/properties/jEdit.props"
77.195 -
77.196 - (
77.197 - cat "$ISABELLE_HOME/Admin/Windows/WinRun4J/Isabelle.ini"
77.198 -
77.199 - declare -a JAVA_ARGS=()
77.200 - eval "JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS)"
77.201 - A=2
77.202 - for ARG in "${JAVA_ARGS[@]}"
77.203 - do
77.204 - echo -e "vmarg.$A=$ARG\r"
77.205 - A=$[ $A + 1 ]
77.206 - done
77.207 -
77.208 - A=1
77.209 - for ENTRY in "${DISTRIBITION_CLASSPATH[@]}"
77.210 - do
77.211 - ENTRY=$(echo "$ENTRY" | perl -p -e 's,/,\\\\,g;')
77.212 - echo -e "classpath.$A=$ENTRY\r"
77.213 - A=$[ $A + 1 ]
77.214 - done
77.215 - ) > "$ISABELLE_TARGET/${ISABELLE_NAME}.ini"
77.216 -
77.217 - cp "$TMP/windows_app/Isabelle.exe" "$ISABELLE_TARGET/${ISABELLE_NAME}.exe"
77.218 - cp "$ISABELLE_HOME/Admin/Windows/WinRun4J/manifest.xml" "$ISABELLE_TARGET/${ISABELLE_NAME}.exe.manifest"
77.219 - cp "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Setup.bat" \
77.220 - "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Terminal.bat" "$ISABELLE_TARGET"
77.221 -
77.222 - (
77.223 - cd "$ISABELLE_TARGET"
77.224 -
77.225 - for NAME in postinstall rebaseall
77.226 - do
77.227 - cp -a "$ISABELLE_HOME/Admin/Windows/Cygwin/isabelle/$NAME" \
77.228 - "contrib/cygwin/isabelle/."
77.229 - done
77.230 -
77.231 - find . -type f -not -name '*.exe' -not -name '*.dll' -perm +100 \
77.232 - -print0 > "contrib/cygwin/isabelle/executables"
77.233 -
77.234 - find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" \
77.235 - > "contrib/cygwin/isabelle/symlinks"
77.236 -
77.237 - touch "contrib/cygwin/isabelle/uninitialized"
77.238 - )
77.239 -
77.240 - perl -pi -e "s,/bin/rebaseall.*,/isabelle/rebaseall,g;" \
77.241 - "$ISABELLE_TARGET/contrib/cygwin/etc/postinstall/autorebase.bat.done"
77.242 -
77.243 - ;;
77.244 - *)
77.245 - ;;
77.246 -esac
77.247 -
77.248 -
77.249 -# archive
77.250 -
77.251 -BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_${PLATFORM_FAMILY}.tar.gz"
77.252 -
77.253 -echo "packaging $(basename "$BUNDLE_ARCHIVE")"
77.254 -tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" "$ISABELLE_NAME" || exit 2
77.255 -
77.256 -
77.257 -# platform-specific setup (outside archive)
77.258 -
77.259 -if [ "$ISABELLE_PLATFORM_FAMILY" = linux -a "$PLATFORM_FAMILY" != macos -o "$ISABELLE_PLATFORM_FAMILY" = macos ]
77.260 -then
77.261 - case "$PLATFORM_FAMILY" in
77.262 - macos)
77.263 - echo "application for $PLATFORM_FAMILY"
77.264 - (
77.265 - cd "$TMP"
77.266 -
77.267 - APP_TEMPLATE="$ISABELLE_HOME/Admin/MacOS"
77.268 - APP="dmg/${ISABELLE_NAME}.app"
77.269 -
77.270 - mkdir -p "dmg/.background"
77.271 - cp "$APP_TEMPLATE/dmg/background.png" "dmg/.background/"
77.272 - cp "$APP_TEMPLATE/dmg/DS_Store" "dmg/.DS_Store"
77.273 - ln -s /Applications "dmg/."
77.274 -
77.275 - for NAME in Java MacOS PlugIns Resources
77.276 - do
77.277 - mkdir -p "$APP/Contents/$NAME"
77.278 - done
77.279 -
77.280 - (
77.281 - cat "$APP_TEMPLATE/Info.plist-part1"
77.282 -
77.283 - declare -a OPTIONS=()
77.284 - eval "OPTIONS=($ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS)"
77.285 - for OPT in "${OPTIONS[@]}"
77.286 - do
77.287 - echo "<string>$OPT</string>"
77.288 - done
77.289 - echo "<string>-Dapple.awt.application.name={ISABELLE_NAME}</string>"
77.290 -
77.291 - cat "$APP_TEMPLATE/Info.plist-part2"
77.292 - ) | perl -p -e "s,{ISABELLE_NAME},${ISABELLE_NAME},g;" > "$APP/Contents/Info.plist"
77.293 -
77.294 - for ENTRY in "${DISTRIBITION_CLASSPATH[@]}"
77.295 - do
77.296 - ln -sf "../Resources/${ISABELLE_NAME}/$ENTRY" "$APP/Contents/Java"
77.297 - done
77.298 -
77.299 - cp -R "$APP_TEMPLATE/Resources/." "$APP/Contents/Resources/."
77.300 -
77.301 - ln -sf "../Resources/${ISABELLE_NAME}/contrib/jdk/x86_64-darwin" \
77.302 - "$APP/Contents/PlugIns/jdk"
77.303 -
77.304 - cp macos_app/JavaAppLauncher "$APP/Contents/MacOS/." && \
77.305 - chmod +x "$APP/Contents/MacOS/JavaAppLauncher"
77.306 -
77.307 - mv "$ISABELLE_NAME" "$APP/Contents/Resources/."
77.308 - ln -sf "Contents/Resources/$ISABELLE_NAME" "$APP/Isabelle"
77.309 -
77.310 - rm -f "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg"
77.311 -
77.312 - cd dmg
77.313 - hdiutil create -srcfolder . -volname Isabelle "${ARCHIVE_DIR}/${ISABELLE_NAME}.dmg"
77.314 - )
77.315 - ;;
77.316 - windows)
77.317 - (
77.318 - cd "$TMP"
77.319 - rm -f "${ARCHIVE_DIR}/${ISABELLE_NAME}.7z"
77.320 - 7z -y -bd a "$TMP/${ISABELLE_NAME}.7z" "$ISABELLE_NAME" || exit 2
77.321 -
77.322 - echo "application for $PLATFORM_FAMILY"
77.323 - (
77.324 - cat "windows_app/7zsd_All.sfx"
77.325 - cat "$ISABELLE_HOME/Admin/Windows/Installer/sfx.txt" | \
77.326 - perl -p -e "s,{ISABELLE_NAME},${ISABELLE_NAME},g;"
77.327 - cat "$TMP/${ISABELLE_NAME}.7z"
77.328 - ) > "${ARCHIVE_DIR}/${ISABELLE_NAME}.exe"
77.329 - chmod +x "${ARCHIVE_DIR}/${ISABELLE_NAME}.exe"
77.330 - )
77.331 - ;;
77.332 - *)
77.333 - ;;
77.334 - esac
77.335 -else
77.336 - echo "### Cannot build application for $PLATFORM_FAMILY on $ISABELLE_PLATFORM_FAMILY"
77.337 -fi
77.338 -
77.339 -
77.340 -# clean up
77.341 -rm -rf "$TMP"
78.1 --- a/Admin/lib/Tools/makedist_cygwin Sat Apr 11 11:28:31 2015 +0200
78.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
78.3 @@ -1,80 +0,0 @@
78.4 -#!/usr/bin/env bash
78.5 -#
78.6 -# DESCRIPTION: produce pre-canned Cygwin distribution for Isabelle
78.7 -
78.8 -## global parameters
78.9 -
78.10 -CYGWIN_MIRROR="http://isabelle.in.tum.de/cygwin_2014"
78.11 -
78.12 -
78.13 -## diagnostics
78.14 -
78.15 -PRG=$(basename "$0")
78.16 -
78.17 -function usage()
78.18 -{
78.19 - echo
78.20 - echo "Usage: isabelle $PRG"
78.21 - echo
78.22 - echo " Produce pre-canned Cygwin distribution for Isabelle."
78.23 - echo
78.24 - exit 1
78.25 -}
78.26 -
78.27 -function fail()
78.28 -{
78.29 - echo "$1" >&2
78.30 - exit 2
78.31 -}
78.32 -
78.33 -
78.34 -## arguments
78.35 -
78.36 -[ "$#" -ne 0 ] && usage
78.37 -
78.38 -
78.39 -## main
78.40 -
78.41 -TARGET="$PWD/cygwin"
78.42 -
78.43 -
78.44 -# download
78.45 -
78.46 -[ ! -e "$TARGET" ] || fail "Target already exists: \"$TARGET\""
78.47 -mkdir -p "$TARGET/isabelle" || fail "Failed to create target directory: \"$TARGET\""
78.48 -
78.49 -perl -MLWP::Simple -e "getprint '$CYGWIN_MIRROR/setup-x86.exe';" > "$TARGET/isabelle/cygwin.exe"
78.50 -chmod +x "$TARGET/isabelle/cygwin.exe"
78.51 -
78.52 -"$TARGET/isabelle/cygwin.exe" -h </dev/null >/dev/null || exit 2
78.53 -
78.54 -
78.55 -# install
78.56 -
78.57 -"$TARGET/isabelle/cygwin.exe" \
78.58 - --site "$CYGWIN_MIRROR" --no-verify \
78.59 - --local-package-dir 'C:\temp' \
78.60 - --root "$(cygpath -w "$TARGET")" \
78.61 - --packages libgmp3,perl,perl_vendor,python,rlwrap,unzip,vim \
78.62 - --no-shortcuts --no-startmenu --no-desktop --quiet-mode
78.63 -
78.64 -[ "$?" = 0 -a -e "$TARGET/etc" ] || exit 2
78.65 -
78.66 -
78.67 -# patches
78.68 -
78.69 -for NAME in hosts protocols services networks passwd group
78.70 -do
78.71 - rm "$TARGET/etc/$NAME"
78.72 -done
78.73 -
78.74 -ln -s cygperl5_14.dll "$TARGET/bin/cygperl5_14_2.dll"
78.75 -
78.76 -rm "$TARGET/Cygwin.bat"
78.77 -
78.78 -
78.79 -# archive
78.80 -
78.81 -DATE=$(date +%Y%m%d)
78.82 -tar -C "$TARGET/.." -cz -f "cygwin-${DATE}.tar.gz" cygwin
78.83 -
79.1 --- a/Admin/lib/Tools/update_keywords Sat Apr 11 11:28:31 2015 +0200
79.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
79.3 @@ -1,15 +0,0 @@
79.4 -#!/usr/bin/env bash
79.5 -#
79.6 -# Author: Makarius
79.7 -#
79.8 -# DESCRIPTION: update standard keyword files for Emacs Proof General
79.9 -# (Proof General legacy)
79.10 -
79.11 -isabelle_admin_build jars || exit $?
79.12 -
79.13 -declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
79.14 -
79.15 -cd "$ISABELLE_HOME/etc"
79.16 -
79.17 -"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Keywords update_keywords
79.18 -
80.1 --- a/Admin/lib/scripts/churn_pie Sat Apr 11 11:28:31 2015 +0200
80.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
80.3 @@ -1,23 +0,0 @@
80.4 -#!/usr/bin/env python
80.5 -
80.6 -import re
80.7 -from pychart import theme, pie_plot, area, fill_style, arrow, legend
80.8 -import sys
80.9 -
80.10 -re_entry = re.compile(R'^(.*\S+)\s+(\d+)\s*\**\s*$')
80.11 -
80.12 -theme.get_options()
80.13 -
80.14 -data = []
80.15 -
80.16 -for line in sys.stdin.readlines():
80.17 - match = re_entry.match(line)
80.18 - data.append((match.group(1), int(match.group(2))))
80.19 -
80.20 -plot = pie_plot.T(data = data, arc_offsets = [],
80.21 - shadow = (2, -2, fill_style.gray50), label_offset = 10, arrow_style = arrow.a3)
80.22 -
80.23 -ar = area.T(size = (500, 500), legend = legend.T(), x_grid_style = None, y_grid_style = None)
80.24 -ar.add_plot(plot)
80.25 -
80.26 -ar.draw()
81.1 --- a/Admin/mira.py Sat Apr 11 11:28:31 2015 +0200
81.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
81.3 @@ -1,347 +0,0 @@
81.4 -"""
81.5 - Test configuration descriptions for mira.
81.6 -"""
81.7 -
81.8 -import os
81.9 -from os import path
81.10 -from glob import glob
81.11 -import subprocess
81.12 -from datetime import datetime
81.13 -import re
81.14 -
81.15 -import util
81.16 -
81.17 -from mira import schedule, misc
81.18 -from mira.environment import scheduler
81.19 -from mira import repositories
81.20 -
81.21 -# build and evaluation tools
81.22 -
81.23 -DEFAULT_TIMEOUT = 2 * 60 * 60
81.24 -SMLNJ_TIMEOUT = 72 * 60 * 60
81.25 -
81.26 -def prepare_isabelle_repository(loc_isabelle, loc_dependency_heaps, more_settings=''):
81.27 -
81.28 - # patch settings
81.29 - extra_settings = '''
81.30 -Z3_NON_COMMERCIAL="yes"
81.31 -
81.32 -init_components "/home/isabelle/contrib" "$ISABELLE_HOME/Admin/components/main"
81.33 -init_components "/home/isabelle/contrib" "$ISABELLE_HOME/Admin/components/optional"
81.34 -init_components "/home/isabelle/contrib" "$ISABELLE_HOME/Admin/components/nonfree"
81.35 -
81.36 -''' + more_settings
81.37 -
81.38 - writer = open(path.join(loc_isabelle, 'etc', 'settings'), 'a')
81.39 - writer.write(extra_settings)
81.40 - writer.close()
81.41 -
81.42 -
81.43 -def isabelle_getenv(isabelle_home, var):
81.44 -
81.45 - _, out = env.run_process('%s/bin/isabelle' % isabelle_home, 'getenv', var)
81.46 - return out.split('=', 1)[1].strip()
81.47 -
81.48 -
81.49 -def extract_isabelle_run_timing(logdata):
81.50 -
81.51 - def to_secs(h, m, s):
81.52 - return (int(h) * 60 + int(m)) * 60 + int(s)
81.53 - pat = r'Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time'
81.54 - pat2 = r'Timing (\S+) \((\d+) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time, factor (\d+\.\d+)\)'
81.55 - t = dict((name, {'elapsed': to_secs(eh,em,es), 'cpu': to_secs(ch,cm,cs)})
81.56 - for name, eh, em, es, ch, cm, cs in re.findall(pat, logdata))
81.57 - for name, threads, elapsed, cpu, gc, factor in re.findall(pat2, logdata):
81.58 -
81.59 - if name not in t:
81.60 - t[name] = {}
81.61 -
81.62 - t[name]['threads'] = int(threads)
81.63 - t[name]['elapsed_inner'] = elapsed
81.64 - t[name]['cpu_inner'] = cpu
81.65 - t[name]['gc'] = gc
81.66 - t[name]['factor'] = factor
81.67 -
81.68 - return t
81.69 -
81.70 -
81.71 -def extract_isabelle_run_summary(logdata):
81.72 -
81.73 - re_error = re.compile(r'^(?:make: )?\*\*\* (.*)$', re.MULTILINE)
81.74 - summary = '\n'.join(re_error.findall(logdata))
81.75 - if summary == '':
81.76 - summary = 'ok'
81.77 -
81.78 - return summary
81.79 -
81.80 -
81.81 -def extract_image_size(isabelle_home):
81.82 -
81.83 - isabelle_output = isabelle_getenv(isabelle_home, 'ISABELLE_OUTPUT')
81.84 - if not path.exists(isabelle_output):
81.85 - return {}
81.86 -
81.87 - return dict((p, path.getsize(path.join(isabelle_output, p))) for p in os.listdir(isabelle_output) if p != "log")
81.88 -
81.89 -def extract_report_data(isabelle_home, logdata):
81.90 -
81.91 - return {
81.92 - 'timing': extract_isabelle_run_timing(logdata),
81.93 - 'image_size': extract_image_size(isabelle_home) }
81.94 -
81.95 -
81.96 -def isabelle_build(env, case, paths, dep_paths, playground, *cmdargs, **kwargs):
81.97 -
81.98 - more_settings = kwargs.get('more_settings', '')
81.99 - keep_results = kwargs.get('keep_results', True)
81.100 - timeout = kwargs.get('timeout', DEFAULT_TIMEOUT)
81.101 -
81.102 - isabelle_home = paths[0]
81.103 -
81.104 - home_user_dir = path.join(isabelle_home, 'home_user')
81.105 - os.makedirs(home_user_dir)
81.106 -
81.107 - # copy over build results from dependencies
81.108 - heap_dir = path.join(isabelle_home, 'heaps')
81.109 - classes_dir = path.join(heap_dir, 'classes')
81.110 - os.makedirs(classes_dir)
81.111 -
81.112 - for dep_path in dep_paths:
81.113 - subprocess.check_call(['cp', '-a'] + glob(dep_path + '/*') + [heap_dir])
81.114 -
81.115 - subprocess.check_call(['ln', '-s', classes_dir, path.join(isabelle_home, 'lib', 'classes')])
81.116 - jars = glob(path.join(classes_dir, 'ext', '*.jar'))
81.117 - if jars:
81.118 - subprocess.check_call(['touch'] + jars)
81.119 -
81.120 - # misc preparations
81.121 - if 'lxbroy10' in misc.hostnames(): # special settings for lxbroy10
81.122 - more_settings += '''
81.123 -ISABELLE_GHC="/usr/bin/ghc"
81.124 -'''
81.125 -
81.126 - prepare_isabelle_repository(isabelle_home, None, more_settings=more_settings)
81.127 - os.chdir(isabelle_home)
81.128 -
81.129 - args = (['-o', 'timeout=%s' % timeout] if timeout is not None else []) + list(cmdargs)
81.130 -
81.131 - # invoke build tool
81.132 - (return_code, log1) = env.run_process('%s/bin/isabelle' % isabelle_home, 'jedit', '-bf',
81.133 - USER_HOME=home_user_dir)
81.134 - (return_code, log2) = env.run_process('%s/bin/isabelle' % isabelle_home, 'build', '-s', '-v', *args,
81.135 - USER_HOME=home_user_dir)
81.136 - log = log1 + log2
81.137 -
81.138 - # collect report
81.139 - return (return_code == 0, extract_isabelle_run_summary(log),
81.140 - extract_report_data(isabelle_home, log), {'log': log}, heap_dir if keep_results else None)
81.141 -
81.142 -
81.143 -
81.144 -# Isabelle configurations
81.145 -
81.146 -@configuration(repos = [Isabelle], deps = [])
81.147 -def Pure(*args):
81.148 - """Pure Image"""
81.149 - return isabelle_build(*(args + ("-b", "Pure")))
81.150 -
81.151 -@configuration(repos = [Isabelle], deps = [(Pure, [0])])
81.152 -def HOL(*args):
81.153 - """HOL Image"""
81.154 - return isabelle_build(*(args + ("-b", "HOL")))
81.155 -
81.156 -@configuration(repos = [Isabelle], deps = [(HOL, [0])])
81.157 -def HOL_Library(*args):
81.158 - """HOL Library"""
81.159 - return isabelle_build(*(args + ("-b", "HOL-Library")))
81.160 -
81.161 -@configuration(repos = [Isabelle], deps = [(HOL, [0])])
81.162 -def HOLCF(*args):
81.163 - """HOLCF"""
81.164 - return isabelle_build(*(args + ("-b", "HOLCF")))
81.165 -
81.166 -@configuration(repos = [Isabelle], deps = [(Pure, [0])])
81.167 -def ZF(*args):
81.168 - """HOLCF"""
81.169 - return isabelle_build(*(args + ("-b", "ZF")))
81.170 -
81.171 -
81.172 -settings64='''
81.173 -# enforce 64 bit, overriding smart detection
81.174 -ML_PLATFORM="$ISABELLE_PLATFORM64"
81.175 -ML_HOME="$(dirname $ML_HOME)/$ML_PLATFORM"
81.176 -'''
81.177 -
81.178 -@configuration(repos = [Isabelle], deps = [])
81.179 -def Isabelle_makeall(*args):
81.180 - """Build all sessions"""
81.181 - return isabelle_build(*(args + ("-j", "6", "-o", "threads=4", "-a")), more_settings=settings64, keep_results=False)
81.182 -
81.183 -
81.184 -# Mutabelle configurations
81.185 -
81.186 -def invoke_mutabelle(theory, env, case, paths, dep_paths, playground):
81.187 -
81.188 - """Mutant testing for counterexample generators in Isabelle"""
81.189 -
81.190 - (loc_isabelle,) = paths
81.191 - (dep_isabelle,) = dep_paths
81.192 - more_settings = '''
81.193 -ISABELLE_GHC="/usr/bin/ghc"
81.194 -'''
81.195 - prepare_isabelle_repository(loc_isabelle, dep_isabelle, more_settings = more_settings)
81.196 - os.chdir(loc_isabelle)
81.197 -
81.198 - (return_code, log) = env.run_process('bin/isabelle',
81.199 - 'mutabelle', '-O', playground, theory)
81.200 -
81.201 - try:
81.202 - mutabelle_log = util.readfile(path.join(playground, 'log'))
81.203 - except IOError:
81.204 - mutabelle_log = ''
81.205 -
81.206 - mutabelle_data = dict(
81.207 - (tool, {'counterexample': c, 'no_counterexample': n, 'timeout': t, 'error': e})
81.208 - for tool, c, n, t, e in re.findall(r'(\S+)\s+: C: (\d+) N: (\d+) T: (\d+) E: (\d+)', log))
81.209 -
81.210 - return (return_code == 0 and mutabelle_log != '', extract_isabelle_run_summary(log),
81.211 - {'mutabelle_results': {theory: mutabelle_data}},
81.212 - {'log': log, 'mutabelle_log': mutabelle_log}, None)
81.213 -
81.214 -@configuration(repos = [Isabelle], deps = [(HOL, [0])])
81.215 -def Mutabelle_Relation(*args):
81.216 - """Mutabelle regression suite on Relation theory"""
81.217 - return invoke_mutabelle('Relation', *args)
81.218 -
81.219 -@configuration(repos = [Isabelle], deps = [(HOL, [0])])
81.220 -def Mutabelle_List(*args):
81.221 - """Mutabelle regression suite on List theory"""
81.222 - return invoke_mutabelle('List', *args)
81.223 -
81.224 -@configuration(repos = [Isabelle], deps = [(HOL, [0])])
81.225 -def Mutabelle_Set(*args):
81.226 - """Mutabelle regression suite on Set theory"""
81.227 - return invoke_mutabelle('Set', *args)
81.228 -
81.229 -@configuration(repos = [Isabelle], deps = [(HOL, [0])])
81.230 -def Mutabelle_Map(*args):
81.231 - """Mutabelle regression suite on Map theory"""
81.232 - return invoke_mutabelle('Map', *args)
81.233 -
81.234 -@configuration(repos = [Isabelle], deps = [(HOL, [0])])
81.235 -def Mutabelle_Divides(*args):
81.236 - """Mutabelle regression suite on Divides theory"""
81.237 - return invoke_mutabelle('Divides', *args)
81.238 -
81.239 -@configuration(repos = [Isabelle], deps = [(HOL, [0])])
81.240 -def Mutabelle_MacLaurin(*args):
81.241 - """Mutabelle regression suite on MacLaurin theory"""
81.242 - return invoke_mutabelle('MacLaurin', *args)
81.243 -
81.244 -@configuration(repos = [Isabelle], deps = [(HOL, [0])])
81.245 -def Mutabelle_Fun(*args):
81.246 - """Mutabelle regression suite on Fun theory"""
81.247 - return invoke_mutabelle('Fun', *args)
81.248 -
81.249 -mutabelle_confs = 'Mutabelle_Relation Mutabelle_List Mutabelle_Set Mutabelle_Map Mutabelle_Divides Mutabelle_MacLaurin Mutabelle_Fun'.split(' ')
81.250 -
81.251 -@scheduler()
81.252 -def mutabelle_scheduler(env):
81.253 - """Scheduler for Mutabelle."""
81.254 - return schedule.age_scheduler(env, 'Isabelle', mutabelle_confs)
81.255 -
81.256 -
81.257 -# Judgement Day configurations
81.258 -
81.259 -judgement_day_provers = ('e', 'spass', 'vampire', 'z3', 'cvc3', 'yices')
81.260 -
81.261 -def judgement_day(base_path, theory, opts, env, case, paths, dep_paths, playground):
81.262 - """Judgement Day regression suite"""
81.263 -
81.264 - isa = paths[0]
81.265 - dep_path = dep_paths[0]
81.266 -
81.267 - os.chdir(path.join(playground, '..', base_path)) # Mirabelle requires specific cwd
81.268 - prepare_isabelle_repository(isa, dep_path)
81.269 -
81.270 - output = {}
81.271 - success_rates = {}
81.272 - some_success = False
81.273 -
81.274 - for atp in judgement_day_provers:
81.275 -
81.276 - log_dir = path.join(playground, 'mirabelle_log_' + atp)
81.277 - os.makedirs(log_dir)
81.278 -
81.279 - cmd = ('%s/bin/isabelle mirabelle -q -O %s sledgehammer[prover=%s,%s] %s.thy'
81.280 - % (isa, log_dir, atp, opts, theory))
81.281 -
81.282 - os.system(cmd)
81.283 - output[atp] = util.readfile(path.join(log_dir, theory + '.log'))
81.284 -
81.285 - percentages = list(re.findall(r'Success rate: (\d+)%', output[atp]))
81.286 - if len(percentages) == 2:
81.287 - success_rates[atp] = {
81.288 - 'sledgehammer': int(percentages[0]),
81.289 - 'metis': int(percentages[1])}
81.290 - if success_rates[atp]['sledgehammer'] > 0:
81.291 - some_success = True
81.292 - else:
81.293 - success_rates[atp] = {}
81.294 -
81.295 -
81.296 - data = {'success_rates': success_rates}
81.297 - raw_attachments = dict((atp + "_output", output[atp]) for atp in judgement_day_provers)
81.298 - # FIXME: summary?
81.299 - return (some_success, '', data, raw_attachments, None)
81.300 -
81.301 -
81.302 -@configuration(repos = [Isabelle], deps = [(HOL, [0])])
81.303 -def JD_NS(*args):
81.304 - """Judgement Day regression suite NS"""
81.305 - return judgement_day('Isabelle/src/HOL/Auth', 'NS_Shared', 'prover_timeout=10', *args)
81.306 -
81.307 -@configuration(repos = [Isabelle], deps = [(HOL, [0])])
81.308 -def JD_FTA(*args):
81.309 - """Judgement Day regression suite FTA"""
81.310 - return judgement_day('Isabelle/src/HOL/Library', 'Fundamental_Theorem_Algebra', 'prover_timeout=10', *args)
81.311 -
81.312 -@configuration(repos = [Isabelle], deps = [(HOL, [0])])
81.313 -def JD_Hoare(*args):
81.314 - """Judgement Day regression suite Hoare"""
81.315 - return judgement_day('Isabelle/src/HOL/IMPP', 'Hoare', 'prover_timeout=10', *args)
81.316 -
81.317 -@configuration(repos = [Isabelle], deps = [(HOL, [0])])
81.318 -def JD_SN(*args):
81.319 - """Judgement Day regression suite SN"""
81.320 - return judgement_day('Isabelle/src/HOL/Proofs/Lambda', 'StrongNorm', 'prover_timeout=10', *args)
81.321 -
81.322 -
81.323 -JD_confs = 'JD_NS JD_FTA JD_Hoare JD_SN JD_Arrow JD_FFT JD_Jinja JD_QE JD_S2S'.split(' ')
81.324 -
81.325 -@scheduler()
81.326 -def judgement_day_scheduler(env):
81.327 - """Scheduler for Judgement Day."""
81.328 - return schedule.age_scheduler(env, 'Isabelle', JD_confs)
81.329 -
81.330 -
81.331 -# SML/NJ
81.332 -
81.333 -smlnj_settings = '''
81.334 -ML_SYSTEM=smlnj
81.335 -ML_HOME="/home/smlnj/110.76/bin"
81.336 -ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
81.337 -ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
81.338 -'''
81.339 -
81.340 -@configuration(repos = [Isabelle], deps = [(Pure, [0])])
81.341 -def SML_HOL(*args):
81.342 - """HOL image built with SML/NJ"""
81.343 - return isabelle_build(*(args + ("-b", "HOL")), more_settings=smlnj_settings, timeout=SMLNJ_TIMEOUT)
81.344 -
81.345 -@configuration(repos = [Isabelle], deps = [])
81.346 -def SML_makeall(*args):
81.347 - """SML/NJ build of all possible sessions"""
81.348 - return isabelle_build(*(args + ("-j", "3", "-a")), more_settings=smlnj_settings, timeout=SMLNJ_TIMEOUT)
81.349 -
81.350 -
82.1 --- a/Admin/polyml/CHECKLIST Sat Apr 11 11:28:31 2015 +0200
82.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
82.3 @@ -1,15 +0,0 @@
82.4 -Notes on building Poly/ML as Isabelle component
82.5 -===============================================
82.6 -
82.7 -* copy README
82.8 -
82.9 -* copy build
82.10 -
82.11 -* copy etc/settings
82.12 -
82.13 -* include full source (without symlink)
82.14 -
82.15 -* include sha1 source and binary for each platform
82.16 -
82.17 -* linux: include copy of libgmp.so with symlinks from build host
82.18 -
83.1 --- a/Admin/polyml/README Sat Apr 11 11:28:31 2015 +0200
83.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
83.3 @@ -1,24 +0,0 @@
83.4 -Poly/ML for Isabelle
83.5 -====================
83.6 -
83.7 -This compilation of Poly/ML 5.5.2 is based on
83.8 -http://sourceforge.net/p/polyml/code/HEAD/tree/fixes-5.5.2 version
83.9 -1955. See also fixes-5.5.2.diff for the differences to the official
83.10 -source distribution polyml.5.5.2.tar.gz from
83.11 -http://sourceforge.net/projects/polyml/.
83.12 -
83.13 -
83.14 -The included build script is used like this:
83.15 -
83.16 - ./build src x86-linux --with-gmp
83.17 - ./build src x86_64-linux --with-gmp
83.18 - ./build src x86-darwin --without-gmp
83.19 - ./build src x86_64-darwin --without-gmp
83.20 - ./build src x86-cygwin --with-gmp
83.21 -
83.22 -Also note that the separate "sha1" library module is required for
83.23 -efficient digesting of strings according to SHA-1.
83.24 -
83.25 -
83.26 - Makarius
83.27 - 25-Jul-2014
84.1 --- a/Admin/polyml/build Sat Apr 11 11:28:31 2015 +0200
84.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
84.3 @@ -1,95 +0,0 @@
84.4 -#!/usr/bin/env bash
84.5 -#
84.6 -# Multi-platform build script for Poly/ML
84.7 -
84.8 -THIS="$(cd "$(dirname "$0")"; pwd)"
84.9 -PRG="$(basename "$0")"
84.10 -
84.11 -
84.12 -# diagnostics
84.13 -
84.14 -function usage()
84.15 -{
84.16 - echo
84.17 - echo "Usage: $PRG SOURCE TARGET [OPTIONS]"
84.18 - echo
84.19 - echo " Build Poly/ML in SOURCE directory for given platform in TARGET,"
84.20 - echo " using the usual Isabelle platform identifiers."
84.21 - echo
84.22 - echo " Additional options for ./configure may be given, e.g. --with-gmp"
84.23 - echo
84.24 - exit 1
84.25 -}
84.26 -
84.27 -function fail()
84.28 -{
84.29 - echo "$1" >&2
84.30 - exit 2
84.31 -}
84.32 -
84.33 -
84.34 -# command line args
84.35 -
84.36 -[ "$#" -eq 0 ] && usage
84.37 -SOURCE="$1"; shift
84.38 -
84.39 -[ "$#" -eq 0 ] && usage
84.40 -TARGET="$1"; shift
84.41 -
84.42 -USER_OPTIONS=("$@")
84.43 -
84.44 -
84.45 -# main
84.46 -
84.47 -[ -d "$SOURCE" ] || fail "Bad source directory: \"$SOURCE\""
84.48 -
84.49 -case "$TARGET" in
84.50 - x86-linux)
84.51 - OPTIONS=()
84.52 - ;;
84.53 - x86_64-linux)
84.54 - OPTIONS=()
84.55 - ;;
84.56 - x86-darwin)
84.57 - OPTIONS=(--build=i686-darwin CFLAGS='-arch i686 -O3 -I../libffi/include'
84.58 - CXXFLAGS='-arch i686 -O3 -I../libffi/include' CCASFLAGS='-arch i686 -O3'
84.59 - LDFLAGS='-segprot POLY rwx rwx')
84.60 - ;;
84.61 - x86_64-darwin)
84.62 - OPTIONS=(--build=x86_64-darwin CFLAGS='-arch x86_64 -O3 -I../libffi/include'
84.63 - CXXFLAGS='-arch x86_64 -O3 -I../libffi/include' CCASFLAGS='-arch x86_64'
84.64 - LDFLAGS='-segprot POLY rwx rwx')
84.65 - ;;
84.66 - x86-cygwin)
84.67 - OPTIONS=()
84.68 - ;;
84.69 - x86-windows)
84.70 - OPTIONS=()
84.71 - ;;
84.72 - x86_64-windows)
84.73 - OPTIONS=()
84.74 - ;;
84.75 - *)
84.76 - fail "Bad platform identifier: \"$TARGET\""
84.77 - ;;
84.78 -esac
84.79 -
84.80 -(
84.81 - cd "$SOURCE"
84.82 - make distclean
84.83 -
84.84 - { ./configure --prefix="$PWD/$TARGET" "${OPTIONS[@]}" "${USER_OPTIONS[@]}" && \
84.85 - make compiler && \
84.86 - make compiler && \
84.87 - make install; } || fail "Build failed"
84.88 -)
84.89 -
84.90 -mkdir -p "$TARGET"
84.91 -mv "$SOURCE/$TARGET/bin/"* "$TARGET/"
84.92 -mv "$SOURCE/$TARGET/lib/"* "$TARGET/"
84.93 -rmdir "$SOURCE/$TARGET/bin" "$SOURCE/$TARGET/lib"
84.94 -rm -rf "$SOURCE/$TARGET/share"
84.95 -
84.96 -if [ "$TARGET" = x86-cygwin ]; then
84.97 - peflags -x8192000 -z500 "$TARGET/poly.exe"
84.98 -fi
85.1 --- a/Admin/polyml/settings Sat Apr 11 11:28:31 2015 +0200
85.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
85.3 @@ -1,50 +0,0 @@
85.4 -# -*- shell-script -*- :mode=shellscript:
85.5 -
85.6 -POLYML_HOME="$COMPONENT"
85.7 -
85.8 -
85.9 -# basic settings
85.10 -
85.11 -#ML_SYSTEM=polyml-5.5.2
85.12 -#ML_PLATFORM="$ISABELLE_PLATFORM32"
85.13 -#ML_HOME="$POLYML_HOME/$ML_PLATFORM"
85.14 -#ML_OPTIONS="-H 500"
85.15 -#ML_SOURCES="$POLYML_HOME/src"
85.16 -
85.17 -
85.18 -# smart settings
85.19 -
85.20 -ML_SYSTEM=polyml-5.5.2
85.21 -
85.22 -case "$ISABELLE_PLATFORM" in
85.23 - *-linux)
85.24 - if env LD_LIBRARY_PATH="$POLYML_HOME/$ISABELLE_PLATFORM32:$LD_LIBRARY_PATH" \
85.25 - "$POLYML_HOME/$ISABELLE_PLATFORM32/poly" -v >/dev/null 2>/dev/null
85.26 - then
85.27 - ML_PLATFORM="$ISABELLE_PLATFORM32"
85.28 - else
85.29 - ML_PLATFORM="$ISABELLE_PLATFORM64"
85.30 - if [ -z "$ML_PLATFORM_FALLBACK" ]; then
85.31 - echo >&2 "### Cannot execute Poly/ML in 32bit mode (missing shared libraries for C/C++)"
85.32 - echo >&2 "### Using bulky 64bit version of Poly/ML instead"
85.33 - ML_PLATFORM_FALLBACK="true"
85.34 - fi
85.35 - fi
85.36 - ;;
85.37 - *)
85.38 - ML_PLATFORM="$ISABELLE_PLATFORM32"
85.39 - ;;
85.40 -esac
85.41 -
85.42 -case "$ML_PLATFORM" in
85.43 - x86_64-*)
85.44 - ML_OPTIONS="-H 1000"
85.45 - ;;
85.46 - *)
85.47 - ML_OPTIONS="-H 500"
85.48 - ;;
85.49 -esac
85.50 -
85.51 -ML_HOME="$POLYML_HOME/$ML_PLATFORM"
85.52 -ML_SOURCES="$POLYML_HOME/src"
85.53 -
86.1 --- a/Admin/user-aliases Sat Apr 11 11:28:31 2015 +0200
86.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
86.3 @@ -1,23 +0,0 @@
86.4 -lcp paulson
86.5 -lp15@cam.ac.uk paulson
86.6 -norbert.schirmer@web.de schirmer
86.7 -schirmer@in.tum.de schirmer
86.8 -urbanc@in.tum.de urbanc
86.9 -nipkow@lapbroy100.local nipkow
86.10 -chaieb@chaieb-laptop chaieb
86.11 -immler@in.tum.de immler
86.12 -tsewell@rubicon.NSW.bigpond.net.au tsewell
86.13 -tsewell@nicta.com.au tsewell
86.14 -thomas.sewell@nicta.com.au tsewell
86.15 -kaliszyk@in.tum.de kaliszyk
86.16 -Philipp\ Meyer meyerp
86.17 -noschinl@in.tum.de noschinl
86.18 -Lars Noschinski\ <noschinl@in.tum.de> noschinl
86.19 -brianh@cs.pdx.edu huffman
86.20 -nik sultana
86.21 -griff Christian Sternagel
86.22 -cezarykaliszyk@gmail.com kaliszyk
86.23 -hellerar@macbroy24.informatik.tu-muenchen.de hellerar
86.24 -tbourke Timothy Bourke
86.25 -gerwin.klein@nicta.com.au kleing
86.26 -Gerwin\ Klein\ <gerwin.klein@nicta.com.au> kleing
87.1 Binary file Isabelle2014 has changed
88.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
88.2 +++ b/Isabelle2014.run Tue Apr 14 13:41:48 2015 +0200
88.3 @@ -0,0 +1,31 @@
88.4 +#!/usr/bin/env bash
88.5 +#
88.6 +# Author: Makarius
88.7 +#
88.8 +# Main Isabelle application script.
88.9 +
88.10 +# dereference executable
88.11 +if [ -L "$0" ]; then
88.12 + TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
88.13 + exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
88.14 +fi
88.15 +
88.16 +
88.17 +# minimal Isabelle environment
88.18 +
88.19 +ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; pwd)"
88.20 +source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
88.21 +
88.22 +
88.23 +# main
88.24 +
88.25 +#paranoia setting -- avoid problems of Java/Swing versus XIM/IBus etc.
88.26 +unset XMODIFIERS
88.27 +
88.28 +exec "$ISABELLE_HOME/contrib/jdk/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/bin/java" \
88.29 + "-Disabelle.home=$ISABELLE_HOME" \
88.30 + -Xms128m -Xmx1024m -Xss2m -Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle \
88.31 + -classpath "$ISABELLE_HOME/lib/classes/Pure.jar:$ISABELLE_HOME/contrib/jfreechart-1.0.14-1/lib/iText-2.1.5.jar:$ISABELLE_HOME/contrib/jfreechart-1.0.14-1/lib/jcommon-1.0.18.jar:$ISABELLE_HOME/contrib/jfreechart-1.0.14-1/lib/jfreechart-1.0.14.jar:$ISABELLE_HOME/contrib/jortho-1.0-2/jortho.jar:$ISABELLE_HOME/contrib/scala-2.11.2/lib/akka-actor_2.11-2.3.4.jar:$ISABELLE_HOME/contrib/scala-2.11.2/lib/config-1.2.1.jar:$ISABELLE_HOME/contrib/scala-2.11.2/lib/jline-2.12.jar:$ISABELLE_HOME/contrib/scala-2.11.2/lib/scala-actors-2.11.0.jar:$ISABELLE_HOME/contrib/scala-2.11.2/lib/scala-actors-migration_2.11-1.1.0.jar:$ISABELLE_HOME/contrib/scala-2.11.2/lib/scala-compiler.jar:$ISABELLE_HOME/contrib/scala-2.11.2/lib/scala-continuations-library_2.11-1.0.2.jar:$ISABELLE_HOME/contrib/scala-2.11.2/lib/scala-continuations-plugin_2.11.2-1.0.2.jar:$ISABELLE_HOME/contrib/scala-2.11.2/lib/scala-library.jar:$ISABELLE_HOME/contrib/scala-2.11.2/lib/scala-parser-combinators_2.11-1.0.2.jar:$ISABELLE_HOME/contrib/scala-2.11.2/lib/scala-reflect.jar:$ISABELLE_HOME/contrib/scala-2.11.2/lib/scala-swing_2.11-1.0.1.jar:$ISABELLE_HOME/contrib/scala-2.11.2/lib/scala-xml_2.11-1.0.2.jar:$ISABELLE_HOME/contrib/scala-2.11.2/lib/scalap-2.11.2.jar:$ISABELLE_HOME/contrib/xz-java-1.2-1/lib/xz.jar:$ISABELLE_HOME/src/Tools/jEdit/dist/jedit.jar" \
88.32 + "-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \
88.33 + isabelle.Main "$@"
88.34 +
89.1 --- a/README Sat Apr 11 11:28:31 2015 +0200
89.2 +++ b/README Tue Apr 14 13:41:48 2015 +0200
89.3 @@ -2,7 +2,7 @@
89.4
89.5 Version information
89.6
89.7 - This is some unidentified repository version of Isabelle2013.
89.8 + This is Isabelle2014: August 2014.
89.9
89.10 See the NEWS file in the distribution for details on user-relevant
89.11 changes.
90.1 --- a/ROOTS Sat Apr 11 11:28:31 2015 +0200
90.2 +++ b/ROOTS Tue Apr 14 13:41:48 2015 +0200
90.3 @@ -9,5 +9,6 @@
90.4 src/LCF
90.5 src/Sequents
90.6 src/Doc
90.7 +src/Tools
90.8 src/Tools/isac
90.9 test/Tools/isac/ADDTESTS/session-get_theory/
91.1 --- a/etc/components Sat Apr 11 11:28:31 2015 +0200
91.2 +++ b/etc/components Tue Apr 14 13:41:48 2015 +0200
91.3 @@ -9,4 +9,17 @@
91.4 src/HOL/Tools/ATP
91.5 src/HOL/TPTP
91.6 #bundled components
91.7 -contrib/ProofGeneral-4.2
91.8 +contrib/cvc3-2.4.1
91.9 +contrib/e-1.8
91.10 +contrib/exec_process-1.0.3
91.11 +contrib/Haskabelle-2014
91.12 +contrib/jdk
91.13 +contrib/jfreechart-1.0.14-1
91.14 +contrib/jortho-1.0-2
91.15 +contrib/kodkodi-1.5.2
91.16 +contrib/polyml-5.5.2-1
91.17 +contrib/scala-2.11.2
91.18 +contrib/spass-3.8ds
91.19 +contrib/z3-3.2-1
91.20 +contrib/z3-4.3.2pre-1
91.21 +contrib/xz-java-1.2-1
92.1 --- a/lib/scripts/getsettings Sat Apr 11 11:28:31 2015 +0200
92.2 +++ b/lib/scripts/getsettings Tue Apr 14 13:41:48 2015 +0200
92.3 @@ -76,8 +76,8 @@
92.4 fi
92.5
92.6 #Isabelle distribution identifier -- filled in automatically!
92.7 -ISABELLE_ID=""
92.8 -[ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER=""
92.9 +ISABELLE_ID="8f4a332500e4"
92.10 +[ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER="Isabelle2014"
92.11
92.12 #sometimes users put strange things in here ...
92.13 unset ENV
93.1 --- a/src/Pure/ROOT.ML Sat Apr 11 11:28:31 2015 +0200
93.2 +++ b/src/Pure/ROOT.ML Tue Apr 14 13:41:48 2015 +0200
93.3 @@ -4,8 +4,8 @@
93.4
93.5 structure Distribution = (*filled-in by makedist*)
93.6 struct
93.7 - val version = "unidentified repository version";
93.8 - val is_identified = false;
93.9 + val version = "repository version: Isabelle2014: August 2014 + Isabelle/Isac";
93.10 + val is_identified = true;
93.11 val is_official = false;
93.12 end;
93.13
94.1 --- a/src/Pure/ROOT.scala Sat Apr 11 11:28:31 2015 +0200
94.2 +++ b/src/Pure/ROOT.scala Tue Apr 14 13:41:48 2015 +0200
94.3 @@ -9,8 +9,8 @@
94.4 {
94.5 object Distribution /*filled-in by makedist*/
94.6 {
94.7 - val version = "unidentified repository version"
94.8 - val is_identified = false
94.9 + val version = "repository version: Isabelle2014: August 2014 + Isabelle/Isac"
94.10 + val is_identified = true
94.11 val is_official = false
94.12 }
94.13 }
