Job 2993

CakeML:7df18a4aaeea9380277b0a3f92bbc3871a73a8b2
  Merge remote-tracking branch 'refs/remotes/origin/thunks' into thunks [Oct 01 20:56:46]
#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:timtam

Oct 02 04:20:13 Claimed job
Oct 02 04:20:19 Reusing HOL
Oct 02 04:20:26 Starting developers
Oct 02 04:20:31 Finished developers                                               3s 189MB
Oct 02 04:20:31 Starting developers/bin
Oct 02 04:20:35 Finished developers/bin                                           2s  89MB
Oct 02 04:20:36 Starting misc
Oct 02 04:21:31 Finished misc                                                    53s   1GB
Oct 02 04:21:31 Starting compiler/proofs
Oct 02 05:32:40 Finished compiler/proofs                                    1h11m07s  31GB
Oct 02 05:32:41 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 02 11:28:03 Finished compiler/bootstrap/compilation/x64/64/proofs       5h55m21s  78GB
Oct 02 11:28:04 Starting semantics/ffi
Oct 02 11:28:13 Finished semantics/ffi                                            7s 540MB
Oct 02 11:28:14 Starting semantics
Oct 02 11:28:15 Finished semantics                                                0s  59MB
Oct 02 11:28:16 Starting semantics/proofs
Oct 02 11:28:37 Finished semantics/proofs                                        20s 872MB
Oct 02 11:28:38 Starting semantics/alt_semantics
Oct 02 11:28:55 Finished semantics/alt_semantics                                 16s 739MB
Oct 02 11:28:56 Starting semantics/alt_semantics/proofs
Oct 02 11:33:01 Finished semantics/alt_semantics/proofs                        4m03s   1GB
Oct 02 11:33:02 Starting basis/pure
Oct 02 11:33:04 Finished basis/pure                                               0s  94MB
Oct 02 11:33:04 Starting translator
Oct 02 11:34:23 Finished translator                                            1m17s   2GB
Oct 02 11:34:24 Starting compiler/parsing
Oct 02 11:34:26 Finished compiler/parsing                                         0s  66MB
Oct 02 11:34:26 Starting characteristic
Oct 02 11:34:28 Finished characteristic                                           1s 121MB
Oct 02 11:34:29 Starting translator/monadic
Oct 02 11:34:31 Finished translator/monadic                                       1s 125MB
Oct 02 11:34:32 Starting translator/monadic/monad_base
Oct 02 11:34:34 Finished translator/monadic/monad_base                            0s  61MB
Oct 02 11:34:34 Starting basis
Oct 02 11:36:23 Finished basis                                                 1m47s   3GB
Oct 02 11:36:24 Starting compiler
Oct 02 11:36:27 Finished compiler                                                 2s 233MB
Oct 02 11:36:28 Starting compiler/inference
Oct 02 11:36:30 Finished compiler/inference                                       1s 115MB
Oct 02 11:36:31 Starting compiler/backend/reg_alloc
Oct 02 11:36:33 Finished compiler/backend/reg_alloc                               0s 100MB
Oct 02 11:36:34 Starting compiler/backend/gc
Oct 02 11:36:36 Finished compiler/backend/gc                                      1s 144MB
Oct 02 11:36:37 Starting compiler/backend
Oct 02 11:36:42 Finished compiler/backend                                         4s 262MB
Oct 02 11:36:43 Starting compiler/encoders/asm
Oct 02 11:36:44 Finished compiler/encoders/asm                                    0s  89MB
Oct 02 11:36:45 Starting compiler/encoders/x64
Oct 02 11:36:47 Finished compiler/encoders/x64                                    0s  93MB
Oct 02 11:36:48 Starting compiler/encoders/arm7
Oct 02 11:36:49 Finished compiler/encoders/arm7                                   0s  91MB
Oct 02 11:36:50 Starting compiler/encoders/arm8
Oct 02 11:36:52 Finished compiler/encoders/arm8                                   0s  92MB
Oct 02 11:36:53 Starting compiler/encoders/arm8_asl
Oct 02 11:38:39 FAILED: compiler/encoders/arm8_asl
  HOLORIG=/scratch/cakeml/regression2/cakeml-2993/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 (38s)     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 (14s)     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  (7s)     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  (7s)     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/regression2/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/regression2/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/regression2/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/regression2/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