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