Skip to content
Commit 346f2887 authored by Makarius Wenzel's avatar Makarius Wenzel
Browse files

result of "Isabelle_MMT-20200421/bin/isabelle mmt_import -b HOL-Analysis -o...

result of "Isabelle_MMT-20200421/bin/isabelle mmt_import -b HOL-Analysis -o threads=8 -d afp-2020/thys -A content/MathHub -C AFP=AFP -C _=Distribution -a -o mmt_watchdog_timeout=14400" (monster 22:33:14 elapsed time, Isabelle/abf3e80bd815 + AFP/91f1cdbeefc0 + MMT/52adb5e338811e)
Finished import of
    7027 theories
 2116638 individuals:
        5291 locale
        5155 locale_dependency
        1236 class
       11724 type
      240404 const
      236186 axiom
     1497689 thm
        2401 datatype
         149 codatatype
       66597 definition
        3576 recursive_definition
       17925 inductive_definition
         256 coinductive_definition
         535 specification
400996957 relations:
         101 dcterms:contributor
        1727 dcterms:license
      233361 ulo:check-time
      232718 ulo:defines
     1022417 ulo:definition
     1540592 ulo:derived
       41278 ulo:experimental
        7026 ulo:external-size
      167195 ulo:function
        1495 ulo:important
        3492 ulo:inductive-on
        5261 ulo:instance-of
      534916 ulo:justifies
     2168970 ulo:name
      241704 ulo:para
      241704 ulo:paratype
       78914 ulo:predicate
        1356 ulo:primitive
       29534 ulo:section
     2139385 ulo:sourceref
     2209350 ulo:specified-in
     2209350 ulo:specifies
     1533440 ulo:statement
       12409 ulo:theory
       12201 ulo:type
         551 ulo:unimportant
        1264 ulo:universe
   386325246 ulo:uses
22:33:14 elapsed time
*** FAILED theory CakeML_Codegen.Test_Composition
*** No command with suitable id for const "Test_Composition.test_code.cake_static_env.empty_sem_env" in theory "CakeML_Codegen.Test_Composition" -- it refers to command ‹.› in "/home/mawenzel/isabelle/afp-2020/thys/CakeML_Codegen/Test/Test_Composition.thy" (line 15)
***
*** FAILED theory CakeML_Codegen.Test_Print
*** No command with suitable id for const "Test_Print.f'.cake_static_env.empty_sem_env" in theory "CakeML_Codegen.Test_Print" -- it refers to command ‹.› in "/home/mawenzel/isabelle/afp-2020/thys/CakeML_Codegen/Test/Test_Print.thy" (line 24)
parent 1ce32ec0
Loading
Loading
Loading
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please to comment