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)
Loading
Please sign in to comment