Menu
▾
▴
[Hol-builds] SUCCESS: --expk:be2d4f0e2:poly590:-j6-t2
|
From: <mic...@gm...> - 2024-09-11 21:32:11
|
Running in /home/mn200/regression-hols/expknl 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: ons, 11 sep 2024 22:30:03 +0200 Extra commandline arguments: -j6 -t2 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 -- Building directory tools/check-builds [11 Sep, 22:30:45] Building directory tools/Holmake/tests/holdep [11 Sep, 22:30:45] Finished $(HOLDIR)/tools/cmp (0.060s) Finished $(HOLDIR)/tools/Holmake/tests/holdep (0.000s) Building directory tools/Holmake/tests/depchainloop [11 Sep, 22:30:45] Building directory tools/Holmake/tests/recursiveclean [11 Sep, 22:30:46] Building directory tools/Holmake/tests/wildcard [11 Sep, 22:30:46] Building directory tools/Holmake/tests/dashn_works [11 Sep, 22:30:46] Building directory tools/Holmake/tests/dupcommands [11 Sep, 22:30:46] Finished $(HOLDIR)/tools/Holmake/tests/dupcommands/sub1 (0.000s) Finished $(HOLDIR)/tools/Holmake/tests/dupcommands/sub2 (0.000s) Finished $(HOLDIR)/tools/Holmake/tests/dupcommands (0.000s) Building directory tools/Holmake/tests/varextension [11 Sep, 22:30:46] Building directory tools/set_mtime [11 Sep, 22:30:46] Building directory tools/mlyacc/mlyacclib [11 Sep, 22:30:46] Building directory src/portableML/poly [11 Sep, 22:30:46] Building directory src/portableML [11 Sep, 22:30:46] Building directory src/portableML/monads [11 Sep, 22:30:46] Building directory src/portableML/poly/concurrent [11 Sep, 22:30:46] Building directory src/portableML/testsrc [11 Sep, 22:30:46] Finished $(HOLDIR)/tools/unicode-grep (1.320s) Finished $(HOLDIR)/src/portableML/testsrc (1.150s) Building directory src/prekernel [11 Sep, 22:30:49] Building directory src/experimental-kernel [11 Sep, 22:30:50] Building directory src/thm [11 Sep, 22:30:50] Building directory src/postkernel [11 Sep, 22:30:50] Building directory src/parse [11 Sep, 22:30:50] Building directory tools/Holmake/tests/badincludes [11 Sep, 22:30:55] Building directory src/opentheory [11 Sep, 22:30:59] Building directory src/bool [11 Sep, 22:30:59] Building directory src/1 [11 Sep, 22:31:05] Building directory src/proofman [11 Sep, 22:31:12] Building directory src/proofman/tests [11 Sep, 22:31:19] Building directory tools/Holmake/tests/preexec [11 Sep, 22:31:20] Building directory tools/Holmake/tests/parallel_tests [11 Sep, 22:31:20] Finished $(HOLDIR)/tools/Holmake/tests/brokenstrings (0.000s) Finished $(HOLDIR)/tools/Holmake/tests/commandmacros (0.010s) Finished $(HOLDIR)/tools/Holmake/tests/commandmacros/subdir (0.000s) Finished $(HOLDIR)/tools/Holmake/tests/altquote1 [#theories: 1] (0.150s) Finished $(HOLDIR)/tools/Holmake/tests/depchain1/dir2/dir1 [#theories: 1] (0.140s) Finished $(HOLDIR)/tools/Holmake/tests/depchain1/dir2 (0.000s) Finished $(HOLDIR)/tools/Holmake/tests/depchain2 [#theories: 1] (0.150s) Finished $(HOLDIR)/tools/Holmake/tests/clinevars (0.160s) Finished $(HOLDIR)/tools/Holmake/tests/cheatspotting (0.260s) Finished $(HOLDIR)/tools/Holmake/tests/depchain_heap [#theories: 1] (0.180s) Finished $(HOLDIR)/tools/Holmake/tests/depchain2/dir1/dir2 [#theories: 1] (0.160s) Finished $(HOLDIR)/tools/Holmake/tests/depchain_heap/dir2 (0.110s) Finished $(HOLDIR)/tools/Holmake/tests/doublecrnl (0.100s) Finished $(HOLDIR)/tools/Holmake/tests/depchain1/dir3 [#theories: 2] (0.290s) Finished $(HOLDIR)/tools/Holmake/tests/depchain2/dir1 [#theories: 1] (0.130s) Finished $(HOLDIR)/tools/Holmake/tests/holdep (0.000s) Finished $(HOLDIR)/tools/Holmake/tests/deps_of_depthys [#theories: 2] (0.300s) Finished $(HOLDIR)/tools/Holmake/tests/hollogs/base [#theories: 1] (0.120s) Finished $(HOLDIR)/tools/Holmake/tests/hollogs [#theories: 1] (0.140s) Finished $(HOLDIR)/tools/Holmake/tests/ignore_errors/j1 (0.000s) Finished $(HOLDIR)/tools/Holmake/tests/ignore_errors/j4 (0.010s) Finished $(HOLDIR)/tools/Holmake/tests/gh604 (0.390s) Finished $(HOLDIR)/tools/Holmake/tests/indepchildren/base [#theories: 1] (0.140s) Finished $(HOLDIR)/tools/Holmake/tests/indepchildren/intermediate (0.000s) Finished $(HOLDIR)/tools/Holmake/tests/noprereqs/dir1 [#theories: 1] (0.150s) Finished $(HOLDIR)/tools/Holmake/tests/noprereqs/dir2 (0.000s) Finished $(HOLDIR)/tools/Holmake/tests/indepchildren/dir1 [#theories: 1] (0.170s) Finished $(HOLDIR)/tools/Holmake/tests/indepchildren/dir2 [#theories: 1] (0.170s) Finished $(HOLDIR)/tools/Holmake/tests/noprereqs/dir3 [#theories: 1] (0.130s) Finished $(HOLDIR)/tools/Holmake/tests/nullary_tgt [#theories: 1] (0.170s) Finished $(HOLDIR)/tools/Holmake/tests/indepchildren [#theories: 1] (0.140s) Finished $(HOLDIR)/tools/Holmake/tests/noprereqs/dir4 [#theories: 1] (0.130s) Finished $(HOLDIR)/tools/Holmake/tests/quote-filter (0.010s) Finished $(HOLDIR)/tools/Holmake/tests/qfreadTheoremsyntax [#theories: 1] (0.130s) Finished $(HOLDIR)/tools/Holmake/tests/phony_tgt [#theories: 1] (0.180s) Finished $(HOLDIR)/tools/Holmake/tests/theorytarget (0.190s) Finished $(HOLDIR)/tools/Holmake/tests/empty_script (0.450s) Finished $(HOLDIR)/tools/Holmake/tests/coproduct (2.670s) Building directory src/1/theory_tests [11 Sep, 22:31:23] Building directory src/compute/src [11 Sep, 22:31:24] Building directory src/HolSat/sat_solvers/minisat [11 Sep, 22:31:25] Building directory src/HolSat/sat_solvers/zc2hs [11 Sep, 22:31:27] Building directory src/HolSat [11 Sep, 22:31:28] Building directory src/taut [11 Sep, 22:31:28] Building directory tools/Holmake/tests/incs_vs_sigobj/dir2 [11 Sep, 22:31:28] Finished $(HOLDIR)/tools/Holmake/tests/incs_vs_sigobj/dir1 (0.000s) Finished $(HOLDIR)/tools/Holmake/tests/incs_vs_sigobj/dir2 [#theories: 1] (0.050s) Building directory src/marker [11 Sep, 22:31:28] Building directory src/q [11 Sep, 22:31:29] Building directory src/combin [11 Sep, 22:31:30] Building directory src/lite [11 Sep, 22:31:31] Building directory src/refute [11 Sep, 22:31:31] Building directory src/simp/src [11 Sep, 22:31:31] Building directory src/metis [11 Sep, 22:31:34] Building directory src/meson/src [11 Sep, 22:31:37] Building directory src/IndDef [11 Sep, 22:31:37] Building directory src/basicProof [11 Sep, 22:31:40] Building directory src/basicProof/theory_tests [11 Sep, 22:31:43] Building directory src/relation [11 Sep, 22:31:47] Building directory src/quotient/src [11 Sep, 22:32:04] Building directory src/coretypes [11 Sep, 22:32:11] Building directory src/meson/test [11 Sep, 22:32:40] Building directory src/tfl/src [11 Sep, 22:32:48] Building directory src/num/theories [11 Sep, 22:32:56] Building directory src/num/theories/cv_compute [11 Sep, 22:33:35] Building directory src/num/reduce/conv [11 Sep, 22:33:41] Building directory src/num/reduce/src [11 Sep, 22:33:41] Building directory src/num/arith/src [11 Sep, 22:33:50] Building directory src/num [11 Sep, 22:34:00] Building directory src/num/termination [11 Sep, 22:34:00] Building directory src/num/extra_theories [11 Sep, 22:34:11] Building directory src/unwind [11 Sep, 22:34:19] Building directory src/pred_set/src [11 Sep, 22:34:19] Building directory src/datatype/record [11 Sep, 22:35:04] Building directory src/datatype [11 Sep, 22:35:04] Building directory src/datatype/theory_tests [11 Sep, 22:35:13] Building directory src/monad [11 Sep, 22:35:19] Building directory src/list/src [11 Sep, 22:35:19] Building directory src/quantHeuristics [11 Sep, 22:36:10] Building directory src/pattern_matches [11 Sep, 22:36:33] Building directory src/pattern_matches/interactive_tests [11 Sep, 22:37:11] Building directory src/HolSat/vector_def_CNF [11 Sep, 22:37:29] Building directory src/boss/ml_evaluation [11 Sep, 22:37:48] Building directory src/opentheory/reader [11 Sep, 22:37:48] Building directory src/boss [11 Sep, 22:37:48] Building directory src/AI [11 Sep, 22:38:04] Building directory src/AI/sml_inspection [11 Sep, 22:38:04] Building directory src/AI/proof_search [11 Sep, 22:38:05] Building directory src/AI/machine_learning [11 Sep, 22:38:06] Building directory src/tactictoe/src [11 Sep, 22:38:09] Building directory src/tactictoe/selftest [11 Sep, 22:38:11] Building directory src/holyhammer [11 Sep, 22:38:19] Building directory src/boss/theory_tests [11 Sep, 22:38:21] Building directory src/tfl/src/test [11 Sep, 22:38:26] Building directory src/parallel_builds/core [11 Sep, 22:38:28] Finished $(HOLDIR)/src/TeX (1.130s) Finished $(HOLDIR)/src/res_quan/src [#theories: 1] (10.260s) Finished $(HOLDIR)/src/sort [#theories: 3] (15.110s) Finished $(HOLDIR)/src/bag [#theories: 2] (16.430s) Finished $(HOLDIR)/src/ring/src [#theories: 6] (12.860s) Finished $(HOLDIR)/src/string [#theories: 4] (19.480s) Finished $(HOLDIR)/src/transfer [#theories: 2] (3.420s) Finished $(HOLDIR)/src/hol88 (0.010s) Finished $(HOLDIR)/src/integer [#theories: 8] (83.140s) Finished $(HOLDIR)/src/pred_set/src/more_theories [#theories: 10] (98.900s) Finished $(HOLDIR)/src/finite_maps [#theories: 13] (166.930s) Finished $(HOLDIR)/src/n-bit [#theories: 7] (155.140s) Finished $(HOLDIR)/src/rational [#theories: 4] (53.910s) Finished $(HOLDIR)/src/monad/more_monads [#theories: 5] (14.020s) Finished $(HOLDIR)/src/algebra/base [#theories: 3] (77.310s) Finished $(HOLDIR)/examples/simple_complexity/lib [#theories: 2] (21.690s) Finished $(HOLDIR)/examples/simple_complexity/loop [#theories: 6] (77.360s) Finished $(HOLDIR)/examples/lambda/basics [#theories: 6] (45.290s) Finished $(HOLDIR)/examples/Crypto/AES [#theories: 4] (139.220s) Finished $(HOLDIR)/src/algebra/construction [#theories: 3] (153.290s) Finished $(HOLDIR)/src/real [#theories: 12] (259.800s) Finished $(HOLDIR)/examples/Crypto/IDEA [#theories: 3] (51.580s) Finished $(HOLDIR)/examples/algebra/field [#theories: 9] (188.740s) Finished $(HOLDIR)/examples/CCS [#theories: 16] (137.460s) Finished $(HOLDIR)/examples/algebra/linear [#theories: 4] (80.800s) Finished $(HOLDIR)/src/num/theories/cv_compute/automation [#theories: 4] (132.290s) Finished $(HOLDIR)/examples/Crypto/RC6 [#theories: 1] (17.600s) Finished $(HOLDIR)/examples/Crypto/DES [#theories: 3] (438.270s) Finished $(HOLDIR)/examples/Crypto/MARS [#theories: 4] (60.250s) Finished $(HOLDIR)/examples/Crypto/SHA-1 [#theories: 1] (18.170s) Finished $(HOLDIR)/examples/Crypto/Keccak [#theories: 1] (95.780s) Finished $(HOLDIR)/src/coalgebras [#theories: 7] (71.960s) Finished $(HOLDIR)/examples/Crypto [#theories: 1] (0.830s) Finished $(HOLDIR)/examples/Crypto/RSA [#theories: 6] (4.640s) Finished $(HOLDIR)/examples/Crypto/TWOFISH [#theories: 1] (25.860s) Finished $(HOLDIR)/examples/fun-op-sem/lprefix_lub [#theories: 1] (7.940s) Finished $(HOLDIR)/src/emit [#theories: 3] (55.320s) Finished $(HOLDIR)/examples/Crypto/TEA [#theories: 2] (31.700s) Finished $(HOLDIR)/examples/Crypto/Serpent/Reference [#theories: 6] (179.440s) Finished $(HOLDIR)/examples/MLsyntax [#theories: 1] (1.670s) Finished $(HOLDIR)/examples/Crypto/Serpent/Bitslice [#theories: 4] (177.300s) Finished $(HOLDIR)/examples/algebra/polynomial [#theories: 21] (581.610s) Finished $(HOLDIR)/examples/AKS/compute [#theories: 6] (150.350s) Finished $(HOLDIR)/examples/PSL/path [#theories: 2] (25.940s) Finished $(HOLDIR)/examples/PSL/regexp [#theories: 2] (17.370s) Finished $(HOLDIR)/examples/Hoare-for-divergence [#theories: 8] (88.770s) Finished $(HOLDIR)/examples/RL_Environment (2.660s) Finished $(HOLDIR)/examples/AKS/machine [#theories: 10] (188.930s) Finished $(HOLDIR)/examples/STE [#theories: 1] (7.280s) Finished $(HOLDIR)/examples/PSL/1.01/official-semantics [#theories: 8] (108.110s) Finished $(HOLDIR)/examples/PSL/1.01/executable-semantics [#theories: 1] (21.620s) Finished $(HOLDIR)/examples/algebra/ring [#theories: 1] (33.980s) Finished $(HOLDIR)/examples/algorithms [#theories: 3] (29.490s) Finished $(HOLDIR)/examples/algorithms/unification/triangular [#theories: 1] (3.050s) Finished $(HOLDIR)/examples/algebra/aat [#theories: 2] (40.390s) Finished $(HOLDIR)/examples/algorithms/boyer_moore [#theories: 4] (26.580s) Finished $(HOLDIR)/src/transfer/examples [#theories: 8] (18.220s) Finished $(HOLDIR)/examples/PSL/1.1/official-semantics [#theories: 11] (141.010s) Finished $(HOLDIR)/examples/algebra/multipoly [#theories: 1] (106.070s) Finished $(HOLDIR)/examples/algorithms/unification/triangular/first-order [#theories: 8] (43.110s) Finished $(HOLDIR)/src/update [#theories: 1] (1.190s) Finished $(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation [#theories: 3] (20.340s) Finished $(HOLDIR)/examples/algorithms/unification/triangular/nominal [#theories: 8] (79.750s) Finished $(HOLDIR)/examples/arm/armv8-memory-model [#theories: 8] (63.200s) Finished $(HOLDIR)/examples/machine-code/hoare-triple [#theories: 5] (48.740s) Finished $(HOLDIR)/examples/machine-code/decompiler (0.000s) Finished $(HOLDIR)/examples/algebra/finitefield [#theories: 12] (339.970s) Finished $(HOLDIR)/examples/arm/arm6-verification [#theories: 6] (103.080s) Finished $(HOLDIR)/examples/set-theory/zfset [#theories: 2] (14.030s) Finished $(HOLDIR)/examples/arm/arm6-verification/correctness [#theories: 6] (217.560s) Finished $(HOLDIR)/examples/arm/v4 [#theories: 9] (200.770s) Finished $(HOLDIR)/examples/category [#theories: 8] (80.150s) Finished $(HOLDIR)/examples/computability [#theories: 5] (19.430s) Finished $(HOLDIR)/examples/AKS/theories [#theories: 8] (267.690s) Finished $(HOLDIR)/examples/balanced_bst [#theories: 2] (283.830s) Finished $(HOLDIR)/examples/arm/experimental [#theories: 3] (69.470s) Finished $(HOLDIR)/examples/lambda/other-models [#theories: 11] (73.010s) Finished $(HOLDIR)/examples/countchars [#theories: 1] (2.850s) Finished $(HOLDIR)/examples/computability/turing [#theories: 2] (30.690s) Finished $(HOLDIR)/examples/lambda/barendregt [#theories: 15] (164.580s) Finished $(HOLDIR)/examples/cv_compute [#theories: 3] (52.860s) Finished $(HOLDIR)/examples/miller/ho_prover [#theories: 1] (0.740s) Finished $(HOLDIR)/examples/miller/subtypes [#theories: 1] (2.160s) Finished $(HOLDIR)/examples/computability/register [#theories: 7] (101.530s) Finished $(HOLDIR)/examples/dev/dff [#theories: 4] (2.430s) Finished $(HOLDIR)/examples/developers/ThmSetData [#theories: 3] (0.910s) Finished $(HOLDIR)/examples/arm/v7 [#theories: 7] (452.480s) Finished $(HOLDIR)/examples/computability/lambda [#theories: 15] (116.230s) Finished $(HOLDIR)/examples/decidable_separationLogic/src [#theories: 2] (55.540s) Finished $(HOLDIR)/examples/computability/recdegrees [#theories: 1] (11.560s) Finished $(HOLDIR)/examples/dev [#theories: 4] (59.010s) Finished $(HOLDIR)/examples/fermat/little [#theories: 10] (98.160s) Finished $(HOLDIR)/examples/formal-languages [#theories: 1] (2.450s) Finished $(HOLDIR)/examples/formal-languages/contig [#theories: 2] (13.270s) Finished $(HOLDIR)/examples/fermat/count [#theories: 3] (48.340s) Finished $(HOLDIR)/examples/fermat/twosq [#theories: 12] (161.420s) Finished $(HOLDIR)/src/real/analysis [#theories: 10] (562.770s) Finished $(HOLDIR)/examples/miller/formalize [#theories: 7] (62.310s) Finished $(HOLDIR)/examples/formal-languages/lambek [#theories: 3] (30.810s) Finished $(HOLDIR)/examples/computability/kolmog [#theories: 12] (246.660s) Finished $(HOLDIR)/examples/formal-languages/regular/regular-play/src [#theories: 4] (9.440s) Finished $(HOLDIR)/examples/formal-languages/regular/regular-play/emit [#theories: 1] (12.290s) Finished $(HOLDIR)/examples/formal-languages/regular/regular-play/lib (0.000s) Finished $(HOLDIR)/examples/formal-languages/regular/regular-play/test (0.000s) Finished $(HOLDIR)/examples/formal-languages/regular/regular-play (1.050s) Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 11] (212.030s) Finished $(HOLDIR)/examples/fun-op-sem/cbv-lc [#theories: 4] (42.780s) Finished $(HOLDIR)/examples/fun-op-sem/imp [#theories: 1] (4.230s) Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 8] (212.860s) Finished $(HOLDIR)/examples/probability/legacy [#theories: 3] (145.200s) Finished $(HOLDIR)/examples/fun-op-sem/for [#theories: 6] (109.360s) Finished $(HOLDIR)/examples/fun-op-sem/ml [#theories: 1] (77.920s) Finished $(HOLDIR)/examples/hardware/port-full/tamarack2 [#theories: 1] (11.390s) Finished $(HOLDIR)/examples/fun-op-sem/small-step [#theories: 6] (145.780s) Finished $(HOLDIR)/examples/hfs [#theories: 2] (2.990s) Finished $(HOLDIR)/examples/hardware/port/tamarack2 [#theories: 4] (6.740s) Finished $(HOLDIR)/examples/generic_graphs [#theories: 4] (66.090s) Finished $(HOLDIR)/examples/imperative [#theories: 2] (3.670s) Finished $(HOLDIR)/examples/ind_def [#theories: 5] (10.180s) Finished $(HOLDIR)/examples/l3-machine-code (21.890s) Finished $(HOLDIR)/examples/l3-machine-code/lib (0.000s) Finished $(HOLDIR)/examples/lambda/examples [#theories: 1] (4.570s) Finished $(HOLDIR)/examples/lambda/typing [#theories: 4] (22.970s) Finished $(HOLDIR)/examples/logic [#theories: 1] (7.100s) Finished $(HOLDIR)/examples/dependability/RBD [#theories: 2] (122.580s) Finished $(HOLDIR)/examples/l3-machine-code/common [#theories: 3] (31.040s) Finished $(HOLDIR)/src/floating-point [#theories: 4] (171.450s) Finished $(HOLDIR)/examples/dependability/FT [#theories: 2] (123.860s) Finished $(HOLDIR)/src/probability [#theories: 9] (541.550s) Finished $(HOLDIR)/examples/l3-machine-code/arm8/model [#theories: 1] (38.450s) Finished $(HOLDIR)/examples/l3-machine-code/arm/model [#theories: 1] (92.990s) Finished $(HOLDIR)/examples/l3-machine-code/arm8/step [#theories: 1] (35.770s) Finished $(HOLDIR)/examples/dependability [#theories: 2] (114.430s) Finished $(HOLDIR)/examples/l3-machine-code/m0/model [#theories: 1] (30.370s) Finished $(HOLDIR)/examples/l3-machine-code/mips/model [#theories: 1] (100.340s) Finished $(HOLDIR)/examples/l3-machine-code/arm8/prog [#theories: 1] (28.050s) Finished $(HOLDIR)/examples/l3-machine-code/m0/step [#theories: 1] (34.810s) Finished $(HOLDIR)/examples/dependability/case_studies [#theories: 4] (216.740s) Finished $(HOLDIR)/examples/l3-machine-code/arm8/decompiler [#theories: 1] (12.620s) Finished $(HOLDIR)/examples/lambda/wcbv-reasonable [#theories: 5] (46.980s) Finished $(HOLDIR)/examples/l3-machine-code/m0/prog [#theories: 1] (22.460s) Finished $(HOLDIR)/examples/l3-machine-code/m0/decompiler [#theories: 3] (17.000s) Finished $(HOLDIR)/examples/l3-machine-code/x64/model [#theories: 1] (45.210s) Finished $(HOLDIR)/examples/l3-machine-code/mips/step [#theories: 1] (87.420s) Finished $(HOLDIR)/examples/logic/folcompactness [#theories: 6] (28.790s) Finished $(HOLDIR)/examples/l3-machine-code/mips/prog [#theories: 1] (63.110s) Finished $(HOLDIR)/examples/l3-machine-code/riscv/model [#theories: 1] (123.170s) Finished $(HOLDIR)/examples/l3-machine-code/arm/step [#theories: 1] (198.660s) Finished $(HOLDIR)/examples/l3-machine-code/arm/prog [#theories: 1] (149.070s) Finished $(HOLDIR)/examples/l3-machine-code/riscv/step [#theories: 1] (94.900s) Finished $(HOLDIR)/examples/l3-machine-code/x64/step [#theories: 1] (160.870s) Finished $(HOLDIR)/examples/l3-machine-code/x64/prog [#theories: 1] (128.440s) Finished $(HOLDIR)/examples/l3-machine-code/riscv/prog [#theories: 1] (16.260s) Finished $(HOLDIR)/examples/l3-machine-code/mips/decompiler [#theories: 1] (126.480s) Finished $(HOLDIR)/examples/l3-machine-code/riscv/decompiler [#theories: 1] (10.360s) Finished $(HOLDIR)/examples/l3-machine-code/arm/decompiler [#theories: 3] (96.980s) Finished $(HOLDIR)/examples/l3-machine-code/x64/decompiler [#theories: 1] (30.190s) Finished $(HOLDIR)/examples/logic/temporal/src [#theories: 3] (12.720s) Finished $(HOLDIR)/examples/logic/temporal_deep/src/tools [#theories: 4] (31.210s) Finished $(HOLDIR)/examples/logic/modal-tableaux [#theories: 5] (43.190s) Finished $(HOLDIR)/examples/logic/ltl-transformations [#theories: 1] (5.450s) Finished $(HOLDIR)/examples/logic/ncfolproofs [#theories: 1] (7.810s) Finished $(HOLDIR)/examples/logic/propositional_logic [#theories: 3] (15.240s) Finished $(HOLDIR)/examples/logic/temporal_deep/src/deep_embeddings [#theories: 14] (169.950s) Finished $(HOLDIR)/examples/logic/relevant-logic [#theories: 7] (138.610s) Finished $(HOLDIR)/examples/logic/temporal_deep/src/translations [#theories: 6] (98.020s) Finished $(HOLDIR)/examples/logic/modal-models [#theories: 13] (261.460s) Finished $(HOLDIR)/examples/logic/temporal_deep/src/model_check [#theories: 1] (10.360s) Finished $(HOLDIR)/examples/logic/temporal_deep/src/examples [#theories: 1] (19.970s) Finished $(HOLDIR)/examples/parity [#theories: 2] (2.570s) Finished $(HOLDIR)/examples/misc [#theories: 9] (72.010s) Finished $(HOLDIR)/examples/miller/groups [#theories: 8] (94.030s) Finished $(HOLDIR)/examples/rings [#theories: 1] (10.990s) Finished $(HOLDIR)/examples/padics [#theories: 4] (54.530s) Finished $(HOLDIR)/examples/probability [#theories: 4] (83.450s) Finished $(HOLDIR)/examples/set-theory/vbg [#theories: 3] (11.280s) Finished $(HOLDIR)/examples/zipper [#theories: 1] (2.360s) Finished $(HOLDIR)/src/HolSmt [#theories: 1] (79.390s) Finished $(HOLDIR)/examples/logic/ltl [#theories: 14] (485.760s) Finished $(HOLDIR)/src/Boolify/src [#theories: 4] (14.520s) Finished $(HOLDIR)/src/HolQbf (0.000s) Finished $(HOLDIR)/src/TeX/theory_tests/proj1 [#theories: 1] (0.410s) Finished $(HOLDIR)/src/TeX/theory_tests [#theories: 8] (22.730s) Finished $(HOLDIR)/src/datatype/inftree [#theories: 1] (1.540s) Finished $(HOLDIR)/src/TeX/theory_tests/proj1paper [#theories: 1] (4.970s) Finished $(HOLDIR)/examples/miller/prob [#theories: 11] (498.660s) Finished $(HOLDIR)/examples/vector [#theories: 3] (76.130s) Finished $(HOLDIR)/src/integer/testing (21.530s) Finished $(HOLDIR)/src/n-bit/interactive_tests [#theories: 1] (18.390s) Finished $(HOLDIR)/src/quotient/choice [#theories: 1] (2.980s) Finished $(HOLDIR)/src/num/theories/cv_compute/automation/theory_tests [#theories: 1] (11.210s) Finished $(HOLDIR)/src/float [#theories: 2] (39.040s) Finished $(HOLDIR)/src/quotient/examples [#theories: 5] (12.690s) Finished $(HOLDIR)/src/search [#theories: 3] (4.000s) Finished $(HOLDIR)/src/string/theorytesting [#theories: 5] (7.010s) Finished $(HOLDIR)/src/quotient/examples/lambda [#theories: 7] (23.960s) Finished $(HOLDIR)/tools/Holmake/tests/Iflag (1.050s) Finished $(HOLDIR)/src/quotient/examples/sigma [#theories: 6] (25.410s) Finished $(HOLDIR)/src/tfl/examples [#theories: 2] (14.860s) Finished $(HOLDIR)/examples/separationLogic/src/holfoot [#theories: 1] (97.810s) Finished $(HOLDIR)/examples/separationLogic/src/holfoot/poly (74.360s) Finished $(HOLDIR)/src/floating-point/native (129.260s) Finished $(HOLDIR)/examples/miller/miller [#theories: 2] (259.620s) Building directory src/emit/ML [11 Sep, 23:29:14] Building directory src/emit/theory_tests [11 Sep, 23:29:14] Building directory src/emit/theory_tests1 [11 Sep, 23:29:23] Finished $(HOLDIR)/src/emit/ML (0.000s) Finished $(HOLDIR)/src/emit/theory_tests1 [#theories: 1] (6.660s) |