Menu
▾
▴
[Hol-builds] SUCCESS: --stdknl:3c30c3247:poly560:-F-t2
|
From: <Mic...@da...> - 2018-04-24 03:53:35
|
Running in /home/michaeln/regressionHOLs/stdknl on machine telemachus Uname info (srm): Linux 3.13.0-143-generic x86_64 Cpu: Intel(R) Core(TM) i7-2600 CPU @ 3.40GHz x 8 Memory: 16005 MB ML Implementation: poly560 Started: Tue, 24 Apr 2018 12:30:12 +1000 Extra commandline arguments: -F -t2 Revision: 3c30c3247 Define monadic parser for LTL formulas >From github.com:mn200/HOL 6ad012b9a..126335620 mjcg -> origin/mjcg Already up-to-date. -- Configuration Description Ends -- Building directory tools/Holmake/tests/holdep [24 Apr, 12:30:59] Building directory tools/Holmake/tests/depchainloop [24 Apr, 12:30:59] Building directory tools/Holmake/tests/recursiveclean [24 Apr, 12:30:59] Building directory tools/set_mtime [24 Apr, 12:30:59] Building directory tools/mlyacc/mlyacclib [24 Apr, 12:30:59] Building directory src/portableML/poly [24 Apr, 12:30:59] Building directory src/portableML [24 Apr, 12:30:59] Building directory src/portableML/monads [24 Apr, 12:30:59] Building directory src/portableML/testsrc [24 Apr, 12:31:00] Building directory src/prekernel [24 Apr, 12:31:03] Building directory src/0 [24 Apr, 12:31:03] Building directory src/thm [24 Apr, 12:31:03] Building directory src/postkernel [24 Apr, 12:31:04] Building directory src/parse [24 Apr, 12:31:04] Building directory src/opentheory [24 Apr, 12:31:07] Building directory src/bool [24 Apr, 12:31:07] Building directory src/1 [24 Apr, 12:31:16] Building directory src/proofman [24 Apr, 12:31:27] Building directory src/proofman/tests [24 Apr, 12:31:33] Building directory src/tactictoe/src [24 Apr, 12:31:33] Building directory src/holyhammer/hh/hh1 [24 Apr, 12:31:34] Building directory src/holyhammer/hh [24 Apr, 12:31:34] Building directory src/holyhammer [24 Apr, 12:31:34] Building directory tools/Holmake/tests/depchain1/dir3 [24 Apr, 12:31:35] Building directory tools/Holmake/tests/depchain2/dir1 [24 Apr, 12:31:36] Building directory tools/Holmake/tests/altquote1 [24 Apr, 12:31:37] Building directory tools/Holmake/tests/brokenstrings [24 Apr, 12:31:37] Building directory tools/Holmake/tests/holdep [24 Apr, 12:31:37] Building directory tools/Holmake/tests/nullary_tgt [24 Apr, 12:31:37] Building directory tools/Holmake/tests/phony_tgt [24 Apr, 12:31:38] Building directory tools/Holmake/tests/quote-filter [24 Apr, 12:31:38] Building directory tools/Holmake/tests/cheatspotting [24 Apr, 12:31:38] Building directory tools/Holmake/tests/depchain_heap/ [24 Apr, 12:31:38] Building directory tools/Holmake/tests/depchain_heap/dir2 [24 Apr, 12:31:38] Building directory tools/Holmake/tests/coproduct [24 Apr, 12:31:39] Building directory tools/Holmake/tests/noprereqs/dir1 [24 Apr, 12:31:43] Building directory tools/Holmake/tests/noprereqs/dir2 [24 Apr, 12:31:43] Building directory tools/Holmake/tests/noprereqs/dir3 [24 Apr, 12:31:43] Building directory tools/Holmake/tests/noprereqs/dir4 [24 Apr, 12:31:44] Building directory tools/Holmake/tests/indepchildren [24 Apr, 12:31:44] Building directory src/1/theory_tests [24 Apr, 12:31:45] Building directory src/compute/src [24 Apr, 12:31:47] Building directory src/HolSat/sat_solvers/minisat [24 Apr, 12:31:47] Building directory src/HolSat/sat_solvers/zc2hs [24 Apr, 12:31:49] Building directory src/HolSat [24 Apr, 12:31:50] Building directory src/taut [24 Apr, 12:31:51] Building directory src/marker [24 Apr, 12:31:51] Building directory src/q [24 Apr, 12:31:51] Building directory src/combin [24 Apr, 12:31:52] Building directory src/lite [24 Apr, 12:31:53] Building directory src/refute [24 Apr, 12:31:54] Building directory src/simp/src [24 Apr, 12:31:57] Building directory src/metis [24 Apr, 12:32:00] Building directory src/meson/src [24 Apr, 12:32:01] Building directory src/IndDef [24 Apr, 12:32:01] Building directory src/basicProof [24 Apr, 12:32:03] Building directory src/relation [24 Apr, 12:32:03] Building directory src/coretypes [24 Apr, 12:32:11] Building directory src/tfl/src [24 Apr, 12:32:31] Building directory src/num/theories [24 Apr, 12:32:39] Building directory src/num/reduce/src [24 Apr, 12:33:12] Building directory src/num/arith/src [24 Apr, 12:33:12] Building directory src/num [24 Apr, 12:33:20] Building directory src/num/termination [24 Apr, 12:33:20] Building directory src/num/extra_theories [24 Apr, 12:33:29] Building directory src/pred_set/src [24 Apr, 12:33:38] Building directory src/datatype/equiv [24 Apr, 12:34:09] Building directory src/datatype/record [24 Apr, 12:34:09] Building directory src/datatype [24 Apr, 12:34:09] Building directory src/datatype/theory_tests [24 Apr, 12:34:15] Building directory src/list/src [24 Apr, 12:34:22] Building directory src/monad [24 Apr, 12:34:44] Building directory src/quantHeuristics [24 Apr, 12:34:49] Building directory src/unwind [24 Apr, 12:35:00] Building directory src/pattern_matches [24 Apr, 12:35:00] Building directory src/HolSat/vector_def_CNF [24 Apr, 12:35:31] Building directory src/boss/ml_evaluation [24 Apr, 12:35:33] Building directory src/boss [24 Apr, 12:35:33] Building directory tools/Holmake/tests/Iflag [24 Apr, 12:35:52] Building directory tools/Holmake/tests/holpathdb/proj2 [24 Apr, 12:35:53] Building directory src/boss/theory_tests [24 Apr, 12:35:55] Building directory src/tfl/src/test [24 Apr, 12:35:57] Building directory src/TeX [24 Apr, 12:36:00] Building directory src/TeX/theory_tests [24 Apr, 12:36:01] Building directory src/TeX/theory_tests/proj1paper [24 Apr, 12:36:05] Building directory examples/RSA [24 Apr, 12:36:08] Building directory examples/zipper [24 Apr, 12:36:11] Building directory src/string [24 Apr, 12:36:13] Building directory src/sort [24 Apr, 12:36:21] Building directory src/string/theorytesting [24 Apr, 12:36:28] Building directory src/tfl/examples [24 Apr, 12:36:30] Building directory examples/STE [24 Apr, 12:36:36] Building directory src/res_quan/src [24 Apr, 12:36:41] Building directory src/quotient/src [24 Apr, 12:36:42] Building directory src/hol88 [24 Apr, 12:36:50] Building directory src/quotient/examples [24 Apr, 12:36:50] Building directory src/finite_map [24 Apr, 12:36:54] Building directory examples/ind_def [24 Apr, 12:37:03] Building directory examples/decidable_separationLogic/src/ [24 Apr, 12:37:06] Building directory src/bag [24 Apr, 12:37:50] Building directory examples/unification/triangular/first-order [24 Apr, 12:38:02] Building directory src/n-bit [24 Apr, 12:38:32] Building directory examples/ARM/arm6-verification [24 Apr, 12:39:24] Building directory examples/ARM/arm6-verification/correctness [24 Apr, 12:40:10] Building directory src/ring/src [24 Apr, 12:42:39] Building directory src/integer [24 Apr, 12:42:45] Building directory src/enumfset [24 Apr, 12:43:13] Building directory examples/rings [24 Apr, 12:43:33] Building directory src/coalgebras [24 Apr, 12:43:35] Building directory src/integer/testing [24 Apr, 12:43:46] Building directory src/patricia [24 Apr, 12:43:52] Building directory src/transfer [24 Apr, 12:44:15] Building directory src/update [24 Apr, 12:44:18] Building directory src/emit [24 Apr, 12:44:19] Building directory examples/ARM/v4 [24 Apr, 12:44:27] Building directory examples/ARM/v7 [24 Apr, 12:46:01] Building directory src/emit/ML [24 Apr, 12:49:51] Building directory src/emit/theory_tests [24 Apr, 12:49:52] Building directory src/emit/theory_tests1 [24 Apr, 12:49:56] Building directory examples/dev [24 Apr, 12:49:59] Building directory examples/imperative [24 Apr, 12:50:53] Building directory src/quotient/examples/lambda [24 Apr, 12:50:57] Building directory src/quotient/examples/sigma [24 Apr, 12:51:20] Building directory src/rational [24 Apr, 12:51:47] Building directory src/datatype/inftree [24 Apr, 12:52:20] Building directory examples/hfs [24 Apr, 12:52:21] Building directory src/search [24 Apr, 12:52:23] Building directory examples/CCS [24 Apr, 12:52:26] Building directory src/real [24 Apr, 12:53:05] Building directory src/HolQbf [24 Apr, 12:53:56] Building directory src/HolSmt [24 Apr, 12:53:56] Building directory examples/separationLogic/src/ [24 Apr, 12:54:31] Building directory examples/separationLogic/src/holfoot [24 Apr, 12:55:48] Building directory examples/separationLogic/src/holfoot/poly [24 Apr, 12:56:42] Building directory examples/misc [24 Apr, 12:57:11] Building directory examples/lambda/basics [24 Apr, 12:57:15] Building directory examples/logic [24 Apr, 12:57:40] Building directory examples/unification/triangular/nominal [24 Apr, 12:57:44] Building directory examples/lambda/barendregt [24 Apr, 12:58:52] Building directory examples/computability [24 Apr, 12:59:43] Building directory examples/lambda/other-models [24 Apr, 12:59:49] Building directory examples/lambda/typing [24 Apr, 13:00:01] Building directory examples/computability/lambda [24 Apr, 13:00:09] Building directory examples/computability/register [24 Apr, 13:01:14] Building directory examples/computability/turing [24 Apr, 13:01:20] Building directory examples/balanced_bst [24 Apr, 13:01:43] Building directory examples/formal-languages/regular [24 Apr, 13:04:57] Building directory src/Boolify/src [24 Apr, 13:06:49] Building directory src/float [24 Apr, 13:06:58] Building directory src/floating-point [24 Apr, 13:07:15] Building directory examples/l3-machine-code/common [24 Apr, 13:07:58] Building directory examples/l3-machine-code/decompilers [24 Apr, 13:08:25] Building directory src/floating-point/native [24 Apr, 13:24:30] Building directory src/probability [24 Apr, 13:26:06] Building directory src/temporal/src [24 Apr, 13:27:24] Building directory examples/parity [24 Apr, 13:27:42] Building directory examples/formal-languages [24 Apr, 13:27:43] Building directory examples/formal-languages/context-free [24 Apr, 13:27:44] Building directory examples/MLsyntax [24 Apr, 13:27:47] Building directory examples/set-theory/zfset [24 Apr, 13:27:48] Building directory examples/set-theory/vbg [24 Apr, 13:27:58] Building directory examples/set-theory/hol_sets [24 Apr, 13:28:07] Building directory examples/category [24 Apr, 13:28:56] Building directory examples/miller/ho_prover [24 Apr, 13:29:48] Building directory examples/miller/miller [24 Apr, 13:29:51] Building directory examples/fun-op-sem/lprefix_lub [24 Apr, 13:33:55] Building directory examples/fun-op-sem/for [24 Apr, 13:34:01] Building directory examples/logic/ltl [24 Apr, 13:35:01] Building directory examples/Crypto/AES [24 Apr, 13:43:00] Building directory examples/Crypto/IDEA [24 Apr, 13:44:42] Building directory examples/Crypto/MARS [24 Apr, 13:45:06] Building directory examples/Crypto/RC6 [24 Apr, 13:47:10] Building directory examples/Crypto/Serpent/Reference [24 Apr, 13:47:18] Building directory examples/Crypto/Serpent/Bitslice [24 Apr, 13:49:38] Building directory examples/Crypto/SHA-1 [24 Apr, 13:51:18] Building directory examples/Crypto/TEA [24 Apr, 13:51:27] Building directory examples/Crypto/TWOFISH [24 Apr, 13:51:40] |