Menu
▾
▴
[Hol-builds] SUCCESS: --expk:d63dce1e1:poly570:-F-t3
|
From: <Mic...@da...> - 2021-04-08 14:39:49
|
Running in /home/michaeln/regressionHOLs/expk on machine telemachus Uname info (srm): Linux 3.13.0-170-generic x86_64 Cpu: Intel(R) Core(TM) i7-2600 CPU @ 3.40GHz x 8 Memory: 16005 MB PATH: /home/michaeln/jdk1.8.0_202/bin:/usr/bin:/bin:/home/michaeln/bin ML Implementation: poly570 Started: Thu, 08 Apr 2021 19:00:13 +1000 Extra commandline arguments: -F -t3 Revision: d63dce1e1 Fixed typo in identical_distribution_def, adding alternative definitions (as theorems) >From github.com:mn200/HOL 80660c1a5..d63dce1e1 develop -> origin/develop Updating 80660c1a5..d63dce1e1 Fast-forward src/probability/probabilityScript.sml | 98 +++++++++++++++++++++++++++++++---- 1 file changed, 89 insertions(+), 9 deletions(-) -- Configuration Description Ends -- Building directory tools/Holmake/tests/holdep [08 Apr, 19:01:13] Building directory tools/Holmake/tests/depchainloop [08 Apr, 19:01:14] Building directory tools/Holmake/tests/recursiveclean [08 Apr, 19:01:15] Building directory tools/Holmake/tests/wildcard [08 Apr, 19:01:15] Building directory tools/Holmake/tests/dashn_works [08 Apr, 19:01:15] Building directory tools/set_mtime [08 Apr, 19:01:15] Building directory tools/mlyacc/mlyacclib [08 Apr, 19:01:16] Building directory src/portableML/poly [08 Apr, 19:01:16] Building directory src/portableML [08 Apr, 19:01:16] Building directory src/portableML/monads [08 Apr, 19:01:18] Building directory src/portableML/poly/concurrent [08 Apr, 19:01:18] Building directory src/portableML/testsrc [08 Apr, 19:01:18] Building directory src/prekernel [08 Apr, 19:01:26] Building directory src/experimental-kernel [08 Apr, 19:01:28] Building directory src/thm [08 Apr, 19:01:28] Building directory src/postkernel [08 Apr, 19:01:28] Building directory src/parse [08 Apr, 19:01:28] Building directory tools/Holmake/tests/badincludes [08 Apr, 19:01:34] Building directory src/opentheory [08 Apr, 19:01:39] Building directory src/bool [08 Apr, 19:01:39] Building directory src/1 [08 Apr, 19:01:50] Building directory src/proofman [08 Apr, 19:02:06] Building directory src/proofman/tests [08 Apr, 19:02:13] Building directory tools/Holmake/tests/holpathdb/proj2 [08 Apr, 19:02:16] Building directory tools/Holmake/tests/holpathdb/proj2/proj2A [08 Apr, 19:02:19] Building directory tools/Holmake/tests/depchain1/dir3 [08 Apr, 19:02:20] Building directory tools/Holmake/tests/depchain2/dir1 [08 Apr, 19:02:22] Building directory tools/Holmake/tests/altquote1 [08 Apr, 19:02:23] Building directory tools/Holmake/tests/brokenstrings [08 Apr, 19:02:24] Building directory tools/Holmake/tests/holdep [08 Apr, 19:02:24] Building directory tools/Holmake/tests/nullary_tgt [08 Apr, 19:02:25] Building directory tools/Holmake/tests/phony_tgt [08 Apr, 19:02:26] Building directory tools/Holmake/tests/quote-filter [08 Apr, 19:02:27] Building directory tools/Holmake/tests/theorytarget [08 Apr, 19:02:28] Building directory tools/Holmake/tests/commandmacros [08 Apr, 19:02:29] Building directory tools/Holmake/tests/cheatspotting [08 Apr, 19:02:29] Building directory tools/Holmake/tests/depchain_heap/ [08 Apr, 19:02:31] Building directory tools/Holmake/tests/depchain_heap/dir2 [08 Apr, 19:02:31] Building directory tools/Holmake/tests/coproduct [08 Apr, 19:02:32] Building directory tools/Holmake/tests/noprereqs/dir1 [08 Apr, 19:02:44] Building directory tools/Holmake/tests/noprereqs/dir2 [08 Apr, 19:02:45] Building directory tools/Holmake/tests/noprereqs/dir3 [08 Apr, 19:02:45] Building directory tools/Holmake/tests/noprereqs/dir4 [08 Apr, 19:02:45] Building directory tools/Holmake/tests/indepchildren [08 Apr, 19:02:46] Building directory tools/Holmake/tests/empty_script [08 Apr, 19:02:48] Building directory tools/Holmake/tests/deps_of_depthys [08 Apr, 19:02:51] Building directory tools/Holmake/tests/gh604 [08 Apr, 19:02:52] Building directory tools/Holmake/tests/ignore_errors/j1 [08 Apr, 19:02:54] Building directory tools/Holmake/tests/qfreadTheoremsyntax [08 Apr, 19:02:54] Building directory tools/Holmake/tests/ignore_errors/j4 [08 Apr, 19:02:54] Building directory tools/Holmake/tests/hollogs [08 Apr, 19:02:54] Building directory src/1/theory_tests [08 Apr, 19:02:56] Building directory src/compute/src [08 Apr, 19:03:02] Building directory src/HolSat/sat_solvers/minisat [08 Apr, 19:03:03] Building directory src/HolSat/sat_solvers/zc2hs [08 Apr, 19:03:05] Building directory src/HolSat [08 Apr, 19:03:06] Building directory src/taut [08 Apr, 19:03:07] Building directory src/marker [08 Apr, 19:03:07] Building directory src/q [08 Apr, 19:03:09] Building directory src/combin [08 Apr, 19:03:10] Building directory src/lite [08 Apr, 19:03:13] Building directory src/refute [08 Apr, 19:03:13] Building directory src/simp/src [08 Apr, 19:03:17] Building directory src/metis [08 Apr, 19:03:22] Building directory src/meson/src [08 Apr, 19:03:27] Building directory src/IndDef [08 Apr, 19:03:27] Building directory src/basicProof [08 Apr, 19:03:30] Building directory src/basicProof/theory_tests [08 Apr, 19:03:35] Building directory src/relation [08 Apr, 19:03:43] Building directory src/coretypes [08 Apr, 19:04:05] Building directory src/meson/test [08 Apr, 19:04:35] Building directory src/tfl/src [08 Apr, 19:04:56] Building directory src/num/theories [08 Apr, 19:05:05] Building directory src/num/reduce/src [08 Apr, 19:05:43] Building directory src/num/arith/src [08 Apr, 19:05:43] Building directory src/num [08 Apr, 19:05:53] Building directory src/num/termination [08 Apr, 19:05:53] Building directory src/AI [08 Apr, 19:06:04] Building directory src/AI/sml_inspection [08 Apr, 19:06:04] Building directory src/AI/proof_search [08 Apr, 19:06:06] Building directory src/AI/machine_learning [08 Apr, 19:06:08] Building directory src/tactictoe/src [08 Apr, 19:06:10] Building directory src/holyhammer [08 Apr, 19:06:13] Building directory src/num/extra_theories [08 Apr, 19:06:17] Building directory src/pred_set/src [08 Apr, 19:06:26] Building directory src/datatype/record [08 Apr, 19:07:08] Building directory src/datatype [08 Apr, 19:07:08] Building directory src/datatype/theory_tests [08 Apr, 19:07:19] Building directory src/monad [08 Apr, 19:07:27] Building directory src/list/src [08 Apr, 19:07:27] Building directory src/quantHeuristics [08 Apr, 19:07:56] Building directory src/unwind [08 Apr, 19:08:08] Building directory src/pattern_matches [08 Apr, 19:08:08] Building directory src/pattern_matches/interactive_tests [08 Apr, 19:08:43] Building directory src/HolSat/vector_def_CNF [08 Apr, 19:08:58] Building directory src/boss/ml_evaluation [08 Apr, 19:09:02] Building directory src/boss [08 Apr, 19:09:02] Building directory tools/Holmake/tests/Iflag [08 Apr, 19:09:16] Building directory src/boss/theory_tests [08 Apr, 19:09:18] Building directory src/tfl/src/test [08 Apr, 19:09:24] Building directory src/TeX [08 Apr, 19:09:28] Building directory src/TeX/theory_tests [08 Apr, 19:09:30] Building directory src/TeX/theory_tests/proj1paper [08 Apr, 19:09:38] Building directory examples/Crypto/RSA [08 Apr, 19:09:43] Building directory examples/zipper [08 Apr, 19:09:48] Building directory src/monad/more_monads [08 Apr, 19:09:50] Building directory src/string [08 Apr, 19:10:03] Building directory src/sort [08 Apr, 19:10:16] Building directory examples/logic/folcompactness [08 Apr, 19:10:30] Building directory examples/logic/ncfolproofs [08 Apr, 19:10:54] Building directory examples/logic/modal-tableaux [08 Apr, 19:10:58] Building directory src/string/theorytesting [08 Apr, 19:11:08] Building directory src/tfl/examples [08 Apr, 19:11:12] Building directory examples/STE [08 Apr, 19:11:25] Building directory src/res_quan/src [08 Apr, 19:11:30] Building directory src/quotient/src [08 Apr, 19:11:32] Building directory src/hol88 [08 Apr, 19:11:41] Building directory src/quotient/examples [08 Apr, 19:11:42] Building directory src/bag [08 Apr, 19:11:46] Building directory src/n-bit [08 Apr, 19:12:02] Building directory src/n-bit/interactive_tests [08 Apr, 19:13:04] Building directory src/finite_maps [08 Apr, 19:13:08] Building directory examples/algorithms/unification/triangular/first-order [08 Apr, 19:13:59] Building directory examples/decidable_separationLogic/src/ [08 Apr, 19:14:28] Building directory examples/ind_def [08 Apr, 19:15:16] Building directory examples/ARM/arm6-verification [08 Apr, 19:15:20] Building directory examples/ARM/arm6-verification/correctness [08 Apr, 19:16:12] Building directory src/ring/src [08 Apr, 19:18:36] Building directory src/integer [08 Apr, 19:18:46] Building directory src/topology [08 Apr, 19:19:19] Building directory examples/rings [08 Apr, 19:19:21] Building directory src/integer/testing [08 Apr, 19:19:26] Building directory src/transfer [08 Apr, 19:19:33] Building directory src/update [08 Apr, 19:19:39] Building directory src/emit [08 Apr, 19:19:40] Building directory examples/ARM/v4 [08 Apr, 19:19:51] Building directory examples/ARM/v7 [08 Apr, 19:21:38] Building directory src/emit/ML [08 Apr, 19:26:13] Building directory src/pred_set/src/more_theories [08 Apr, 19:26:15] Building directory src/coalgebras [08 Apr, 19:27:17] Building directory src/emit/theory_tests [08 Apr, 19:27:35] Building directory src/emit/theory_tests1 [08 Apr, 19:27:40] Building directory examples/dev [08 Apr, 19:27:46] Building directory examples/imperative [08 Apr, 19:28:41] Building directory src/quotient/examples/lambda [08 Apr, 19:28:47] Building directory src/quotient/examples/sigma [08 Apr, 19:29:12] Building directory src/rational [08 Apr, 19:29:40] Building directory src/datatype/inftree [08 Apr, 19:30:15] Building directory examples/hfs [08 Apr, 19:30:16] Building directory src/search [08 Apr, 19:30:20] Building directory examples/CCS [08 Apr, 19:30:23] Building directory examples/formal-languages/lambek [08 Apr, 19:32:01] Building directory examples/PSL/1.01/executable-semantics [08 Apr, 19:32:19] Building directory examples/PSL/1.1/official-semantics [08 Apr, 19:33:16] Building directory examples/algorithms/boyer_moore [08 Apr, 19:34:22] Building directory src/real [08 Apr, 19:34:48] Building directory src/HolQbf [08 Apr, 19:36:15] Building directory src/HolSmt [08 Apr, 19:36:16] Building directory examples/separationLogic/src/ [08 Apr, 19:36:52] Building directory examples/separationLogic/src/holfoot [08 Apr, 19:38:15] Building directory examples/separationLogic/src/holfoot/poly [08 Apr, 19:39:16] Building directory examples/misc [08 Apr, 19:39:48] Building directory examples/lambda/basics [08 Apr, 19:39:55] Building directory examples/logic [08 Apr, 19:39:58] Building directory examples/algorithms/unification/triangular/nominal [08 Apr, 19:40:03] Building directory examples/lambda/barendregt [08 Apr, 19:41:11] Building directory examples/computability [08 Apr, 19:42:06] Building directory examples/lambda/other-models [08 Apr, 19:42:19] Building directory examples/lambda/typing [08 Apr, 19:42:34] Building directory examples/computability/lambda [08 Apr, 19:42:42] Building directory examples/computability/register [08 Apr, 19:43:57] Building directory examples/computability/turing [08 Apr, 19:45:32] Building directory examples/balanced_bst [08 Apr, 19:45:58] Building directory examples/formal-languages/regular [08 Apr, 19:50:04] Building directory src/Boolify/src [08 Apr, 19:51:42] Building directory src/float [08 Apr, 19:51:55] Building directory src/floating-point [08 Apr, 19:52:15] Building directory examples/l3-machine-code/common [08 Apr, 19:52:58] Building directory examples/l3-machine-code/decompilers [08 Apr, 19:53:30] Building directory src/floating-point/native [08 Apr, 19:53:31] Building directory src/probability [08 Apr, 19:55:37] Building directory src/temporal/src [08 Apr, 20:04:32] Building directory examples/temporal_deep [08 Apr, 20:04:50] Building directory examples/temporal_deep/src/examples [08 Apr, 20:06:11] Building directory examples/computability/kolmog [08 Apr, 20:06:16] Building directory examples/computability/recdegrees [08 Apr, 20:07:20] Building directory examples/RL_Environment [08 Apr, 20:07:28] Building directory examples/parity [08 Apr, 20:07:30] Building directory examples/formal-languages [08 Apr, 20:07:33] Building directory examples/formal-languages/context-free [08 Apr, 20:07:33] Building directory examples/formal-languages/regular/regular-play [08 Apr, 20:09:35] Building directory examples/Hoare-for-divergence [08 Apr, 20:09:50] Building directory examples/MLsyntax [08 Apr, 20:10:22] Building directory examples/set-theory/zfset [08 Apr, 20:10:25] Building directory examples/set-theory/vbg [08 Apr, 20:10:36] Building directory examples/category [08 Apr, 20:10:46] Building directory examples/miller [08 Apr, 20:11:44] Building directory examples/miller/miller [08 Apr, 20:13:52] Building directory examples/ARM_security_properties [08 Apr, 20:17:51] Building directory examples/fun-op-sem/lprefix_lub [08 Apr, 20:54:22] Building directory examples/fun-op-sem/for [08 Apr, 20:54:22] Building directory examples/logic/propositional_logic [08 Apr, 20:55:20] Building directory examples/logic/ltl [08 Apr, 20:55:26] Building directory examples/logic/ltl-transformations [08 Apr, 21:01:53] Building directory examples/fun-op-sem [08 Apr, 21:01:56] Building directory examples/algorithms [08 Apr, 21:01:56] Building directory examples/Crypto/AES [08 Apr, 21:02:14] Building directory examples/Crypto/IDEA [08 Apr, 21:03:52] Building directory examples/Crypto/MARS [08 Apr, 21:04:18] Building directory examples/Crypto/RC6 [08 Apr, 21:07:00] Building directory examples/Crypto/Serpent/Reference [08 Apr, 21:07:09] Building directory examples/Crypto/Serpent/Bitslice [08 Apr, 21:10:05] Building directory examples/Crypto/SHA-1 [08 Apr, 21:12:07] Building directory examples/Crypto/TEA [08 Apr, 21:12:16] Building directory examples/Crypto/TWOFISH [08 Apr, 21:12:31] Building directory examples/l3-machine-code/cheri/step [08 Apr, 21:12:43] Building directory examples/theorem-prover [08 Apr, 21:18:55] Building directory examples/machine-code [08 Apr, 22:56:17] Building directory examples/diningcryptos [08 Apr, 23:45:24] Building directory examples/algebra [09 Apr, 00:24:47] Building directory examples/simple_complexity [09 Apr, 00:31:43] Building directory examples/AKS [09 Apr, 00:32:07] Building directory examples/dependability/ [09 Apr, 00:34:12] Building directory examples/lassie/ [09 Apr, 00:35:34] |
