Menu
▾
▴
[Hol-builds] FAILURE: --expk:07dca05:poly570:-F-t2
|
From: <Mic...@da...> - 2021-01-13 13:00:36
|
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: Mon, 11 Jan 2021 09:00:04 +1100 Extra commandline arguments: -F -t2 Revision: 07dca05 Fix bugs in Makefiles/lib files preventing Lassie from compiling Already up-to-date. -- Configuration Description Ends -- munge.exe real: 2s user: 1s OK Starting work on stringlit_output stringlit_output real: 0s user: 0s OK Starting work on stringlit_output stringlit_output real: 0s user: 0s OK Self-test directory /OSM/CBR/D61_HRT/work/scratch/regressionHOLs/expknl/src/string/theorytesting built successfully. Building directory src/tfl/examples [11 Jan, 09:15:19] Starting work on ctlTheory ctlTheory real: 14s user: 13s OK Self-test directory /OSM/CBR/D61_HRT/work/scratch/regressionHOLs/expknl/src/tfl/examples built successfully. Building directory examples/STE [11 Jan, 09:15:34] Starting work on STETheory STETheory real: 6s user: 5s OK Self-test directory /OSM/CBR/D61_HRT/work/scratch/regressionHOLs/expknl/examples/STE built successfully. Building directory src/res_quan/src [11 Jan, 09:15:40] Starting work on res_quanTheory res_quanTheory real: 2s user: 1s OK Uploading files to /OSM/CBR/D61_HRT/work/scratch/regressionHOLs/expknl/sigobj Building directory src/quotient/src [11 Jan, 09:15:43] Starting work on quotientTheory quotientTheory real: 3s user: 2s OK Starting work on quotient_listTheory Starting work on quotient_optionTheory Starting work on quotient_pairTheory Starting work on quotient_sumTheory quotient_optionTheory real: 2s user: 1s OK quotient_pairTheory real: 2s user: 1s OK Starting work on quotient_pred_setTheory quotient_sumTheory real: 3s user: 1s OK quotient_listTheory real: 3s user: 1s OK quotient_pred_setTheory real: 2s user: 2s OK Performing self-test... Attempting quotient where reln has symbolic name <<HOL message: Initialising SRW simpset ... done>> Saved theorem _____ "mod3_ABS_REP_CLASS" Saved theorem _____ "mod3_QUOTIENT" Saved theorem _____ "num2foo_foo2num" Saved theorem _____ "foo2num_num2foo" Saved theorem _____ "num2foo_11" Saved theorem _____ "foo2num_11" Saved theorem _____ "num2foo_ONTO" Saved theorem _____ "foo2num_ONTO" Saved theorem _____ "num2foo_thm" Saved theorem _____ "foo2num_thm" Saved theorem _____ "foo_EQ_foo" Saved theorem _____ "foo_case_def" Saved theorem _____ "datatype_foo" Saved theorem _____ "foo_distinct" Saved theorem _____ "foo_nchotomy" Saved theorem _____ "foo_Axiom" Saved theorem _____ "foo_induction" Saved theorem _____ "foo_case_cong" Saved theorem _____ "foo_case_eq" <<HOL message: Defined type: "foo">> Saved theorem _____ "lfoo_ABS_REP_CLASS" Saved theorem _____ "lfoo_QUOTIENT" Saved theorem _____ "lfoo2_ABS_REP_CLASS" Saved theorem _____ "lfoo2_QUOTIENT" Self-test was successful Uploading files to /OSM/CBR/D61_HRT/work/scratch/regressionHOLs/expknl/sigobj Building directory src/hol88 [11 Jan, 09:15:56] Uploading files to /OSM/CBR/D61_HRT/work/scratch/regressionHOLs/expknl/sigobj Building directory src/quotient/examples [11 Jan, 09:15:56] Scanning $(HOLDIR)/src/hol88 Starting work on ext_finite_setTheory Starting work on finite_setTheory Starting work on more_setTheory Starting work on msgTheory more_setTheory real: 2s user: 1s OK Starting work on more_listTheory more_listTheory real: 2s user: 1s OK msgTheory real: 7s user: 3s OK finite_setTheory real: 7s user: 4s OK ext_finite_setTheory real: 7s user: 3s OK Self-test directory /OSM/CBR/D61_HRT/work/scratch/regressionHOLs/expknl/src/quotient/examples built successfully. Building directory src/bag [11 Jan, 09:16:05] Starting work on bagTheory bagTheory real: 16s user: 15s OK Starting work on primeFactorTheory *** FATAL: Build failed in directory /OSM/CBR/D61_HRT/work/scratch/regressionHOLs/expknl/src/bag (with signal 9) |