[Hol-builds] FAILURE: --stdknl:be2d4f0e2:poly590:-j6-t3

[<mic...@gm...>]

Running in /home/mn200/regression-hols/stdknl on machine oven2
Uname info (srm): Linux 5.15.0-87-generic x86_64
Cpu: Intel(R) Core(TM) i7-7700K CPU @ 4.20GHz  x 8
Memory: 64156 MB
PATH: /usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games:/snap/bin
ML Implementation: poly590
Started: tor, 12 sep 2024 01:00:03 +0200
Extra commandline arguments: -j6 -t3
Revision: be2d4f0e2 Fix typo.
>From github.com:HOL-Theorem-Prover/HOL
   14b4197fb..be2d4f0e2  develop    -> origin/develop
Updating 14b4197fb..be2d4f0e2
Fast-forward
 examples/formal-languages/FormalLangScript.sml     |  297 ++-
 examples/formal-languages/regular/regexp2dfa.sml   |    6 +-
 .../formal-languages/regular/regularScript.sml     | 2717 ++++++++++++++++++++
 3 files changed, 2943 insertions(+), 77 deletions(-)
 create mode 100644 examples/formal-languages/regular/regularScript.sml
-- Configuration Description Ends --

Starting work on permutationTheory
permutationTheory                            examples/fermat/count (20s)     OK
Finished $(HOLDIR)/examples/fermat/count [#theories: 3]               (48.440s)
Starting work on FormalLangTheory
FormalLangTheory                         examples/formal-languages  (2s)     OK
Finished $(HOLDIR)/examples/formal-languages [#theories: 1]            (2.880s)
Starting work on locationTheory
locationTheory              examples/formal-languages/context-free  (2s)     OK
Starting work on grammarTheory
kraft_ineqTheory                     examples/computability/kolmog (74s)     OK
Starting work on prefix_free_kolmogTheory
real_borelTheory                                   src/probability (45s)     OK
Starting work on real_measureTheory
grammarTheory               examples/formal-languages/context-free  (5s)     OK
Starting work on NTpropertiesTheory
hoppingTheory                                examples/fermat/twosq (39s)     OK
Finished $(HOLDIR)/examples/fermat/twosq [#theories: 12]             (167.930s)
Starting work on pegTheory
NTpropertiesTheory          examples/formal-languages/context-free  (8s)     OK
Starting work on precparserTheory
precparserTheory            examples/formal-languages/context-free  (1s)     OK
Starting work on contig_supportTheory
extrealTheory                                      src/probability (61s)     OK
Starting work on measureTheory
contig_supportTheory              examples/formal-languages/contig  (1s)     OK
Starting work on prob-selftest.log
pegTheory                   examples/formal-languages/context-free  (9s)     OK
Starting work on pegexecTheory
pegexecTheory               examples/formal-languages/context-free  (5s)     OK
Starting work on simpleSexpTheory
simpleSexpTheory            examples/formal-languages/context-free  (9s)     OK
Starting work on simpleSexpPEGTheory
prefix_free_kolmogTheory             examples/computability/kolmog (30s)     OK
Finished $(HOLDIR)/examples/computability/kolmog [#theories: 12]     (259.190s)
Starting work on pegSampleTheory
pegSampleTheory             examples/formal-languages/context-free  (3s)     OK
Starting work on sexpcodeTheory
simpleSexpPEGTheory         examples/formal-languages/context-free  (6s)     OK
Starting work on context-free-test.log
sexpcodeTheory              examples/formal-languages/context-free  (5s)     OK
Starting work on simpleSexpParseTheory
context-free-test.log       examples/formal-languages/context-free  (5s)     OK
Starting work on contigTheory
real_measureTheory                     examples/probability/legacy (41s)     OK
Starting work on real_lebesgueTheory
prob-selftest.log                                  src/probability (34s)     OK
Starting work on heap
heap                              examples/formal-languages/lambek  (0s)     OK
Starting work on LambekTheory
contigTheory                      examples/formal-languages/contig (11s)     OK
Finished $(HOLDIR)/examples/formal-languages/contig [#theories: 2]    (12.950s)
Starting work on charsetTheory
simpleSexpParseTheory       examples/formal-languages/context-free (19s)     OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 11] (81.990s)
Starting work on vec_mapTheory
LambekTheory                      examples/formal-languages/lambek  (8s)     OK
Starting work on CutFreeTheory
vec_mapTheory                    examples/formal-languages/regular  (3s)     OK
Starting work on regularTheory
CutFreeTheory                     examples/formal-languages/lambek  (8s)     OK
Starting work on ExampleTheory
charsetTheory                    examples/formal-languages/regular (18s)     OK
Starting work on regexpTheory
regularTheory                    examples/formal-languages/regular  (9s)FAIL<1>
 wf_nfa N ⇒ (is_dfa (rename_states N base) ⇔ is_dfa N)

 failed.
 Failed to prove theorem is_dfa_rename_states.

 Exception raised at Tactical.THEN1:
 first subgoal not solved by second tactic (THEN1 on line 1788)
 error in quse /home/mn200/regression-hols/stdknl/examples/formal-languages/regular/regularScript.sml : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 1788)", origin_function = "THEN1", origin_structure = "Tactical"}
 error in load /home/mn200/regression-hols/stdknl/examples/formal-languages/regular/regularScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 1788)", origin_function = "THEN1", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 1788)", origin_function = "THEN1", origin_structure = "Tactical"}
user_lemma_primitive_operationsTheory ...m/ARM_security_properties(172s)MKILLED
measureTheory                                      src/probability (58s)MKILLED
real_lebesgueTheory                    examples/probability/legacy (30s)MKILLED
ExampleTheory                     examples/formal-languages/lambek  (4s)MKILLED
regexpTheory                     examples/formal-languages/regular  (1s)MKILLED
*** FATAL: Build failed in directory /home/mn200/regression-hols/stdknl/src/parallel_builds/core (exited with code 1)