--- a/Admin/isatest/crontab.lxbroy10 Wed Jul 13 17:20:21 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-03 00 * * * $HOME/bin/checkout-admin
-17 00 * * * $HOME/bin/isatest-makedist
-01 08 * * * $HOME/bin/isatest-check
-
-04 23 31 1,3,5,7,8,10,12 * $HOME/bin/logmove
-04 23 30 4,6,9,11 * $HOME/bin/logmove
-04 23 28 2 * $HOME/bin/logmove
--- a/Admin/isatest/crontab.macbroy2 Wed Jul 13 17:20:21 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-MAILTO=isatest@mailbroy.informatik.tu-muenchen.de
-
-28 06 * * 0-5 $HOME/afp/devel/admin/regression -
-28 06 * * 6 export ISABELLE_FULL_TEST=true && $HOME/afp/devel/admin/regression -
-# 17 11 * * 6 $HOME/afp/devel/admin/regression -f -
-# 32 11 * * 0 $HOME/afp/release/admin/regression Isabelle2011-1
-
--- a/Admin/isatest/isatest-check Wed Jul 13 17:20:21 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,106 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Gerwin Klein, TU Muenchen
-#
-# DESCRIPTION: sends email for failed tests, checks for error.log,
-# generates development snapshot if test ok
-
-## global settings
-. ~/admin/isatest/isatest-settings
-
-# produce empty list for patterns like isatest-*.log if no
-# such file exists
-shopt -s nullglob
-
-# mail program
-MAIL=$HOME/bin/pmail
-
-# tmp file for sending mail
-TMP=/tmp/isatest-makedist.$$
-
-export DISTPREFIX
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: $PRG"
- echo
- echo " sends email for failed tests, checks for error.log,"
- echo " generates development snapshot if test ok."
- echo " To be called by cron."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-## main
-
-# check if tests are still running, wait for them a couple of hours
-i=0
-while [ -n "$(ls $RUNNING)" -a $i -lt 40 ]; do
- sleep 900
- let "i = i+1"
-done
-
-FAIL=0
-
-# still running -> give up
-if [ -n "$(ls $RUNNING)" ]; then
- echo "Giving up waiting for test to finish at $(date)." > $TMP
- echo >> $TMP
- echo "Sessions still running:" >> $TMP
- echo "$(ls $RUNNING)" >> $TMP
- echo >> $TMP
- echo "Attaching all error logs collected so far." >> $TMP
- echo >> $TMP
-
- if [ -e $ERRORLOG ]; then
- cat $ERRORLOG >> $TMP
- fi
-
- echo "Have a nice day," >> $TMP
- echo " isatest" >> $TMP
-
- for R in $MAILTO; do
- LOGS=$ERRORDIR/isatest*.log
- $MAIL "isabelle test taking too long" $R $TMP $LOGS
- done
-
- rm $TMP
-
- FAIL=1
-elif [ -e $ERRORLOG ]; then
- # no tests running, check if there were errors
- cat $ERRORLOG > $TMP
- echo "Have a nice day," >> $TMP
- echo " isatest" >> $TMP
-
- for R in $MAILTO; do
- LOGS=$ERRORDIR/isatest*.log
- $MAIL "isabelle test failed" $R $TMP $LOGS
- done
-
- rm $TMP
-fi
-
-# generate development snapshot page only for successful tests
-# (failures in experimental sessions ok)
-if [ "$FAIL"=="0" -a "$(echo $ERRORDIR/isatest*[^e].log)" == "$(echo)" ]; then
- (cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isabelle getenv -b ISABELLE_IDENTIFIER` make)
- log "generated development snapshot web page."
-else
- log "test failures, no web snapshot generated."
-fi
-
-exit 0
-## end
--- a/Admin/isatest/isatest-makeall Wed Jul 13 17:20:21 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,158 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Gerwin Klein, TU Muenchen
-#
-# DESCRIPTION: Run isabelle build from specified distribution and settings.
-
-## global settings
-. ~/admin/isatest/isatest-settings
-
-# max time until test is aborted (in sec)
-MAXTIME=28800
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: $PRG [-x SESSION] [-l SESSIONS] settings1 [settings2 ...]"
- echo
- echo " Runs isabelle build for specified settings."
- echo " Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
- echo
- echo "Examples:"
- echo " $PRG ~/settings/at-poly"
- echo " $PRG -l \"HOL-Library HOL-Bali\" ~/settings/at-poly"
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- log "FAILED, $1"
- exit 2
-}
-
-
-## main
-
-# argument checking
-
-[ "$1" = "-?" ] && usage
-[ "$#" -lt "1" ] && usage
-
-[ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
-
-# build args and nice setup for different target platforms
-BUILD_ARGS="-v"
-NICE="nice"
-case $HOSTNAME in
- macbroy2 | macbroy6 | macbroy30)
- NICE=""
- ;;
- lxbroy[234])
- BUILD_ARGS="$BUILD_ARGS -j 2"
- NICE=""
- ;;
-
-esac
-
-ISABELLE_TOOL="$DISTPREFIX/Isabelle/bin/isabelle"
-[ -x $ISABELLE_TOOL ] || fail "Cannot run $ISABELLE_TOOL"
-
-ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)"
-
-if [ "$1" = "-x" ]; then
- shift
- [ "$#" -lt 2 ] && usage
- BUILD_ARGS="$BUILD_ARGS -x $1"
- shift
-fi
-
-if [ "$1" = "-l" ]; then
- shift
- [ "$#" -lt 2 ] && usage
- BUILD_ARGS="$BUILD_ARGS $1"
- shift
-else
- BUILD_ARGS="$BUILD_ARGS -a"
-fi
-
-IDENT=$(cat "$DISTPREFIX/ISABELLE_IDENT")
-
-
-# main test loop
-
-log "starting [$@]"
-
-for SETTINGS in $@; do
-
- [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
-
- BUILD_ARGS="-o timeout=10800 $BUILD_ARGS"
-
- # logfile setup
-
- DATE=$(date "+%Y-%m-%d")
- SHORT=${SETTINGS##*/}
-
- if [ "${SHORT%-e}" == "$SHORT" ]; then
- # normal test
- TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
- else
- # experimental test
- TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME-e.log
- fi
-
- # the test
-
- touch $RUNNING/$SHORT.running
-
- echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
-
- echo "Isabelle version: $IDENT" >> $TESTLOG 2>&1
-
- if [ "${ISABELLE_HOME_USER:0:14}" == "/tmp/isabelle-" ]; then
- echo "--- cleaning up old $ISABELLE_HOME_USER"
- rm -rf $ISABELLE_HOME_USER
- fi
-
- cp $DISTPREFIX/Isabelle/etc/settings.orig $DISTPREFIX/Isabelle/etc/settings
- cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
- (ulimit -t $MAXTIME; $NICE "$ISABELLE_TOOL" build $BUILD_ARGS >> $TESTLOG 2>&1)
-
- if [ $? -eq 0 ]
- then
- # test log and cleanup
- echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
- gzip -f $TESTLOG
- else
- # test log
- echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
-
- # error log
- echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG
- echo "[...]" >> $ERRORLOG
- tail -4 $TESTLOG >> $ERRORLOG
- echo >> $ERRORLOG
-
- FAIL="$FAIL$SHORT "
- (cd $ERRORDIR; cp $TESTLOG .)
- fi
-
- rm -f $RUNNING/$SHORT.running
-done
-
-# time and success/failure to master log
-ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
-
-if [ -z "$FAIL" ]; then
- log "all tests successful, elapsed time $ELAPSED."
-else
- log "targets ${FAIL}FAILED, elapsed time $ELAPSED."
- exit 1
-fi
-
--- a/Admin/isatest/isatest-makedist Wed Jul 13 17:20:21 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,122 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Gerwin Klein, TU Muenchen
-#
-# DESCRIPTION: Build distribution and run isatest-make for lots of platforms.
-
-## global settings
-. "$HOME/hg-isabelle/Admin/isatest/isatest-settings"
-
-TMP=/tmp/isatest-makedist.$$
-MAIL=$HOME/bin/pmail
-
-MAKEALL=$HOME/bin/isatest-makeall
-TAR=tar
-
-SSH="ssh -f"
-
-export THIS_IS_ISATEST_MAKEDIST=true
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: $PRG"
- echo
- echo " Build distribution and run isatest-make for lots of platforms."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## main
-
-# cleanup old error log and test-still-running files
-rm -f $ERRORLOG
-rm -f $ERRORDIR/isatest-*.log
-rm -f $RUNNING/*.runnning
-
-export DISTPREFIX
-
-DATE=$(date "+%Y-%m-%d")
-DISTLOG=$LOGPREFIX/isatest-makedist-$DATE.log
-
-echo ------------------- preparing test release --- `date` --- $HOSTNAME > $DISTLOG 2>&1
-
-echo "### cleaning up old dist directory" >> $DISTLOG 2>&1
-rm -rf $DISTPREFIX >> $DISTLOG 2>&1
-
-echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1
-rm -rf $HOME/isabelle-*
-
-echo "### building distribution" >> $DISTLOG 2>&1
-mkdir -p $DISTPREFIX
-"$HOME/hg-isabelle/bin/isabelle" makedist >> $DISTLOG 2>&1
-
-if [ $? -ne 0 ]
-then
- echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
- ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
- log "dist build FAILED, elapsed time $ELAPSED."
-
- echo "Could not build isabelle distribution. Log file available at" > $TMP
- echo "$HOSTNAME:$DISTLOG" >> $TMP
-
- for R in $MAILTO; do
- $MAIL "isabelle dist build failed" $R $TMP
- done
-
- rm $TMP
-
- exit 1
-fi
-
-cd $DISTPREFIX >> $DISTLOG 2>&1
-ISABELLE_DIST=`cat $DISTPREFIX/ISABELLE_DIST`
-$TAR xvzf $ISABELLE_DIST >> $DISTLOG 2>&1
-ln -sf $(basename $ISABELLE_DIST .tar.gz) Isabelle
-cp Isabelle/etc/settings Isabelle/etc/settings.orig
-
-echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
-
-ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
-log "dist build successful, elapsed time $ELAPSED."
-
-
-## clean up var/running
-rm -f $RUNNING/*
-mkdir -p $RUNNING
-
-
-## spawn test runs
-
-$SSH lxbroy10 "$MAKEALL -x HOL-Proofs $HOME/settings/at64-poly"
-sleep 15
-$SSH lxbroy4 "$MAKEALL -l HOL-Library $HOME/settings/at-poly"
-sleep 15
-$SSH macbroy2 "
- $MAKEALL $HOME/settings/mac-poly64-M4;
- $MAKEALL $HOME/settings/mac-poly64-M8;
- $MAKEALL $HOME/settings/mac-poly-M4;
- $MAKEALL $HOME/settings/mac-poly-M8;
- $MAKEALL $HOME/settings/mac-poly-M8-skip_proofs;
- $MAKEALL $HOME/settings/mac-poly-M8-quick_and_dirty"
-sleep 15
-$SSH macbroy30 "$MAKEALL $HOME/settings/mac-poly-M2"
-sleep 15
-$SSH macbroy31 "$MAKEALL $HOME/settings/mac-poly64-M2"
-
-echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
-
-gzip -f $DISTLOG
-
--- a/Admin/isatest/isatest-settings Wed Jul 13 17:20:21 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-#
-# Author: Gerwin Klein, NICTA
-#
-# DESCRIPTION: common settings for the isatest-* scripts
-
-# source bashrc, we're called by cron
-. ~/.bashrc
-
-# canoncical home for all platforms
-HOME=/home/isatest
-
-## send email on failure to
-MAILTO="\
-kleing@cse.unsw.edu.au \
-nipkow@in.tum.de \
-berghofe@in.tum.de \
-lp15@cam.ac.uk \
-makarius@sketis.net \
-blanchet@in.tum.de \
-boehmes@in.tum.de \
-bulwahn@in.tum.de \
-hoelzl@in.tum.de \
-krauss@in.tum.de \
-noschinl@in.tum.de \
-kuncar@in.tum.de \
-ns441@cam.ac.uk \
-traytel@in.tum.de"
-
-LOGPREFIX=$HOME/log
-MASTERLOG=$LOGPREFIX/isatest.log
-LOGSERVER=lxbroy10.informatik.tu-muenchen.de
-
-ERRORDIR=$HOME/var
-ERRORLOG=$ERRORDIR/error.log
-
-RUNNING=$HOME/var/running
-
-DISTPREFIX=$HOME/isadist
-
-HOSTNAME="$(hostname -s)"
-
-# this function avoids NFS inconsistencies with multiple writers by
-# sshing to one central machine and writing locally. There is stil a
-# race condition, but at least it should not corrupt a whole set of entries
-# any more.
-function log()
-{
- MSG="$1"
- TIMESTAMP="$(date)"
- echo "[$TIMESTAMP $HOSTNAME $PRG]: $MSG" | ssh $LOGSERVER "cat >> $MASTERLOG"
-}
--- a/Admin/isatest/isatest-statistics Wed Jul 13 17:20:21 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,112 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: Produce statistics from isatest session logs.
-
-## platform settings
-
-case $(uname) in
- SunOS)
- ZGREP=xgrep
- TE="png color"
- ;;
- *)
- ZGREP=zgrep
- TE="png"
- ;;
-esac
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: $PRG DIR PLATFORM TIMESPAN SESSIONS..."
- echo
- echo " Produce statistics from isatest session logs, looking TIMESPAN"
- echo " days into the past. Outputs .png files into DIR."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## arguments
-
-[ "$1" = "-?" ] && usage
-[ "$#" -lt "4" ] && usage
-
-DIR="$1"; shift
-PLATFORM="$1"; shift
-TIMESPAN="$1"; shift
-SESSIONS="$@"
-
-case "$PLATFORM" in
- *para* | *-M* | afp)
- PARALLEL=true
- ;;
- *)
- PARALLEL=false
- ;;
-esac
-
-if [ "$PLATFORM" = afp ]; then
- LOG_DIR=~isatest/afp/log
- LOG_NAME="afp-test-devel*"
-else
- LOG_DIR=~isatest/log
- LOG_NAME="isatest-makeall-${PLATFORM}*"
-fi
-
-
-## main
-
-ALL_DATA="/tmp/isatest-all$$.dat"
-SESSION_DATA="/tmp/isatest$$.dat"
-mkdir -p "$DIR" || fail "Bad directory: $DIR"
-
-$ZGREP "^Finished .*elapsed" \
- $(find "$LOG_DIR" -name "$LOG_NAME" -mtime "-${TIMESPAN}") | \
-perl -e '
- while (<>) {
- if (m/(\d\d\d\d)-(\d\d)-(\d\d).*:Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time/) {
- my $year = $1;
- my $month = $2;
- my $day = $3;
- my $name = $4;
- my $elapsed_time = ($5 * 3600 + $6 * 60 + $7) / 60;
- my $cpu_time = ($8 * 3600 + $9 * 60 + $10) / 60;
-
- printf "$name $year-$month-$day %.2f %.2f\n", $cpu_time, $elapsed_time;
- }
- }' > "$ALL_DATA"
-
-for SESSION in $SESSIONS
-do
- grep "^${SESSION} " "$ALL_DATA" > "$SESSION_DATA"
- PLOT="plot [] [0:] \"$SESSION_DATA\" using 2:3 smooth sbezier title \"interpolated cpu time\", \"$SESSION_DATA\" using 2:3 smooth csplines title \"cpu time\""
- if [ "$PARALLEL" = true ]; then
- PLOT="${PLOT}, \"$SESSION_DATA\" using 2:4 smooth sbezier title \"interpolated elapsed time\", \"$SESSION_DATA\" using 2:4 smooth csplines title \"elapsed time\""
- fi
- gnuplot <<EOF
-set terminal $TE
-set output "$DIR/${SESSION}.png"
-set xdata time
-set timefmt "%Y-%m-%d"
-set format x "%d-%b"
-set xlabel "$SESSION"
-set key left top
-$PLOT
-EOF
-done
-
-rm -f "$ALL_DATA" "$SESSION_DATA"
--- a/Admin/isatest/isatest-stats Wed Jul 13 17:20:21 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,385 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: Standard statistics.
-
-THIS="$(cd "$(dirname "$0")"; pwd)"
-
-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"
-
-ISABELLE_SESSIONS="
- HOL
- HOL-Algebra
- HOL-Auth
- HOL-Bali
- HOL-Cardinals
- HOL-Codegenerator_Test
- HOL-Datatype_Examples
- HOL-Decision_Procs
- HOL-Eisbach
- HOL-Hahn_Banach
- HOL-Hoare
- HOL-Hoare_Parallel
- HOL-IMP
- HOL-IMPP
- HOL-IOA
- HOL-Imperative_HOL
- HOL-Import
- HOL-Induct
- HOL-Isar_Examples
- HOL-Lattice
- HOL-Library
- HOL-Matrix_LP
- HOL-Metis_Examples
- HOL-MicroJava
- HOL-Mirabelle
- HOL-Mirabelle-ex
- HOL-Multivariate_Analysis
- HOL-Multivariate_Analysis-ex
- HOL-Mutabelle
- HOL-NSA
- HOL-NSA-Examples
- HOL-NanoJava
- HOL-Nitpick_Examples
- HOL-Nominal
- HOL-Nominal-Examples
- HOL-Number_Theory
- HOL-Old_Number_Theory
- HOL-Predicate_Compile_Examples
- HOL-Probability
- HOL-Prolog
- HOL-Proofs
- HOL-Proofs-Extraction
- HOL-Proofs-Lambda
- HOL-Proofs-ex
- HOL-Quickcheck_Benchmark
- HOL-Quickcheck_Examples
- HOL-Quotient_Examples
- HOL-Record_Benchmark
- HOL-SET_Protocol
- HOL-SPARK
- HOL-SPARK-Examples
- HOL-SPARK-Manual
- HOL-Statespace
- HOL-TLA
- HOL-TLA-Buffer
- HOL-TLA-Inc
- HOL-TLA-Memory
- HOL-TPTP
- HOL-UNITY
- HOL-Unix
- HOL-Word
- HOL-Word-Examples
- HOL-Word-SMT_Examples
- HOL-ZF
- HOL-ex
- HOLCF
- HOLCF-FOCUS
- HOLCF-IMP
- HOLCF-Library
- HOLCF-Tutorial
- HOLCF-ex
- IOA
- IOA-ABP
- IOA-NTP
- IOA-Storage
- IOA-ex
- Pure
- Spec_Check
- ZF
- ZF-AC
- ZF-Coind
- ZF-Constructible
- ZF-IMP
- ZF-Induct
- ZF-Resid
- ZF-UNITY
- ZF-ex
-"
-
-AFP_SESSIONS="
- AODV
- AVL-Trees
- AWN
- Abortable_Linearizable_Modules
- Abstract-Hoare-Logics
- Abstract-Rewriting
- Abstract_Completeness
- Affine_Arithmetic
- Akra_Bazzi
- Amortized_Complexity
- ArrowImpossibilityGS
- AutoFocus-Stream
- Automatic_Refinement
- BDD
- BinarySearchTree
- Binomial-Heaps
- Binomial-Queues
- Bondy
- Boolean_Expression_Checkers
- Bounded_Deducibility_Security
- BytecodeLogicJmlTypes
- CAVA_Automata
- CAVA_Base
- CAVA_LTL_Modelchecker
- CAVA_buildchain1
- CAVA_buildchain3
- CCS
- CISC-Kernel
- Call_Arity
- Case_Labeling
- Category
- Category2
- Cauchy
- Cayley_Hamilton
- Certification_Monads
- Circus
- ClockSynchInst
- CofGroups
- Coinductive
- Coinductive_Languages
- Collections
- Collections_Examples
- Compiling-Exceptions-Correctly
- Completeness
- ComponentDependencies
- ConcurrentGC
- ConcurrentIMP
- Consensus_Refined
- Containers
- Containers-Benchmarks
- CoreC++
- CryptoBasedCompositionalProperties
- DPT-SAT-Solver
- DataRefinementIBP
- Datatype_Order_Generator
- Decreasing-Diagrams
- Decreasing-Diagrams-II
- Density_Compiler
- Depth-First-Search
- Derangements
- Deriving
- Dijkstra_Shortest_Path
- Discrete_Summation
- DiskPaxos
- Dynamic_Tables
- Echelon_Form
- Efficient-Mergesort
- Encodability_Process_Calculi
- Example-Submission
- FFT
- FOL-Fitting
- FeatherweightJava
- Featherweight_OCL
- Fermat3_4
- FileRefinement
- FinFun
- Finger-Trees
- Finite_Automata_HF
- Flyspeck-Tame
- FocusStreamsCaseStudies
- Formula_Derivatives
- Formula_Derivatives-Examples
- Free-Boolean-Algebra
- Free-Groups
- FunWithFunctions
- FunWithTilings
- Functional-Automata
- GPU_Kernel_PL
- Gabow_SCC
- Gauss-Jordan-Elim-Fun
- Gauss_Jordan
- GenClock
- General-Triangle
- Girth_Chromatic
- GoedelGod
- GraphMarkingIBP
- Graph_Theory
- Group-Ring-Module
- HOLCF-HOL-Library
- HOLCF-Nominal2
- HRB-Slicing
- Heard_Of
- HereditarilyFinite
- Hermite
- HotelKeyCards
- Huffman
- HyperCTL
- IEEE_Floating_Point
- Imperative_Insertion_Sort
- Impossible_Geometry
- Incompleteness
- Inductive_Confidentiality
- InformationFlowSlicing
- InformationFlowSlicing_Inter
- InformationFlowSlicing_Intra
- Integration
- JNF-AFP-Lib
- JNF-HOL-Lib
- Jinja
- JinjaThreads
- JiveDataStoreModel
- Jordan_Hoelder
- Jordan_Normal_Form
- KAT_and_DRA
- KBPs
- Kleene_Algebra
- Koenigsberg_Friendship
- Koenigsberg_Friendship_Base
- LTL_to_GBA
- Lam-ml-Normalization
- Landau_Symbols
- LatticeProperties
- Launchbury
- Lazy-Lists-II
- Lehmer
- Lifting_Definition_Option
- LightweightJava
- LinearQuantifierElim
- List-Index
- List-Infinite
- List_Interleaving
- Locally-Nameless-Sigma
- Lower_Semicontinuous
- MSO_Examples
- MSO_Regex_Equivalence
- Markov_Models
- Marriage
- Matrix
- Max-Card-Matching
- MiniML
- MonoBoolTranAlgebra
- MuchAdoAboutTwo
- Multirelations
- Myhill-Nerode
- Nat-Interval-Logic
- Native_Word
- Network_Security_Policy_Verification
- Nominal2
- Noninterference_CSP
- Noninterference_Generic_Unwinding
- Noninterference_Inductive_Unwinding
- Noninterference_Ipurge_Unwinding
- NormByEval
- Old_Datatype_Show
- Open_Induction
- Ordinal
- Ordinals_and_Cardinals
- Ordinary_Differential_Equations
- PCF
- POPLmark-deBruijn
- Partial_Function_MR
- Perfect-Number-Thm
- Pi_Calculus
- Polynomials
- Pop_Refinement
- Possibilistic_Noninterference
- Pratt_Certificate
- Presburger-Automata
- Priority_Queue_Braun
- Probabilistic_Noninterference
- Probabilistic_System_Zoo
- Probabilistic_System_Zoo-BNFs
- Probabilistic_System_Zoo-Non_BNFs
- Program-Conflict-Analysis
- Promela
- PseudoHoops
- Psi_Calculi
- QR_Decomposition
- RIPEMD-160-SPARK
- RSAPSS
- Ramsey-Infinite
- Random_Graph_Subgraph_Threshold
- Rank_Nullity_Theorem
- Real_Impl
- Recursion-Theory-I
- Refine_Monadic
- RefinementReactive
- Regex_Equivalence
- Regex_Equivalence_Examples
- Regular-Sets
- Regular_Algebras
- Relation_Algebra
- Rep_Fin_Groups
- Residuated_Lattices
- Ribbon_Proofs
- Robbins-Conjecture
- Roy_Floyd_Warshall
- SATSolverVerification
- SIFPL
- SIFUM_Type_Systems
- Secondary_Sylow
- Selection_Heap_Sort
- SenSocialChoice
- Separation_Algebra
- Separation_Logic_Imperative_HOL
- SequentInvertibility
- Shivers-CFA
- ShortestPath
- Show
- Simpl
- Skew_Heap
- Slicing
- Sort_Encodings
- Special_Function_Bounds
- Splay_Tree
- Sqrt_Babylonian
- Statecharts
- Stream-Fusion
- Stream_Fusion_Code
- Strong_Security
- Sturm_Sequences
- Sturm_Tarski
- Stuttering_Equivalence
- SumSquares
- TLA
- Tail_Recursive_Functions
- Tarskis_Geometry
- Topology
- Transitive-Closure
- Transitive-Closure-II
- Tree-Automata
- Trie
- Tycon
- UPF
- UpDown_Scheme
- Valuation
- VectorSpace
- Verified-Prover
- Vickrey_Clarke_Groves
- VolpanoSmith
- WHATandWHERE_Security
- Well_Quasi_Orders
- WorkerWrapper
- XML
- pGCL
-"
-
-for PLATFORM in $PLATFORMS
-do
- if [ "$PLATFORM" = afp ]; then
- SESSIONS="$AFP_SESSIONS"
- else
- SESSIONS="$ISABELLE_SESSIONS"
- fi
-
- "$THIS/isatest-statistics" "stats/$PLATFORM" "$PLATFORM" ${1:-100} $SESSIONS
- cat > "stats/$PLATFORM.html" <<EOF
-<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
-<html>
-<head><title>Development Snapshot -- Performance Statistics</title></head>
-
-<body>
-<h1>$PLATFORM</h1>
-EOF
-
-for SESSION in $SESSIONS
-do
- echo "<br><img src="$PLATFORM/$SESSION.png"><br>" >> "stats/$PLATFORM.html"
-done
-
-echo "</body>" >> "stats/$PLATFORM.html"
-echo "</html>" >> "stats/$PLATFORM.html"
-
-done
--- a/Admin/isatest/pmail Wed Jul 13 17:20:21 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Gerwin Klein, TU Muenchen
-#
-# DESCRIPTION: send email with text attachments.
-# (works for "mail" command of SunOS 5.8)
-#
-
-PRG="$(basename "$0")"
-
-MIME_BOUNDARY="==PM_=_37427935"
-
-function usage()
-{
- echo
- echo "Usage: $PRG subject recipient <body> [<attachments>]"
- echo
- echo " Send email with text attachments. <body> is a file."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-#
-# print_attachment <file>
-#
-# print mime "encoded" <file> to stdout (text/plain, 8bit)
-#
-function print_attachment()
-{
- local FILE=$1
- local NAME=${FILE##*/}
-
- cat <<EOF
---$MIME_BOUNDARY
-Content-Type: text/plain
-Content-Transfer-Encoding: 8bit
-Content-Disposition: attachment; filename="$NAME"
-
-EOF
- cat $FILE
- echo
-}
-
-
-#
-# print_body subject <message-file> [<attachments>]
-#
-# prints mime "encoded" message with text attachments to stdout
-#
-function print_body()
-{
- local SUBJECT=$1
- local BODY=$2
- local TO=$3
- shift 3
-
- cat <<EOF
-Subject: $SUBJECT
-To: $TO
-Mime-Version: 1.0
-Content-Type: multipart/mixed; boundary="$MIME_BOUNDARY"
-
---$MIME_BOUNDARY
-Content-Type: text/plain
-Content-Transfer-Encoding: 8bit
-
-EOF
- cat $BODY
- echo
-
- for a in $@; do print_attachment $a; done
-
- echo "--$MIME_BOUNDARY--"
- echo
-}
-
-## main
-
-# argument checking
-
-[ "$1" = "-?" ] && usage
-[ "$#" -lt "3" ] && usage
-
-SUBJECT="$1"
-TO="$2"
-BODY="$3"
-
-shift 3
-
-[ -r "$BODY" ] || fail "could not read $BODY"
-
-case `hostname` in
- lxbroy*)
- print_body "$SUBJECT" "$BODY" "$TO" $@ | sendmail "$TO"
- ;;
- macbroy*) for F in $@; do ATTACH="$ATTACH -a $F"; done
- cat "$BODY" | mail -s "$SUBJECT" $ATTACH "$TO"
- ;;
- sunbroy*)
- print_body "$SUBJECT" "$BODY" "$TO" $@ | mail -t "$TO"
- ;;
- *)
- fail "unknown host/platform"
- ;;
-esac
--- a/Admin/isatest/settings/afp-poly Wed Jul 13 17:20:21 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-init_components /home/isabelle/contrib "$HOME/admin/components/main"
-
-ML_PLATFORM="$ISABELLE_PLATFORM64"
-ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-ML_OPTIONS="-H 2000"
-
-ISABELLE_GHC=ghc
-
-ISABELLE_HOME_USER=~/afp/isabelle-afp-poly
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_BUILD_OPTIONS="parallel_proofs=2"
-
--- a/Admin/isatest/settings/at-poly Wed Jul 13 17:20:21 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-init_components /home/isabelle/contrib "$HOME/admin/components/main"
-
-ML_OPTIONS="-H 1000 --gcthreads 1"
-
-ISABELLE_GHC=/usr/bin/ghc
-
-ISABELLE_HOME_USER=~/isabelle-at-poly
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_BUILD_OPTIONS="browser_info=true document=pdf"
-
-ISABELLE_GHC=ghc
-#ISABELLE_MLTON=mlton
-ISABELLE_OCAML=ocaml
-ISABELLE_OCAMLC=ocamlc
-ISABELLE_POLYML="$ML_HOME/poly"
-ISABELLE_SCALA="$SCALA_HOME/bin"
-ISABELLE_SMLNJ="/home/smlnj/bin/sml"
--- a/Admin/isatest/settings/at64-poly Wed Jul 13 17:20:21 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-init_components /home/isabelle/contrib "$HOME/admin/components/main"
-
-ML_PLATFORM="$ISABELLE_PLATFORM64"
-ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-ML_OPTIONS="--minheap 2000 --maxheap 8000 --gcthreads 4"
-
-ISABELLE_HOME_USER=~/isabelle-at64-poly
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_BUILD_OPTIONS="threads=1"
--- a/Admin/isatest/settings/mac-poly-M2 Wed Jul 13 17:20:21 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-init_components /home/isabelle/contrib "$HOME/admin/components/main"
-init_components /home/isabelle/contrib "$HOME/admin/components/optional"
-init_components /home/isabelle/contrib "$HOME/admin/components/nonfree"
-
-ML_PLATFORM="$ISABELLE_PLATFORM32"
-ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-ML_OPTIONS="-H 1000 --gcthreads 4"
-
-ISABELLE_GHC=ghc
-
-ISABELLE_HOME_USER=~/isabelle-mac-poly-M2
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_BUILD_OPTIONS="browser_info=true document=pdf threads=2 parallel_proofs=2"
--- a/Admin/isatest/settings/mac-poly-M4 Wed Jul 13 17:20:21 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-init_components /home/isabelle/contrib "$HOME/admin/components/main"
-init_components /home/isabelle/contrib "$HOME/admin/components/optional"
-init_components /home/isabelle/contrib "$HOME/admin/components/nonfree"
-
-ML_PLATFORM="$ISABELLE_PLATFORM32"
-ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-ML_OPTIONS="-H 1000 --gcthreads 4"
-
-ISABELLE_HOME_USER=~/isabelle-mac-poly-M4
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_BUILD_OPTIONS="browser_info=false document=pdf document_variants=document:outline=/proof,/ML threads=4 parallel_proofs=2"
-
-ISABELLE_GHC=ghc
-ISABELLE_MLTON=mlton
-ISABELLE_OCAML=ocaml
-ISABELLE_OCAMLC=ocamlc
-ISABELLE_POLYML="$ML_HOME/poly"
-#ISABELLE_SCALA="$SCALA_HOME/bin"
-ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"
--- a/Admin/isatest/settings/mac-poly-M8 Wed Jul 13 17:20:21 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-init_components /home/isabelle/contrib "$HOME/admin/components/main"
-init_components /home/isabelle/contrib "$HOME/admin/components/optional"
-init_components /home/isabelle/contrib "$HOME/admin/components/nonfree"
-
-ML_PLATFORM="$ISABELLE_PLATFORM32"
-ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-ML_OPTIONS="-H 1000 --gcthreads 8"
-
-ISABELLE_HOME_USER=~/isabelle-mac-poly-M8
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_BUILD_OPTIONS="browser_info=false document=pdf document_variants=document:outline=/proof,/ML threads=8 parallel_proofs=2"
-
-ISABELLE_GHC=ghc
-ISABELLE_MLTON=mlton
-ISABELLE_OCAML=ocaml
-ISABELLE_OCAMLC=ocamlc
-ISABELLE_POLYML="$ML_HOME/poly"
-#ISABELLE_SCALA="$SCALA_HOME/bin"
-ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"
--- a/Admin/isatest/settings/mac-poly-M8-quick_and_dirty Wed Jul 13 17:20:21 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-init_components /home/isabelle/contrib "$HOME/admin/components/main"
-init_components /home/isabelle/contrib "$HOME/admin/components/optional"
-init_components /home/isabelle/contrib "$HOME/admin/components/nonfree"
-
-ML_PLATFORM="$ISABELLE_PLATFORM32"
-ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-ML_OPTIONS="-H 1000 --gcthreads 8"
-
-ISABELLE_HOME_USER=~/isabelle-mac-poly-M8-quick_and_dirty
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_BUILD_OPTIONS="threads=8 quick_and_dirty"
-
-ISABELLE_GHC=ghc
-ISABELLE_MLTON=mlton
-ISABELLE_OCAML=ocaml
-ISABELLE_OCAMLC=ocamlc
-ISABELLE_POLYML="$ML_HOME/poly"
-#ISABELLE_SCALA="$SCALA_HOME/bin"
-ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"
--- a/Admin/isatest/settings/mac-poly-M8-skip_proofs Wed Jul 13 17:20:21 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-init_components /home/isabelle/contrib "$HOME/admin/components/main"
-init_components /home/isabelle/contrib "$HOME/admin/components/optional"
-init_components /home/isabelle/contrib "$HOME/admin/components/nonfree"
-
-ML_PLATFORM="$ISABELLE_PLATFORM32"
-ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-ML_OPTIONS="-H 1000 --gcthreads 8"
-
-ISABELLE_HOME_USER=~/isabelle-mac-poly-M8-skip_proofs
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_BUILD_OPTIONS="threads=8 skip_proofs"
-
-ISABELLE_GHC=ghc
-ISABELLE_MLTON=mlton
-ISABELLE_OCAML=ocaml
-ISABELLE_OCAMLC=ocamlc
-ISABELLE_POLYML="$ML_HOME/poly"
-#ISABELLE_SCALA="$SCALA_HOME/bin"
-ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"
--- a/Admin/isatest/settings/mac-poly64-M2 Wed Jul 13 17:20:21 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-init_components /home/isabelle/contrib "$HOME/admin/components/main"
-init_components /home/isabelle/contrib "$HOME/admin/components/optional"
-init_components /home/isabelle/contrib "$HOME/admin/components/nonfree"
-
-ML_PLATFORM="$ISABELLE_PLATFORM64"
-ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-ML_OPTIONS="-H 2000 --gcthreads 2"
-
-ISABELLE_GHC=ghc
-
-ISABELLE_HOME_USER=~/isabelle-at-mac-poly64-M2
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_BUILD_OPTIONS="browser_info=false document=false threads=2 parallel_proofs=2"
--- a/Admin/isatest/settings/mac-poly64-M4 Wed Jul 13 17:20:21 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-init_components /home/isabelle/contrib "$HOME/admin/components/main"
-init_components /home/isabelle/contrib "$HOME/admin/components/optional"
-init_components /home/isabelle/contrib "$HOME/admin/components/nonfree"
-
-ML_PLATFORM="$ISABELLE_PLATFORM64"
-ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-ML_OPTIONS="-H 2000 --gcthreads 4"
-
-ISABELLE_HOME_USER=~/isabelle-mac-poly64-M4
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_BUILD_OPTIONS="browser_info=false document=false threads=4 parallel_proofs=2"
-
-ISABELLE_GHC=ghc
-ISABELLE_MLTON=mlton
-ISABELLE_OCAML=ocaml
-ISABELLE_OCAMLC=ocamlc
-ISABELLE_POLYML="$ML_HOME/poly"
-#ISABELLE_SCALA="$SCALA_HOME/bin"
-ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"
--- a/Admin/isatest/settings/mac-poly64-M8 Wed Jul 13 17:20:21 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-init_components /home/isabelle/contrib "$HOME/admin/components/main"
-init_components /home/isabelle/contrib "$HOME/admin/components/optional"
-init_components /home/isabelle/contrib "$HOME/admin/components/nonfree"
-
-ML_PLATFORM="$ISABELLE_PLATFORM64"
-ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-ML_OPTIONS="-H 2000 --gcthreads 8"
-
-ISABELLE_HOME_USER=~/isabelle-mac-poly64-M8
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_BUILD_OPTIONS="browser_info=false document=false threads=8 parallel_proofs=2"
-
-ISABELLE_GHC=ghc
-ISABELLE_MLTON=mlton
-ISABELLE_OCAML=ocaml
-ISABELLE_OCAMLC=ocamlc
-ISABELLE_POLYML="$ML_HOME/poly"
-#ISABELLE_SCALA="$SCALA_HOME/bin"
-ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"
--- a/Admin/mira.py Wed Jul 13 17:20:21 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,346 +0,0 @@
-"""
- Test configuration descriptions for mira.
-"""
-
-import os
-from os import path
-from glob import glob
-import subprocess
-from datetime import datetime
-import re
-
-import util
-
-from mira import schedule, misc
-from mira.environment import scheduler
-from mira import repositories
-
-# build and evaluation tools
-
-DEFAULT_TIMEOUT = 2 * 60 * 60
-SMLNJ_TIMEOUT = 72 * 60 * 60
-
-def prepare_isabelle_repository(loc_isabelle, loc_dependency_heaps, more_settings=''):
-
- # patch settings
- extra_settings = '''
-
-init_components "/home/isabelle/contrib" "$ISABELLE_HOME/Admin/components/main"
-init_components "/home/isabelle/contrib" "$ISABELLE_HOME/Admin/components/optional"
-init_components "/home/isabelle/contrib" "$ISABELLE_HOME/Admin/components/nonfree"
-
-''' + more_settings
-
- writer = open(path.join(loc_isabelle, 'etc', 'settings'), 'a')
- writer.write(extra_settings)
- writer.close()
-
-
-def isabelle_getenv(isabelle_home, var):
-
- _, out = env.run_process('%s/bin/isabelle' % isabelle_home, 'getenv', var)
- return out.split('=', 1)[1].strip()
-
-
-def extract_isabelle_run_timing(logdata):
-
- def to_secs(h, m, s):
- return (int(h) * 60 + int(m)) * 60 + int(s)
- pat = r'Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time'
- pat2 = r'Timing (\S+) \((\d+) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time, factor (\d+\.\d+)\)'
- t = dict((name, {'elapsed': to_secs(eh,em,es), 'cpu': to_secs(ch,cm,cs)})
- for name, eh, em, es, ch, cm, cs in re.findall(pat, logdata))
- for name, threads, elapsed, cpu, gc, factor in re.findall(pat2, logdata):
-
- if name not in t:
- t[name] = {}
-
- t[name]['threads'] = int(threads)
- t[name]['elapsed_inner'] = elapsed
- t[name]['cpu_inner'] = cpu
- t[name]['gc'] = gc
- t[name]['factor'] = factor
-
- return t
-
-
-def extract_isabelle_run_summary(logdata):
-
- re_error = re.compile(r'^(?:make: )?\*\*\* (.*)$', re.MULTILINE)
- summary = '\n'.join(re_error.findall(logdata))
- if summary == '':
- summary = 'ok'
-
- return summary
-
-
-def extract_image_size(isabelle_home):
-
- isabelle_output = isabelle_getenv(isabelle_home, 'ISABELLE_OUTPUT')
- if not path.exists(isabelle_output):
- return {}
-
- return dict((p, path.getsize(path.join(isabelle_output, p))) for p in os.listdir(isabelle_output) if p != "log")
-
-def extract_report_data(isabelle_home, logdata):
-
- return {
- 'timing': extract_isabelle_run_timing(logdata),
- 'image_size': extract_image_size(isabelle_home) }
-
-
-def isabelle_build(env, case, paths, dep_paths, playground, *cmdargs, **kwargs):
-
- more_settings = kwargs.get('more_settings', '')
- keep_results = kwargs.get('keep_results', True)
- timeout = kwargs.get('timeout', DEFAULT_TIMEOUT)
-
- isabelle_home = paths[0]
-
- home_user_dir = path.join(isabelle_home, 'home_user')
- os.makedirs(home_user_dir)
-
- # copy over build results from dependencies
- heap_dir = path.join(isabelle_home, 'heaps')
- classes_dir = path.join(heap_dir, 'classes')
- os.makedirs(classes_dir)
-
- for dep_path in dep_paths:
- subprocess.check_call(['cp', '-a'] + glob(dep_path + '/*') + [heap_dir])
-
- subprocess.check_call(['ln', '-s', classes_dir, path.join(isabelle_home, 'lib', 'classes')])
- jars = glob(path.join(classes_dir, 'ext', '*.jar'))
- if jars:
- subprocess.check_call(['touch'] + jars)
-
- # misc preparations
- if 'lxbroy10' in misc.hostnames(): # special settings for lxbroy10
- more_settings += '''
-ISABELLE_GHC="/usr/bin/ghc"
-'''
-
- prepare_isabelle_repository(isabelle_home, None, more_settings=more_settings)
- os.chdir(isabelle_home)
-
- args = (['-o', 'timeout=%s' % timeout] if timeout is not None else []) + list(cmdargs)
-
- # invoke build tool
- (return_code, log1) = env.run_process('%s/bin/isabelle' % isabelle_home, 'jedit', '-bf',
- USER_HOME=home_user_dir)
- (return_code, log2) = env.run_process('%s/bin/isabelle' % isabelle_home, 'build', '-s', '-v', *args,
- USER_HOME=home_user_dir)
- log = log1 + log2
-
- # collect report
- return (return_code == 0, extract_isabelle_run_summary(log),
- extract_report_data(isabelle_home, log), {'log': log}, heap_dir if keep_results else None)
-
-
-
-# Isabelle configurations
-
-@configuration(repos = [Isabelle], deps = [])
-def Pure(*args):
- """Pure Image"""
- return isabelle_build(*(args + ("-b", "Pure")))
-
-@configuration(repos = [Isabelle], deps = [(Pure, [0])])
-def HOL(*args):
- """HOL Image"""
- return isabelle_build(*(args + ("-b", "HOL")))
-
-@configuration(repos = [Isabelle], deps = [(HOL, [0])])
-def HOL_Library(*args):
- """HOL Library"""
- return isabelle_build(*(args + ("-b", "HOL-Library")))
-
-@configuration(repos = [Isabelle], deps = [(HOL, [0])])
-def HOLCF(*args):
- """HOLCF"""
- return isabelle_build(*(args + ("-b", "HOLCF")))
-
-@configuration(repos = [Isabelle], deps = [(Pure, [0])])
-def ZF(*args):
- """HOLCF"""
- return isabelle_build(*(args + ("-b", "ZF")))
-
-
-settings64='''
-# enforce 64 bit, overriding smart detection
-ML_PLATFORM="$ISABELLE_PLATFORM64"
-ML_HOME="$(dirname $ML_HOME)/$ML_PLATFORM"
-'''
-
-@configuration(repos = [Isabelle], deps = [])
-def Isabelle_makeall(*args):
- """Build all sessions"""
- return isabelle_build(*(args + ("-j", "6", "-o", "threads=4", "-a")), more_settings=settings64, keep_results=False)
-
-
-# Mutabelle configurations
-
-def invoke_mutabelle(theory, env, case, paths, dep_paths, playground):
-
- """Mutant testing for counterexample generators in Isabelle"""
-
- (loc_isabelle,) = paths
- (dep_isabelle,) = dep_paths
- more_settings = '''
-ISABELLE_GHC="/usr/bin/ghc"
-'''
- prepare_isabelle_repository(loc_isabelle, dep_isabelle, more_settings = more_settings)
- os.chdir(loc_isabelle)
-
- (return_code, log) = env.run_process('bin/isabelle',
- 'mutabelle', '-O', playground, theory)
-
- try:
- mutabelle_log = util.readfile(path.join(playground, 'log'))
- except IOError:
- mutabelle_log = ''
-
- mutabelle_data = dict(
- (tool, {'counterexample': c, 'no_counterexample': n, 'timeout': t, 'error': e})
- for tool, c, n, t, e in re.findall(r'(\S+)\s+: C: (\d+) N: (\d+) T: (\d+) E: (\d+)', log))
-
- return (return_code == 0 and mutabelle_log != '', extract_isabelle_run_summary(log),
- {'mutabelle_results': {theory: mutabelle_data}},
- {'log': log, 'mutabelle_log': mutabelle_log}, None)
-
-@configuration(repos = [Isabelle], deps = [(HOL, [0])])
-def Mutabelle_Relation(*args):
- """Mutabelle regression suite on Relation theory"""
- return invoke_mutabelle('Relation', *args)
-
-@configuration(repos = [Isabelle], deps = [(HOL, [0])])
-def Mutabelle_List(*args):
- """Mutabelle regression suite on List theory"""
- return invoke_mutabelle('List', *args)
-
-@configuration(repos = [Isabelle], deps = [(HOL, [0])])
-def Mutabelle_Set(*args):
- """Mutabelle regression suite on Set theory"""
- return invoke_mutabelle('Set', *args)
-
-@configuration(repos = [Isabelle], deps = [(HOL, [0])])
-def Mutabelle_Map(*args):
- """Mutabelle regression suite on Map theory"""
- return invoke_mutabelle('Map', *args)
-
-@configuration(repos = [Isabelle], deps = [(HOL, [0])])
-def Mutabelle_Divides(*args):
- """Mutabelle regression suite on Divides theory"""
- return invoke_mutabelle('Divides', *args)
-
-@configuration(repos = [Isabelle], deps = [(HOL, [0])])
-def Mutabelle_MacLaurin(*args):
- """Mutabelle regression suite on MacLaurin theory"""
- return invoke_mutabelle('MacLaurin', *args)
-
-@configuration(repos = [Isabelle], deps = [(HOL, [0])])
-def Mutabelle_Fun(*args):
- """Mutabelle regression suite on Fun theory"""
- return invoke_mutabelle('Fun', *args)
-
-mutabelle_confs = 'Mutabelle_Relation Mutabelle_List Mutabelle_Set Mutabelle_Map Mutabelle_Divides Mutabelle_MacLaurin Mutabelle_Fun'.split(' ')
-
-@scheduler()
-def mutabelle_scheduler(env):
- """Scheduler for Mutabelle."""
- return schedule.age_scheduler(env, 'Isabelle', mutabelle_confs)
-
-
-# Judgement Day configurations
-
-judgement_day_provers = ('e', 'spass', 'vampire', 'z3', 'cvc3', 'yices')
-
-def judgement_day(base_path, theory, opts, env, case, paths, dep_paths, playground):
- """Judgement Day regression suite"""
-
- isa = paths[0]
- dep_path = dep_paths[0]
-
- os.chdir(path.join(playground, '..', base_path)) # Mirabelle requires specific cwd
- prepare_isabelle_repository(isa, dep_path)
-
- output = {}
- success_rates = {}
- some_success = False
-
- for atp in judgement_day_provers:
-
- log_dir = path.join(playground, 'mirabelle_log_' + atp)
- os.makedirs(log_dir)
-
- cmd = ('%s/bin/isabelle mirabelle -q -O %s sledgehammer[prover=%s,%s] %s.thy'
- % (isa, log_dir, atp, opts, theory))
-
- os.system(cmd)
- output[atp] = util.readfile(path.join(log_dir, theory + '.log'))
-
- percentages = list(re.findall(r'Success rate: (\d+)%', output[atp]))
- if len(percentages) == 2:
- success_rates[atp] = {
- 'sledgehammer': int(percentages[0]),
- 'metis': int(percentages[1])}
- if success_rates[atp]['sledgehammer'] > 0:
- some_success = True
- else:
- success_rates[atp] = {}
-
-
- data = {'success_rates': success_rates}
- raw_attachments = dict((atp + "_output", output[atp]) for atp in judgement_day_provers)
- # FIXME: summary?
- return (some_success, '', data, raw_attachments, None)
-
-
-@configuration(repos = [Isabelle], deps = [(HOL, [0])])
-def JD_NS(*args):
- """Judgement Day regression suite NS"""
- return judgement_day('Isabelle/src/HOL/Auth', 'NS_Shared', 'prover_timeout=10', *args)
-
-@configuration(repos = [Isabelle], deps = [(HOL, [0])])
-def JD_FTA(*args):
- """Judgement Day regression suite FTA"""
- return judgement_day('Isabelle/src/HOL/Library', 'Fundamental_Theorem_Algebra', 'prover_timeout=10', *args)
-
-@configuration(repos = [Isabelle], deps = [(HOL, [0])])
-def JD_Hoare(*args):
- """Judgement Day regression suite Hoare"""
- return judgement_day('Isabelle/src/HOL/IMPP', 'Hoare', 'prover_timeout=10', *args)
-
-@configuration(repos = [Isabelle], deps = [(HOL, [0])])
-def JD_SN(*args):
- """Judgement Day regression suite SN"""
- return judgement_day('Isabelle/src/HOL/Proofs/Lambda', 'StrongNorm', 'prover_timeout=10', *args)
-
-
-JD_confs = 'JD_NS JD_FTA JD_Hoare JD_SN JD_Arrow JD_FFT JD_Jinja JD_QE JD_S2S'.split(' ')
-
-@scheduler()
-def judgement_day_scheduler(env):
- """Scheduler for Judgement Day."""
- return schedule.age_scheduler(env, 'Isabelle', JD_confs)
-
-
-# SML/NJ
-
-smlnj_settings = '''
-ML_SYSTEM=smlnj
-ML_HOME="/home/smlnj/110.76/bin"
-ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
-ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
-'''
-
-@configuration(repos = [Isabelle], deps = [(Pure, [0])])
-def SML_HOL(*args):
- """HOL image built with SML/NJ"""
- return isabelle_build(*(args + ("-b", "HOL")), more_settings=smlnj_settings, timeout=SMLNJ_TIMEOUT)
-
-@configuration(repos = [Isabelle], deps = [])
-def SML_makeall(*args):
- """SML/NJ build of all possible sessions"""
- return isabelle_build(*(args + ("-j", "3", "-a")), more_settings=smlnj_settings, timeout=SMLNJ_TIMEOUT)
-
-