Menu
▾
▴
[Hol-builds] FAILURE: --expk:07dca05:poly570:-F-t2
|
From: <Mic...@da...> - 2021-01-08 04:26:32
|
Running in /OSM/HOME-CDC/nor190/scratch/regressionHOLs/expknl on machine d61-04-cdc Uname info (srm): Linux 3.2.0-4-amd64 x86_64 Cpu: Intel(R) Xeon(R) CPU E5-2640 v4 @ 2.40GHz x 2 Memory: 8008 MB ML Implementation: poly570 Started: Fri, 08 Jan 2021 15:00:06 +1100 Extra commandline arguments: -F -t2 Revision: 07dca05 Fix bugs in Makefiles/lib files preventing Lassie from compiling >From https://github.com/HOL-Theorem-Prover/HOL 748b1a6..89e07c5 master -> origin/master Already up-to-date. -- Configuration Description Ends -- at.LESS_EQ OK 0.004 0.000 0.000 at.LESS_CASES_IMP OK 0.000 0.000 0.000 at.LESS_CASES OK 0.000 0.000 0.000 at.LESS_ANTISYM OK 0.004 0.000 0.000 at.LESS_ADD_SUC OK 0.000 0.000 0.000 at.LESS_ADD_NONZERO OK 0.004 0.000 0.000 at.LESS_ADD_1 OK 0.000 0.000 0.000 at.LESS_ADD OK 0.004 0.000 0.000 at.LESS_0_CASES OK 0.004 0.000 0.000 at.LE OK 0.004 0.000 0.000 at.INV_PRE_LESS_EQ OK 0.012 0.000 0.000 at.INV_PRE_LESS OK 0.004 0.000 0.000 at.INV_PRE_EQ OK 0.028 0.000 0.000 pt1 OK 0.004 0.000 0.000 pt2 OK 0.004 0.004 0.000 pt3 OK 0.004 0.000 0.000 pt4 OK 0.000 0.000 0.000 pt5 OK 0.008 0.000 0.000 pt6 OK 0.016 0.000 0.000 pt7 OK 0.012 0.000 0.000 pt8 OK 0.004 0.000 0.000 pt9 OK 0.004 0.000 0.000 pt10 OK 0.008 0.000 0.000 pt11 OK 0.048 0.000 0.004 NONPB1 OK 0.008 0.000 0.000 NONPB2 OK 0.012 0.000 0.000 AG_NAT OK 0.020 0.000 0.000 AG_INT OK 0.012 0.000 0.000 IMUL_NORM OK 0.000 0.000 0.000 NMUL_NORM OK 0.000 0.000 0.000 Num1 OK 0.000 0.000 0.000 Num2 OK 0.032 0.000 0.000 Num3 OK 0.004 0.000 0.000 Num4a OK 0.000 0.000 0.000 Num4b OK 0.004 0.000 0.000 Github677 OK 0.028 0.000 0.004 Testing goals van Leeuwen OK natural number 1 OK natural number 2 OK Testing Omega terms MOD_ADD1001 OK 0.060 0.000 0.000 DIV_LT100000 OK 0.032 0.000 0.000 MATTHEWS_I256 OK 0.020 0.000 0.000 MATTHEWS_N256 OK 0.032 0.000 0.000 MATTHEWS_I2^31 OK 0.032 0.000 0.004 MATTHEWS_N2^31 OK 0.048 0.000 0.000 MATTHEWS_Num OK 0.020 0.004 0.000 MATTHEWS_Num' OK 0.028 0.000 0.004 Testing Cooper's: bogus commandline: --holstate=/OSM/CBR/D61_HRT/work/scratch/regressionHOLs/expknl/bin/hol.state selftest Testing simplifier integration F ==> F equivalent shouldn't loop ... (0.000s) OK Self-test was successful Self-test directory /OSM/CBR/D61_HRT/work/scratch/regressionHOLs/expknl/src/integer/testing built successfully. Building directory src/transfer [08 Jan, 15:25:51] Starting work on transferTheory transferTheory real: 2s user: 1s OK Starting work on fmspTheory Starting work on fsetsTheory Starting work on liftingTheory liftingTheory real: 1s user: 1s OK fmspTheory real: 2s user: 1s OK fsetsTheory real: 2s user: 1s OK Performing self-test... Self-test was successful Uploading files to /OSM/CBR/D61_HRT/work/scratch/regressionHOLs/expknl/sigobj Building directory src/update [08 Jan, 15:25:57] Starting work on updateTheory updateTheory real: 1s user: 0s OK Uploading files to /OSM/CBR/D61_HRT/work/scratch/regressionHOLs/expknl/sigobj Building directory src/emit [08 Jan, 15:25:59] Starting work on basis_emitTheory basis_emitTheory real: 2s user: 1sFAIL<1> error in quse /OSM/CBR/D61_HRT/work/scratch/regressionHOLs/expknl/src/integer/integer_wordTheory.sml : TheoryReader "Exception raised: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}" error in load $(HOLDIR)/sigobj/integer_wordTheory : TheoryReader "Exception raised: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}" error in load /OSM/CBR/D61_HRT/work/scratch/regressionHOLs/expknl/src/emit/basis_emitScript : TheoryReader "Exception raised: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}" <<HOL message: link_parents: the following parents of "integer_word" should already be in the theory graph (but aren't): ("Omega",1610079883,869403), ("int_arith",1610079883,776873)>> Uncaught exception: TheoryReader "Exception raised: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}" *** FATAL: Build failed in directory /OSM/CBR/D61_HRT/work/scratch/regressionHOLs/expknl/src/emit (exited with code 1) |