Job 2992

CakeML:356477cd5f082c762f68f6145b80ffa810e03ea6
  Merge remote-tracking branch 'origin/mcandidate-fix' into thunks [Oct 01 11:15:10]
#1246 (thunks)
Merging into:6ddaf6f8d86d8d5f57f0bcfc8fdd78f855e3daae
  Make it clearer that HOL master should be used [Sep 29 10:18:48]
HOL:77749ad4d0926abb872e3704d8b98abc98f87c73
  Decompiler into Interaction Trees (#1664) [Sep 29 12:05:48]
Machine:pavlova

Oct 01 12:09:14 Claimed job
Oct 01 12:09:18 Reusing HOL
Oct 01 12:09:25 Starting developers
Oct 01 12:09:30 Finished developers                                               3s 216MB
Oct 01 12:09:31 Starting developers/bin
Oct 01 12:09:35 Finished developers/bin                                           2s  89MB
Oct 01 12:09:35 Starting misc
Oct 01 12:10:28 Finished misc                                                    51s   1GB
Oct 01 12:10:29 Starting compiler/proofs
Oct 01 13:21:57 Finished compiler/proofs                                    1h11m27s  32GB
Oct 01 13:21:58 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 01 19:17:13 Finished compiler/bootstrap/compilation/x64/64/proofs       5h55m13s  95GB
Oct 01 19:17:14 Starting semantics/ffi
Oct 01 19:17:22 Finished semantics/ffi                                            7s 540MB
Oct 01 19:17:23 Starting semantics
Oct 01 19:17:24 Finished semantics                                                0s  59MB
Oct 01 19:17:25 Starting semantics/proofs
Oct 01 19:17:47 Finished semantics/proofs                                        20s 878MB
Oct 01 19:17:48 Starting semantics/alt_semantics
Oct 01 19:18:05 Finished semantics/alt_semantics                                 16s 758MB
Oct 01 19:18:06 Starting semantics/alt_semantics/proofs
Oct 01 19:22:14 Finished semantics/alt_semantics/proofs                        4m07s   3GB
Oct 01 19:22:15 Starting basis/pure
Oct 01 19:22:16 Finished basis/pure                                               0s  95MB
Oct 01 19:22:17 Starting translator
Oct 01 19:23:38 Finished translator                                            1m20s   2GB
Oct 01 19:23:39 Starting compiler/parsing
Oct 01 19:23:41 Finished compiler/parsing                                         0s  63MB
Oct 01 19:23:41 Starting characteristic
Oct 01 19:23:44 Finished characteristic                                           1s 126MB
Oct 01 19:23:44 Starting translator/monadic
Oct 01 19:23:46 Finished translator/monadic                                       1s 123MB
Oct 01 19:23:47 Starting translator/monadic/monad_base
Oct 01 19:23:49 Finished translator/monadic/monad_base                            0s  62MB
Oct 01 19:23:49 Starting basis
Oct 01 19:25:41 Finished basis                                                 1m50s   3GB
Oct 01 19:25:42 Starting compiler
Oct 01 19:25:45 Finished compiler                                                 2s 227MB
Oct 01 19:25:46 Starting compiler/inference
Oct 01 19:25:48 Finished compiler/inference                                       1s 125MB
Oct 01 19:25:49 Starting compiler/backend/reg_alloc
Oct 01 19:25:50 Finished compiler/backend/reg_alloc                               0s  96MB
Oct 01 19:25:51 Starting compiler/backend/gc
Oct 01 19:25:53 Finished compiler/backend/gc                                      1s 149MB
Oct 01 19:25:54 Starting compiler/backend
Oct 01 19:25:59 Finished compiler/backend                                         4s 263MB
Oct 01 19:26:00 Starting compiler/encoders/asm
Oct 01 19:26:02 Finished compiler/encoders/asm                                    0s  93MB
Oct 01 19:26:03 Starting compiler/encoders/x64
Oct 01 19:26:05 Finished compiler/encoders/x64                                    0s  92MB
Oct 01 19:26:05 Starting compiler/encoders/arm7
Oct 01 19:26:07 Finished compiler/encoders/arm7                                   0s  95MB
Oct 01 19:26:08 Starting compiler/encoders/arm8
Oct 01 19:26:10 Finished compiler/encoders/arm8                                   0s  92MB
Oct 01 19:26:11 Starting compiler/encoders/arm8_asl
Oct 01 19:27:59 FAILED: compiler/encoders/arm8_asl
  HOLORIG=/scratch/cakeml/regression/cakeml-2992/compiler/encoders/arm8_asl [ -d "armv8.6-asl-snapshot" ] || ./get-armv8.6-hol-snapshot
Cloning into 'armv8.6-asl-snapshot'...
Note: switching to '791b9fd690e3101dec972efa2cf7eb20d51b0412'.

You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by switching back to a branch.

If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -c with the switch command. Example:

  git switch -c <new-branch-name>

Or undo this operation with:

  git switch -

Turn off this advice by setting config variable advice.detachedHead to false

HEAD is now at 791b9fd Rename tc to transitive_closure, to align with HOL4 commit 564ff4a.
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/sail
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/TeX
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanned 39 directories
Starting work on lemTheory
Starting work on lem_boolTheory
lem_boolTheory ...-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem  (0s)     OK
Starting work on lem_basic_classesTheory
lemTheory ...8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem  (3s)     OK
Starting work on lem_assert_extraTheory
lem_basic_classesTheory ...mv8.6-asl-snapshot/A64_ISA_v86A/lib/lem  (4s)     OK
Starting work on lem_functionTheory
Starting work on lem_numTheory
Starting work on lem_tupleTheory
lem_tupleTheory ...equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem  (0s)     OK
lem_functionTheory ...iv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem  (0s)     OK
Starting work on lem_maybeTheory
lem_assert_extraTheory ...rmv8.6-asl-snapshot/A64_ISA_v86A/lib/lem  (1s)     OK
lem_maybeTheory ...equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem  (0s)     OK
Starting work on lem_maybe_extraTheory
lem_maybe_extraTheory ...armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem  (1s)     OK
lem_numTheory ...l-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (37s)     OK
Starting work on lem_function_extraTheory
Starting work on lem_listTheory
Starting work on lem_set_helpersTheory
lem_set_helpersTheory ...armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem  (6s)     OK
lem_function_extraTheory ...v8.6-asl-snapshot/A64_ISA_v86A/lib/lem  (6s)     OK
lem_listTheory ...-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (15s)     OK
Starting work on lem_list_extra_sailTheory
Starting work on lem_string_sailTheory
Starting work on lem_setTheory
Starting work on lem_eitherTheory
lem_string_sailTheory ...armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem  (6s)     OK
Starting work on lem_showTheory
lem_eitherTheory ...quiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem  (7s)     OK
Starting work on lem_num_extraTheory
lem_list_extra_sailTheory ...8.6-asl-snapshot/A64_ISA_v86A/lib/lem  (7s)     OK
Starting work on lem_sortingTheory
lem_setTheory ...l-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem  (8s)     OK
Starting work on lem_mapTheory
lem_num_extraTheory ...v/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem  (7s)     OK
Starting work on lem_relationTheory
lem_mapTheory ...l-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem  (6s)     OK
Starting work on lem_map_extraTheory
lem_sortingTheory ...uiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem  (8s)     OK
Starting work on lem_wordTheory
lem_showTheory ...-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem  (9s)     OK
Starting work on lem_machine_wordTheory
lem_map_extraTheory ...v/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem  (7s)     OK
Starting work on lem_set_extra_sailTheory
lem_machine_wordTheory ...rmv8.6-asl-snapshot/A64_ISA_v86A/lib/lem  (8s)     OK
Starting work on lem_string_extra_sailTheory
lem_relationTheory ...iv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (17s)     OK
lem_set_extra_sailTheory ...v8.6-asl-snapshot/A64_ISA_v86A/lib/lem  (7s)FAIL<1>
 <<HOL message: Created theory "lem_set_extra_sail">>
 Saved definition ____ "chooseAndSplit_def"
 Saved definition ____ "setCompareBy_def"
 Saved definition ____ "setCompare_def"
 Saved definition ____ "leastFixedPointUnbounded_alt_def"
 /scratch/cakeml/regression/HOL-77749ad4d0926abb872e3704d8b98abc98f87c73/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem/lem_set_extra_sailScript.sml:125: error: Structure (whileTheory) has not been declared Found near [whileTheory.WHILE]
 error in quse /scratch/cakeml/regression/HOL-77749ad4d0926abb872e3704d8b98abc98f87c73/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem/lem_set_extra_sailScript.sml : Fail "Static Errors"
 error in load /scratch/cakeml/regression/HOL-77749ad4d0926abb872e3704d8b98abc98f87c73/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem/lem_set_extra_sailScript : Fail "Static Errors"
 Uncaught exception at ./basis/FinalPolyML.sml:492: Fail "Static Errors"
 Full log: /scratch/cakeml/regression/HOL-77749ad4d0926abb872e3704d8b98abc98f87c73/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem/.hol/logs/lem_set_extra_sailTheory
lem_wordTheory ...-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem (16s)MKILLED
lem_string_extra_sailTheory ...6-asl-snapshot/A64_ISA_v86A/lib/lem  (6s)MKILLED