Menu
▾
▴
[Hol-builds] SUCCESS: -expk:e9aa956:mosml2.01
|
From: <Mic...@ni...> - 2012-05-27 00:23:31
|
Running in /import/atp-linhome/home/1/michaeln/current-hols/expkhol on machine atp-login1 Uname info (srm): Linux 2.6.32-5-686 i686 Cpu: Intel(R) Xeon(R) CPU E5405 @ 2.00GHz x 8 Memory: 3037 MB ML Implementation: mosml2.01 Started: Sun, 27 May 2012 02:00:13 +1000 Extra commandline arguments: -selftest 2 Revision: e9aa956 Define sup for ordinals; fail to prove anything about it. >From git://github.com/mn200/HOL d377aa9..e9aa956 master -> origin/master Updating d377aa9..e9aa956 Fast-forward examples/set-theory/hol_sets/wellorderScript.sml | 256 +++++++++++++++++++++- 1 files changed, 247 insertions(+), 9 deletions(-) -- Configuration Description Ends -- Building directory tools/mlyacc/mlyacclib [27 May, 02:00:51] Building directory src/portableML/mosml [27 May, 02:00:52] Building directory src/portableML [27 May, 02:00:53] Building directory src/prekernel [27 May, 02:00:58] Building directory src/experimental-kernel [27 May, 02:01:02] Building directory src/postkernel [27 May, 02:01:04] Building directory src/parse [27 May, 02:01:06] Building directory src/bool [27 May, 02:01:25] Building directory src/1 [27 May, 02:01:32] Building directory src/proofman [27 May, 02:01:52] Building directory src/compute/src [27 May, 02:01:54] Building directory src/HolSat/sat_solvers/minisat [27 May, 02:01:55] Building directory src/HolSat/sat_solvers/zc2hs [27 May, 02:01:55] Building directory src/HolSat [27 May, 02:01:55] Building directory src/taut [27 May, 02:02:00] Building directory src/marker [27 May, 02:02:00] Building directory src/q [27 May, 02:02:03] Building directory src/combin [27 May, 02:02:05] Building directory src/lite [27 May, 02:02:09] Building directory src/refute [27 May, 02:02:10] Building directory src/simp/src [27 May, 02:02:11] Building directory src/metis [27 May, 02:02:20] Building directory src/meson/src [27 May, 02:02:39] Building directory src/IndDef [27 May, 02:02:41] Building directory src/basicProof [27 May, 02:02:45] Building directory src/relation [27 May, 02:02:46] Building directory src/one [27 May, 02:03:13] Building directory src/pair/src [27 May, 02:03:17] Building directory src/sum [27 May, 02:03:49] Building directory src/tfl/src [27 May, 02:03:55] Building directory src/option [27 May, 02:04:03] Building directory src/num/theories [27 May, 02:04:16] Building directory src/num/reduce/src [27 May, 02:05:44] Building directory src/num/arith/src [27 May, 02:05:46] Building directory src/num [27 May, 02:06:02] Building directory src/num/termination [27 May, 02:06:02] Building directory src/num/extra_theories [27 May, 02:06:03] Building directory src/pred_set/src [27 May, 02:07:13] Building directory src/datatype/equiv [27 May, 02:12:41] Building directory src/datatype/record [27 May, 02:12:42] Building directory src/datatype [27 May, 02:12:43] Building directory src/list/src [27 May, 02:13:29] Building directory src/quantHeuristics [27 May, 02:15:08] Building directory src/unwind [27 May, 02:15:38] Building directory src/boss [27 May, 02:15:39] Building directory src/tfl/src/test [27 May, 02:15:40] Building directory src/TeX [27 May, 02:16:27] Building directory examples/RSA [27 May, 02:16:42] Building directory src/sort [27 May, 02:17:43] Building directory src/string [27 May, 02:18:32] Building directory src/string/theorytesting [27 May, 02:19:34] Building directory examples/STE [27 May, 02:19:54] Building directory src/res_quan/src [27 May, 02:20:36] Building directory src/quotient/src [27 May, 02:20:46] Building directory src/quotient/examples [27 May, 02:22:25] Building directory src/finite_map [27 May, 02:23:39] Building directory examples/ind_def [27 May, 02:25:05] Building directory examples/decidable_separationLogic/src/ [27 May, 02:26:21] Building directory src/bag [27 May, 02:35:08] Building directory examples/unification/triangular/first-order [27 May, 02:36:35] Building directory src/n-bit [27 May, 02:40:26] Building directory examples/ARM/arm6-verification [27 May, 02:50:51] Building directory examples/ARM/arm6-verification/correctness [27 May, 02:59:06] Building directory src/ring/src [27 May, 03:41:48] Building directory src/integer [27 May, 03:43:32] Building directory examples/rings [27 May, 03:49:37] Building directory src/llist [27 May, 03:50:37] Building directory src/path [27 May, 03:52:46] Building directory src/integer/testing [27 May, 03:53:34] Building directory src/patricia [27 May, 03:55:24] Building directory src/update [27 May, 03:58:35] Building directory src/emit [27 May, 03:58:48] Building directory examples/ARM/v4 [27 May, 04:07:35] Building directory examples/ARM/v7 [27 May, 04:36:23] Building directory src/hol88 [27 May, 05:55:46] Building directory src/quotient/examples/lambda [27 May, 05:55:47] Building directory src/quotient/examples/sigma [27 May, 05:58:59] Building directory src/rational [27 May, 06:02:25] Building directory src/real [27 May, 06:05:39] Building directory src/complex [27 May, 06:10:24] Building directory examples/separationLogic/src/ [27 May, 06:11:04] Building directory src/HolQbf [27 May, 06:25:38] Building directory src/HolSmt [27 May, 06:25:48] Building directory src/opentheory [27 May, 06:31:15] Building directory examples/misc [27 May, 06:31:16] Building directory examples/muddy/muddyC [27 May, 06:32:14] Building directory examples/muddy [27 May, 06:32:14] Building directory examples/HolBdd [27 May, 06:32:15] Building directory examples/HolCheck [27 May, 06:32:44] Building directory src/datatype/inftree [27 May, 06:45:53] Building directory examples/lambda/basics [27 May, 06:46:05] Building directory examples/logic [27 May, 06:49:40] Building directory examples/unification/triangular/nominal [27 May, 06:50:43] Building directory examples/lambda/barendregt [27 May, 07:02:23] Building directory examples/computability [27 May, 07:11:46] Building directory examples/lambda/other-models [27 May, 07:13:08] Building directory examples/lambda/typing [27 May, 07:18:46] Building directory examples/computability/lambda [27 May, 07:20:48] Building directory examples/computability/register [27 May, 07:38:55] Building directory src/Boolify/src [27 May, 07:39:41] Building directory src/float [27 May, 07:41:16] Building directory src/prob [27 May, 07:43:15] Building directory src/temporal/src [27 May, 07:46:21] Building directory examples/parity [27 May, 07:47:29] Building directory examples/MLsyntax [27 May, 07:47:52] Building directory examples/set-theory/zfset [27 May, 07:48:11] Building directory examples/set-theory/vbg [27 May, 07:49:51] Building directory examples/set-theory/hol_sets [27 May, 07:51:11] Building directory examples/category [27 May, 07:54:19] Building directory examples/miller/ho_prover [27 May, 08:02:06] Building directory examples/miller/miller [27 May, 08:02:19] Building directory examples/ordinal [27 May, 08:38:11] Building directory examples/Crypto/AES [27 May, 08:39:49] Building directory examples/Crypto/IDEA [27 May, 09:09:01] Building directory examples/Crypto/MARS [27 May, 09:11:20] Building directory examples/Crypto/RC6 [27 May, 09:13:45] Building directory examples/Crypto/Serpent/Reference [27 May, 09:14:37] Building directory examples/Crypto/Serpent/Bitslice [27 May, 09:48:16] Building directory examples/Crypto/SHA-1 [27 May, 10:19:41] Building directory examples/Crypto/TEA [27 May, 10:20:34] Building directory examples/Crypto/TWOFISH [27 May, 10:21:27] |